Monoid.Coprod.fst_prod_snd
theorem Monoid.Coprod.fst_prod_snd :
∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
Monoid.Coprod.fst.prod Monoid.Coprod.snd = Monoid.Coprod.toProd
This theorem states that for any two types `M` and `N` that form monoids, the product of the natural projections `Monoid.Coprod.fst` and `Monoid.Coprod.snd`, which are homomorphisms from the coproduct monoid `M * N` to `M` and `N` respectively, is equal to the natural projection `Monoid.Coprod.toProd`, which is a homomorphism from the coproduct monoid `M * N` to the product `M × N`. In other words, applying `Monoid.Coprod.fst` and `Monoid.Coprod.snd` to an element of `M * N` and combining them into a pair is the same as directly applying `Monoid.Coprod.toProd` to that element.
More concisely: The natural projections `Monoid.Coprod.fst` and `Monoid.Coprod.snd` of a monoidal coproduct are equal to the projection map `Monoid.Coprod.toProd`, i.e., `Monoid.Coprod.fst (x, y) = x`, `Monoid.Coprod.snd (x, y) = y`, and `Monoid.Coprod.toProd (x, y) = (x, y)` for all `x : M` and `y : N`, where `M` and `N` are monoids.
|
AddMonoid.Coprod.mk_eq_mk
theorem AddMonoid.Coprod.mk_eq_mk :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {w₁ w₂ : FreeAddMonoid (M ⊕ N)},
AddMonoid.Coprod.mk w₁ = AddMonoid.Coprod.mk w₂ ↔ (AddMonoid.coprodCon M N) w₁ w₂
The theorem `AddMonoid.Coprod.mk_eq_mk` states that for any two types `M` and `N` which are both instances of the `AddZeroClass`, and for any two variables `w₁` and `w₂` that are members of the free additive monoid over the sum of `M` and `N`, the equality of the additive monoid coproducts of `w₁` and `w₂` is equivalent to the relation defined by the congruence `AddMonoid.coprodCon M N` applied to `w₁` and `w₂`. In simpler terms, it describes a condition under which two elements of the coproduct of two additive monoids are equal.
More concisely: For any additive monoids M and N with instances of AddZeroClass, and any w₁ and w₂ in their free additive monoid over their sum, w₁ = w₂ holds if and only if AddMonoid.coprodCon M N (w₁, w₂) holds.
|
AddMonoid.Coprod.fst_sum_snd
theorem AddMonoid.Coprod.fst_sum_snd :
∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
AddMonoid.Coprod.fst.prod AddMonoid.Coprod.snd = AddMonoid.Coprod.toSum
This theorem states that for any two types `M` and `N` that have an `AddMonoid` structure (i.e., they are additive monoids), the add monoid homomorphism produced by combining the natural projection from the coproduct of `M` and `N` to `M` (`AddMonoid.Coprod.fst`) and to `N` (`AddMonoid.Coprod.snd`) using `AddMonoidHom.prod` is the same as the natural projection from the coproduct of `M` and `N` to the pair `(M, N)` (`AddMonoid.Coprod.toSum`). In other words, projecting to `M` and `N` separately and then pairing is the same as directly projecting to the pair `(M, N)`.
More concisely: The add monoid homomorphism from the coproduct of two additive monoids `M` and `N` obtained by projecting to each summand using `AddMonoid.Coprod.fst` and `AddMonoid.Coprod.snd`, and then pairing using `AddMonoidHom.prod`, is equal to the natural projection to the pair `(M, N)` using `AddMonoid.Coprod.toSum`.
|
AddMonoid.Coprod.mclosure_range_inl_union_inr
theorem AddMonoid.Coprod.mclosure_range_inl_union_inr :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
AddSubmonoid.closure (Set.range ⇑AddMonoid.Coprod.inl ∪ Set.range ⇑AddMonoid.Coprod.inr) = ⊤
This theorem states that for any two types `M` and `N` that have additive monoid structures, the additive submonoid generated by the union of the ranges of the natural embeddings of `M` and `N` into the coproduct of `M` and `N` is the whole coproduct. In other words, every element of the coproduct of `M` and `N` can be expressed as a sum of elements coming from `M` and `N` via their respective natural embeddings.
More concisely: For any additive monoids M and N, the submonoid of their coproduct generated by the images of their natural embeddings is the whole coproduct.
|
Monoid.Coprod.mk_eq_mk
theorem Monoid.Coprod.mk_eq_mk :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {w₁ w₂ : FreeMonoid (M ⊕ N)},
Monoid.Coprod.mk w₁ = Monoid.Coprod.mk w₂ ↔ (Monoid.coprodCon M N) w₁ w₂
This theorem, `Monoid.Coprod.mk_eq_mk`, states that for all types `M` and `N` that have a `MulOneClass` instance (i.e., they are monoids), and for all elements `w₁` and `w₂` of the free monoid over the coproduct of `M` and `N`, the application of the `Monoid.Coprod.mk` function to `w₁` and `w₂` results in the same output if and only if `w₁` and `w₂` are connected by the congruence relation `Monoid.coprodCon M N`. In simpler terms, it asserts that two elements of the free monoid are mapped to the same element in the coproduct monoid if and only if they are equivalent under the defining relation of the coproduct.
More concisely: For all monoids M and N, the elements w₁ and w₂ of the free monoid over M ⊕ N are mapped to the same element in the coproduct monoid M ⊕\_* N if and only if they are related by the congruence relation of Monoid.coprod on M and N.
|
AddMonoid.Coprod.swap_injective
theorem AddMonoid.Coprod.swap_injective :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
Function.Injective ⇑(AddMonoid.Coprod.swap M N)
The theorem `AddMonoid.Coprod.swap_injective` states that for any types `M` and `N` that are instances of the `AddZeroClass`, the function `AddMonoid.Coprod.swap M N`, which swaps the components in the coproduct of `M` and `N`, is injective. In mathematical terms, this means if we have two elements from the coproduct of `M` and `N` and applying the `AddMonoid.Coprod.swap` function to them gives the same result, then the two original elements from the coproduct were the same. This injectivity property is important in many areas of abstract algebra.
More concisely: If `M` and `N` are instances of `AddZeroClass`, then the function swapping components in the coproduct of `M` and `N` (`AddMonoid.Coprod.swap M N`) is an injection.
|
Monoid.Coprod.mclosure_range_inl_union_inr
theorem Monoid.Coprod.mclosure_range_inl_union_inr :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
Submonoid.closure (Set.range ⇑Monoid.Coprod.inl ∪ Set.range ⇑Monoid.Coprod.inr) = ⊤
This theorem states that for any types `M` and `N` that are instances of the `MulOneClass`, the submonoid generated by the union of the ranges of the natural embeddings `Monoid.Coprod.inl` and `Monoid.Coprod.inr` is the top monoid. In other words, every element of the coproduct monoid `M ∗ N` can be expressed as a product of elements coming from `M` (via the `inl` function) and `N` (via the `inr` function).
More concisely: For any types `M` and `N` that are instances of `MulOneClass`, the submonoid generated by the ranges of the natural embeddings `inl : M → M ∗ N` and `inr : N → M ∗ N` in the monoid `M ∗ N` is the entire monoid.
|
AddMonoid.Coprod.lift_comp_swap
theorem AddMonoid.Coprod.lift_comp_swap :
∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : AddMonoid P] (f : M →+ P) (g : N →+ P),
(AddMonoid.Coprod.lift f g).comp (AddMonoid.Coprod.swap N M) = AddMonoid.Coprod.lift g f
The theorem `AddMonoid.Coprod.lift_comp_swap` states that for any types `M`, `N`, and `P` that have the structure of an additive monoid with zero (`AddZeroClass`), and for any additive monoid morphisms `f` from `M` to `P` and `g` from `N` to `P`, the composition of the `lift` operation from the coproduct of `M` and `N` with the `swap` operation on the coproduct of `N` and `M` is equal to the `lift` operation from the coproduct of `g` and `f`. In mathematical terms, this theorem asserts the commutativity property of the `lift` and `swap` operations in the context of additive monoids and their morphisms.
More concisely: For any additive monoids `M`, `N`, and `P` with zero, and additive monoid morphisms `f: M → P` and `g: N → P`, the commutativity of `lift` and `swap` operations holds: `lift (coproduct f g) = lift (g ⊕ f)`.
|
Monoid.Coprod.swap_injective
theorem Monoid.Coprod.swap_injective :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
Function.Injective ⇑(Monoid.Coprod.swap M N)
The theorem `Monoid.Coprod.swap_injective` states that for any types `M` and `N` that are instances of the `MulOneClass` (meaning they are monoids with respect to multiplication operation that also have an identity element), the function `Monoid.Coprod.swap` that maps pairs `(M, N)` to `(N, M)` is injective. In other words, if `Monoid.Coprod.swap M N` of two pairs are equal, then those pairs must be the same. This function injectivity implies that no two different pairs in the domain map to the same pair in the codomain under the `swap` operation.
More concisely: For any monoids `M` and `N` with respect to multiplication, the function `Monoid.Coprod.swap : (M, N) -> (N, M)` is an injection.
|
Monoid.Coprod.lift_comp_swap
theorem Monoid.Coprod.lift_comp_swap :
∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
(f : M →* P) (g : N →* P), (Monoid.Coprod.lift f g).comp (Monoid.Coprod.swap N M) = Monoid.Coprod.lift g f
The theorem `Monoid.Coprod.lift_comp_swap` states that for any types `M`, `N`, and `P`, where `M` and `N` are instances of the class `MulOneClass` and `P` is an instance of `Monoid`, and given two monoid homomorphisms `f : M →* P` and `g : N →* P`, the composition of the function `Monoid.Coprod.lift f g` with the function `Monoid.Coprod.swap N M` is equal to `Monoid.Coprod.lift g f`. In other words, swapping the inputs of the operation `Monoid.Coprod.lift` and then applying the original operation is the same as directly applying the operation to the swapped inputs.
More concisely: For any types `M`, `N`, and `P` where `M` and `N` are monoids with one, and `P` is a monoid, the functions `Monoid.Coprod.lift f g` and `Monoid.Coprod.lift g f` are equal as maps from `M × N` to `P`, where `f : M →* P` and `g : N →* P` are homomorphisms.
|
AddMonoid.Coprod.swap_surjective
theorem AddMonoid.Coprod.swap_surjective :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
Function.Surjective ⇑(AddMonoid.Coprod.swap M N)
The theorem `AddMonoid.Coprod.swap_surjective` states that for all types `M` and `N` that have the structure of an additive monoid (i.e., they have zero and addition operations that satisfy certain properties), the function `AddMonoid.Coprod.swap M N` is surjective. This means that for every element in the coproduct additive monoid of `N` and `M`, there exists an element in the coproduct additive monoid of `M` and `N` such that applying the `AddMonoid.Coprod.swap M N` function to this element results in the original element. In other words, every element in the target monoid is an image of some element in the source monoid under the `AddMonoid.Coprod.swap M N` function.
More concisely: For every additive monoid `M` and `N`, the function `AddMonoid.Coprod.swap : M ⊎ N ↔ N ⊎ M` is a surjection.
|
Monoid.Coprod.swap_surjective
theorem Monoid.Coprod.swap_surjective :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
Function.Surjective ⇑(Monoid.Coprod.swap M N)
The theorem `Monoid.Coprod.swap_surjective` states that for any types `M` and `N` that have multiplication and unity (i.e., they are instances of the `MulOneClass`), the function `Monoid.Coprod.swap M N`, which swaps the elements of the pairs `(M,N)` to `(N,M)`, is surjective. In other words, for every pair `(n, m)` in `N x M`, there exists a pair `(m, n)` in `M x N` such that applying `Monoid.Coprod.swap M N` to `(m, n)` results in the pair `(n, m)`.
More concisely: For any types `M` and `N` with multiplication and unity, the function swapping elements of pairs in the product `M x N` is a surjection.
|
Monoid.Coprod.hom_ext
theorem Monoid.Coprod.hom_ext :
∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N]
[inst_2 : MulOneClass P] {f g : Monoid.Coprod M N →* P},
f.comp Monoid.Coprod.inl = g.comp Monoid.Coprod.inl →
f.comp Monoid.Coprod.inr = g.comp Monoid.Coprod.inr → f = g
This theorem is an extensionality lemma for monoid homomorphisms from the coproduct of two monoids `M` and `N` to a monoid `P`. It states that if two homomorphisms `f` and `g` from `M ∗ N` to `P` agree on the ranges of the natural embeddings `Monoid.Coprod.inl` and `Monoid.Coprod.inr`, then `f` and `g` are equal. In other words, two such monoid homomorphisms are determined entirely by their behavior on the original monoids `M` and `N`.
More concisely: Given monoids M, N, and P, and homomorphisms f and g from their coproduct M ∗ N to P, if f(inl x) = g(inl x) for all x in M and f(inr y) = g(inr y) for all y in N, then f = g.
|
AddMonoid.Coprod.hom_ext
theorem AddMonoid.Coprod.hom_ext :
∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : AddZeroClass P] {f g : AddMonoid.Coprod M N →+ P},
f.comp AddMonoid.Coprod.inl = g.comp AddMonoid.Coprod.inl →
f.comp AddMonoid.Coprod.inr = g.comp AddMonoid.Coprod.inr → f = g
This theorem, known as the Extensionality Lemma for Additive Monoid Homomorphisms from the Coproduct of M and N to P, states that given two additive monoid homomorphisms, f and g, from the coproduct of monoids M and N into a monoid P, if these homomorphisms agree on the ranges of the natural embeddings of M and N into the coproduct (termed as `AddMonoid.Coprod.inl` and `AddMonoid.Coprod.inr` respectively), then these homomorphisms are equal. In other words, the mapping properties of f and g through these natural embeddings uniquely determine these homomorphisms.
More concisely: Given additive monoid homomorphisms f and g from the coproduct of monoids M and N to monoid P, if f (AddMonoid.Coprod.inl x) = g (AddMonoid.Coprod.inl x) for all x in M and f (AddMonoid.Coprod.inr y) = g (AddMonoid.Coprod.inr y) for all y in N, then f = g.
|