AddMonoidHom.noncommPiCoprod_single
theorem AddMonoidHom.noncommPiCoprod_single :
∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
{N : ι → Type u_3} [inst_3 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
{hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)} (i : ι) (y : N i),
(AddMonoidHom.noncommPiCoprod ϕ hcomm) (Pi.single i y) = (ϕ i) y
This theorem, named `AddMonoidHom.noncommPiCoprod_single`, states that for any type `M` with an `AddMonoid` structure, type `ι` with a `DecidableEq` and `Fintype` structure, and a function `N` from `ι` to a type with an `AddMonoid` structure, given a family of additively homomorphic functions `ϕ` from `N i` to `M` for each `i : ι`, and under the condition that for every pair of different indices `i` and `j`, the additive results of `ϕ i` and `ϕ j` commute for all values `x : N i` and `y : N j`. Then, for any `i : ι` and `y : N i`, the result of applying the non-commutative version of the `Pi`-coproduct operation (`AddMonoidHom.noncommPiCoprod ϕ hcomm`) to the function supported at `i` with value `y` and `0` elsewhere (`Pi.single i y`) is equal to the result of applying `ϕ i` to `y`. In simpler words, under these conditions, this theorem says that applying the additive homomorphism at a specific index to a specific value equals using the non-commuting coproduct operation to the function that only has value at that index.
More concisely: For any type `M` with an `AddMonoid` structure, type `ι` with a `DecidableEq` and `Fintype` structure, and a function `N : ι -> Types` to a type with an `AddMonoid` structure, if `ϕ : ∀ i : ι, N i -> M` is a family of additively homomorphic functions satisfying commutativity condition, then for all `i : ι` and `y : N i`, `AddMonoidHom.noncommPiCoprod ϕ hcomm (Pi.single i y) = ϕ i y`.
|
Subgroup.eq_one_of_noncommProd_eq_one_of_independent
theorem Subgroup.eq_one_of_noncommProd_eq_one_of_independent :
∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} (s : Finset ι) (f : ι → G)
(comm : (↑s).Pairwise fun a b => Commute (f a) (f b)) (K : ι → Subgroup G),
CompleteLattice.Independent K → (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
The theorem `Subgroup.eq_one_of_noncommProd_eq_one_of_independent` states that for a given type `G` with group structure, an index type `ι`, a finite set `s` of type `ι`, a function `f` from `ι` to `G`, and a function `K` mapping each index to a subgroup of `G`, if the pairwise product of each pair of elements in the set `s` commutes (i.e., `a * b = b * a` for any `a` and `b` in `s`), the subgroups `K` are independent, and each element of `f` applied to `s` belongs to the corresponding subgroup `K`, then if the noncommutative product of `f` over `s` equals the identity element `1`, every element `f(i)` for `i` in `s` must also equal `1`. This is effectively saying that the function `f` is "injective" when mapped into independent subgroups, which is a generalization of one direction of the property that disjoint subgroups multiply to yield the identity.
More concisely: If `G` is a group, `ι` is a finite index type, `s` is a set of `ι` elements, `f : ι → G`, and `K : ι → subgroup G` satisfy commutativity of pairwise products `a * b = b * a` for all `a, b ∈ s`, subgroup independence `∏ i in ι K i ⊨ ∏ j in ι K j`, and `∏ i in s f i ∈ ∏ j in s K j`, then `∏ i in s f i = 1` implies `f i = 1` for all `i ∈ s`.
|
AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_independent
theorem AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_independent :
∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} (s : Finset ι) (f : ι → G)
(comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)) (K : ι → AddSubgroup G),
CompleteLattice.Independent K → (∀ x ∈ s, f x ∈ K x) → s.noncommSum f comm = 0 → ∀ i ∈ s, f i = 0
The theorem `AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_independent` states that for any type `G` with an additive group structure, any type `ι`, any finite set `s` of elements of type `ι`, any function `f` from `ι` to `G`, and any function `K` from `ι` to additive subgroups of `G`, if the elements of the image of `s` under `f` pairwise commute, the subgroups given by `K` are independent, every element of the image of `s` under `f` belongs to the subgroup given by `K` at that element, and the non-commutative sum of the image of `s` under `f` equals zero, then every element of the image of `s` under `f` equals zero. In simpler terms, if we have a bunch of elements in different independent subgroups that add up to zero and they pairwise commute, then each of those elements must be zero.
More concisely: If `G` is an additive group, `s` is a finite set of pairwise commuting elements of `ι`, `f : ι → G`, and `K : ι → additive subgroups of G` satisfy `∑ (s : ι) in s, f s ∈ K s` and `∑ (i j in s × s) (i ≠ j) [f i - f j] = 0`, then `∑ (s : ι) in s, f s = 0`.
|
MonoidHom.noncommPiCoprod_mulSingle
theorem MonoidHom.noncommPiCoprod_mulSingle :
∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {N : ι → Type u_3}
[inst_3 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
{hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)} (i : ι) (y : N i),
(MonoidHom.noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = (ϕ i) y
The theorem `MonoidHom.noncommPiCoprod_mulSingle` states that for any monoid `M`, index type `ι` with decidable equality and being finite, a family of monoids `N` indexed by `ι`, a family of monoid homomorphisms `ϕ` from `N` to `M`, and a pairwise commuting condition `hcomm` on the homomorphisms, if we have an index `i` and an element `y` from `N i`, then the canonical homomorphism (given by `MonoidHom.noncommPiCoprod`) applied to the function supported at `i`, with value `y` there and `1` elsewhere (given by `Pi.mulSingle`), is equal to the homomorphism `ϕ i` applied to `y`. That is to say, within a commutative context, the overall effect of the canonical homomorphism on the specific function `Pi.mulSingle i y` is the same as simply applying the specific homomorphism `ϕ i` to `y`.
More concisely: For any finite index type `ι`, monoid `M`, family of monoids `N` indexed by `ι`, family of monoid homomorphisms `ϕ` from `N` to `M` satisfying pairwise commutativity condition `hcomm`, and `i` in `ι` and `y` in `N i`, the canonical homomorphism from the noncommutative product of `N` applying `Pi.mulSingle i y` is equal to `ϕ i (y)`.
|