Canonical homomorphism from a finite family of monoids #
This file defines the construction of the canonical homomorphism from a family of monoids.
Given a family of morphisms ϕ i : N i →* M
for each i : ι
where elements in the
images of different morphisms commute, we obtain a canonical morphism
MonoidHom.noncommPiCoprod : (Π i, N i) →* M
that coincides with ϕ
Main definitions #
MonoidHom.noncommPiCoprod : (Π i, N i) →* M
is the main homomorphismSubgroup.noncommPiCoprod : (Π i, H i) →* G
is the specialization toH i : Subgroup G
and the subgroup embedding.
Main theorems #
MonoidHom.noncommPiCoprod
coincides withϕ i
when restricted toN i
MonoidHom.noncommPiCoprod_mrange
: The range ofMonoidHom.noncommPiCoprod
is⨆ (i : ι), (ϕ i).mrange
MonoidHom.noncommPiCoprod_range
: The range ofMonoidHom.noncommPiCoprod
is⨆ (i : ι), (ϕ i).range
Subgroup.noncommPiCoprod_range
: The range ofSubgroup.noncommPiCoprod
is⨆ (i : ι), H i
.MonoidHom.injective_noncommPiCoprod_of_iSupIndep
: in the case of groups,pi_hom.hom
is injective if theϕ
are injective and the ranges of theϕ
are independent.MonoidHom.independent_range_of_coprime_order
: If theN i
have coprime orders, then the ranges of theϕ
are independent.Subgroup.independent_of_coprime_order
: If commuting normal subgroupsH i
have coprime orders, they are independent.
Finset.noncommProd
is “injective” in f
if f
maps into independent subgroups. This
generalizes (one direction of) Subgroup.disjoint_iff_mul_eq_one
.
Finset.noncommSum
is “injective” in f
if f
maps into independent subgroups.
This generalizes (one direction of) AddSubgroup.disjoint_iff_add_eq_zero
.
Alias of Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep
.
Finset.noncommProd
is “injective” in f
if f
maps into independent subgroups. This
generalizes (one direction of) Subgroup.disjoint_iff_mul_eq_one
.
The canonical homomorphism from a family of monoids.
Equations
- MonoidHom.noncommPiCoprod ϕ hcomm = { toFun := fun (f : (i : ι) → N i) => Finset.univ.noncommProd (fun (i : ι) => (ϕ i) (f i)) ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The canonical homomorphism from a family of additive monoids. See also
LinearMap.lsum
for a linear version without the commutativity assumption.
Equations
- AddMonoidHom.noncommPiCoprod ϕ hcomm = { toFun := fun (f : (i : ι) → N i) => Finset.univ.noncommSum (fun (i : ι) => (ϕ i) (f i)) ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The universal property of MonoidHom.noncommPiCoprod
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal property of AddMonoidHom.noncommPiCoprod
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical homomorphism from a family of subgroups where elements from different subgroups commute
Equations
- Subgroup.noncommPiCoprod hcomm = MonoidHom.noncommPiCoprod (fun (i : ι) => (H i).subtype) ⋯
Instances For
The canonical homomorphism from a family of additive subgroups where elements from different subgroups commute
Equations
- AddSubgroup.noncommPiCoprod hcomm = AddMonoidHom.noncommPiCoprod (fun (i : ι) => (H i).subtype) ⋯