Homomorphisms out of a product of monoids, and products of isomorphisms

A product of two monoids is their coproduct in commutative monoids: a homomorphism M × N →* P with P commutative is the same data as a pair of homomorphisms M →* P and N →* P, recovered by restricting along the two inclusions. Mathlib has the two directions separately, as MonoidHom.coprod and composition with MonoidHom.inl and MonoidHom.inr, together with the fact that they are mutually inverse; this file packages them as the corresponding equivalence.

The file also records the value and the inverse of a product MulEquiv.prodCongr of two multiplicative isomorphisms, which Mathlib states only for the underlying Equiv.prodCongr, and recognizes a commutative monoid with projections and inclusions satisfying the biproduct identities as the product of the two factors.

Main definitions

• MonoidHom.coprodEquiv: the multiplicative equivalence ((M →* P) × (N →* P)) ≃* (M × N →* P) for P a commutative monoid.
• MulEquiv.ofProdCoprod: the multiplicative equivalence P ≃* A × B determined by projections P →* A, P →* B and inclusions A →* P, B →* P satisfying the biproduct identities.
• MulEquiv.prodCongr_apply, MulEquiv.prodCongr_symm: the product of two isomorphisms acts componentwise, and its inverse is the product of the inverses.

def MonoidHom.coprodEquiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [CommMonoid P] : (M →* P) × (N →* P) ≃* (M × N →* P)

Homomorphisms from a product of two monoids to a commutative monoid P are pairs of homomorphisms out of the factors: the forward map is MonoidHom.coprod and the inverse restricts along MonoidHom.inl and MonoidHom.inr.

Equations

• One or more equations did not get rendered due to their size.

def AddMonoidHom.coprodEquiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] : (M →+ P) × (N →+ P) ≃+ (M × N →+ P)

Homomorphisms from a product of two additive monoids to a commutative additive monoid P are pairs of homomorphisms out of the factors: the forward map is AddMonoidHom.coprod and the inverse restricts along AddMonoidHom.inl and AddMonoidHom.inr.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidHom.coprodEquiv_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : (M →* P) × (N →* P)) (x : M × N) : (coprodEquiv f) x = f.1 x.1 * f.2 x.2

@[simp]

theorem AddMonoidHom.coprodEquiv_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : (M →+ P) × (N →+ P)) (x : M × N) : (coprodEquiv f) x = f.1 x.1 + f.2 x.2

The homomorphism attached to a pair of homomorphisms out of the factors is their coproduct.

@[simp]

theorem MonoidHom.coprodEquiv_symm_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M × N →* P) : coprodEquiv.symm f = (f.comp (inl M N), f.comp (inr M N))

@[simp]

theorem AddMonoidHom.coprodEquiv_symm_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M × N →+ P) : coprodEquiv.symm f = (f.comp (inl M N), f.comp (inr M N))

The pair of homomorphisms attached to a homomorphism out of a product restricts it along the two inclusions.

@[simp]

theorem MulEquiv.prodCongr_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M ≃* M') (g : N ≃* N') (x : M × N) : (f.prodCongr g) x = (f x.1, g x.2)

The product of two multiplicative isomorphisms acts componentwise.

@[simp]

theorem AddEquiv.prodCongr_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') (x : M × N) : (f.prodCongr g) x = (f x.1, g x.2)

The product of two additive isomorphisms acts componentwise.

@[simp]

theorem MulEquiv.prodCongr_symm {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [MulOneClass M] [MulOneClass N] [MulOneClass M'] [MulOneClass N'] (f : M ≃* M') (g : N ≃* N') : (f.prodCongr g).symm = f.symm.prodCongr g.symm

The inverse of a product of two multiplicative isomorphisms is the product of the inverses.

@[simp]

theorem AddEquiv.prodCongr_symm {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') : (f.prodCongr g).symm = f.symm.prodCongr g.symm

The inverse of a product of two additive isomorphisms is the product of the inverses.

def MulEquiv.ofProdCoprod {P : Type u_5} {A : Type u_6} {B : Type u_7} [CommMonoid P] [MulOneClass A] [MulOneClass B] (fst : P →* A) (snd : P →* B) (inl : A →* P) (inr : B →* P) (h : (inl.coprod inr).comp (fst.prod snd) = MonoidHom.id P) (fst_inl : fst.comp inl = MonoidHom.id A) (fst_inr : fst.comp inr = 1) (snd_inl : snd.comp inl = 1) (snd_inr : snd.comp inr = MonoidHom.id B) : P ≃* A × B

A commutative monoid P with projections fst : P →* A, snd : P →* B and inclusions inl : A →* P, inr : B →* P satisfying the biproduct identities is the product A × B: the forward map is fst.prod snd and the inverse is inl.coprod inr.

Equations

• MulEquiv.ofProdCoprod fst snd inl inr h fst_inl fst_inr snd_inl snd_inr = { toFun := ⇑(fst.prod snd), invFun := ⇑(inl.coprod inr), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

def AddEquiv.ofProdCoprod {P : Type u_5} {A : Type u_6} {B : Type u_7} [AddCommMonoid P] [AddZeroClass A] [AddZeroClass B] (fst : P →+ A) (snd : P →+ B) (inl : A →+ P) (inr : B →+ P) (h : (inl.coprod inr).comp (fst.prod snd) = AddMonoidHom.id P) (fst_inl : fst.comp inl = AddMonoidHom.id A) (fst_inr : fst.comp inr = 0) (snd_inl : snd.comp inl = 0) (snd_inr : snd.comp inr = AddMonoidHom.id B) : P ≃+ A × B

An additive commutative monoid P with projections fst : P →+ A, snd : P →+ B and inclusions inl : A →+ P, inr : B →+ P satisfying the biproduct identities is the product A × B: the forward map is fst.prod snd and the inverse is inl.coprod inr.

Equations

• AddEquiv.ofProdCoprod fst snd inl inr h fst_inl fst_inr snd_inl snd_inr = { toFun := ⇑(fst.prod snd), invFun := ⇑(inl.coprod inr), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem MulEquiv.ofProdCoprod_apply {P : Type u_5} {A : Type u_6} {B : Type u_7} [CommMonoid P] [MulOneClass A] [MulOneClass B] (fst : P →* A) (snd : P →* B) (inl : A →* P) (inr : B →* P) (h : (inl.coprod inr).comp (fst.prod snd) = MonoidHom.id P) (fst_inl : fst.comp inl = MonoidHom.id A) (fst_inr : fst.comp inr = 1) (snd_inl : snd.comp inl = 1) (snd_inr : snd.comp inr = MonoidHom.id B) (x : P) : (ofProdCoprod fst snd inl inr h fst_inl fst_inr snd_inl snd_inr) x = (fst x, snd x)

The equivalence MulEquiv.ofProdCoprod is given by the two projections.

@[simp]

theorem AddEquiv.ofProdCoprod_apply {P : Type u_5} {A : Type u_6} {B : Type u_7} [AddCommMonoid P] [AddZeroClass A] [AddZeroClass B] (fst : P →+ A) (snd : P →+ B) (inl : A →+ P) (inr : B →+ P) (h : (inl.coprod inr).comp (fst.prod snd) = AddMonoidHom.id P) (fst_inl : fst.comp inl = AddMonoidHom.id A) (fst_inr : fst.comp inr = 0) (snd_inl : snd.comp inl = 0) (snd_inr : snd.comp inr = AddMonoidHom.id B) (x : P) : (ofProdCoprod fst snd inl inr h fst_inl fst_inr snd_inl snd_inr) x = (fst x, snd x)

The equivalence AddEquiv.ofProdCoprod is given by the two projections.

@[simp]

theorem MulEquiv.ofProdCoprod_symm_apply {P : Type u_5} {A : Type u_6} {B : Type u_7} [CommMonoid P] [MulOneClass A] [MulOneClass B] (fst : P →* A) (snd : P →* B) (inl : A →* P) (inr : B →* P) (h : (inl.coprod inr).comp (fst.prod snd) = MonoidHom.id P) (fst_inl : fst.comp inl = MonoidHom.id A) (fst_inr : fst.comp inr = 1) (snd_inl : snd.comp inl = 1) (snd_inr : snd.comp inr = MonoidHom.id B) (x : A × B) : (ofProdCoprod fst snd inl inr h fst_inl fst_inr snd_inl snd_inr).symm x = inl x.1 * inr x.2

The inverse of MulEquiv.ofProdCoprod multiplies the two inclusions.

@[simp]

theorem AddEquiv.ofProdCoprod_symm_apply {P : Type u_5} {A : Type u_6} {B : Type u_7} [AddCommMonoid P] [AddZeroClass A] [AddZeroClass B] (fst : P →+ A) (snd : P →+ B) (inl : A →+ P) (inr : B →+ P) (h : (inl.coprod inr).comp (fst.prod snd) = AddMonoidHom.id P) (fst_inl : fst.comp inl = AddMonoidHom.id A) (fst_inr : fst.comp inr = 0) (snd_inl : snd.comp inl = 0) (snd_inr : snd.comp inr = AddMonoidHom.id B) (x : A × B) : (ofProdCoprod fst snd inl inr h fst_inl fst_inr snd_inl snd_inr).symm x = inl x.1 + inr x.2

The inverse of AddEquiv.ofProdCoprod adds the two inclusions.