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.

@[simp]

theorem MonoidWithZeroHom.one_apply_apply_eq {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [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 (f x) = 1 x

The trivial group-with-zero hom is absorbing for composition.

@[simp]

theorem MonoidWithZeroHom.one_comp {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [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₀) : comp 1 f = 1

The trivial group-with-zero hom is absorbing for composition.

def MonoidWithZeroHom.inl (G₀ : Type u_1) (H₀ : Type u_2) [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] : G₀ →*₀ WithZero (G₀ˣ × 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.

Equations

• MonoidWithZeroHom.inl G₀ H₀ = (WithZero.map' (MonoidHom.inl G₀ˣ H₀ˣ)).comp ↑WithZero.withZeroUnitsEquiv.symm

def MonoidWithZeroHom.inr (G₀ : Type u_1) (H₀ : Type u_2) [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] : H₀ →*₀ WithZero (G₀ˣ × H₀ˣ)

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.

Equations

• MonoidWithZeroHom.inr G₀ H₀ = (WithZero.map' (MonoidHom.inr G₀ˣ H₀ˣ)).comp ↑WithZero.withZeroUnitsEquiv.symm

def MonoidWithZeroHom.fst (G₀ : Type u_1) (H₀ : Type u_2) [GroupWithZero G₀] [GroupWithZero H₀] : WithZero (G₀ˣ × H₀ˣ) →*₀ G₀

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.

Equations

• MonoidWithZeroHom.fst G₀ H₀ = WithZero.lift' ((Units.coeHom G₀).comp (MonoidHom.fst G₀ˣ H₀ˣ))

def MonoidWithZeroHom.snd (G₀ : Type u_1) (H₀ : Type u_2) [GroupWithZero G₀] [GroupWithZero H₀] : WithZero (G₀ˣ × H₀ˣ) →*₀ H₀

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.

Equations

• MonoidWithZeroHom.snd G₀ H₀ = WithZero.lift' ((Units.coeHom H₀).comp (MonoidHom.snd G₀ˣ H₀ˣ))

@[simp]

theorem MonoidWithZeroHom.inl_apply_unit {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] (x : G₀ˣ) : (inl G₀ H₀) ↑x = ↑(x, 1)

@[simp]

theorem MonoidWithZeroHom.inr_apply_unit {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] (x : H₀ˣ) : (inr G₀ H₀) ↑x = ↑(1, x)

@[simp]

theorem MonoidWithZeroHom.fst_apply_coe {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] (x : G₀ˣ × H₀ˣ) : (fst G₀ H₀) ↑x = ↑x.1

@[simp]

theorem MonoidWithZeroHom.snd_apply_coe {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] (x : G₀ˣ × H₀ˣ) : (snd G₀ H₀) ↑x = ↑x.2

@[simp]

theorem MonoidWithZeroHom.fst_inl {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] (x : G₀) : (fst G₀ H₀) ((inl G₀ H₀) x) = x

@[simp]

theorem MonoidWithZeroHom.fst_comp_inl {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] : (fst G₀ H₀).comp (inl G₀ H₀) = id G₀

@[simp]

theorem MonoidWithZeroHom.snd_comp_inl {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] : (snd G₀ H₀).comp (inl G₀ H₀) = 1

theorem MonoidWithZeroHom.snd_inl_apply_of_ne_zero {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] {x : G₀} (hx : x ≠ 0) : (snd G₀ H₀) ((inl G₀ H₀) x) = 1

@[simp]

theorem MonoidWithZeroHom.fst_comp_inr {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] : (fst G₀ H₀).comp (inr G₀ H₀) = 1

theorem MonoidWithZeroHom.fst_inr_apply_of_ne_zero {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] {x : H₀} (hx : x ≠ 0) : (fst G₀ H₀) ((inr G₀ H₀) x) = 1

@[simp]

theorem MonoidWithZeroHom.snd_inr {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] (x : H₀) : (snd G₀ H₀) ((inr G₀ H₀) x) = x

@[simp]

theorem MonoidWithZeroHom.snd_comp_inr {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] : (snd G₀ H₀).comp (inr G₀ H₀) = id H₀

theorem MonoidWithZeroHom.inl_injective {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] : Function.Injective ⇑(inl G₀ H₀)

theorem MonoidWithZeroHom.inr_injective {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] : Function.Injective ⇑(inr G₀ H₀)

theorem MonoidWithZeroHom.fst_surjective {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] : Function.Surjective ⇑(fst G₀ H₀)

theorem MonoidWithZeroHom.snd_surjective {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : H₀) => x = 0] : Function.Surjective ⇑(snd G₀ H₀)

theorem MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] [DecidablePred fun (x : H₀) => x = 0] (m : G₀ˣ) (n : H₀ˣ) : (inl G₀ H₀) ↑m * (inr G₀ H₀) ↑n = ↑(m, n)

theorem MonoidWithZeroHom.commute_inl_inr {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] [DecidablePred fun (x : G₀) => x = 0] [DecidablePred fun (x : H₀) => x = 0] (m : G₀) (n : H₀) : Commute ((inl G₀ H₀) m) ((inr G₀ H₀) n)