DirectSum.GSemiring.mul_one
theorem DirectSum.GSemiring.mul_one :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A] (a : GradedMonoid A), a * 1 = a
This theorem states that for any graded monoid `A`, which is a type dependent on an index type `ι` and equipped with an additional structure of 'G-Semiring', the multiplication by the multiplicative identity `one` on the right side doesn't change the value of any element `a` of the graded monoid. Here, the graded monoid is modelled as a sigma type, and the additional structures on the type `ι` and the type family `A` are an additive monoid structure and additive commutative monoid structures respectively. In mathematical terms, it's stating that in such a "graded semiring", multiplying any element by the multiplicative identity yields the original element, i.e., for all `a` in the semiring, `a * 1 = a`.
More concisely: In a graded semiring (modeled as a sig-type with additional structures of an additive monoid and additive commutative monoid), multiplication by the multiplicative identity (one) on the right side leaves every element unchanged.
|
DirectSum.of_natCast
theorem DirectSum.of_natCast :
∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
[inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (n : ℕ), (DirectSum.of A 0) ↑n = ↑n
The theorem `DirectSum.of_natCast` states that for any type `ι` with a decidable equality and a natural number `n`, the operation of casting `n` to the direct sum and then applying the direct sum function `DirectSum.of` at 0, results in the same value as just directly casting `n`. This is under the conditions that `A` is a function from `ι` to some type, where each element in the range of `A` forms an additive commutative monoid, `ι` forms an additive monoid, and `A` forms a grade-semiring.
More concisely: For any decidably equal type `ι` and natural number `n`, the operation of casting `n` to the direct sum of a grade-semiring `A` from `ι` and then applying `DirectSum.of` at 0 is equivalent to directly casting `n` to the direct sum of `A`.
|
DirectSum.GSemiring.natCast_zero
theorem DirectSum.GSemiring.natCast_zero :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A], DirectSum.GSemiring.natCast 0 = 0
The theorem `DirectSum.GSemiring.natCast_zero` states that for all types `ι` and a type function `A : ι → Type`, where `ι` is an additive monoid and for every `i` of type `ι`, `A i` is an additive commutative monoid, if `A` forms a graded semiring, then the canonical map from natural numbers to the zeroth component of the graded semiring sends `0` (zero) to `0` (zero). In simple words, the canonical mapping respects zero in such a graded semiring structure.
More concisely: If `A : ι → Type` is a graded semiring over the additive monoid `ι` such that `A i` is an additive commutative monoid for every `i` in `ι`, then the canonical map from natural numbers to the zeroth component of `A` sends `0` to `0`.
|
DirectSum.GNonUnitalNonAssocSemiring.add_mul
theorem DirectSum.GNonUnitalNonAssocSemiring.add_mul :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : Add ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a b : A i) (c : A j),
GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
The theorem `DirectSum.GNonUnitalNonAssocSemiring.add_mul` states that for any type `ι`, any type family `A` indexed by `ι`, any addition operation on `ι`, any commutative monoid operation on each `A i`, and any non-unital non-associative semiring structure on `A`, given any `i` and `j` in `ι` and any elements `a`, `b` of `A i` and `c` of `A j`, the homogeneous multiplication `mul` defined in the `GradedMonoid.GMul` class distributes over addition in the `A i` component. In other words, multiplying the sum of `a` and `b` with `c` results in the same result as multiplying `a` and `b` with `c` separately and then adding the results.
More concisely: For any non-unital non-associative semiring `A` indexed by a commutative monoid `(ι, +)`, the homogeneous multiplication distributes over addition, that is, `(a + b) * c = a * c + b * c` for all `a, b, c` in `A`.
|
DirectSum.GNonUnitalNonAssocSemiring.mul_zero
theorem DirectSum.GNonUnitalNonAssocSemiring.mul_zero :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : Add ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i), GradedMonoid.GMul.mul a 0 = 0
The theorem `DirectSum.GNonUnitalNonAssocSemiring.mul_zero` states that for any type `ι`, any function `A` from `ι` to some type, with `ι` having an addition operation, and for each `i` in `ι`, `A i` forms an abelian (commutative) monoid. Furthermore, if `A` has a structure of a non-unital, non-associative semiring, then for any `i`, `j` in `ι` and any element `a` of `A i`, the homogeneous multiplication of `a` with the zero element of `A j` (i.e., `GradedMonoid.GMul.mul a 0`) gives zero. In other words, multiplying any graded component with zero on the right results in zero.
More concisely: For any non-unital, non-associative semiring `A` indexed over an abelian monoid `ι`, the multiplication of any element `a` in `A i` with the zero element in `A j` results in zero for all `i, j` in `ι`.
|
DirectSum.GSemiring.one_mul
theorem DirectSum.GSemiring.one_mul :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A] (a : GradedMonoid A), 1 * a = a
This theorem states that for any graded monoid `A`, multiplication by `one` on the left gives the original element. More formally, let `ι` be a type and `A` be a function mapping each `ι` to a type. If `ι` forms an additive monoid and each `A i` forms an additive commutative monoid, then for any element `a` of the graded monoid `A`, the result of the operation `1 * a` is `a`. This adheres to the identity property of multiplication in a semiring.
More concisely: For any graded additive commutative monoid `A`, multiplication by the identity element `1` yields the identity element on each component of `A`.
|
DirectSum.GSemiring.mul_assoc
theorem DirectSum.GSemiring.mul_assoc :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A] (a b c : GradedMonoid A), a * b * c = a * (b * c)
This theorem states that multiplication is associative in a graded semiring. More specifically, for any type `ι`, any function `A` which assigns to each element of `ι` a type, and given that `ι` is an additive monoid and each `A i` is an additive commutative monoid, if we have a graded semiring structure on `A`, then for any three elements `a`, `b`, and `c` in the graded monoid `GradedMonoid A`, the product of `a`, `b`, and `c` remains the same regardless of how they are grouped. In other words, `(a * b) * c` is equal to `a * (b * c)`.
More concisely: In a graded semiring with each component an additive commutative monoid, the graded multiplication is associative: `(a * b) * c = a * (b * c)` for all elements `a`, `b`, and `c` in the graded monoid.
|
DirectSum.ringHom_ext
theorem DirectSum.ringHom_ext :
∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
[inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R]
⦃f g : (DirectSum ι fun i => A i) →+* R⦄,
(∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)) → f = g
This theorem states that for any type `ι` with decidable equality, a family of additive commutative monoids `A i` indexed by `ι`, a semiring `R`, and two ring homomorphisms `f` and `g` from the direct sum of the `A i` to `R`, if `f` and `g` agree on the values of all elements of the direct sum when mapped from their respective `A i` via the natural inclusion map, then `f` and `g` are equal. In other words, two ring homomorphisms from a direct sum to another ring are identical if they agree on the images of the generators of the direct sum.
More concisely: If `ι` is a type with decidable equality, `A i` is a family of additive commutative monoids indexed by `ι`, `R` is a ring, `f` and `g` are ring homomorphisms from the direct sum of the `A i` to `R`, and `f` and `g` agree on the images of all generators under the natural inclusion map, then `f` and `g` are equal.
|
DirectSum.ringHom_ext'
theorem DirectSum.ringHom_ext' :
∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
[inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R]
⦃F G : (DirectSum ι fun i => A i) →+* R⦄,
(∀ (i : ι), (↑F).comp (DirectSum.of A i) = (↑G).comp (DirectSum.of A i)) → F = G
This theorem states that for a given type `ι` with decidable equality, a family of additive commutative monoids `A i`, a semiring `R`, and two ring homomorphisms `F` and `G` from the direct sum of `A i` to `R`, if these two ring homomorphisms are equal when composed with the natural inclusion map `DirectSum.of A i` for each `i` in `ι`, then the two ring homomorphisms `F` and `G` are themselves equal. This is an extensionality lemma for ring homomorphisms, emphasizing that the behavior of a ring homomorphism is fully determined by its action on the individual elements of the direct sum.
More concisely: If two ring homomorphisms from a direct sum of additive commutative monoids to a semiring agree on each summand component, then they are equal.
|
DirectSum.of_zero_pow
theorem DirectSum.of_zero_pow :
∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
[inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (a : A 0) (n : ℕ),
(DirectSum.of A 0) (a ^ n) = (DirectSum.of A 0) a ^ n
The theorem `DirectSum.of_zero_pow` states that for any type `ι` with decidable equality, a function `A : ι → Type`, where each `A i` is an additive commutative monoid, an additive monoid structure on `ι`, a graded semiring structure on `A`, a value `a : A 0`, and a natural number `n`, the image of `a^n` under the natural inclusion map from `A 0` to the direct sum of `A` over `ι` is equal to the `n`-th power of the image of `a` under the same map. In simpler terms, it asserts that the direct sum operation respects the power operation for the zeroth element of the grading.
More concisely: For any additive commutative monoid `A` indexed by a decidably equal type `ι`, the power `a^n` of the zeroth element `a` in `A` maps to the `n`-th power of its image under the natural inclusion map in the direct sum of `A` over `ι`.
|
DirectSum.of_zero_smul
theorem DirectSum.of_zero_smul :
∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : AddZeroClass ι]
[inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} (a : A 0)
(b : A i), (DirectSum.of A i) (a • b) = (DirectSum.of A 0) a * (DirectSum.of A i) b
The theorem `DirectSum.of_zero_smul` states that for any type `ι` with decidable equality and any function `A` from `ι` to some Type `u_2` (with additional structures of additive zero class, an additive commutative monoid for each `i : ι` and a non-unital and non-associative semiring structure for the direct sum of `A i`), for any elements `a` of `A 0` and `b` of `A i`, the operation of mapping the scaled value `(a • b)` by the natural inclusion map `DirectSum.of A i` is equivalent to multiplying the inclusion-map-transformed `a` and `b` where `a` is transformed via `DirectSum.of A 0` and `b` is transformed via `DirectSum.of A i`. In essence, this theorem associates the scalar multiplication in the additively commutative monoids with the multiplication in the non-unital, non-associative semiring.
More concisely: For any additively commutative monoid `A` indexed by a decidably equalizable type `ι` with non-unital, non-associative semiring structure on its direct sum, the scalar multiplication of elements `a` and `b` in `A 0` and `A i`, respectively, is equal to the multiplication of their images under the inclusion maps in the semiring.
|
DirectSum.GNonUnitalNonAssocSemiring.mul_add
theorem DirectSum.GNonUnitalNonAssocSemiring.mul_add :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : Add ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b c : A j),
GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
The theorem `DirectSum.GNonUnitalNonAssocSemiring.mul_add` states that for any type `ι`, for any type family `A` indexed over `ι`, given an addition operation over `ι` and for each `i` of type `ι`, an additive commutative monoid structure on `A i`, and a structure of non-unital and non-associative semiring on `A`, then for any elements `i` and `j` of type `ι`, and any elements `a` of `A i`, `b` and `c` of `A j`, the result of the graded multiplication of `a` with the sum of `b` and `c` is equal to the sum of the result of the graded multiplication of `a` with `b` and the result of the graded multiplication of `a` with `c`. In simpler terms, this theorem is stating a form of distributivity property for the multiplication operation in the context of graded monoids.
More concisely: For any type `ι`, given a non-unital and non-associative semiring `A` indexed over `ι` with additive commutative monoid structures, the graded multiplication distributes over addition: `(a ⊕ b) * c = a * b ⊕ a * c` for all `i, j ∈ ι` and `a ∈ A i, b, c ∈ A j`.
|
DirectSum.GCommSemiring.mul_comm
theorem DirectSum.GCommSemiring.mul_comm :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddCommMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GCommSemiring A] (a b : GradedMonoid A), a * b = b * a
The theorem `DirectSum.GCommSemiring.mul_comm` states that multiplication is commutative for every graded monoid. More specifically, for any type `ι`, any function `A` from `ι` to another type, given that `ι` is an additive commutative monoid and for each element of `ι`, `A i` is an additive commutative monoid, and assuming that `A` forms a graded commutative semiring, if `a` and `b` are elements of the graded monoid constructed from `A`, then the product of `a` and `b` is the same as the product of `b` and `a`.
More concisely: If `A` is a graded commutative semiring whose underlying additive monoids are commutative, then for all elements `a` and `b` in `A`, `a * b` = `b * a`.
|
DirectSum.mul_eq_sum_support_ghas_mul
theorem DirectSum.mul_eq_sum_support_ghas_mul :
∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
[inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)]
(a a' : DirectSum ι fun i => A i),
a * a' =
(DFinsupp.support a ×ˢ DFinsupp.support a').sum fun ij =>
(DirectSum.of (fun i => A i) (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))
The theorem `DirectSum.mul_eq_sum_support_ghas_mul` states that for any type `ι` with decidable equality, any type family `A` over `ι` consisting of additive commutative monoids, and given that `ι` forms an additive monoid, any two elements `a` and `a'` of the direct sum over `A` (denoted `DirectSum ι fun i => A i`), their multiplication `a * a'` is equivalent to the sum, over the Cartesian product of the supports of `a` and `a'`, of the application of the function `GradedMonoid.GMul.mul` to `a ij.1` and `a' ij.2`, and then embedding it back into the direct sum using the function `DirectSum.of`. Here, 'support' of a direct sum refers to the set of indices at which the elements are non-zero.
More concisely: For any additive commutative monoid type family `A` over a decidably equalizable index type `ι` that forms an additive monoid, the multiplication of two elements in the direct sum of `A` is equal to the sum, over the Cartesian product of their supports, of the pointwise multiplications of their corresponding components and embedding the results back into the direct sum.
|
DirectSum.of_eq_of_gradedMonoid_eq
theorem DirectSum.of_eq_of_gradedMonoid_eq :
∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : (i : ι) → AddCommMonoid (A i)] {i j : ι}
{a : A i} {b : A j}, GradedMonoid.mk i a = GradedMonoid.mk j b → (DirectSum.of A i) a = (DirectSum.of A j) b
This theorem states that for any types `ι` and `A` where `ι` has a decidable equality and `A` is an index type for a collection of additive commutative monoids, if two elements `a` and `b` from types `A i` and `A j` respectively are such that their corresponding elements in the graded monoid, created via `GradedMonoid.mk`, are equal, then their images under the natural inclusion maps into the direct sum of the collection of monoids, created via `DirectSum.of`, are also equal.
In other words, if `GradedMonoid.mk i a = GradedMonoid.mk j b`, then `(DirectSum.of A i) a = (DirectSum.of A j) b`.
More concisely: If `ι` is a type with decidable equality and `A` is an indexed collection of additive commutative monoids, then for all `i, j` and elements `a in A i` and `b in A j` with equal images in the graded monoid of `A`, their images under the natural inclusion maps in the direct sum of `A` are also equal: `(DirectSum.of A i) a = (DirectSum.of A j) b`.
|
DirectSum.GRing.intCast_negSucc_ofNat
theorem DirectSum.GRing.intCast_negSucc_ofNat :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommGroup (A i)]
[self : DirectSum.GRing A] (n : ℕ),
DirectSum.GRing.intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)
This theorem states that for any natural number `n`, the canonical map from the set of integers `ℤ` to a graded ring, when applied on the negative successor of `n`, is equal to the negative of the canonical map from the set of natural numbers `ℕ` to the underlying graded semiring when applied on `n + 1`. In simpler terms, it is describing a relationship between the mappings of negative integers and natural numbers+1 into certain algebraic structures known as graded rings and semirings.
More concisely: For any natural number `n`, the canonical map from `ℤ` to a graded ring sending `-(n+1)` equals the negative of the canonical map from `ℕ` to the underlying graded semiring sending `n+1`.
|
DirectSum.of_mul_of
theorem DirectSum.of_mul_of :
∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : Add ι] [inst_2 : (i : ι) → AddCommMonoid (A i)]
[inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j),
(DirectSum.of A i) a * (DirectSum.of A j) b = (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul a b)
The theorem `DirectSum.of_mul_of` states that for any type `ι` with decidable equality, a type `A` which is a function from `ι` to another type, and for any `i` and `j` of type `ι`, and `a` and `b` of type `A i` and `A j` respectively, the product of the direct sum of `A i` and `A j` equals the direct sum of `A` at the sum of `i` and `j` with the graded monoid multiplication of `a` and `b`. This theorem is applicable under the condition that `A i` and `A j` are additive commutative monoids and `A` is a graded non-unital non-associative semiring. The result basically outlines the interaction between the direct sum operation and the multiplication operation in a graded algebraic structure.
More concisely: For any additive commutative monoids `A i` indexed by a decidably equal type `ι`, the graded product of `A i` in a graded non-unital non-associative semiring equals the direct sum of the graded multiplication of their elements.
|
DirectSum.of_zero_one
theorem DirectSum.of_zero_one :
∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : Zero ι] [inst_2 : GradedMonoid.GOne A]
[inst_3 : (i : ι) → AddCommMonoid (A i)], (DirectSum.of A 0) 1 = 1
The theorem `DirectSum.of_zero_one` states that for any type `ι`, given that `ι` has a decidable equality and a zero element, and for any type function `A` such that every `A i` forms an additive commutative monoid and `A` itself forms a Graded Monoid with a unit element, the image of the unit element under the natural inclusion map from `A 0` to the direct sum of `A i` across all `i` in `ι` is equal to the unit element in the direct sum. In other words, if you take the unit element from the additive commutative monoid `A 0` and include it in the direct sum of all `A i`, its identity remains unchanged.
More concisely: Given a type `ι` with decidable equality and a zero element, and a graded monoid `A` over `ι` with a unit element, the unit element in `A 0` maps to the unit element in the direct sum of `A i` for all `i` in `ι`.
|
DirectSum.GCommRing.mul_comm
theorem DirectSum.GCommRing.mul_comm :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddCommMonoid ι] [inst_1 : (i : ι) → AddCommGroup (A i)]
[self : DirectSum.GCommRing A] (a b : GradedMonoid A), a * b = b * a
The theorem `DirectSum.GCommRing.mul_comm` states that multiplication is commutative in a general graded commutative ring. Specifically, for any types `ι` and `A`, where `A` is a function from `ι` to a type and `ι` has an additive commutative monoid structure, and for each `i` in `ι`, `A i` forms an additive commutative group, if `A` forms a graded commutative ring (`DirectSum.GCommRing`), then for any two elements `a` and `b` in the graded monoid of `A` (`GradedMonoid A`), the multiplication of `a` and `b` equals the multiplication of `b` and `a`. In other words, `a * b = b * a`.
More concisely: In a graded commutative ring `A` over an additive commutative monoid `ι`, the multiplication is commutative: `a * b = b * a` for all `a, b` in the graded monoid of `A`.
|
DirectSum.GSemiring.gnpow_succ'
theorem DirectSum.GSemiring.gnpow_succ' :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A] (n : ℕ) (a : GradedMonoid A),
GradedMonoid.mk (n.succ • a.fst) (DirectSum.GSemiring.gnpow n.succ a.snd) =
⟨n • a.fst, DirectSum.GSemiring.gnpow n a.snd⟩ * a
The theorem `DirectSum.GSemiring.gnpow_succ'` states that, for any types `ι` and `A` such that `A` is an `ι`-indexed type, where `ι` has an `AddMonoid` structure and each type `A i` has an `AddCommMonoid` structure, and given a `DirectSum.GSemiring` structure on `A`, the successor power function on elements of the graded monoid `A` behaves as expected. More specifically, for any natural number `n` and an element `a` of the graded monoid `A`, the graded monoid element constructed from the successor power of `n` and `a`, is equal to the product of the graded monoid element constructed from the `n`-th power of `a` and `a` itself.
More concisely: For any type `A` indexed by an additive monoid `ι`, equipped with a DirectSum.GSemiring structure, the successor power of an element `a` in `A` equals the `n`-th power of `a` multiplied by `a`, where `n` is a natural number.
|
DirectSum.GSemiring.natCast_succ
theorem DirectSum.GSemiring.natCast_succ :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A] (n : ℕ),
DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
The theorem `DirectSum.GSemiring.natCast_succ` states that for any natural number `n`, the canonical map from the natural numbers to a graded semiring respects the successor function. In other words, the canonical mapping of the successor of `n` (i.e., `n + 1`) is equal to the canonical mapping of `n` plus the term `one` of grade 0. This applies to a graded semiring `A` indexed by a type `ι` that forms an additive monoid, where each grade `i` of the semiring has the structure of an additive commutative monoid.
More concisely: The canonical map from the natural numbers to a graded semiring preserves the successor operation, that is, the canonical image of `n + 1` equals the canonical image of `n` plus the grade 0 element.
|
DirectSum.GSemiring.gnpow_zero'
theorem DirectSum.GSemiring.gnpow_zero' :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GSemiring A] (a : GradedMonoid A),
GradedMonoid.mk (0 • a.fst) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
This theorem, named `DirectSum.GSemiring.gnpow_zero'`, states that for any graded monoid `a` in a direct sum graded semiring `A`, the zeroth power (i.e., the power `0`) of `a` is always equal to the multiplicative identity (`1`). Here, `A` is a type function that maps elements from the type `ι` to another type, and `ι` is equipped with the structure of an additive monoid. Each type `A i` for `i` in `ι` is equipped with the structure of an additive commutative monoid. The theorem holds for all types `ι` and type functions `A` that satisfy these conditions.
More concisely: For any graded monoid `a` in a direct sum graded semiring `A`, where `A` maps elements from an additive monoid `ι` to commutative additive monoids, the zeroth power of `a` equals the multiplicative identity `1`.
|
DirectSum.GRing.intCast_ofNat
theorem DirectSum.GRing.intCast_ofNat :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : (i : ι) → AddCommGroup (A i)]
[self : DirectSum.GRing A] (n : ℕ), DirectSum.GRing.intCast ↑n = DirectSum.GSemiring.natCast n
The theorem `DirectSum.GRing.intCast_ofNat` states that for any natural number `n`, the canonical mapping from integers (`ℤ`) to a graded ring, when applied to `n`, yields the same result as the canonical mapping from natural numbers (`ℕ`) to the underlying graded semiring. Here, `ι` is a type with an `AddMonoid` structure, and `A` is a graded semiring or ring; that is, a type indexed by `ι` whose elements have an additive commutative group or monoid structure. This theorem essentially claims the compatibility of these two canonical maps for natural numbers.
More concisely: The theorem asserts that the canonical map from integers to a graded semiring/ring, specialized to a natural number, is equal to the canonical map from natural numbers to the underlying graded semiring/ring.
|
DirectSum.GNonUnitalNonAssocSemiring.zero_mul
theorem DirectSum.GNonUnitalNonAssocSemiring.zero_mul :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : Add ι] [inst_1 : (i : ι) → AddCommMonoid (A i)]
[self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (b : A j), GradedMonoid.GMul.mul 0 b = 0
The theorem `DirectSum.GNonUnitalNonAssocSemiring.zero_mul` states that for any types `ι` and `A`, where `A` is a function from `ι` to some type, and `A` has an additive commutative monoid structure for each `ι`, under the structure of a non-unital, non-associative semiring, the multiplication of any graded component's zero with another element from the graded monoid vanishes. In other words, for any `ι` and `j` from type `ι`, and any element `b` from `A j`, the multiplication of `0` (the zero of the graded component `A i`) with `b` results in `0`. This is a common property in ring theory, which is the notion that anything multiplied by zero yields zero, extended to the setting of graded monoids.
More concisely: For any non-unital, non-associative semiring `A` modeled as a function from an index type `ι` to types, with additive commutative monoid structures on each `A i`, the product of any element in `A i` with the zero of `A i` is the zero of `A i`.
|
DirectSum.of_zero_mul
theorem DirectSum.of_zero_mul :
∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : AddZeroClass ι]
[inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] (a b : A 0),
(DirectSum.of A 0) (a * b) = (DirectSum.of A 0) a * (DirectSum.of A 0) b
This theorem states that for any type `ι` with decidable equality, a function `A` mapping from `ι` to another type, assuming `ι` is an additive zero class and `A i` is an additive commutative monoid for each `i` in `ι`, and `A` forms a generalized non-unital non-associative semiring, then for any two elements `a` and `b` of `A 0`, the value of `DirectSum.of A 0` applied to the product of `a` and `b` is the same as the product of `DirectSum.of A 0` applied to `a` and `DirectSum.of A 0` applied to `b`. In simpler terms, this theorem confirms the distributive property of multiplication over addition for `DirectSum.of A 0`.
More concisely: For any additive zero class ι with decidable equality, and a function A from ι to an additive commutative monoid such that A forms a generalized non-unital non-associative semiring, the distribution law holds for DirectSum.of A 0, that is, DirectSum.of A 0 (A i j) = A i (DirectSum.of A 0 j) * A i (DirectSum.of A 0 k) for all i, j, k in ι.
|