Canonical homomorphism from a finite family of monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 monoid_hom.noncomm_pi_coprod : (Π i, N i) →* M that coincides with ϕ

Main definitions #

monoid_hom.noncomm_pi_coprod : (Π i, N i) →* M is the main homomorphism
subgroup.noncomm_pi_coprod : (Π i, H i) →* G is the specialization to H i : subgroup G and the subgroup embedding.

Main theorems #

monoid_hom.noncomm_pi_coprod coincides with ϕ i when restricted to N i
monoid_hom.noncomm_pi_coprod_mrange: The range of monoid_hom.noncomm_pi_coprod is ⨆ (i : ι), (ϕ i).mrange
monoid_hom.noncomm_pi_coprod_range: The range of monoid_hom.noncomm_pi_coprod is ⨆ (i : ι), (ϕ i).range
subgroup.noncomm_pi_coprod_range: The range of subgroup.noncomm_pi_coprod is ⨆ (i : ι), H i.
monoid_hom.injective_noncomm_pi_coprod_of_independent: in the case of groups, pi_hom.hom is injective if the ϕ are injective and the ranges of the ϕ are independent.
monoid_hom.independent_range_of_coprime_order: If the N i have coprime orders, then the ranges of the ϕ are independent.
subgroup.independent_of_coprime_order: If commuting normal subgroups H i have coprime orders, they are independent.

source

theorem add_subgroup.eq_zero_of_noncomm_sum_eq_zero_of_independent {G : Type u_1} [add_group G] {ι : Type u_2} (s : finset ι) (f : ι → G) (comm : ↑s.pairwise (λ (a b : ι), add_commute (f a) (f b))) (K : ι → add_subgroup G) (hind : complete_lattice.independent K) (hmem : ∀ (x : ι), x ∈ s → f x ∈ K x) (heq1 : s.noncomm_sum f comm = 0) (i : ι) (H : i ∈ s) :

f i = 0

finset.noncomm_sum is “injective” in f if f maps into independent subgroups. This generalizes (one direction of) add_subgroup.disjoint_iff_add_eq_zero.

source

theorem subgroup.eq_one_of_noncomm_prod_eq_one_of_independent {G : Type u_1} [group G] {ι : Type u_2} (s : finset ι) (f : ι → G) (comm : ↑s.pairwise (λ (a b : ι), commute (f a) (f b))) (K : ι → subgroup G) (hind : complete_lattice.independent K) (hmem : ∀ (x : ι), x ∈ s → f x ∈ K x) (heq1 : s.noncomm_prod f comm = 1) (i : ι) (H : i ∈ s) :

f i = 1

finset.noncomm_prod is “injective” in f if f maps into independent subgroups. This generalizes (one direction of) subgroup.disjoint_iff_mul_eq_one.

source

def monoid_hom.noncomm_pi_coprod {M : Type u_1} [monoid M] {ι : Type u_2} [fintype ι] {N : ι → Type u_3} [Π (i : ι), monoid (N i)] (ϕ : Π (i : ι), N i →* M) (hcomm : pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), commute (⇑(ϕ i) x) (⇑(ϕ j) y))) :

(Π (i : ι), N i) →* M

The canonical homomorphism from a family of monoids.

Equations

monoid_hom.noncomm_pi_coprod ϕ hcomm = {to_fun := λ (f : Π (i : ι), N i), finset.univ.noncomm_prod (λ (i : ι), ⇑(ϕ i) (f i)) _, map_one' := _, map_mul' := _}

source

def add_monoid_hom.noncomm_pi_coprod {M : Type u_1} [add_monoid M] {ι : Type u_2} [fintype ι] {N : ι → Type u_3} [Π (i : ι), add_monoid (N i)] (ϕ : Π (i : ι), N i →+ M) (hcomm : pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y))) :

(Π (i : ι), N i) →+ M

The canonical homomorphism from a family of additive monoids.

See also linear_map.lsum for a linear version without the commutativity assumption.

Equations

add_monoid_hom.noncomm_pi_coprod ϕ hcomm = {to_fun := λ (f : Π (i : ι), N i), finset.univ.noncomm_sum (λ (i : ι), ⇑(ϕ i) (f i)) _, map_zero' := _, map_add' := _}

source

@[simp]

theorem monoid_hom.noncomm_pi_coprod_mul_single {M : Type u_1} [monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι → Type u_3} [Π (i : ι), monoid (N i)] (ϕ : Π (i : ι), N i →* M) {hcomm : pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), commute (⇑(ϕ i) x) (⇑(ϕ j) y))} (i : ι) (y : N i) :

⇑(monoid_hom.noncomm_pi_coprod ϕ hcomm) (pi.mul_single i y) = ⇑(ϕ i) y

source

@[simp]

theorem add_monoid_hom.noncomm_pi_coprod_single {M : Type u_1} [add_monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι → Type u_3} [Π (i : ι), add_monoid (N i)] (ϕ : Π (i : ι), N i →+ M) {hcomm : pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y))} (i : ι) (y : N i) :

⇑(add_monoid_hom.noncomm_pi_coprod ϕ hcomm) (pi.single i y) = ⇑(ϕ i) y

source

def monoid_hom.noncomm_pi_coprod_equiv {M : Type u_1} [monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι → Type u_3} [Π (i : ι), monoid (N i)] :

{ϕ // pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), commute (⇑(ϕ i) x) (⇑(ϕ j) y))} ≃ ((Π (i : ι), N i) →* M)

The universal property of noncomm_pi_coprod

Equations

monoid_hom.noncomm_pi_coprod_equiv = {to_fun := λ (ϕ : {ϕ // pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), commute (⇑(ϕ i) x) (⇑(ϕ j) y))}), monoid_hom.noncomm_pi_coprod ϕ.val _, inv_fun := λ (f : (Π (i : ι), N i) →* M), ⟨λ (i : ι), f.comp (monoid_hom.single N i), _⟩, left_inv := _, right_inv := _}

source

def add_monoid_hom.noncomm_pi_coprod_equiv {M : Type u_1} [add_monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι → Type u_3} [Π (i : ι), add_monoid (N i)] :

{ϕ // pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y))} ≃ ((Π (i : ι), N i) →+ M)

The universal property of noncomm_pi_coprod

Equations

add_monoid_hom.noncomm_pi_coprod_equiv = {to_fun := λ (ϕ : {ϕ // pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y))}), add_monoid_hom.noncomm_pi_coprod ϕ.val _, inv_fun := λ (f : (Π (i : ι), N i) →+ M), ⟨λ (i : ι), f.comp (add_monoid_hom.single N i), _⟩, left_inv := _, right_inv := _}

source

theorem add_monoid_hom.noncomm_pi_coprod_mrange {M : Type u_1} [add_monoid M] {ι : Type u_2} [fintype ι] {N : ι → Type u_3} [Π (i : ι), add_monoid (N i)] (ϕ : Π (i : ι), N i →+ M) {hcomm : pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y))} :

add_monoid_hom.mrange (add_monoid_hom.noncomm_pi_coprod ϕ hcomm) = ⨆ (i : ι), add_monoid_hom.mrange (ϕ i)

source

theorem monoid_hom.noncomm_pi_coprod_mrange {M : Type u_1} [monoid M] {ι : Type u_2} [fintype ι] {N : ι → Type u_3} [Π (i : ι), monoid (N i)] (ϕ : Π (i : ι), N i →* M) {hcomm : pairwise (λ (i j : ι), ∀ (x : N i) (y : N j), commute (⇑(ϕ i) x) (⇑(ϕ j) y))} :

monoid_hom.mrange (monoid_hom.noncomm_pi_coprod ϕ hcomm) = ⨆ (i : ι), monoid_hom.mrange (ϕ i)

source

theorem add_monoid_hom.noncomm_pi_coprod_range {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → Type u_3} [Π (i : ι), add_group (H i)] (ϕ : Π (i : ι), H i →+ G) {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y)} :

(add_monoid_hom.noncomm_pi_coprod ϕ hcomm).range = ⨆ (i : ι), (ϕ i).range

source

theorem monoid_hom.noncomm_pi_coprod_range {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → Type u_3} [Π (i : ι), group (H i)] (ϕ : Π (i : ι), H i →* G) {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), commute (⇑(ϕ i) x) (⇑(ϕ j) y)} :

(monoid_hom.noncomm_pi_coprod ϕ hcomm).range = ⨆ (i : ι), (ϕ i).range

source

theorem monoid_hom.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → Type u_3} [Π (i : ι), group (H i)] (ϕ : Π (i : ι), H i →* G) {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), commute (⇑(ϕ i) x) (⇑(ϕ j) y)} (hind : complete_lattice.independent (λ (i : ι), (ϕ i).range)) (hinj : ∀ (i : ι), function.injective ⇑(ϕ i)) :

function.injective ⇑(monoid_hom.noncomm_pi_coprod ϕ hcomm)

source

theorem add_monoid_hom.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → Type u_3} [Π (i : ι), add_group (H i)] (ϕ : Π (i : ι), H i →+ G) {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y)} (hind : complete_lattice.independent (λ (i : ι), (ϕ i).range)) (hinj : ∀ (i : ι), function.injective ⇑(ϕ i)) :

function.injective ⇑(add_monoid_hom.noncomm_pi_coprod ϕ hcomm)

source

theorem add_monoid_hom.independent_range_of_coprime_order {G : Type u_1} [add_group G] {ι : Type u_2} {H : ι → Type u_3} [Π (i : ι), add_group (H i)] (ϕ : Π (i : ι), H i →+ G) (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), add_commute (⇑(ϕ i) x) (⇑(ϕ j) y)) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : ∀ (i j : ι), i ≠ j → (fintype.card (H i)).coprime (fintype.card (H j))) :

complete_lattice.independent (λ (i : ι), (ϕ i).range)

source

theorem monoid_hom.independent_range_of_coprime_order {G : Type u_1} [group G] {ι : Type u_2} {H : ι → Type u_3} [Π (i : ι), group (H i)] (ϕ : Π (i : ι), H i →* G) (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), commute (⇑(ϕ i) x) (⇑(ϕ j) y)) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : ∀ (i j : ι), i ≠ j → (fintype.card (H i)).coprime (fintype.card (H j))) :

complete_lattice.independent (λ (i : ι), (ϕ i).range)

source

theorem subgroup.commute_subtype_of_commute {G : Type u_1} [group G] {ι : Type u_2} {H : ι → subgroup G} (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → commute x y) (i j : ι) (hne : i ≠ j) (x : ↥(H i)) (y : ↥(H j)) :

commute (⇑((H i).subtype) x) (⇑((H j).subtype) y)

source

theorem add_subgroup.commute_subtype_of_commute {G : Type u_1} [add_group G] {ι : Type u_2} {H : ι → add_subgroup G} (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → add_commute x y) (i j : ι) (hne : i ≠ j) (x : ↥(H i)) (y : ↥(H j)) :

add_commute (⇑((H i).subtype) x) (⇑((H j).subtype) y)

source

def add_subgroup.noncomm_pi_coprod {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → add_subgroup G} (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → add_commute x y) :

(Π (i : ι), ↥(H i)) →+ G

The canonical homomorphism from a family of additive subgroups where elements from different subgroups commute

Equations

add_subgroup.noncomm_pi_coprod hcomm = add_monoid_hom.noncomm_pi_coprod (λ (i : ι), (H i).subtype) _

source

def subgroup.noncomm_pi_coprod {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → subgroup G} (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → commute x y) :

(Π (i : ι), ↥(H i)) →* G

The canonical homomorphism from a family of subgroups where elements from different subgroups commute

Equations

subgroup.noncomm_pi_coprod hcomm = monoid_hom.noncomm_pi_coprod (λ (i : ι), (H i).subtype) _

source

@[simp]

theorem add_subgroup.noncomm_pi_coprod_single {G : Type u_1} [add_group G] {ι : Type u_2} [hdec : decidable_eq ι] [hfin : fintype ι] {H : ι → add_subgroup G} {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → add_commute x y} (i : ι) (y : ↥(H i)) :

⇑(add_subgroup.noncomm_pi_coprod hcomm) (pi.single i y) = ↑y

source

@[simp]

theorem subgroup.noncomm_pi_coprod_mul_single {G : Type u_1} [group G] {ι : Type u_2} [hdec : decidable_eq ι] [hfin : fintype ι] {H : ι → subgroup G} {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → commute x y} (i : ι) (y : ↥(H i)) :

⇑(subgroup.noncomm_pi_coprod hcomm) (pi.mul_single i y) = ↑y

source

theorem subgroup.noncomm_pi_coprod_range {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → subgroup G} {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → commute x y} :

(subgroup.noncomm_pi_coprod hcomm).range = ⨆ (i : ι), H i

source

theorem add_subgroup.noncomm_pi_coprod_range {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → add_subgroup G} {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → add_commute x y} :

(add_subgroup.noncomm_pi_coprod hcomm).range = ⨆ (i : ι), H i

source

theorem add_subgroup.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → add_subgroup G} {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → add_commute x y} (hind : complete_lattice.independent H) :

function.injective ⇑(add_subgroup.noncomm_pi_coprod hcomm)

source

theorem subgroup.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → subgroup G} {hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → commute x y} (hind : complete_lattice.independent H) :

function.injective ⇑(subgroup.noncomm_pi_coprod hcomm)

source

theorem subgroup.independent_of_coprime_order {G : Type u_1} [group G] {ι : Type u_2} {H : ι → subgroup G} (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → commute x y) [finite ι] [Π (i : ι), fintype ↥(H i)] (hcoprime : ∀ (i j : ι), i ≠ j → (fintype.card ↥(H i)).coprime (fintype.card ↥(H j))) :

complete_lattice.independent H

source

theorem add_subgroup.independent_of_coprime_order {G : Type u_1} [add_group G] {ι : Type u_2} {H : ι → add_subgroup G} (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → add_commute x y) [finite ι] [Π (i : ι), fintype ↥(H i)] (hcoprime : ∀ (i j : ι), i ≠ j → (fintype.card ↥(H i)).coprime (fintype.card ↥(H j))) :

complete_lattice.independent H