TrivSqZeroExt.inl_zero
theorem TrivSqZeroExt.inl_zero :
∀ {R : Type u} (M : Type v) [inst : Zero R] [inst_1 : Zero M], TrivSqZeroExt.inl 0 = 0
The theorem `TrivSqZeroExt.inl_zero` states that for any two types `R` and `M` where `R` and `M` both have a zero element (i.e., are instances of the `Zero` typeclass), the canonical inclusion mapping of `0` from `R` to `TrivSqZeroExt R M` (performed using the `TrivSqZeroExt.inl` function) results in `0`. In simple terms, when `0` from the type `R` is mapped to the trivial square zero extension of `R` and `M`, it remains `0`.
More concisely: For any types `R` and `M` with zero elements, the `TrivSqZeroExt.inl` function applied to the zero element of `R` results in the zero element of `TrivSqZeroExt R M`.
|
TrivSqZeroExt.inl_add
theorem TrivSqZeroExt.inl_add :
∀ {R : Type u} (M : Type v) [inst : Add R] [inst_1 : AddZeroClass M] (r₁ r₂ : R),
TrivSqZeroExt.inl (r₁ + r₂) = TrivSqZeroExt.inl r₁ + TrivSqZeroExt.inl r₂
This theorem, `TrivSqZeroExt.inl_add`, states that for any two elements `r₁` and `r₂` of type `R` (where `R` is any type with an addition operation) and `M` is any type with zero and an addition operation, the function `TrivSqZeroExt.inl` (which maps an element of `R` to a pair in `TrivSqZeroExt R M` consisting of that element and zero) preserves the addition operation. In other words, applying this function to the sum of `r₁` and `r₂` yields the same result as summing the results of applying this function to `r₁` and `r₂` separately.
More concisely: For any types `R` with addition and `M` with zero and addition, the function `TrivSqZeroExt.inl : R -> TrivSqZeroExt R M` preserves addition, that is, `TrivSqZeroExt.inl (r₁ + r₂) = TrivSqZeroExt.inl r₁ + TrivSqZeroExt.inl r₂`.
|
TrivSqZeroExt.fst_inl
theorem TrivSqZeroExt.fst_inl : ∀ {R : Type u} (M : Type v) [inst : Zero M] (r : R), (TrivSqZeroExt.inl r).fst = r := by
sorry
The theorem `TrivSqZeroExt.fst_inl` states that for all types `R` and `M`, where `M` is an instance of the `Zero` type class, and for all elements `r` of type `R`, the first component (obtained by the `TrivSqZeroExt.fst` function) of the trivial square zero extension of `R` by `M` (obtained by the `TrivSqZeroExt.inl` function) applied to `r` is equal to `r`. In simpler terms, when you add zero from `M` to any element `r` from `R`, the result's first component is still `r`.
More concisely: For all types R with an instance of Zero M, and all elements r in R, the first component of the trivial square zero extension of R by M applied to r is equal to r. In mathematical notation: `fst (TrivSqZeroExt.inl r) = r`.
|
TrivSqZeroExt.linearMap_ext
theorem TrivSqZeroExt.linearMap_ext :
∀ {S : Type u_2} {R : Type u} {M : Type v} {N : Type u_3} [inst : Semiring S] [inst_1 : AddCommMonoid R]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module S R] [inst_5 : Module S M]
[inst_6 : Module S N] ⦃f g : TrivSqZeroExt R M →ₗ[S] N⦄,
(∀ (r : R), f (TrivSqZeroExt.inl r) = g (TrivSqZeroExt.inl r)) →
(∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) → f = g
This theorem states that for a given semiring `S`, commutative additive monoids `R`, `M`, `N` and modules `R`, `M`, `N` over `S`, two linear maps `f` and `g` from the trivial square-zero extension of `M` over `R` to `N` are equal if they map an element `r` from `R` and an element `m` from `M` to the same elements under the canonical inclusion maps into the trivial square-zero extension of `M` over `R`. That is, if `f` and `g` agree on the image of every `r` in `R` and every `m` in `M` under the canonical inclusion maps, then `f` and `g` are equal.
More concisely: If two linear maps from the trivial square-zero extension of an abelian group `M` over a commutative semiring `R` to another abelian group `N` agree on the images of every element `r` in `R` and every element `m` in `M` under the canonical inclusion maps, then `f` and `g` are equal.
|
TrivSqZeroExt.ext
theorem TrivSqZeroExt.ext :
∀ {R : Type u} {M : Type v} {x y : TrivSqZeroExt R M}, x.fst = y.fst → x.snd = y.snd → x = y
The theorem `TrivSqZeroExt.ext` states that for any two objects `x` and `y` of the type `TrivSqZeroExt R M` (where `R` is a type and `M` is a module over the ring `R`), if the first component (obtained by `TrivSqZeroExt.fst`) of `x` is equal to the first component of `y`, and the second component (obtained by `TrivSqZeroExt.snd`) of `x` is equal to the second component of `y`, then `x` and `y` are indeed equal. This theorem essentially enforces that objects in the Trivial Square-Zero Extension are uniquely defined by their two components.
More concisely: If two objects in the Trivial Square-Zero Extension of a ring `R` over a module `M` have equal first and second components, then they are equal.
|
TrivSqZeroExt.snd_list_prod
theorem TrivSqZeroExt.snd_list_prod :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Module Rᵐᵒᵖ M] [inst_4 : SMulCommClass R Rᵐᵒᵖ M] (l : List (TrivSqZeroExt R M)),
l.prod.snd =
(List.map
(fun x =>
MulOpposite.op (List.drop x.1.succ (List.map TrivSqZeroExt.fst l)).prod •
(List.take x.1 (List.map TrivSqZeroExt.fst l)).prod • x.2.snd)
l.enum).sum
This theorem pertains to the Trivial Square-Zero Extension over a ring `R` and a module `M`. Given a list `l` of such extensions, the second element of the product of the list is equal to the sum of specific terms. Each term in the sum involves an operation on the elements of the list `l`, which is enumerated (`l.enum`). For each enumerated element `x`, the operation involves dropping the first `x.1.succ` elements from the list of the first elements of `l` (`List.drop x.1.succ (List.map TrivSqZeroExt.fst l)`), taking the product of the remaining list, and multiplying it by the product of the first `x.1` elements of the first elements of `l` (`List.take x.1 (List.map TrivSqZeroExt.fst l)`). Finally, the resulting product is multiplied by the second element of `x` (`x.2.snd`). The theorem states that the sum of all such terms is equal to the second element of the product of the list `l`.
More concisely: Given a list of Trivial Square-Zero Extensions over a ring and a module, the second element of their product equals the sum of products of the sub-list obtained by dropping the first `succ(i)` elements of each extension, multiplied by the product of the first `i` first elements of the extension's first component, and the second component of the `i`-th extension.
|
TrivSqZeroExt.inl_mul
theorem TrivSqZeroExt.inl_mul :
∀ {R : Type u} (M : Type v) [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
[inst_3 : DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R),
TrivSqZeroExt.inl (r₁ * r₂) = TrivSqZeroExt.inl r₁ * TrivSqZeroExt.inl r₂
This theorem, named `TrivSqZeroExt.inl_mul`, states that for any types `R` and `M`, where `R` is a monoid, `M` is an add monoid, and `R` (and its opposite) acts distributively on `M`, the multiplication in `R` respects the canonical inclusion into its trivial square-zero extension. In other words, if you have two elements `r₁` and `r₂` from `R`, then the result of mapping the product `r₁ * r₂` into the trivial square-zero extension of `R` and `M` using the canonical inclusion `TrivSqZeroExt.inl` is the same as the product of the images of `r₁` and `r₂` under the same inclusion. This theorem connects the multiplication in the original type `R` with the operation in the extension, showing that the canonical inclusion respects the multiplication operation.
More concisely: For any monoid `R` and add monoid `M` with `R` (and its opposite) distributively acting on `M`, the multiplication in `R` commutes with the canonical inclusion into its trivial square-zero extension in `M`.
|
TrivSqZeroExt.inr_mul_inr
theorem TrivSqZeroExt.inr_mul_inr :
∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Module Rᵐᵒᵖ M] (m₁ m₂ : M), TrivSqZeroExt.inr m₁ * TrivSqZeroExt.inr m₂ = 0
This theorem states that for any semiring `R`, and a commutative additive monoid `M` that is also both a left `R`-module and a right `R`-opposite module, the product of `TrivSqZeroExt.inr m₁` and `TrivSqZeroExt.inr m₂` is always zero. Here, `TrivSqZeroExt.inr` is a function that maps a member of `M` to a member of the trivials square-zero extension of `R` and `M`, and `m₁` and `m₂` are any two members of `M`. The trivial square-zero extension of `R` and `M` is a way of creating a ring from a semiring `R` and an `R`-module `M`. The product being always zero suggests that the square-zero extension is a "trivial" extension.
More concisely: For any commutative additive monoid `M` that is both a left and right `R-`module of a semiring `R`, the product of the images of any two elements of `M` under the function `TrivSqZeroExt.inr` in the trivial square-zero extension of `R` and `M` is always zero.
|
TrivSqZeroExt.lift_inlAlgHom_inrHom
theorem TrivSqZeroExt.lift_inlAlgHom_inrHom :
∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
[inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
[inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M],
TrivSqZeroExt.lift (TrivSqZeroExt.inlAlgHom S R M) (↑S (TrivSqZeroExt.inrHom R M)) ⋯ ⋯ ⋯ =
AlgHom.id S (TrivSqZeroExt R M)
The theorem `TrivSqZeroExt.lift_inlAlgHom_inrHom` states that for any commutative semiring `S`, semiring `R`, and an `R`-module `M`, under certain conditions (specifically, `M` is also an `S`-module, `M` is a module over the opposite ring of `R`, and `S` and `R` are scalar towers over `M`), the lift operation applied to the canonical `R`-linear inclusion `M → TrivSqZeroExt R M` (denoted `inrHom`) and the ring homomorphism `R → TrivSqZeroExt R M` (denoted `inlAlgHom`) is the identity on the trivial square-zero extension of `M` over `R`. In other words, it's saying that lifting these specific maps is the same as doing nothing in the algebra of the trivial square-zero extension.
More concisely: For any commutative semirings S and R, and an R-module M that is also an S-module, module over the opposite ring of R, and scalar tower over S and R, the lift of the canonical inclusion map and ring homomorphism from M to its trivial square-zero extension over R are equal.
|
TrivSqZeroExt.ind
theorem TrivSqZeroExt.ind :
∀ {R : Type u_3} {M : Type u_4} [inst : AddZeroClass R] [inst_1 : AddZeroClass M] {P : TrivSqZeroExt R M → Prop},
(∀ (r : R) (m : M), P (TrivSqZeroExt.inl r + TrivSqZeroExt.inr m)) → ∀ (x : TrivSqZeroExt R M), P x
The theorem `TrivSqZeroExt.ind` states that, for any types `R` and `M` with addition and zero structures, and for any property `P` on the elements of the trivial square-zero extension of `M` over `R`, if this property `P` holds for all elements of the form `TrivSqZeroExt.inl r + TrivSqZeroExt.inr m` (where `r` is an element from `R` and `m` is an element from `M`), then the property `P` holds for all elements `x` in the trivial square-zero extension of `M` over `R`. In simpler terms, the property `P` holds for all elements in the extension if it holds for all possible combinations of elements from `R` and `M`.
More concisely: If a property holds for all elements of the form `r + m` in the trivial square-zero extension of `M` over `R`, where `r` is from `R` and `m` is from `M`, then the property holds for all elements in the extension.
|
TrivSqZeroExt.fst_one
theorem TrivSqZeroExt.fst_one : ∀ {R : Type u} {M : Type v} [inst : One R] [inst_1 : Zero M], TrivSqZeroExt.fst 1 = 1
The theorem `TrivSqZeroExt.fst_one` states that for any types `R` and `M`, given that `R` has a multiplicative identity (denoted by `One R`) and `M` has an additive identity (denoted by `Zero M`), the first component (obtained via the function `TrivSqZeroExt.fst`) of the multiplicative identity in the trivial square zero extension of `R` and `M` is equal to the multiplicative identity in `R`. In other words, denoting the trivial square zero extension of `R` and `M` by `1`, we have `TrivSqZeroExt.fst 1 = 1` in `R`.
More concisely: In the trivial square zero extension of rings `R` with identity `One R` and `M` with additive identity `Zero M`, the first component of the extension's identity equals the identity of `R`, i.e., `TrivSqZeroExt.fst 1 = One R`.
|