Mathlib.GroupTheory.NoncommPiCoprod

Module docstring

{"# 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 homomorphism
Subgroup.noncommPiCoprod : (Π i, H i) →* G is the specialization to H i : Subgroup G and the subgroup embedding.

Main theorems

MonoidHom.noncommPiCoprod coincides with ϕ i when restricted to N i
MonoidHom.noncommPiCoprod_mrange: The range of MonoidHom.noncommPiCoprod is ⨆ (i : ι), (ϕ i).mrange
MonoidHom.noncommPiCoprod_range: The range of MonoidHom.noncommPiCoprod is ⨆ (i : ι), (ϕ i).range
Subgroup.noncommPiCoprod_range: The range of Subgroup.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 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.

MonoidHom.noncommPiCoprod definition

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

Full source

/-- The canonical homomorphism from a family of monoids. -/
@[to_additive "The canonical homomorphism from a family of additive monoids. See also
`LinearMap.lsum` for a linear version without the commutativity assumption."]
def noncommPiCoprod : (∀ i : ι, N i) →* M where
  toFun f := Finset.univ.noncommProd (fun i => ϕ i (f i)) fun _ _ _ _ h => hcomm h _ _
  map_one' := by
    apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)
    simp
  map_mul' f g := by
    classical
    convert @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
    · exact map_mul _ _ _
    · rintro i - j - h
      exact hcomm h _ _

Canonical homomorphism from a product of monoids with commuting images

Informal description

Given an index set $\iota$ and a family of monoids $N_i$ for each $i \in \iota$, together with monoid homomorphisms $\phi_i : N_i \to M$ such that the images of any two distinct homomorphisms commute, there exists a canonical homomorphism $\text{noncommPiCoprod} : \prod_{i \in \iota} N_i \to M$ that combines the $\phi_i$ into a single homomorphism. More precisely, for any element $f \in \prod_{i \in \iota} N_i$, the homomorphism is defined by: \[ \text{noncommPiCoprod}(f) = \prod_{i \in \iota} \phi_i(f(i)) \] where the product is taken in any order (since the images commute pairwise). This homomorphism satisfies $\text{noncommPiCoprod}(\text{mulSingle}_i(y)) = \phi_i(y)$ for any $i \in \iota$ and $y \in N_i$, where $\text{mulSingle}_i(y)$ is the element of $\prod_{i \in \iota} N_i$ that is $y$ at index $i$ and $1$ elsewhere.

MonoidHom.noncommPiCoprod_mulSingle theorem

[DecidableEq ι] (i : ι) (y : N i) : noncommPiCoprod ϕ hcomm (Pi.mulSingle i y) = ϕ i y

Full source

@[to_additive (attr := simp)]
theorem noncommPiCoprod_mulSingle [DecidableEq ι] (i : ι) (y : N i) :
    noncommPiCoprod ϕ hcomm (Pi.mulSingle i y) = ϕ i y := by
  change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _)
    = ϕ i y
  rw [← Finset.insert_erase (Finset.mem_univ i)]
  rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ (Finset.not_mem_erase i _)]
  rw [Pi.mulSingle_eq_same]
  rw [Finset.noncommProd_eq_pow_card]
  · rw [one_pow]
    exact mul_one _
  · intro j hj
    simp only [Finset.mem_erase] at hj
    simp [hj]

Canonical Homomorphism Evaluated on Single Component: $\text{noncommPiCoprod}(\text{mulSingle}_i(y)) = \phi_i(y)$

Informal description

Let $\iota$ be a finite index set with decidable equality, and let $(N_i)_{i \in \iota}$ be a family of monoids. Given a family of monoid homomorphisms $\phi_i \colon N_i \to M$ such that the images of any two distinct homomorphisms commute, the canonical homomorphism $\text{noncommPiCoprod} \colon \prod_{i \in \iota} N_i \to M$ satisfies \[ \text{noncommPiCoprod}(\text{mulSingle}_i(y)) = \phi_i(y) \] for any $i \in \iota$ and $y \in N_i$, where $\text{mulSingle}_i(y)$ denotes the element of $\prod_{i \in \iota} N_i$ that is $y$ at index $i$ and the identity elsewhere.

MonoidHom.noncommPiCoprodEquiv definition

 [DecidableEq ι] : { ϕ : ∀ i, N i →* M // Pairwise fun i j => ∀ x y, Commute (ϕ i x) (ϕ j y) } ≃ ((∀ i, N i) →* M)

Full source

/--
The universal property of `MonoidHom.noncommPiCoprod`

Given monoid morphisms `φᵢ : Nᵢ → M` whose images pairwise commute,
there exists a unique monoid morphism `φ : Πᵢ Nᵢ → M` that induces the `φᵢ`,
and it is given by `MonoidHom.noncommPiCoprod`. -/
@[to_additive "The universal property of `MonoidHom.noncommPiCoprod`

Given monoid morphisms `φᵢ : Nᵢ → M` whose images pairwise commute,
there exists a unique monoid morphism `φ : Πᵢ Nᵢ → M` that induces the `φᵢ`,
and it is given by `AddMonoidHom.noncommPiCoprod`."]
def noncommPiCoprodEquiv [DecidableEq ι] :
    { ϕ : ∀ i, N i →* M // Pairwise fun i j => ∀ x y, Commute (ϕ i x) (ϕ j y) }{ ϕ : ∀ i, N i →* M // Pairwise fun i j => ∀ x y, Commute (ϕ i x) (ϕ j y) } ≃
      ((∀ i, N i) →* M) where
  toFun ϕ := noncommPiCoprod ϕ.1 ϕ.2
  invFun f :=
    ⟨fun i => f.comp (MonoidHom.mulSingle N i), fun _ _ hij x y =>
      Commute.map (Pi.mulSingle_commute hij x y) f⟩
  left_inv ϕ := by
    ext
    simp only [coe_comp, Function.comp_apply, mulSingle_apply, noncommPiCoprod_mulSingle]
  right_inv f := pi_ext fun i x => by
    simp only [noncommPiCoprod_mulSingle, coe_comp, Function.comp_apply, mulSingle_apply]

Equivalence between families of commuting homomorphisms and product homomorphisms

Informal description

Given a finite index set $\iota$ and a family of monoids $N_i$ for each $i \in \iota$, there is an equivalence between: 1. The type of pairs $(\phi, h_{\text{comm}})$ where $\phi = (\phi_i : N_i \to M)_{i \in \iota}$ is a family of monoid homomorphisms whose images pairwise commute (i.e., for any $i \neq j$ and any $x \in N_i$, $y \in N_j$, the elements $\phi_i(x)$ and $\phi_j(y)$ commute in $M$), and 2. The type of monoid homomorphisms $\prod_{i \in \iota} N_i \to M$. The equivalence is given by: - The forward map takes $(\phi, h_{\text{comm}})$ to the canonical homomorphism $\text{noncommPiCoprod} \phi$ which combines the $\phi_i$ into a single homomorphism. - The inverse map takes a homomorphism $f : \prod_{i \in \iota} N_i \to M$ and produces the family of homomorphisms $(f \circ \text{mulSingle}_i)_{i \in \iota}$, where $\text{mulSingle}_i$ is the inclusion of $N_i$ into the product. This equivalence establishes that $\text{noncommPiCoprod}$ is the universal construction for combining commuting homomorphisms from a product of monoids.

MonoidHom.noncommPiCoprod_mrange theorem

: MonoidHom.mrange (noncommPiCoprod ϕ hcomm) = ⨆ i : ι, MonoidHom.mrange (ϕ i)

Full source

@[to_additive]
theorem noncommPiCoprod_mrange :
    MonoidHom.mrange (noncommPiCoprod ϕ hcomm) = ⨆ i : ι, MonoidHom.mrange (ϕ i) := by
  letI := Classical.decEq ι
  apply le_antisymm
  · rintro x ⟨f, rfl⟩
    refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
    apply Submonoid.mem_sSup_of_mem
    · use i
    simp
  · refine iSup_le ?_
    rintro i x ⟨y, rfl⟩
    exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

Range of Canonical Homomorphism from Product of Monoids with Commuting Images

Informal description

Let $\iota$ be an index set and $(N_i)_{i \in \iota}$ be a family of monoids. Given a family of monoid homomorphisms $\phi_i \colon N_i \to M$ such that the images of any two distinct homomorphisms commute, the range of the canonical homomorphism $\text{noncommPiCoprod} \colon \prod_{i \in \iota} N_i \to M$ is equal to the supremum of the ranges of the individual homomorphisms $\phi_i$: \[ \text{range}(\text{noncommPiCoprod}) = \bigsqcup_{i \in \iota} \text{range}(\phi_i) \]

MonoidHom.commute_noncommPiCoprod theorem

 {m : M} (comm : ∀ i (x : N i), Commute m ((ϕ i x))) (h : (i : ι) → N i) :
  Commute m (MonoidHom.noncommPiCoprod ϕ hcomm h)

Full source

@[to_additive]
lemma commute_noncommPiCoprod {m : M}
    (comm : ∀ i (x : N i), Commute m ((ϕ i x))) (h : (i : ι) → N i) :
    Commute m (MonoidHom.noncommPiCoprod ϕ hcomm h) := by
  dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]
  apply Finset.noncommProd_induction
  · exact fun x y ↦ Commute.mul_right
  · exact Commute.one_right _
  · exact fun x _ ↦ comm x (h x)

Commutation with Canonical Homomorphism from Product of Monoids

Informal description

Let $M$ be a monoid and $\{N_i\}_{i \in \iota}$ be a family of monoids indexed by $\iota$. Given a family of monoid homomorphisms $\phi_i : N_i \to M$ such that the images of any two distinct homomorphisms commute, and an element $m \in M$ that commutes with $\phi_i(x)$ for all $i \in \iota$ and $x \in N_i$, then $m$ commutes with the image of any element $h \in \prod_{i \in \iota} N_i$ under the canonical homomorphism $\text{noncommPiCoprod}(\phi, h_{\text{comm}})$. In other words, if $m$ commutes with every $\phi_i(x)$, then for any $h \in \prod_{i \in \iota} N_i$, we have: \[ m \cdot \text{noncommPiCoprod}(\phi, h_{\text{comm}})(h) = \text{noncommPiCoprod}(\phi, h_{\text{comm}})(h) \cdot m \]

MonoidHom.noncommPiCoprod_apply theorem

 (h : (i : ι) → N i) :
  MonoidHom.noncommPiCoprod ϕ hcomm h =
    Finset.noncommProd Finset.univ (fun i ↦ ϕ i (h i)) (Pairwise.set_pairwise (fun ⦃i j⦄ a ↦ hcomm a (h i) (h j)) _)

Full source

@[to_additive]
lemma noncommPiCoprod_apply (h : (i : ι) → N i) :
    MonoidHom.noncommPiCoprod ϕ hcomm h = Finset.noncommProd Finset.univ (fun i ↦ ϕ i (h i))
      (Pairwise.set_pairwise (fun ⦃i j⦄ a ↦ hcomm a (h i) (h j)) _) := by
  dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

Evaluation of Canonical Homomorphism from Product of Monoids with Commuting Images

Informal description

For any family of elements $h \in \prod_{i \in \iota} N_i$, the canonical homomorphism $\text{noncommPiCoprod}$ evaluates as: \[ \text{noncommPiCoprod}(\phi, h_{\text{comm}})(h) = \prod_{i \in \iota} \phi_i(h(i)) \] where the product is taken over all indices $i \in \iota$ in any order (since the images of $\phi_i$ and $\phi_j$ commute for all $i \neq j$).

MonoidHom.noncommPiCoprod_range theorem

 [Fintype ι] {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} :
  (noncommPiCoprod ϕ hcomm).range = ⨆ i : ι, (ϕ i).range

Full source

@[to_additive]
theorem noncommPiCoprod_range [Fintype ι]
    {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} :
    (noncommPiCoprod ϕ hcomm).range = ⨆ i : ι, (ϕ i).range := by
  letI := Classical.decEq ι
  apply le_antisymm
  · rintro x ⟨f, rfl⟩
    refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_
    intro i _hi
    apply Subgroup.mem_sSup_of_mem
    · use i
    simp
  · refine iSup_le ?_
    rintro i x ⟨y, rfl⟩
    exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

Range of Canonical Homomorphism from Product of Groups with Commuting Images Equals Supremum of Component Ranges

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $H_i$ be a subgroup of a group $G$ and $\phi_i \colon H_i \to G$ be a group homomorphism. Suppose that for any distinct $i, j \in \iota$, the images of $\phi_i$ and $\phi_j$ commute pairwise, i.e., $\phi_i(x)$ commutes with $\phi_j(y)$ for all $x \in H_i$ and $y \in H_j$. Then the range of the canonical homomorphism $\text{noncommPiCoprod}(\phi, h_{\text{comm}}) \colon \prod_{i \in \iota} H_i \to G$ is equal to the supremum of the ranges of the $\phi_i$: \[ \text{range}(\text{noncommPiCoprod}(\phi, h_{\text{comm}})) = \bigsqcup_{i \in \iota} \text{range}(\phi_i). \]

MonoidHom.injective_noncommPiCoprod_of_iSupIndep theorem

 [Fintype ι] {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)}
  (hind : iSupIndep fun i => (ϕ i).range) (hinj : ∀ i, Function.Injective (ϕ i)) :
  Function.Injective (noncommPiCoprod ϕ hcomm)

Full source

@[to_additive]
theorem injective_noncommPiCoprod_of_iSupIndep [Fintype ι]
    {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)}
    (hind : iSupIndep fun i => (ϕ i).range)
    (hinj : ∀ i, Function.Injective (ϕ i)) : Function.Injective (noncommPiCoprod ϕ hcomm) := by
  classical
    apply (MonoidHom.ker_eq_bot_iff _).mp
    rw [eq_bot_iff]
    intro f heq1
    have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
      Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
        _ hind (by simp) heq1
    ext i
    apply hinj
    simp [this i (Finset.mem_univ i)]

Injectivity of Canonical Homomorphism from Product of Groups with Independent Ranges

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $H_i$ be a subgroup of a group $G$ and $\phi_i : H_i \to G$ be a group homomorphism. Suppose that: 1. For any distinct $i, j \in \iota$, the images of $\phi_i$ and $\phi_j$ commute pairwise, i.e., $\phi_i(x)$ commutes with $\phi_j(y)$ for all $x \in H_i$ and $y \in H_j$. 2. The family of ranges $(\phi_i(H_i))_{i \in \iota}$ is independent (i.e., their supremum is independent). 3. Each $\phi_i$ is injective. Then the canonical homomorphism $\text{noncommPiCoprod} : \prod_{i \in \iota} H_i \to G$ combining the $\phi_i$ is injective.

MonoidHom.independent_range_of_coprime_order theorem

 (hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)) [Finite ι] [∀ i, Fintype (H i)]
  (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
  iSupIndep fun i => (ϕ i).range

Full source

@[to_additive]
theorem independent_range_of_coprime_order
    (hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y))
    [Finite ι] [∀ i, Fintype (H i)]
    (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
    iSupIndep fun i => (ϕ i).range := by
  cases nonempty_fintype ι
  letI := Classical.decEq ι
  rintro i
  rw [disjoint_iff_inf_le]
  rintro f ⟨hxi, hxp⟩
  dsimp at hxi hxp
  rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
  rotate_left
  · intro _ _ hj
    apply hcomm
    exact hj ∘ Subtype.ext
  obtain ⟨g, hgf⟩ := hxp
  obtain ⟨g', hg'f⟩ := hxi
  have hxi : orderOforderOf f ∣ Fintype.card (H i) := by
    rw [← hg'f]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
  have hxp : orderOforderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) := by
    rw [← hgf, ← Fintype.card_pi]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
  change f = 1
  rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
  obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
  use c
  rw [← hc]
  symm
  rw [← Nat.coprime_iff_gcd_eq_one, Nat.coprime_fintype_prod_left_iff, Subtype.forall]
  intro j h
  exact hcoprime h

Independence of Homomorphic Ranges for Groups with Pairwise Commuting Images and Coprime Orders

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $H_i$ be a finite subgroup of a group $G$ and $\phi_i \colon H_i \to G$ be a group homomorphism. Suppose that: 1. For any distinct $i, j \in \iota$, the images of $\phi_i$ and $\phi_j$ commute pairwise, i.e., $\phi_i(x)$ commutes with $\phi_j(y)$ for all $x \in H_i$ and $y \in H_j$. 2. The orders of $H_i$ and $H_j$ are coprime for any distinct $i, j \in \iota$. Then the family of ranges $(\phi_i(H_i))_{i \in \iota}$ is independent, meaning that their supremum is independent.

Subgroup.commute_subtype_of_commute theorem

 (hcomm : Pairwise fun 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)

Full source

@[to_additive]
theorem commute_subtype_of_commute
    (hcomm : Pairwise fun 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) := by
  rintro ⟨x, hx⟩ ⟨y, hy⟩
  exact hcomm hne x y hx hy

Commutation of Subgroup Inclusions Under Pairwise Commutativity

Informal description

Let $G$ be a group with subgroups $H_i$ for $i$ in some index set $\iota$. Suppose that for any distinct $i,j \in \iota$, any $x \in H_i$ and $y \in H_j$ commute in $G$. Then for any distinct $i,j \in \iota$, the images of $x \in H_i$ and $y \in H_j$ under the inclusion maps $H_i \hookrightarrow G$ and $H_j \hookrightarrow G$ commute in $G$.

Subgroup.independent_of_coprime_order theorem

 (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) [Finite ι] [∀ i, Fintype (H i)]
  (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) : iSupIndep H

Full source

@[to_additive]
theorem independent_of_coprime_order
    (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
    [Finite ι] [∀ i, Fintype (H i)]
    (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
    iSupIndep H := by
  simpa using
    MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
      (commute_subtype_of_commute hcomm) hcoprime

Independence of Commuting Subgroups with Coprime Orders

Informal description

Let $G$ be a group with a finite family of subgroups $(H_i)_{i \in \iota}$ such that: 1. For any distinct $i, j \in \iota$, the elements of $H_i$ and $H_j$ commute in $G$. 2. The orders of $H_i$ and $H_j$ are coprime for any distinct $i, j \in \iota$. Then the family of subgroups $(H_i)_{i \in \iota}$ is independent, meaning their supremum is independent.

Subgroup.noncommPiCoprod definition

(hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) : (∀ i : ι, H i) →* G

Full source

/-- The canonical homomorphism from a family of subgroups where elements from different subgroups
commute -/
@[to_additive "The canonical homomorphism from a family of additive subgroups where elements from
different subgroups commute"]
def noncommPiCoprod (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) :
    (∀ i : ι, H i) →* G :=
  MonoidHom.noncommPiCoprod (fun i => (H i).subtype) (commute_subtype_of_commute hcomm)

Canonical homomorphism from a product of commuting subgroups

Informal description

Given a group $G$ and a family of subgroups $H_i$ indexed by $i \in \iota$, if for any distinct $i, j \in \iota$ the elements of $H_i$ and $H_j$ commute in $G$, then there exists a canonical group homomorphism $\text{noncommPiCoprod} : \prod_{i \in \iota} H_i \to G$ that combines the inclusion maps $H_i \hookrightarrow G$ into a single homomorphism. More precisely, for any element $f \in \prod_{i \in \iota} H_i$, the homomorphism is defined by: \[ \text{noncommPiCoprod}(f) = \prod_{i \in \iota} f(i) \] where the product is taken in any order (since the subgroups commute pairwise). This homomorphism satisfies $\text{noncommPiCoprod}(\text{mulSingle}_i(y)) = y$ for any $i \in \iota$ and $y \in H_i$, where $\text{mulSingle}_i(y)$ is the element of $\prod_{i \in \iota} H_i$ that is $y$ at index $i$ and $1$ elsewhere.

Subgroup.noncommPiCoprod_mulSingle theorem

 [DecidableEq ι] {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} (i : ι) (y : H i) :
  noncommPiCoprod hcomm (Pi.mulSingle i y) = y

Full source

@[to_additive (attr := simp)]
theorem noncommPiCoprod_mulSingle [DecidableEq ι]
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}(i : ι) (y : H i) :
    noncommPiCoprod hcomm (Pi.mulSingle i y) = y := by apply MonoidHom.noncommPiCoprod_mulSingle

Canonical Homomorphism Evaluated on Single Component: $\text{noncommPiCoprod}(\text{mulSingle}_i(y)) = y$

Informal description

Let $G$ be a group with a family of subgroups $(H_i)_{i \in \iota}$ indexed by a finite set $\iota$ with decidable equality. Suppose that for any distinct $i, j \in \iota$, the elements of $H_i$ and $H_j$ commute in $G$. Then for any $i \in \iota$ and $y \in H_i$, the canonical homomorphism $\text{noncommPiCoprod} \colon \prod_{i \in \iota} H_i \to G$ satisfies \[ \text{noncommPiCoprod}(\text{mulSingle}_i(y)) = y, \] where $\text{mulSingle}_i(y)$ denotes the element of $\prod_{i \in \iota} H_i$ that is $y$ at index $i$ and the identity elsewhere.

Subgroup.noncommPiCoprod_range theorem

 {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} :
  (noncommPiCoprod hcomm).range = ⨆ i : ι, H i

Full source

@[to_additive]
theorem noncommPiCoprod_range
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} :
    (noncommPiCoprod hcomm).range = ⨆ i : ι, H i := by
  simp [noncommPiCoprod, MonoidHom.noncommPiCoprod_range]

Range of Canonical Homomorphism from Product of Commuting Subgroups Equals Their Supremum

Informal description

Let $G$ be a group with a family of subgroups $(H_i)_{i \in \iota}$. Suppose that for any distinct $i, j \in \iota$, the elements of $H_i$ and $H_j$ commute in $G$. Then the range of the canonical homomorphism $\text{noncommPiCoprod} \colon \prod_{i \in \iota} H_i \to G$ is equal to the supremum of the subgroups $(H_i)_{i \in \iota}$: \[ \text{range}(\text{noncommPiCoprod}) = \bigsqcup_{i \in \iota} H_i. \]

Subgroup.injective_noncommPiCoprod_of_iSupIndep theorem

 {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} (hind : iSupIndep H) :
  Function.Injective (noncommPiCoprod hcomm)

Full source

@[to_additive]
theorem injective_noncommPiCoprod_of_iSupIndep
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}
    (hind : iSupIndep H) :
    Function.Injective (noncommPiCoprod hcomm) := by
  apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
  · simpa using hind
  · intro i
    exact Subtype.coe_injective

Injectivity of the Canonical Homomorphism from Product of Commuting Independent Subgroups

Informal description

Let $G$ be a group with a family of subgroups $(H_i)_{i \in \iota}$. Suppose that: 1. For any distinct $i, j \in \iota$, the elements of $H_i$ and $H_j$ commute in $G$. 2. The family of subgroups $(H_i)_{i \in \iota}$ is independent (i.e., their supremum is independent). Then the canonical homomorphism $\text{noncommPiCoprod} \colon \prod_{i \in \iota} H_i \to G$ is injective.

Subgroup.noncommPiCoprod_apply theorem

 (comm) (u : (i : ι) → H i) :
  Subgroup.noncommPiCoprod comm u =
    Finset.noncommProd Finset.univ (fun i ↦ u i) (fun i _ j _ h ↦ comm h _ _ (u i).prop (u j).prop)

Full source

@[to_additive]
theorem noncommPiCoprod_apply (comm) (u : (i : ι) → H i) :
    Subgroup.noncommPiCoprod comm u = Finset.noncommProd Finset.univ (fun i ↦ u i)
      (fun i _ j _ h ↦ comm h _ _ (u i).prop (u j).prop) := by
  simp only [Subgroup.noncommPiCoprod, MonoidHom.noncommPiCoprod,
    coe_subtype, MonoidHom.coe_mk, OneHom.coe_mk]

Evaluation of Canonical Homomorphism from Product of Commuting Subgroups

Informal description

Let $G$ be a group with subgroups $H_i$ for $i$ in some index set $\iota$, and suppose that for any distinct $i,j \in \iota$, any $x \in H_i$ and $y \in H_j$ commute in $G$. Then for any family of elements $u \in \prod_{i \in \iota} H_i$, the canonical homomorphism $\text{noncommPiCoprod}$ satisfies: \[ \text{noncommPiCoprod}(u) = \prod_{i \in \iota} u(i), \] where the product on the right is taken in any order (since the elements from different subgroups commute).