[Merged by Bors] - feat(GroupWithZero): monoid with zero homs to (co)products

Mathlib.lean

@@ -468,6 +468,7 @@ import Mathlib.Algebra.GroupWithZero.Pointwise.Finset
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
 import Mathlib.Algebra.GroupWithZero.Prod
+import Mathlib.Algebra.GroupWithZero.ProdHom
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.GroupWithZero.Subgroup
 import Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise

Mathlib/Algebra/GroupWithZero/Hom.lean

@@ -214,6 +214,26 @@ instance {β} [CommMonoidWithZero β] : Mul (α →*₀ β) where
     { (f * g : α →* β) with
       map_zero' := by dsimp; rw [map_zero, zero_mul] }
 
+/-- The trivial homomorphism between monoids with zero, sending everything to 1 other than 0. -/
+protected instance one (M₀ N₀ : Type*) [MulZeroOneClass M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] :
+    One (M₀ →*₀ N₀) where
+  one.toFun x := if x = 0 then 0 else 1
+  one.map_zero' := by simp
+  one.map_one' := by simp
+  one.map_mul' x y := by split_ifs <;> simp_all
+
+@[simp]
+lemma one_apply_zero {M₀ N₀ : Type*} [MulZeroOneClass M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] :
+    (1 : M₀ →*₀ N₀) 0 = 0 :=
+  if_pos rfl
+
+lemma one_apply_of_ne_zero {M₀ N₀ : Type*} [MulZeroOneClass M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] {x : M₀} (hx : x ≠ 0) :
+    (1 : M₀ →*₀ N₀) x = 1 :=
+  if_neg hx
+
 end MonoidWithZeroHom
 
 section CommMonoidWithZero

Mathlib/Algebra/GroupWithZero/Prod.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser, Yaël Dillies
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.GroupWithZero.Units.Basic
+import Mathlib.Algebra.GroupWithZero.WithZero
 
 /-!
 # Products of monoids with zero, groups with zero
@@ -49,6 +50,14 @@ instance instCommMonoidWithZero [CommMonoidWithZero M₀] [CommMonoidWithZero N
 
 end Prod
 
+variable (M₀) in
+@[simp]
+lemma WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv [GroupWithZero M₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] :
+    MonoidWithZeroHomClass.toMonoidWithZeroHom WithZero.withZeroUnitsEquiv =
+      WithZero.lift' (Units.coeHom M₀) :=
+  rfl
+
 /-! ### Multiplication and division as homomorphisms -/
 
 section BundledMulDiv

Mathlib/Algebra/GroupWithZero/ProdHom.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2025 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.Group.Prod
+import Mathlib.Algebra.GroupWithZero.Commute
+import Mathlib.Algebra.GroupWithZero.Units.Lemmas
+import Mathlib.Algebra.GroupWithZero.WithZero
+
+/-!
+# Homomorphisms for products of groups with zero
+
+This file defines homomorphisms for products of groups with zero,
+which is identified with the `WithZero` of the product of the units of the groups.
+
+The product of groups with zero `WithZero (αˣ × βˣ)` is a
+group with zero itself with natural inclusions.
+
+TODO: Give `GrpWithZero` instances of `HasBinaryProducts` and `HasBinaryCoproducts`,
+as well as a terminal object.
+
+-/
+
+namespace MonoidWithZeroHom
+
+/-- The trivial group-with-zero hom is absorbing for composition. -/
+@[simp]
+lemma one_apply_apply_eq {M₀ N₀ G₀ : Type*}
+    [GroupWithZero M₀]
+    [MulZeroOneClass N₀] [Nontrivial N₀] [NoZeroDivisors N₀]
+    [MulZeroOneClass G₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [DecidablePred fun x : N₀ ↦ x = 0]
+    (f : M₀ →*₀ N₀) (x : M₀) :
+    (1 : N₀ →*₀ G₀) (f x) = (1 : M₀ →*₀ G₀) x := by
+  rcases eq_or_ne x 0 with rfl | hx
+  · simp
+  · rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero]
+    rwa [map_ne_zero f]
+
+/-- The trivial group-with-zero hom is absorbing for composition. -/
+@[simp]
+lemma one_comp {M₀ N₀ G₀ : Type*}
+    [GroupWithZero M₀]
+    [MulZeroOneClass N₀] [Nontrivial N₀] [NoZeroDivisors N₀]
+    [MulZeroOneClass G₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [DecidablePred fun x : N₀ ↦ x = 0]
+    (f : M₀ →*₀ N₀) :
+    (1 : N₀ →*₀ G₀).comp f = (1 : M₀ →*₀ G₀) :=
+  ext <| one_apply_apply_eq _
+
+variable (G₀ H₀ : Type*) [GroupWithZero G₀] [GroupWithZero H₀]
+
+/-- Given groups with zero `G₀`, `H₀`, the natural inclusion ordered homomorphism from
+`G₀` to `WithZero (G₀ˣ × H₀ˣ)`, which is the group with zero that can be identified
+as their product. -/
+def inl [DecidablePred fun x : G₀ ↦ x = 0] : G₀ →*₀ WithZero (G₀ˣ × H₀ˣ) :=
+  (WithZero.map' (.inl _ _)).comp
+    (MonoidWithZeroHomClass.toMonoidWithZeroHom WithZero.withZeroUnitsEquiv.symm)
+
+/-- Given groups with zero `G₀`, `H₀`, the natural inclusion ordered homomorphism from
+`H₀` to `WithZero (G₀ˣ × H₀ˣ)`, which is the group with zero that can be identified
+as their product. -/
+def inr [DecidablePred fun x : H₀ ↦ x = 0] : H₀ →*₀ WithZero (G₀ˣ × H₀ˣ) :=
+  (WithZero.map' (.inr _ _)).comp
+    (MonoidWithZeroHomClass.toMonoidWithZeroHom WithZero.withZeroUnitsEquiv.symm)
+
+/-- Given groups with zero `G₀`, `H₀`, the natural projection homomorphism from
+`WithZero (G₀ˣ × H₀ˣ)` to `G₀`, which is the group with zero that can be identified
+as their product. -/
+def fst : WithZero (G₀ˣ × H₀ˣ) →*₀ G₀ :=
+  WithZero.lift' ((Units.coeHom _).comp (.fst ..))
+
+/-- Given groups with zero `G₀`, `H₀`, the natural projection homomorphism from
+`WithZero (G₀ˣ × H₀ˣ)` to `H₀`, which is the group with zero that can be identified
+as their product. -/
+def snd : WithZero (G₀ˣ × H₀ˣ) →*₀ H₀ :=
+  WithZero.lift' ((Units.coeHom _).comp (.snd ..))
+
+variable {G₀ H₀}
+
+@[simp]
+lemma inl_apply_unit [DecidablePred fun x : G₀ ↦ x = 0] (x : G₀ˣ) :
+    inl G₀ H₀ x = ((x, (1 : H₀ˣ)) : WithZero (G₀ˣ × H₀ˣ)) := by
+  simp [inl]
+
+@[simp]
+lemma inr_apply_unit [DecidablePred fun x : H₀ ↦ x = 0] (x : H₀ˣ) :
+    inr G₀ H₀ x = (((1 : G₀ˣ), x) : WithZero (G₀ˣ × H₀ˣ)) := by
+  simp [inr]
+
+@[simp] lemma fst_apply_coe (x : G₀ˣ × H₀ˣ) : fst G₀ H₀ x = x.fst := by rfl
+@[simp] lemma snd_apply_coe (x : G₀ˣ × H₀ˣ) : snd G₀ H₀ x = x.snd := by rfl
+
+@[simp]
+theorem fst_inl [DecidablePred fun x : G₀ ↦ x = 0] (x : G₀) :
+    fst _ H₀ (inl _ _ x) = x := by
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  simp [WithZero.withZeroUnitsEquiv, fst, inl]
+
+@[simp]
+theorem fst_comp_inl [DecidablePred fun x : G₀ ↦ x = 0] :
+    (fst ..).comp (inl G₀ H₀) = .id _ :=
+  MonoidWithZeroHom.ext fun _ ↦ fst_inl _
+
+@[simp]
+theorem snd_comp_inl [DecidablePred fun x : G₀ ↦ x = 0] :
+    (snd ..).comp (inl G₀ H₀) = 1 := by
+  ext x
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  simp_all [WithZero.withZeroUnitsEquiv, snd, inl]
+
+theorem snd_inl_apply_of_ne_zero [DecidablePred fun x : G₀ ↦ x = 0] {x : G₀} (hx : x ≠ 0) :
+    snd _ _ (inl _ H₀ x) = 1 := by
+  rw [← MonoidWithZeroHom.comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]
+
+@[simp]
+theorem fst_comp_inr [DecidablePred fun x : H₀ ↦ x = 0] :
+    (fst ..).comp (inr G₀ H₀) = 1 := by
+  ext x
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  simp_all [WithZero.withZeroUnitsEquiv, fst, inr]
+
+theorem fst_inr_apply_of_ne_zero [DecidablePred fun x : H₀ ↦ x = 0] {x : H₀} (hx : x ≠ 0) :
+    fst _ _ (inr G₀ _ x) = 1 := by
+  rw [← MonoidWithZeroHom.comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]
+
+@[simp]
+theorem snd_inr [DecidablePred fun x : H₀ ↦ x = 0] (x : H₀) :
+    snd _ _ (inr G₀ _ x) = x := by
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  simp [WithZero.withZeroUnitsEquiv, snd, inr]
+
+@[simp]
+theorem snd_comp_inr [DecidablePred fun x : H₀ ↦ x = 0] :
+    (snd ..).comp (inr G₀ H₀) = .id _ :=
+  MonoidWithZeroHom.ext fun _ ↦ snd_inr _
+
+lemma inl_injective [DecidablePred fun x : G₀ ↦ x = 0] :
+    Function.Injective (inl G₀ H₀) :=
+  Function.HasLeftInverse.injective ⟨fst .., fun _ ↦ by simp⟩
+lemma inr_injective [DecidablePred fun x : H₀ ↦ x = 0] :
+    Function.Injective (inr G₀ H₀) :=
+  Function.HasLeftInverse.injective ⟨snd .., fun _ ↦ by simp⟩
+lemma fst_surjective [DecidablePred fun x : G₀ ↦ x = 0] :
+    Function.Surjective (fst G₀ H₀) :=
+  Function.HasRightInverse.surjective ⟨inl .., fun _ ↦ by simp⟩
+lemma snd_surjective [DecidablePred fun x : H₀ ↦ x = 0] :
+    Function.Surjective (snd G₀ H₀) :=
+  Function.HasRightInverse.surjective ⟨inr .., fun _ ↦ by simp⟩
+
+variable [DecidablePred fun x : G₀ ↦ x = 0] [DecidablePred fun x : H₀ ↦ x = 0]
+
+theorem inl_mul_inr_eq_mk_of_unit (m : G₀ˣ) (n : H₀ˣ) :
+    (inl G₀ H₀ m * inr G₀ H₀ n) = (m, n) := by
+  simp [inl, WithZero.withZeroUnitsEquiv, inr, ← WithZero.coe_mul]
+
+theorem commute_inl_inr (m : G₀) (n : H₀) : Commute (inl G₀ H₀ m) (inr G₀ H₀ n) := by
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit m <;>
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n <;>
+  simp [inl, inr, WithZero.withZeroUnitsEquiv, commute_iff_eq, ← WithZero.coe_mul]
+
+end MonoidWithZeroHom

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -61,19 +61,31 @@ protected lemma inv_mul_eq_inv_mul_iff (hbd : Commute b d) (hb : b ≠ 0) (hd :
 
 end Commute
 
-section MonoidWithZero
+section MulZeroOneClass
 
-variable [GroupWithZero G₀] [Nontrivial M₀] [MonoidWithZero M₀'] [FunLike F G₀ M₀]
-  [MonoidWithZeroHomClass F G₀ M₀] [FunLike F' G₀ M₀']
+variable [GroupWithZero G₀] [MulZeroOneClass M₀'] [Nontrivial M₀'] [FunLike F G₀ M₀']
+  [MonoidWithZeroHomClass F G₀ M₀']
   (f : F) {a : G₀}
 
-theorem map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
-  ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, fun ha => ((IsUnit.mk0 a ha).map f).ne_zero⟩
+theorem map_ne_zero : f a ≠ 0 ↔ a ≠ 0 := by
+  refine ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩
+  intro hx H
+  lift a to G₀ˣ using isUnit_iff_ne_zero.mpr hx
+  apply one_ne_zero (α := M₀')
+  rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]
 
 @[simp]
 theorem map_eq_zero : f a = 0 ↔ a = 0 :=
   not_iff_not.1 (map_ne_zero f)
 
+end MulZeroOneClass
+
+section MonoidWithZero
+
+variable [GroupWithZero G₀] [Nontrivial M₀] [MonoidWithZero M₀'] [FunLike F G₀ M₀]
+  [MonoidWithZeroHomClass F G₀ M₀] [FunLike F' G₀ M₀']
+  (f : F) {a : G₀}
+
 theorem eq_on_inv₀ [MonoidWithZeroHomClass F' G₀ M₀'] (f g : F') (h : f a = g a) :
     f a⁻¹ = g a⁻¹ := by
   rcases eq_or_ne a 0 with (rfl | ha)

Mathlib/Algebra/GroupWithZero/WithZero.lean

@@ -35,6 +35,11 @@ instance one : One (WithZero α) where
 
 @[simp, norm_cast] lemma coe_one : ((1 : α) : WithZero α) = 1 := rfl
 
+@[simp]
+lemma recZeroCoe_one {M N : Type*} [One M] (f : M → N) (z : N) :
+    recZeroCoe z f 1 = f 1 :=
+  rfl
+
 end One
 
 section Mul
@@ -268,6 +273,11 @@ def withZeroUnitsEquiv {G : Type*} [GroupWithZero G]
   right_inv _ := by simp only; split <;> simp_all
   map_mul' := (by induction · <;> induction · <;> simp [← WithZero.coe_mul])
 
+lemma withZeroUnitsEquiv_symm_apply_coe {G : Type*} [GroupWithZero G]
+    [DecidablePred (fun a : G ↦ a = 0)] (a : Gˣ) :
+    WithZero.withZeroUnitsEquiv.symm (a : G) = a := by
+  simp
+
 /-- A version of `Equiv.optionCongr` for `WithZero`. -/
 @[simps!]
 def _root_.MulEquiv.withZero [Group β] :
@@ -297,3 +307,44 @@ instance instAddMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (WithZero
   natCast_succ n := by cases n <;> simp
 
 end WithZero
+
+namespace MonoidWithZeroHom
+
+protected lemma map_eq_zero_iff {G₀ G₀' : Type*} [GroupWithZero G₀]
+    [MulZeroOneClass G₀'] [Nontrivial G₀']
+    {f : G₀ →*₀ G₀'} {x : G₀}:
+    f x = 0 ↔ x = 0 := by
+  refine ⟨?_, by simp +contextual⟩
+  contrapose!
+  intro hx H
+  lift x to G₀ˣ using isUnit_iff_ne_zero.mpr hx
+  apply one_ne_zero (α := G₀')
+  rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]
+
+variable {M₀ N₀}
+
+@[simp]
+lemma one_apply_val_unit {M₀ N₀ : Type*} [MonoidWithZero M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] (x : M₀ˣ) :
+    (1 : M₀ →*₀ N₀) x = (1 : N₀) :=
+  one_apply_of_ne_zero x.ne_zero
+
+/-- The trivial group-with-zero hom is absorbing for composition. -/
+@[simp]
+lemma apply_one_apply_eq {M₀ N₀ G₀ : Type*} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀]
+    [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun x : M₀ ↦ x = 0]
+    (f : N₀ →*₀ G₀) (x : M₀) :
+    f ((1 : M₀ →*₀ N₀) x) = (1 : M₀ →*₀ G₀) x := by
+  rcases eq_or_ne x 0 with rfl | hx
+  · simp
+  · rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]
+
+/-- The trivial group-with-zero hom is absorbing for composition. -/
+@[simp]
+lemma comp_one {M₀ N₀ G₀ : Type*} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀]
+    [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun x : M₀ ↦ x = 0]
+    (f : N₀ →*₀ G₀) :
+    f.comp (1 : M₀ →*₀ N₀) = (1 : M₀ →*₀ G₀) :=
+  ext <| apply_one_apply_eq _
+
+end MonoidWithZeroHom