Mathlib.Algebra.TrivSqZeroExt

TrivSqZeroExt definition

(R : Type u) (M : Type v)

Full source

/-- "Trivial Square-Zero Extension".

Given a module `M` over a ring `R`, the trivial square-zero extension of `M` over `R` is defined
to be the `R`-algebra `R × M` with multiplication given by
`(r₁ + m₁) * (r₂ + m₂) = r₁ r₂ + r₁ m₂ + r₂ m₁`.

It is a square-zero extension because `M^2 = 0`.
-/
def TrivSqZeroExt (R : Type u) (M : Type v) :=
  R × M

Trivial Square-Zero Extension

Informal description

The trivial square-zero extension of a module $M$ over a ring $R$ is the $R$-algebra structure on the direct product $R \times M$, with multiplication defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + r_2 m_1)$. This construction is called "square-zero" because the submodule $M$ squares to zero, i.e., the product of any two elements in $M$ is zero.

TrivSqZeroExt.inl definition

[Zero M] (r : R) : tsze R M

Full source

/-- The canonical inclusion `R → TrivSqZeroExt R M`. -/
def inl [Zero M] (r : R) : tsze R M :=
  (r, 0)

Canonical inclusion into trivial square-zero extension

Informal description

The canonical inclusion map from a ring $R$ into the trivial square-zero extension $R \oplus M$, sending an element $r \in R$ to $(r, 0) \in R \oplus M$.

TrivSqZeroExt.inr definition

[Zero R] (m : M) : tsze R M

Full source

/-- The canonical inclusion `M → TrivSqZeroExt R M`. -/
def inr [Zero R] (m : M) : tsze R M :=
  (0, m)

Inclusion of module into trivial square-zero extension

Informal description

The canonical inclusion map from the module $M$ into the trivial square-zero extension $\text{TrivSqZeroExt}\, R\, M$, defined by sending an element $m \in M$ to $(0, m) \in R \oplus M$.

TrivSqZeroExt.fst definition

(x : tsze R M) : R

Full source

/-- The canonical projection `TrivSqZeroExt R M → R`. -/
def fst (x : tsze R M) : R :=
  x.1

First projection of trivial square-zero extension

Informal description

The function projects an element of the trivial square-zero extension $R \oplus M$ to its first component in $R$.

TrivSqZeroExt.snd definition

(x : tsze R M) : M

Full source

/-- The canonical projection `TrivSqZeroExt R M → M`. -/
def snd (x : tsze R M) : M :=
  x.2

Projection to the module component of a trivial square-zero extension

Informal description

The function maps an element $x$ of the trivial square-zero extension $R \oplus M$ to its second component in $M$.

TrivSqZeroExt.fst_mk theorem

(r : R) (m : M) : fst (r, m) = r

Full source

@[simp]
theorem fst_mk (r : R) (m : M) : fst (r, m) = r :=
  rfl

First Projection of Trivial Square-Zero Extension Element

Informal description

For any element $r \in R$ and $m \in M$, the first projection of the trivial square-zero extension $(r, m)$ is equal to $r$, i.e., $\text{fst}(r, m) = r$.

TrivSqZeroExt.snd_mk theorem

(r : R) (m : M) : snd (r, m) = m

Full source

@[simp]
theorem snd_mk (r : R) (m : M) : snd (r, m) = m :=
  rfl

Second Projection of Trivial Square-Zero Extension Element

Informal description

For any element $r \in R$ and $m \in M$, the second projection of the trivial square-zero extension $(r, m)$ is equal to $m$, i.e., $\text{snd}(r, m) = m$.

TrivSqZeroExt.ext theorem

{x y : tsze R M} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y

Full source

@[ext]
theorem ext {x y : tsze R M} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y :=
  Prod.ext h1 h2

Extensionality of Trivial Square-Zero Extension Elements

Informal description

For any two elements $x$ and $y$ in the trivial square-zero extension $R \oplus M$, if their first projections to $R$ are equal ($x_1 = y_1$) and their second projections to $M$ are equal ($x_2 = y_2$), then $x = y$.

TrivSqZeroExt.fst_inl theorem

[Zero M] (r : R) : (inl r : tsze R M).fst = r

Full source

@[simp]
theorem fst_inl [Zero M] (r : R) : (inl r : tsze R M).fst = r :=
  rfl

First Projection of Inclusion in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ with zero element, the first projection of the canonical inclusion $\mathrm{inl}(r) \in R \oplus M$ equals $r$, i.e., $\mathrm{fst}(\mathrm{inl}(r)) = r$ for all $r \in R$.

TrivSqZeroExt.snd_inl theorem

[Zero M] (r : R) : (inl r : tsze R M).snd = 0

Full source

@[simp]
theorem snd_inl [Zero M] (r : R) : (inl r : tsze R M).snd = 0 :=
  rfl

Second Component of Inclusion in Trivial Square-Zero Extension is Zero

Informal description

For any ring $R$ and $R$-module $M$ with zero element, the second component of the canonical inclusion $\mathrm{inl}(r) \in R \oplus M$ is zero, i.e., $\mathrm{snd}(\mathrm{inl}(r)) = 0$ for all $r \in R$.

TrivSqZeroExt.fst_comp_inl theorem

[Zero M] : fst ∘ (inl : R → tsze R M) = id

Full source

@[simp]
theorem fst_comp_inl [Zero M] : fstfst ∘ (inl : R → tsze R M) = id :=
  rfl

First projection composed with inclusion is identity

Informal description

For any ring $R$ and $R$-module $M$ with zero element, the composition of the first projection $\mathrm{fst} : R \oplus M \to R$ with the canonical inclusion $\mathrm{inl} : R \to R \oplus M$ is equal to the identity map on $R$.

TrivSqZeroExt.snd_comp_inl theorem

[Zero M] : snd ∘ (inl : R → tsze R M) = 0

Full source

@[simp]
theorem snd_comp_inl [Zero M] : sndsnd ∘ (inl : R → tsze R M) = 0 :=
  rfl

Second projection composed with inclusion is zero map

Informal description

For any ring $R$ and $R$-module $M$ with zero element, the composition of the second projection $\mathrm{snd} : R \oplus M \to M$ with the canonical inclusion $\mathrm{inl} : R \to R \oplus M$ is equal to the zero map, i.e., $\mathrm{snd} \circ \mathrm{inl} = 0$.

TrivSqZeroExt.fst_inr theorem

[Zero R] (m : M) : (inr m : tsze R M).fst = 0

Full source

@[simp]
theorem fst_inr [Zero R] (m : M) : (inr m : tsze R M).fst = 0 :=
  rfl

First Projection of Module Inclusion in Trivial Square-Zero Extension is Zero

Informal description

For any ring $R$ with zero element and any $R$-module $M$, the first projection of the inclusion of an element $m \in M$ into the trivial square-zero extension $R \oplus M$ equals $0$, i.e., $\mathrm{fst}(\mathrm{inr}(m)) = 0$.

TrivSqZeroExt.snd_inr theorem

[Zero R] (m : M) : (inr m : tsze R M).snd = m

Full source

@[simp]
theorem snd_inr [Zero R] (m : M) : (inr m : tsze R M).snd = m :=
  rfl

Second Projection of Module Inclusion in Trivial Square-Zero Extension

Informal description

For any ring $R$ with zero element and any $R$-module $M$, the second projection of the inclusion of an element $m \in M$ into the trivial square-zero extension $R \oplus M$ equals $m$, i.e., $\mathrm{snd}(\mathrm{inr}(m)) = m$.

TrivSqZeroExt.fst_comp_inr theorem

[Zero R] : fst ∘ (inr : M → tsze R M) = 0

Full source

@[simp]
theorem fst_comp_inr [Zero R] : fstfst ∘ (inr : M → tsze R M) = 0 :=
  rfl

First Projection of Module Inclusion is Zero Map

Informal description

For any ring $R$ with zero element and any $R$-module $M$, the composition of the first projection $\mathrm{fst} \colon R \oplus M \to R$ with the inclusion map $\mathrm{inr} \colon M \to R \oplus M$ is the zero map, i.e., $\mathrm{fst} \circ \mathrm{inr} = 0$.

TrivSqZeroExt.snd_comp_inr theorem

[Zero R] : snd ∘ (inr : M → tsze R M) = id

Full source

@[simp]
theorem snd_comp_inr [Zero R] : sndsnd ∘ (inr : M → tsze R M) = id :=
  rfl

Projection-Inclusion Composition Yields Identity on Module

Informal description

For any module $M$ over a ring $R$ with zero element, the composition of the projection map $\text{snd} : R \oplus M \to M$ with the inclusion map $\text{inr} : M \to R \oplus M$ is equal to the identity map on $M$. That is, $\text{snd} \circ \text{inr} = \text{id}_M$.

TrivSqZeroExt.fst_surjective theorem

[Nonempty M] : Function.Surjective (fst : tsze R M → R)

Full source

theorem fst_surjective [Nonempty M] : Function.Surjective (fst : tsze R M → R) :=
  Prod.fst_surjective

Surjectivity of the First Projection in Trivial Square-Zero Extension

Informal description

If the module $M$ is nonempty, then the first projection map $\mathrm{fst} \colon R \oplus M \to R$ is surjective.

TrivSqZeroExt.snd_surjective theorem

[Nonempty R] : Function.Surjective (snd : tsze R M → M)

Full source

theorem snd_surjective [Nonempty R] : Function.Surjective (snd : tsze R M → M) :=
  Prod.snd_surjective

Surjectivity of Module Projection in Trivial Square-Zero Extension

Informal description

If the ring $R$ is nonempty, then the projection map $\mathrm{snd} \colon R \oplus M \to M$ from the trivial square-zero extension to the module $M$ is surjective.

TrivSqZeroExt.inl_injective theorem

[Zero M] : Function.Injective (inl : R → tsze R M)

Full source

theorem inl_injective [Zero M] : Function.Injective (inl : R → tsze R M) :=
  Function.LeftInverse.injective <| fst_inl _

Injectivity of Canonical Inclusion in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ with zero element, the canonical inclusion map $\mathrm{inl} \colon R \to R \oplus M$ defined by $r \mapsto (r, 0)$ is injective.

TrivSqZeroExt.inr_injective theorem

[Zero R] : Function.Injective (inr : M → tsze R M)

Full source

theorem inr_injective [Zero R] : Function.Injective (inr : M → tsze R M) :=
  Function.LeftInverse.injective <| snd_inr _

Injectivity of Module Inclusion in Trivial Square-Zero Extension

Informal description

For any ring $R$ with a zero element, the canonical inclusion map $\mathrm{inr} \colon M \to R \oplus M$ from an $R$-module $M$ into the trivial square-zero extension is injective. That is, if $\mathrm{inr}(m_1) = \mathrm{inr}(m_2)$ for $m_1, m_2 \in M$, then $m_1 = m_2$.

TrivSqZeroExt.inhabited instance

[Inhabited R] [Inhabited M] : Inhabited (tsze R M)

Full source

instance inhabited [Inhabited R] [Inhabited M] : Inhabited (tsze R M) :=
  instInhabitedProd

Inhabitedness of Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ that are both inhabited (i.e., have at least one element), the trivial square-zero extension $\text{TrivSqZeroExt}\, R\, M$ is also inhabited.

TrivSqZeroExt.zero instance

[Zero R] [Zero M] : Zero (tsze R M)

Full source

instance zero [Zero R] [Zero M] : Zero (tsze R M) :=
  Prod.instZero

Zero Element in Trivial Square-Zero Extension

Informal description

The trivial square-zero extension $R \oplus M$ has a zero element $(0, 0)$ when both $R$ and $M$ have zero elements.

TrivSqZeroExt.add instance

[Add R] [Add M] : Add (tsze R M)

Full source

instance add [Add R] [Add M] : Add (tsze R M) :=
  Prod.instAdd

Addition on Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with addition operations, the trivial square-zero extension $R \oplus M$ inherits an addition operation defined componentwise.

TrivSqZeroExt.sub instance

[Sub R] [Sub M] : Sub (tsze R M)

Full source

instance sub [Sub R] [Sub M] : Sub (tsze R M) :=
  Prod.instSub

Subtraction in Trivial Square-Zero Extension

Informal description

For a ring $R$ and an $R$-module $M$, the trivial square-zero extension $R \oplus M$ inherits a subtraction operation from the subtraction operations on $R$ and $M$, defined componentwise.

TrivSqZeroExt.neg instance

[Neg R] [Neg M] : Neg (tsze R M)

Full source

instance neg [Neg R] [Neg M] : Neg (tsze R M) :=
  Prod.instNeg

Negation on Trivial Square-Zero Extension

Informal description

For any ring $R$ and module $M$ over $R$ with negation operations on both $R$ and $M$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \times M$ inherits a negation operation defined componentwise.

TrivSqZeroExt.addSemigroup instance

[AddSemigroup R] [AddSemigroup M] : AddSemigroup (tsze R M)

Full source

instance addSemigroup [AddSemigroup R] [AddSemigroup M] : AddSemigroup (tsze R M) :=
  Prod.instAddSemigroup

Additive Semigroup Structure on Trivial Square-Zero Extension

Informal description

For any ring $R$ and module $M$ over $R$, the trivial square-zero extension $R \oplus M$ inherits an additive semigroup structure from the additive semigroup structures on $R$ and $M$.

TrivSqZeroExt.addZeroClass instance

[AddZeroClass R] [AddZeroClass M] : AddZeroClass (tsze R M)

Full source

instance addZeroClass [AddZeroClass R] [AddZeroClass M] : AddZeroClass (tsze R M) :=
  Prod.instAddZeroClass

Additive Zero Class Structure on Trivial Square-Zero Extensions

Informal description

For any ring $R$ and module $M$ over $R$ both equipped with an additive zero class structure, the trivial square-zero extension $R \oplus M$ inherits an additive zero class structure with componentwise addition and zero elements.

TrivSqZeroExt.addMonoid instance

[AddMonoid R] [AddMonoid M] : AddMonoid (tsze R M)

Full source

instance addMonoid [AddMonoid R] [AddMonoid M] : AddMonoid (tsze R M) :=
  Prod.instAddMonoid

Additive Monoid Structure on Trivial Square-Zero Extension

Informal description

For any ring $R$ and module $M$ over $R$, the trivial square-zero extension $R \oplus M$ inherits an additive monoid structure from the additive monoid structures on $R$ and $M$.

TrivSqZeroExt.addGroup instance

[AddGroup R] [AddGroup M] : AddGroup (tsze R M)

Full source

instance addGroup [AddGroup R] [AddGroup M] : AddGroup (tsze R M) :=
  Prod.instAddGroup

Additive Group Structure on Trivial Square-Zero Extensions

Informal description

For any additive groups $R$ and $M$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \times M$ is also an additive group, with the componentwise addition and negation operations.

TrivSqZeroExt.addCommSemigroup instance

[AddCommSemigroup R] [AddCommSemigroup M] : AddCommSemigroup (tsze R M)

Full source

instance addCommSemigroup [AddCommSemigroup R] [AddCommSemigroup M] : AddCommSemigroup (tsze R M) :=
  Prod.instAddCommSemigroup

Additive Commutative Semigroup Structure on Trivial Square-Zero Extension

Informal description

For any additive commutative semigroups $R$ and $M$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M)$ is also an additive commutative semigroup with componentwise addition.

TrivSqZeroExt.addCommMonoid instance

[AddCommMonoid R] [AddCommMonoid M] : AddCommMonoid (tsze R M)

Full source

instance addCommMonoid [AddCommMonoid R] [AddCommMonoid M] : AddCommMonoid (tsze R M) :=
  Prod.instAddCommMonoid

Additive Commutative Monoid Structure on Trivial Square-Zero Extension

Informal description

For any ring $R$ and module $M$ over $R$ where both $R$ and $M$ are additive commutative monoids, the trivial square-zero extension $\mathrm{TrivSqZeroExt}(R, M)$ is also an additive commutative monoid.

TrivSqZeroExt.addCommGroup instance

[AddCommGroup R] [AddCommGroup M] : AddCommGroup (tsze R M)

Full source

instance addCommGroup [AddCommGroup R] [AddCommGroup M] : AddCommGroup (tsze R M) :=
  Prod.instAddCommGroup

Additive Commutative Group Structure on Trivial Square-Zero Extension

Informal description

For any two additive commutative groups $R$ and $M$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \oplus M$ is also an additive commutative group, with the group operations defined componentwise.

TrivSqZeroExt.smul instance

[SMul S R] [SMul S M] : SMul S (tsze R M)

Full source

instance smul [SMul S R] [SMul S M] : SMul S (tsze R M) :=
  Prod.instSMul

Scalar Multiplication on Trivial Square-Zero Extensions

Informal description

For any scalar multiplication operations defined on a ring $R$ and an $(R, R)$-bimodule $M$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \oplus M$ inherits a scalar multiplication operation from $S$, defined componentwise.

TrivSqZeroExt.isScalarTower instance

 [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMul T S] [IsScalarTower T S R] [IsScalarTower T S M] :
  IsScalarTower T S (tsze R M)

Full source

instance isScalarTower [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMul T S]
    [IsScalarTower T S R] [IsScalarTower T S M] : IsScalarTower T S (tsze R M) :=
  Prod.isScalarTower

Scalar Tower Property for Trivial Square-Zero Extensions

Informal description

For any types $R$ and $M$ with scalar multiplication operations from $T$ and $S$, if $T$ acts on $R$ and $M$ through $S$ (i.e., $T$ is a scalar tower over $S$ for both $R$ and $M$), then the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \oplus M$ also forms a scalar tower with $T$ acting through $S$.

TrivSqZeroExt.smulCommClass instance

[SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMulCommClass T S R] [SMulCommClass T S M] : SMulCommClass T S (tsze R M)

Full source

instance smulCommClass [SMul T R] [SMul T M] [SMul S R] [SMul S M]
    [SMulCommClass T S R] [SMulCommClass T S M] : SMulCommClass T S (tsze R M) :=
  Prod.smulCommClass

Commuting Scalar Actions on Trivial Square-Zero Extensions

Informal description

For any types $R$ and $M$ with scalar multiplication operations from $T$ and $S$, if the actions of $T$ and $S$ commute on both $R$ and $M$, then the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \oplus M$ also has commuting scalar actions from $T$ and $S$.

TrivSqZeroExt.isCentralScalar instance

 [SMul S R] [SMul S M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsCentralScalar S R] [IsCentralScalar S M] :
  IsCentralScalar S (tsze R M)

Full source

instance isCentralScalar [SMul S R] [SMul S M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsCentralScalar S R]
    [IsCentralScalar S M] : IsCentralScalar S (tsze R M) :=
  Prod.isCentralScalar

Central Scalar Property for Trivial Square-Zero Extensions

Informal description

For any scalar multiplication operations defined on a ring $R$ and an $(R, R)$-bimodule $M$ where the actions of $S$ and its opposite $S^{\text{op}}$ coincide on both $R$ and $M$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M) = R \oplus M$ also has coinciding actions of $S$ and $S^{\text{op}}$.

TrivSqZeroExt.mulAction instance

[Monoid S] [MulAction S R] [MulAction S M] : MulAction S (tsze R M)

Full source

instance mulAction [Monoid S] [MulAction S R] [MulAction S M] : MulAction S (tsze R M) :=
  Prod.mulAction

Multiplicative Action on Trivial Square-Zero Extension

Informal description

For any monoid $S$ acting on a ring $R$ and a module $M$ over $R$, the trivial square-zero extension $\text{TrivSqZeroExt}(R, M)$ inherits a multiplicative action from $S$.

TrivSqZeroExt.distribMulAction instance

[Monoid S] [AddMonoid R] [AddMonoid M] [DistribMulAction S R] [DistribMulAction S M] : DistribMulAction S (tsze R M)

Full source

instance distribMulAction [Monoid S] [AddMonoid R] [AddMonoid M]
    [DistribMulAction S R] [DistribMulAction S M] : DistribMulAction S (tsze R M) :=
  Prod.distribMulAction

Distributive Multiplicative Action on Trivial Square-Zero Extension

Informal description

For any monoid $S$ and additive monoids $R$ and $M$ equipped with distributive multiplicative actions of $S$, the trivial square-zero extension $R \oplus M$ inherits a distributive multiplicative action from $S$ where the scalar multiplication is defined componentwise.

TrivSqZeroExt.module instance

[Semiring S] [AddCommMonoid R] [AddCommMonoid M] [Module S R] [Module S M] : Module S (tsze R M)

Full source

instance module [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [Module S R] [Module S M] :
    Module S (tsze R M) :=
  Prod.instModule

Module Structure on Trivial Square-Zero Extension

Informal description

For any semiring $S$ and additive commutative monoids $R$ and $M$ equipped with $S$-module structures, the trivial square-zero extension $\mathrm{TrivSqZeroExt}(R, M)$ inherits an $S$-module structure where the scalar multiplication is defined componentwise.

TrivSqZeroExt.instNontrivial_of_left instance

{R M : Type*} [Nontrivial R] [Nonempty M] : Nontrivial (TrivSqZeroExt R M)

Full source

/-- The trivial square-zero extension is nontrivial if it is over a nontrivial ring. -/
instance instNontrivial_of_left {R M : Type*} [Nontrivial R] [Nonempty M] :
    Nontrivial (TrivSqZeroExt R M) :=
  fst_surjective.nontrivial

Nontriviality of Trivial Square-Zero Extension from Nontrivial Base Ring

Informal description

For any nontrivial ring $R$ and nonempty module $M$ over $R$, the trivial square-zero extension $R \oplus M$ is also a nontrivial ring.

TrivSqZeroExt.instNontrivial_of_right instance

{R M : Type*} [Nonempty R] [Nontrivial M] : Nontrivial (TrivSqZeroExt R M)

Full source

/-- The trivial square-zero extension is nontrivial if it is over a nontrivial module. -/
instance instNontrivial_of_right {R M : Type*} [Nonempty R] [Nontrivial M] :
    Nontrivial (TrivSqZeroExt R M) :=
  snd_surjective.nontrivial

Nontriviality of Trivial Square-Zero Extension from Nontrivial Module

Informal description

For any ring $R$ and module $M$ over $R$, if $R$ is nonempty and $M$ is nontrivial, then the trivial square-zero extension $R \oplus M$ is also nontrivial.

TrivSqZeroExt.fst_zero theorem

[Zero R] [Zero M] : (0 : tsze R M).fst = 0

Full source

@[simp]
theorem fst_zero [Zero R] [Zero M] : (0 : tsze R M).fst = 0 :=
  rfl

First Projection of Zero in Trivial Square-Zero Extension

Informal description

For the trivial square-zero extension $R \oplus M$ where $R$ and $M$ have zero elements, the first projection of the zero element $(0,0)$ is equal to $0 \in R$, i.e., $\text{fst}(0) = 0$.

TrivSqZeroExt.snd_zero theorem

[Zero R] [Zero M] : (0 : tsze R M).snd = 0

Full source

@[simp]
theorem snd_zero [Zero R] [Zero M] : (0 : tsze R M).snd = 0 :=
  rfl

Second Projection of Zero in Trivial Square-Zero Extension

Informal description

For the trivial square-zero extension $R \oplus M$ where $R$ and $M$ have zero elements, the second projection of the zero element $(0,0)$ is equal to $0 \in M$, i.e., $\text{snd}(0) = 0$.

TrivSqZeroExt.fst_add theorem

[Add R] [Add M] (x₁ x₂ : tsze R M) : (x₁ + x₂).fst = x₁.fst + x₂.fst

Full source

@[simp]
theorem fst_add [Add R] [Add M] (x₁ x₂ : tsze R M) : (x₁ + x₂).fst = x₁.fst + x₂.fst :=
  rfl

Additivity of the Ring Component in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with addition operations, and for any two elements $x_1, x_2$ in the trivial square-zero extension $R \oplus M$, the first component of their sum equals the sum of their first components, i.e., $(x_1 + x_2)_1 = (x_1)_1 + (x_2)_1$.

TrivSqZeroExt.snd_add theorem

[Add R] [Add M] (x₁ x₂ : tsze R M) : (x₁ + x₂).snd = x₁.snd + x₂.snd

Full source

@[simp]
theorem snd_add [Add R] [Add M] (x₁ x₂ : tsze R M) : (x₁ + x₂).snd = x₁.snd + x₂.snd :=
  rfl

Additivity of the Module Component in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with addition operations, and for any two elements $x_1, x_2$ in the trivial square-zero extension $R \oplus M$, the second component of their sum equals the sum of their second components, i.e., $(x_1 + x_2)_2 = (x_1)_2 + (x_2)_2$.

TrivSqZeroExt.fst_neg theorem

[Neg R] [Neg M] (x : tsze R M) : (-x).fst = -x.fst

Full source

@[simp]
theorem fst_neg [Neg R] [Neg M] (x : tsze R M) : (-x).fst = -x.fst :=
  rfl

Negation Preserves First Component in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with negation operations, and for any element $x$ in the trivial square-zero extension $R \oplus M$, the first component of $-x$ is equal to the negation of the first component of $x$, i.e., $(-x)_1 = -x_1$.

TrivSqZeroExt.snd_neg theorem

[Neg R] [Neg M] (x : tsze R M) : (-x).snd = -x.snd

Full source

@[simp]
theorem snd_neg [Neg R] [Neg M] (x : tsze R M) : (-x).snd = -x.snd :=
  rfl

Negation Preserves Second Component in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with negation operations, and for any element $x$ in the trivial square-zero extension $R \oplus M$, the second component of $-x$ is equal to the negation of the second component of $x$, i.e., $(-x)_2 = -x_2$.

TrivSqZeroExt.fst_sub theorem

[Sub R] [Sub M] (x₁ x₂ : tsze R M) : (x₁ - x₂).fst = x₁.fst - x₂.fst

Full source

@[simp]
theorem fst_sub [Sub R] [Sub M] (x₁ x₂ : tsze R M) : (x₁ - x₂).fst = x₁.fst - x₂.fst :=
  rfl

First Projection Preserves Subtraction in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with subtraction operations, and for any elements $x₁, x₂$ in the trivial square-zero extension $R \oplus M$, the first component of their difference equals the difference of their first components, i.e., $(x₁ - x₂)_1 = x₁_1 - x₂_1$.

TrivSqZeroExt.snd_sub theorem

[Sub R] [Sub M] (x₁ x₂ : tsze R M) : (x₁ - x₂).snd = x₁.snd - x₂.snd

Full source

@[simp]
theorem snd_sub [Sub R] [Sub M] (x₁ x₂ : tsze R M) : (x₁ - x₂).snd = x₁.snd - x₂.snd :=
  rfl

Second Projection Preserves Subtraction in Trivial Square-Zero Extension

Informal description

For any ring $R$ and $R$-module $M$ equipped with subtraction operations, and for any elements $x₁, x₂$ in the trivial square-zero extension $R \oplus M$, the second component of their difference equals the difference of their second components, i.e., $(x₁ - x₂)_2 = x₁_2 - x₂_2$.

TrivSqZeroExt.fst_smul theorem

[SMul S R] [SMul S M] (s : S) (x : tsze R M) : (s • x).fst = s • x.fst

Full source

@[simp]
theorem fst_smul [SMul S R] [SMul S M] (s : S) (x : tsze R M) : (s • x).fst = s • x.fst :=
  rfl

First Projection Commutes with Scalar Multiplication in Trivial Square-Zero Extension

Informal description

For any scalar multiplication operations defined on a ring $R$ and an $(R, R)$-bimodule $M$, and for any scalar $s \in S$ and element $x \in R \oplus M$ of the trivial square-zero extension, the first projection of the scalar multiple $s \cdot x$ equals the scalar multiple of the first projection of $x$, i.e., $(s \cdot x)_1 = s \cdot x_1$.

TrivSqZeroExt.snd_smul theorem

[SMul S R] [SMul S M] (s : S) (x : tsze R M) : (s • x).snd = s • x.snd

Full source

@[simp]
theorem snd_smul [SMul S R] [SMul S M] (s : S) (x : tsze R M) : (s • x).snd = s • x.snd :=
  rfl

Second Projection Commutes with Scalar Multiplication in Trivial Square-Zero Extension

Informal description

For any scalar multiplication operations defined on a ring $R$ and an $(R, R)$-bimodule $M$, and for any scalar $s \in S$ and element $x \in R \oplus M$ of the trivial square-zero extension, the second projection of the scalar multiple $s \cdot x$ equals the scalar multiple of the second projection of $x$, i.e., $(s \cdot x)_2 = s \cdot x_2$.

TrivSqZeroExt.fst_sum theorem

 {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) : (∑ i ∈ s, f i).fst = ∑ i ∈ s, (f i).fst

Full source

theorem fst_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) :
    (∑ i ∈ s, f i).fst = ∑ i ∈ s, (f i).fst :=
  Prod.fst_sum

First Projection Preserves Finite Sums in Trivial Square-Zero Extension

Informal description

Let $R$ and $M$ be additive commutative monoids, and let $\mathrm{TrivSqZeroExt}(R, M)$ be their trivial square-zero extension. For any finite set $\iota$ and function $f : \iota \to \mathrm{TrivSqZeroExt}(R, M)$, the first projection of the sum $\sum_{i \in s} f(i)$ equals the sum of the first projections $\sum_{i \in s} (f(i)).\mathrm{fst}$.

TrivSqZeroExt.snd_sum theorem

 {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) : (∑ i ∈ s, f i).snd = ∑ i ∈ s, (f i).snd

Full source

theorem snd_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) :
    (∑ i ∈ s, f i).snd = ∑ i ∈ s, (f i).snd :=
  Prod.snd_sum

Second Projection Preserves Finite Sums in Trivial Square-Zero Extension

Informal description

Let $R$ and $M$ be additive commutative monoids, and let $\mathrm{TrivSqZeroExt}(R, M)$ be their trivial square-zero extension. For any finite set $I$ and function $f : I \to \mathrm{TrivSqZeroExt}(R, M)$, the second projection of the sum $\sum_{i \in s} f(i)$ equals the sum of the second projections $\sum_{i \in s} (f(i))_2$.

TrivSqZeroExt.inl_zero theorem

[Zero R] [Zero M] : (inl 0 : tsze R M) = 0

Full source

@[simp]
theorem inl_zero [Zero R] [Zero M] : (inl 0 : tsze R M) = 0 :=
  rfl

Inclusion of Zero in Trivial Square-Zero Extension Equals Zero

Informal description

Let $R$ be a ring with zero element $0_R$ and $M$ be an $(R, R)$-bimodule with zero element $0_M$. The canonical inclusion of $0_R$ into the trivial square-zero extension $R \oplus M$ equals the zero element of $R \oplus M$, i.e., $(0_R, 0_M) = 0_{R \oplus M}$.

TrivSqZeroExt.inl_add theorem

[Add R] [AddZeroClass M] (r₁ r₂ : R) : (inl (r₁ + r₂) : tsze R M) = inl r₁ + inl r₂

Full source

@[simp]
theorem inl_add [Add R] [AddZeroClass M] (r₁ r₂ : R) :
    (inl (r₁ + r₂) : tsze R M) = inl r₁ + inl r₂ :=
  ext rfl (add_zero 0).symm

Inclusion Preserves Addition in Trivial Square-Zero Extension

Informal description

For any ring $R$ with addition and any $R$-module $M$ with an additive zero class, the canonical inclusion map $\mathrm{inl} : R \to R \oplus M$ preserves addition. That is, for any $r_1, r_2 \in R$, we have $\mathrm{inl}(r_1 + r_2) = \mathrm{inl}(r_1) + \mathrm{inl}(r_2)$ in the trivial square-zero extension $R \oplus M$.

TrivSqZeroExt.inl_neg theorem

[Neg R] [NegZeroClass M] (r : R) : (inl (-r) : tsze R M) = -inl r

Full source

@[simp]
theorem inl_neg [Neg R] [NegZeroClass M] (r : R) : (inl (-r) : tsze R M) = -inl r :=
  ext rfl neg_zero.symm

Inclusion Preserves Negation in Trivial Square-Zero Extension

Informal description

For any ring $R$ with negation and any $(R, R)$-bimodule $M$ with a negation operation that preserves zero, the canonical inclusion of the additive inverse $-r$ of an element $r \in R$ into the trivial square-zero extension $R \oplus M$ equals the additive inverse of the inclusion of $r$. That is, $$( -r, 0 ) = - (r, 0).$$

TrivSqZeroExt.inl_sub theorem

[Sub R] [SubNegZeroMonoid M] (r₁ r₂ : R) : (inl (r₁ - r₂) : tsze R M) = inl r₁ - inl r₂

Full source

@[simp]
theorem inl_sub [Sub R] [SubNegZeroMonoid M] (r₁ r₂ : R) :
    (inl (r₁ - r₂) : tsze R M) = inl r₁ - inl r₂ :=
  ext rfl (sub_zero _).symm

Inclusion Preserves Subtraction in Trivial Square-Zero Extension

Informal description

For any elements $r_1, r_2$ in a ring $R$ and a module $M$ over $R$ with subtraction and negation operations, the canonical inclusion of the difference $r_1 - r_2$ into the trivial square-zero extension $R \oplus M$ equals the difference of the inclusions of $r_1$ and $r_2$, i.e., $$(r_1 - r_2, 0) = (r_1, 0) - (r_2, 0).$$

TrivSqZeroExt.inl_smul theorem

[Monoid S] [AddMonoid M] [SMul S R] [DistribMulAction S M] (s : S) (r : R) : (inl (s • r) : tsze R M) = s • inl r

Full source

@[simp]
theorem inl_smul [Monoid S] [AddMonoid M] [SMul S R] [DistribMulAction S M] (s : S) (r : R) :
    (inl (s • r) : tsze R M) = s • inl r :=
  ext rfl (smul_zero s).symm

Scalar Multiplication Commutes with Inclusion in Trivial Square-Zero Extension

Informal description

Let $S$ be a monoid, $M$ an additive monoid, and $R$ a ring with a scalar multiplication operation $S \times R \to R$. Suppose $M$ is a distributive $S$-module. Then for any $s \in S$ and $r \in R$, the canonical inclusion of the scalar multiple $s \cdot r$ into the trivial square-zero extension $R \oplus M$ equals the scalar multiple of the inclusion of $r$, i.e., $$(s \cdot r, 0) = s \cdot (r, 0).$$

TrivSqZeroExt.inl_sum theorem

 {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → R) :
  (inl (∑ i ∈ s, f i) : tsze R M) = ∑ i ∈ s, inl (f i)

Full source

theorem inl_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → R) :
    (inl (∑ i ∈ s, f i) : tsze R M) = ∑ i ∈ s, inl (f i) :=
  map_sum (LinearMap.inl ℕ _ _) _ _

Inclusion Preserves Finite Sums in Trivial Square-Zero Extension

Informal description

Let $R$ be a commutative additive monoid, $M$ an additive commutative monoid, and $\mathrm{TrivSqZeroExt}(R, M)$ their trivial square-zero extension. For any finite index set $\iota$ and function $f \colon \iota \to R$, the canonical inclusion $\mathrm{inl} \colon R \to \mathrm{TrivSqZeroExt}(R, M)$ preserves finite sums. That is, \[ \mathrm{inl}\left(\sum_{i \in s} f(i)\right) = \sum_{i \in s} \mathrm{inl}(f(i)) \] for any finite subset $s \subseteq \iota$.

TrivSqZeroExt.inr_zero theorem

[Zero R] [Zero M] : (inr 0 : tsze R M) = 0

Full source

@[simp]
theorem inr_zero [Zero R] [Zero M] : (inr 0 : tsze R M) = 0 :=
  rfl

Inclusion of Zero in Trivial Square-Zero Extension Preserves Zero

Informal description

For a ring $R$ with zero element and a module $M$ over $R$ with zero element, the inclusion of the zero element of $M$ into the trivial square-zero extension $R \oplus M$ equals the zero element of the extension, i.e., $(0, 0_M) = 0_{R \oplus M}$.

TrivSqZeroExt.inr_add theorem

[AddZeroClass R] [Add M] (m₁ m₂ : M) : (inr (m₁ + m₂) : tsze R M) = inr m₁ + inr m₂

Full source

@[simp]
theorem inr_add [AddZeroClass R] [Add M] (m₁ m₂ : M) :
    (inr (m₁ + m₂) : tsze R M) = inr m₁ + inr m₂ :=
  ext (add_zero 0).symm rfl

Additivity of the Inclusion Map in Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive zero class and any $R$-module $M$ with an addition operation, the inclusion map $\operatorname{inr} : M \to R \oplus M$ preserves addition. That is, for any $m_1, m_2 \in M$, we have $\operatorname{inr}(m_1 + m_2) = \operatorname{inr}(m_1) + \operatorname{inr}(m_2)$ in the trivial square-zero extension $R \oplus M$.

TrivSqZeroExt.inr_neg theorem

[NegZeroClass R] [Neg M] (m : M) : (inr (-m) : tsze R M) = -inr m

Full source

@[simp]
theorem inr_neg [NegZeroClass R] [Neg M] (m : M) : (inr (-m) : tsze R M) = -inr m :=
  ext neg_zero.symm rfl

Negation Preservation in Trivial Square-Zero Extension Inclusion

Informal description

For any ring $R$ with a negation operation and zero element, and any $R$-module $M$ with a negation operation, the inclusion map $\operatorname{inr} : M \to R \oplus M$ preserves negation. That is, for any $m \in M$, we have $\operatorname{inr}(-m) = -\operatorname{inr}(m)$ in the trivial square-zero extension $R \oplus M$.

TrivSqZeroExt.inr_sub theorem

[SubNegZeroMonoid R] [Sub M] (m₁ m₂ : M) : (inr (m₁ - m₂) : tsze R M) = inr m₁ - inr m₂

Full source

@[simp]
theorem inr_sub [SubNegZeroMonoid R] [Sub M] (m₁ m₂ : M) :
    (inr (m₁ - m₂) : tsze R M) = inr m₁ - inr m₂ :=
  ext (sub_zero _).symm rfl

Subtraction Preservation in Trivial Square-Zero Extension Inclusion

Informal description

Let $R$ be a ring with a subtraction operation and negation, and let $M$ be an $R$-module with a subtraction operation. For any elements $m_1, m_2 \in M$, the inclusion map $\operatorname{inr} : M \to R \oplus M$ preserves subtraction, i.e., $\operatorname{inr}(m_1 - m_2) = \operatorname{inr}(m_1) - \operatorname{inr}(m_2)$ in the trivial square-zero extension $R \oplus M$.

TrivSqZeroExt.inr_smul theorem

[Zero R] [SMulZeroClass S R] [SMul S M] (r : S) (m : M) : (inr (r • m) : tsze R M) = r • inr m

Full source

@[simp]
theorem inr_smul [Zero R] [SMulZeroClass S R] [SMul S M] (r : S) (m : M) :
    (inr (r • m) : tsze R M) = r • inr m :=
  ext (smul_zero _).symm rfl

Linearity of Inclusion in Trivial Square-Zero Extension: $\text{inr}(r \cdot m) = r \cdot \text{inr}(m)$

Informal description

Let $R$ be a ring with a zero element, $M$ be an $R$-module, and $S$ be a scalar type with a scalar multiplication action on both $R$ and $M$. For any scalar $r \in S$ and any element $m \in M$, the inclusion of the scalar multiple $r \cdot m$ into the trivial square-zero extension $R \oplus M$ is equal to the scalar multiple $r$ applied to the inclusion of $m$ in $R \oplus M$. In other words, the inclusion map $\text{inr} : M \to R \oplus M$ is $S$-linear.

TrivSqZeroExt.inr_sum theorem

 {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
  (inr (∑ i ∈ s, f i) : tsze R M) = ∑ i ∈ s, inr (f i)

Full source

theorem inr_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
    (inr (∑ i ∈ s, f i) : tsze R M) = ∑ i ∈ s, inr (f i) :=
  map_sum (LinearMap.inr ℕ _ _) _ _

Sum Preservation by Inclusion in Trivial Square-Zero Extension

Informal description

Let $R$ be a ring and $M$ an $R$-module, both equipped with additive commutative monoid structures. For any finite index set $\iota$, any finite subset $s \subseteq \iota$, and any function $f : \iota \to M$, the inclusion map $\operatorname{inr} : M \to R \oplus M$ preserves finite sums. That is, \[ \operatorname{inr}\left(\sum_{i \in s} f(i)\right) = \sum_{i \in s} \operatorname{inr}(f(i)). \]

TrivSqZeroExt.inl_fst_add_inr_snd_eq theorem

[AddZeroClass R] [AddZeroClass M] (x : tsze R M) : inl x.fst + inr x.snd = x

Full source

theorem inl_fst_add_inr_snd_eq [AddZeroClass R] [AddZeroClass M] (x : tsze R M) :
    inl x.fst + inr x.snd = x :=
  ext (add_zero x.1) (zero_add x.2)

Decomposition of Trivial Square-Zero Extension Elements: $x = (r, 0) + (0, m)$

Informal description

For any element $x$ in the trivial square-zero extension $R \oplus M$ of a ring $R$ and an $R$-module $M$, the sum of the inclusion of its first projection to $R$ and the inclusion of its second projection to $M$ equals $x$ itself. That is, if $x = (r, m) \in R \oplus M$, then $(r, 0) + (0, m) = (r, m)$.

TrivSqZeroExt.ind theorem

 {R M} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R M → Prop} (inl_add_inr : ∀ r m, P (inl r + inr m)) (x) :
  P x

Full source

/-- To show a property hold on all `TrivSqZeroExt R M` it suffices to show it holds
on terms of the form `inl r + inr m`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
theorem ind {R M} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R M → Prop}
    (inl_add_inr : ∀ r m, P (inl r + inr m)) (x) : P x :=
  inl_fst_add_inr_snd_eq x ▸ inl_add_inr x.1 x.2

Induction Principle for Trivial Square-Zero Extension

Informal description

Let $R$ be a ring and $M$ an $R$-module, both equipped with additive structures. For any predicate $P$ on the trivial square-zero extension $R \oplus M$, if $P$ holds for all elements of the form $(r, 0) + (0, m) = (r, m)$, then $P$ holds for all elements of $R \oplus M$.

TrivSqZeroExt.linearMap_ext theorem

 {N} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [AddCommMonoid N] [Module S R] [Module S M] [Module S N]
  ⦃f g : tsze R M →ₗ[S] N⦄ (hl : ∀ r, f (inl r) = g (inl r)) (hr : ∀ m, f (inr m) = g (inr m)) : f = g

Full source

/-- This cannot be marked `@[ext]` as it ends up being used instead of `LinearMap.prod_ext` when
working with `R × M`. -/
theorem linearMap_ext {N} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [AddCommMonoid N]
    [Module S R] [Module S M] [Module S N] ⦃f g : tszetsze R M →ₗ[S] N⦄
    (hl : ∀ r, f (inl r) = g (inl r)) (hr : ∀ m, f (inr m) = g (inr m)) : f = g :=
  LinearMap.prod_ext (LinearMap.ext hl) (LinearMap.ext hr)

Extensionality of Linear Maps on Trivial Square-Zero Extension via Componentwise Equality

Informal description

Let $S$ be a semiring, and let $R$, $M$, and $N$ be additive commutative monoids equipped with $S$-module structures. For any two $S$-linear maps $f, g \colon R \oplus M \to N$, if $f$ and $g$ agree on the canonical inclusions of $R$ and $M$ into $R \oplus M$ (i.e., $f(r, 0) = g(r, 0)$ for all $r \in R$ and $f(0, m) = g(0, m)$ for all $m \in M$), then $f = g$.

TrivSqZeroExt.inrHom definition

[Semiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] tsze R M

Full source

/-- The canonical `R`-linear inclusion `M → TrivSqZeroExt R M`. -/
@[simps apply]
def inrHom [Semiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] tsze R M :=
  { LinearMap.inr R R M with toFun := inr }

Canonical linear inclusion into trivial square-zero extension

Informal description

The canonical $R$-linear inclusion map from the module $M$ into the trivial square-zero extension $\text{TrivSqZeroExt}\, R\, M$, defined by $m \mapsto (0, m)$. This map preserves addition and scalar multiplication.

TrivSqZeroExt.sndHom definition

[Semiring R] [AddCommMonoid M] [Module R M] : tsze R M →ₗ[R] M

Full source

/-- The canonical `R`-linear projection `TrivSqZeroExt R M → M`. -/
@[simps apply]
def sndHom [Semiring R] [AddCommMonoid M] [Module R M] : tszetsze R M →ₗ[R] M :=
  { LinearMap.snd _ _ _ with toFun := snd }

Projection to module component (linear map)

Informal description

The $R$-linear map that projects an element of the trivial square-zero extension $R \oplus M$ to its second component in $M$.

TrivSqZeroExt.one instance

[One R] [Zero M] : One (tsze R M)

Full source

instance one [One R] [Zero M] : One (tsze R M) :=
  ⟨(1, 0)⟩

Multiplicative Identity in Trivial Square-Zero Extension

Informal description

For any ring $R$ with a multiplicative identity and any $R$-module $M$ with a zero element, the trivial square-zero extension $R \oplus M$ has a multiplicative identity given by $(1, 0)$.

TrivSqZeroExt.mul instance

[Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] : Mul (tsze R M)

Full source

instance mul [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] : Mul (tsze R M) :=
  ⟨fun x y => (x.1 * y.1, x.1 •> y.2 + x.2 <• y.1)⟩

Multiplication in the Trivial Square-Zero Extension

Informal description

The trivial square-zero extension $R \oplus M$ of a ring $R$ with an $(R, R)$-bimodule $M$ is equipped with a multiplication operation defined by $(r_1 + m_1) \cdot (r_2 + m_2) = r_1 r_2 + r_1 m_2 + m_1 r_2$ for all $r_1, r_2 \in R$ and $m_1, m_2 \in M$.

TrivSqZeroExt.fst_one theorem

[One R] [Zero M] : (1 : tsze R M).fst = 1

Full source

@[simp]
theorem fst_one [One R] [Zero M] : (1 : tsze R M).fst = 1 :=
  rfl

First Projection of Identity in Trivial Square-Zero Extension is One

Informal description

For any ring $R$ with a multiplicative identity and any $R$-module $M$ with a zero element, the first projection of the multiplicative identity $(1, 0)$ in the trivial square-zero extension $R \oplus M$ is equal to $1$, i.e., $\text{fst}(1) = 1$.

TrivSqZeroExt.snd_one theorem

[One R] [Zero M] : (1 : tsze R M).snd = 0

Full source

@[simp]
theorem snd_one [One R] [Zero M] : (1 : tsze R M).snd = 0 :=
  rfl

Second Component of Identity in Trivial Square-Zero Extension is Zero

Informal description

For any ring $R$ with a multiplicative identity and any $R$-module $M$ with a zero element, the second component of the multiplicative identity $(1, 0)$ in the trivial square-zero extension $R \oplus M$ is equal to $0$, i.e., $\text{snd}(1) = 0$.

TrivSqZeroExt.fst_mul theorem

[Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : tsze R M) : (x₁ * x₂).fst = x₁.fst * x₂.fst

Full source

@[simp]
theorem fst_mul [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : tsze R M) :
    (x₁ * x₂).fst = x₁.fst * x₂.fst :=
  rfl

First projection preserves multiplication in trivial square-zero extension

Informal description

Let $R$ be a ring with multiplication and $M$ be an $R$-bimodule with addition. For any two elements $x_1, x_2$ in the trivial square-zero extension $R \oplus M$, the first projection of their product equals the product of their first projections, i.e., $(x_1 \cdot x_2)_1 = x_{1,1} \cdot x_{2,1}$.

TrivSqZeroExt.snd_mul theorem

 [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : tsze R M) : (x₁ * x₂).snd = x₁.fst •> x₂.snd + x₁.snd <• x₂.fst

Full source

@[simp]
theorem snd_mul [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : tsze R M) :
    (x₁ * x₂).snd = x₁.fst •> x₂.snd + x₁.snd <• x₂.fst :=
  rfl

Second Component of Product in Trivial Square-Zero Extension

Informal description

Let $R$ be a ring with multiplication and $M$ be an $(R, R)$-bimodule with addition. For any two elements $x_1 = (r_1, m_1)$ and $x_2 = (r_2, m_2)$ in the trivial square-zero extension $R \oplus M$, the second component of their product is given by: $$(x_1 \cdot x_2)_2 = r_1 \cdot m_2 + m_1 \cdot r_2$$ where $\cdot$ denotes the left and right module actions of $R$ on $M$.

TrivSqZeroExt.inl_one theorem

[One R] [Zero M] : (inl 1 : tsze R M) = 1

Full source

@[simp]
theorem inl_one [One R] [Zero M] : (inl 1 : tsze R M) = 1 :=
  rfl

Inclusion of Multiplicative Identity in Trivial Square-Zero Extension

Informal description

Let $R$ be a ring with multiplicative identity $1$ and $M$ be an $R$-module with zero element $0$. The canonical inclusion map $\text{inl}$ from $R$ into the trivial square-zero extension $R \oplus M$ satisfies $\text{inl}(1) = 1$, where the right-hand side $1$ is the multiplicative identity in $R \oplus M$ given by $(1, 0)$.

TrivSqZeroExt.inl_mul theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R) :
  (inl (r₁ * r₂) : tsze R M) = inl r₁ * inl r₂

Full source

@[simp]
theorem inl_mul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (r₁ r₂ : R) : (inl (r₁ * r₂) : tsze R M) = inl r₁ * inl r₂ :=
  ext rfl <| show (0 : M) = r₁ •> (0 : M) + (0 : M) <• r₂ by rw [smul_zero, zero_add, smul_zero]

Inclusion of Product Equals Product of Inclusions in Trivial Square-Zero Extension

Informal description

Let $R$ be a monoid and $M$ an $(R, R)$-bimodule. For any two elements $r_1, r_2 \in R$, the canonical inclusion $\operatorname{inl}$ of their product into the trivial square-zero extension $R \oplus M$ equals the product of their individual inclusions, i.e., $$\operatorname{inl}(r_1 r_2) = \operatorname{inl}(r_1) \cdot \operatorname{inl}(r_2)$$ where the multiplication on the right is the multiplication in $R \oplus M$.

TrivSqZeroExt.inl_mul_inl theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R) :
  (inl r₁ * inl r₂ : tsze R M) = inl (r₁ * r₂)

Full source

theorem inl_mul_inl [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (r₁ r₂ : R) : (inl r₁ * inl r₂ : tsze R M) = inl (r₁ * r₂) :=
  (inl_mul M r₁ r₂).symm

Product of Ring Elements in Trivial Square-Zero Extension Equals Inclusion of Their Product

Informal description

Let $R$ be a monoid and $M$ an $(R, R)$-bimodule. For any two elements $r_1, r_2 \in R$, the product of their canonical inclusions $\operatorname{inl}(r_1)$ and $\operatorname{inl}(r_2)$ in the trivial square-zero extension $R \oplus M$ equals the canonical inclusion of their product in $R$, i.e., $$(r_1, 0) \cdot (r_2, 0) = (r_1 r_2, 0)$$ where the multiplication on the left is the multiplication in $R \oplus M$.

TrivSqZeroExt.inr_mul_inr theorem

 [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ m₂ : M) : (inr m₁ * inr m₂ : tsze R M) = 0

Full source

@[simp]
theorem inr_mul_inr [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ m₂ : M) :
    (inr m₁ * inr m₂ : tsze R M) = 0 :=
  ext (mul_zero _) <|
    show (0 : R) •> m₂ + m₁ <• (0 : R) = 0 by rw [zero_smul, zero_add, op_zero, zero_smul]

Square-zero property of module elements: $(0, m_1) \cdot (0, m_2) = 0$

Informal description

Let $R$ be a semiring and $M$ an $R$-bimodule. For any two elements $m_1, m_2 \in M$, the product of their images under the inclusion map $\operatorname{inr}$ in the trivial square-zero extension $R \oplus M$ is zero, i.e., $(0, m_1) \cdot (0, m_2) = 0$.

TrivSqZeroExt.inl_mul_inr theorem

 [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) :
  (inl r * inr m : tsze R M) = inr (r • m)

Full source

theorem inl_mul_inr [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) : (inl r * inr m : tsze R M) = inr (r • m) :=
  ext (mul_zero r) <|
    show r • m + (0 : Rᵐᵒᵖ) • (0 : M) = r • m by rw [smul_zero, add_zero]

Left multiplication by ring element on module element in trivial square-zero extension: $(r, 0) \cdot (0, m) = (0, r \cdot m)$

Informal description

Let $R$ be a monoid with zero and $M$ an additive monoid equipped with left and right distributive multiplicative actions of $R$. For any $r \in R$ and $m \in M$, the product of the canonical inclusion $(r, 0)$ with the inclusion $(0, m)$ in the trivial square-zero extension $R \oplus M$ equals the inclusion of the left scalar multiplication $r \cdot m$, i.e., $(r, 0) \cdot (0, m) = (0, r \cdot m)$.

TrivSqZeroExt.inr_mul_inl theorem

 [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) :
  (inr m * inl r : tsze R M) = inr (m <• r)

Full source

theorem inr_mul_inl [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) : (inr m * inl r : tsze R M) = inr (m <• r) :=
  ext (zero_mul r) <|
    show (0 : R) •> (0 : M) + m <• r = m <• r by rw [smul_zero, zero_add]

Right scalar multiplication in trivial square-zero extension: $(0, m) \cdot (r, 0) = (0, m <• r)$

Informal description

Let $R$ be a monoid with zero and $M$ an additive monoid equipped with left and right distributive multiplicative actions of $R$. For any $r \in R$ and $m \in M$, the product of the module element $m$ (embedded via $\operatorname{inr}$) with the ring element $r$ (embedded via $\operatorname{inl}$) in the trivial square-zero extension $R \oplus M$ equals the embedding of the right scalar multiplication $m <• r$ (i.e., $(0, m) \cdot (r, 0) = (0, m <• r)$).

TrivSqZeroExt.inl_mul_eq_smul theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (x : tsze R M) : inl r * x = r •> x

Full source

theorem inl_mul_eq_smul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (r : R) (x : tsze R M) :
    inl r * x = r •> x :=
  ext rfl (by dsimp; rw [smul_zero, add_zero])

Left multiplication by inclusion equals left scalar multiplication in trivial square-zero extension

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with left and right distributive multiplicative actions of $R$. For any $r \in R$ and $x \in R \oplus M$, the product of the canonical inclusion $(r, 0)$ with $x$ in the trivial square-zero extension equals the left scalar multiplication of $r$ on $x$, i.e., $(r, 0) \cdot x = r \cdot x$.

TrivSqZeroExt.mul_inl_eq_op_smul theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : tsze R M) (r : R) : x * inl r = x <• r

Full source

theorem mul_inl_eq_op_smul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (x : tsze R M) (r : R) :
    x * inl r = x <• r :=
  ext rfl (by dsimp; rw [smul_zero, zero_add])

Right Multiplication by Inclusion Equals Right Scalar Multiplication in Trivial Square-Zero Extension

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with left and right distributive multiplicative actions of $R$. For any element $x$ in the trivial square-zero extension $R \oplus M$ and any $r \in R$, the product of $x$ with the canonical inclusion $(r, 0)$ equals the right scalar multiplication of $x$ by $r$, i.e., $x \cdot (r, 0) = x <• r$.

TrivSqZeroExt.mulOneClass instance

[Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] : MulOneClass (tsze R M)

Full source

instance mulOneClass [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] :
    MulOneClass (tsze R M) :=
  { TrivSqZeroExt.one, TrivSqZeroExt.mul with
    one_mul := fun x =>
      ext (one_mul x.1) <|
        show (1 : R) •> x.2 + (0 : M) <• x.1 = x.2 by rw [one_smul, smul_zero, add_zero]
    mul_one := fun x =>
      ext (mul_one x.1) <|
        show x.1 • (0 : M) + x.2 <• (1 : R) = x.2 by rw [smul_zero, zero_add, op_one, one_smul] }

Monoid Structure on Trivial Square-Zero Extension

Informal description

For any monoid $R$ and any $R$-bimodule $M$ (with left and right distributive multiplicative actions), the trivial square-zero extension $R \oplus M$ forms a multiplicative monoid with identity $(1, 0)$, where the multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$.

TrivSqZeroExt.addMonoidWithOne instance

[AddMonoidWithOne R] [AddMonoid M] : AddMonoidWithOne (tsze R M)

Full source

instance addMonoidWithOne [AddMonoidWithOne R] [AddMonoid M] : AddMonoidWithOne (tsze R M) :=
  { TrivSqZeroExt.addMonoid, TrivSqZeroExt.one with
    natCast := fun n => inl n
    natCast_zero := by simp [Nat.cast]
    natCast_succ := fun _ => by ext <;> simp [Nat.cast] }

Additive Monoid with One Structure on Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive monoid structure and a one element, and any $R$-module $M$ with an additive monoid structure, the trivial square-zero extension $R \oplus M$ inherits an additive monoid structure with one from $R$ and $M$.

TrivSqZeroExt.fst_natCast theorem

[AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (n : tsze R M).fst = n

Full source

@[simp]
theorem fst_natCast [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (n : tsze R M).fst = n :=
  rfl

First Projection of Natural Number in Trivial Square-Zero Extension Equals Itself

Informal description

For any ring $R$ with an additive monoid structure and a one element, and any $R$-module $M$ with an additive monoid structure, the first projection of the natural number $n$ (viewed as an element of the trivial square-zero extension $R \oplus M$) equals $n$ itself, i.e., $\operatorname{fst}(n) = n$.

TrivSqZeroExt.snd_natCast theorem

[AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (n : tsze R M).snd = 0

Full source

@[simp]
theorem snd_natCast [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (n : tsze R M).snd = 0 :=
  rfl

Vanishing of Module Component for Natural Numbers in Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive monoid structure and a one element, and any $R$-module $M$ with an additive monoid structure, the projection to the module component of the natural number $n$ (viewed as an element of the trivial square-zero extension $R \oplus M$) is zero, i.e., $\operatorname{snd}(n) = 0$.

TrivSqZeroExt.inl_natCast theorem

[AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (inl n : tsze R M) = n

Full source

@[simp]
theorem inl_natCast [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (inl n : tsze R M) = n :=
  rfl

Natural Number Inclusion in Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive monoid structure and a one element, and any $R$-module $M$ with an additive monoid structure, the canonical inclusion of a natural number $n$ into the trivial square-zero extension $R \oplus M$ coincides with the natural number $n$ viewed as an element of $R \oplus M$, i.e., $\operatorname{inl}(n) = n$.

TrivSqZeroExt.addGroupWithOne instance

[AddGroupWithOne R] [AddGroup M] : AddGroupWithOne (tsze R M)

Full source

instance addGroupWithOne [AddGroupWithOne R] [AddGroup M] : AddGroupWithOne (tsze R M) :=
  { TrivSqZeroExt.addGroup, TrivSqZeroExt.addMonoidWithOne with
    intCast := fun z => inl z
    intCast_ofNat := fun _n => ext (Int.cast_natCast _) rfl
    intCast_negSucc := fun _n => ext (Int.cast_negSucc _) neg_zero.symm }

Additive Group with One Structure on Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive group structure and a one element, and any $R$-module $M$ with an additive group structure, the trivial square-zero extension $R \oplus M$ inherits an additive group structure with one from $R$ and $M$.

TrivSqZeroExt.fst_intCast theorem

[AddGroupWithOne R] [AddGroup M] (z : ℤ) : (z : tsze R M).fst = z

Full source

@[simp]
theorem fst_intCast [AddGroupWithOne R] [AddGroup M] (z : ℤ) : (z : tsze R M).fst = z :=
  rfl

First Projection of Integer Cast in Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive group structure and a one element, and any $R$-module $M$ with an additive group structure, the first projection of the trivial square-zero extension $R \oplus M$ maps any integer $z$ to itself, i.e., $(z : R \oplus M).\text{fst} = z$.

TrivSqZeroExt.snd_intCast theorem

[AddGroupWithOne R] [AddGroup M] (z : ℤ) : (z : tsze R M).snd = 0

Full source

@[simp]
theorem snd_intCast [AddGroupWithOne R] [AddGroup M] (z : ℤ) : (z : tsze R M).snd = 0 :=
  rfl

Second Projection of Integer Cast in Trivial Square-Zero Extension is Zero

Informal description

For any ring $R$ with an additive group structure and a one element, and any $R$-module $M$ with an additive group structure, the second projection of the trivial square-zero extension $R \oplus M$ maps any integer $z$ to zero, i.e., $(z : R \oplus M).\text{snd} = 0$.

TrivSqZeroExt.inl_intCast theorem

[AddGroupWithOne R] [AddGroup M] (z : ℤ) : (inl z : tsze R M) = z

Full source

@[simp]
theorem inl_intCast [AddGroupWithOne R] [AddGroup M] (z : ℤ) : (inl z : tsze R M) = z :=
  rfl

Preservation of Integer Casts by Canonical Inclusion in Trivial Square-Zero Extension

Informal description

For any ring $R$ with an additive group structure and a one element, and any $R$-module $M$ with an additive group structure, the canonical inclusion map $\operatorname{inl}$ from $R$ into the trivial square-zero extension $R \oplus M$ preserves integer casts. That is, for any integer $z \in \mathbb{Z}$, we have $\operatorname{inl}(z) = z$ in $R \oplus M$.

TrivSqZeroExt.nonAssocSemiring instance

[Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : NonAssocSemiring (tsze R M)

Full source

instance nonAssocSemiring [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] :
    NonAssocSemiring (tsze R M) :=
  { TrivSqZeroExt.addMonoidWithOne, TrivSqZeroExt.mulOneClass, TrivSqZeroExt.addCommMonoid with
    zero_mul := fun x =>
      ext (zero_mul x.1) <|
        show (0 : R) •> x.2 + (0 : M) <• x.1 = 0 by rw [zero_smul, zero_add, smul_zero]
    mul_zero := fun x =>
      ext (mul_zero x.1) <|
        show x.1 • (0 : M) + (0 : Rᵐᵒᵖ) • x.2 = 0 by rw [smul_zero, zero_add, zero_smul]
    left_distrib := fun x₁ x₂ x₃ =>
      ext (mul_add x₁.1 x₂.1 x₃.1) <|
        show
          x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) =
            x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
          by simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]
    right_distrib := fun x₁ x₂ x₃ =>
      ext (add_mul x₁.1 x₂.1 x₃.1) <|
        show
          (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 =
            x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
          by simp_rw [add_smul, smul_add, add_add_add_comm] }

Non-Associative Semiring Structure on Trivial Square-Zero Extensions

Informal description

For any semiring $R$ and any $R$-bimodule $M$ (where $M$ is an additive commutative monoid with compatible left and right $R$-module structures), the trivial square-zero extension $R \oplus M$ forms a non-associative semiring. The multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, and the addition is componentwise.

TrivSqZeroExt.nonAssocRing instance

[Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] : NonAssocRing (tsze R M)

Full source

instance nonAssocRing [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] :
    NonAssocRing (tsze R M) :=
  { TrivSqZeroExt.addGroupWithOne, TrivSqZeroExt.nonAssocSemiring with }

Non-Associative Ring Structure on Trivial Square-Zero Extensions

Informal description

For any ring $R$ and any $R$-bimodule $M$ (where $M$ is an additive commutative group with compatible left and right $R$-module structures), the trivial square-zero extension $R \oplus M$ forms a non-associative ring. The multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, and the addition is componentwise.

TrivSqZeroExt.instPowNatOfDistribMulActionMulOpposite instance

[Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] : Pow (tsze R M) ℕ

Full source

/-- In the general non-commutative case, the power operator is

$$\begin{align}
(r + m)^n &= r^n + r^{n-1}m + r^{n-2}mr + \cdots + rmr^{n-2} + mr^{n-1} \\
          & =r^n + \sum_{i = 0}^{n - 1} r^{(n - 1) - i} m r^{i}
\end{align}$$

In the commutative case this becomes the simpler $(r + m)^n = r^n + nr^{n-1}m$.
-/
instance [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] :
    Pow (tsze R M) ℕ :=
  ⟨fun x n =>
    ⟨x.fst ^ n, ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum⟩⟩

Power Operation on Trivial Square-Zero Extensions

Informal description

For any monoid $R$ and additive monoid $M$ equipped with compatible left and right distributive multiplicative actions of $R$ on $M$, the trivial square-zero extension $R \oplus M$ has a natural power operation defined by: $$(r + m)^n = r^n + \sum_{i=0}^{n-1} r^{n-1-i} \cdot m \cdot r^i$$ where $\cdot$ denotes the left and right actions of $R$ on $M$.

TrivSqZeroExt.fst_pow theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ) :
  fst (x ^ n) = x.fst ^ n

Full source

@[simp]
theorem fst_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (x : tsze R M) (n : ℕ) : fst (x ^ n) = x.fst ^ n :=
  rfl

First Component of Power in Trivial Square-Zero Extension Equals Power of First Component

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$. For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ and any natural number $n$, the first component of $x^n$ is equal to $r^n$, i.e., $\text{fst}(x^n) = r^n$.

TrivSqZeroExt.snd_pow_eq_sum theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ) :
  snd (x ^ n) = ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum

Full source

theorem snd_pow_eq_sum [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    (x : tsze R M) (n : ℕ) :
    snd (x ^ n) = ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum :=
  rfl

Sum Formula for Second Component of Power in Trivial Square-Zero Extension

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$. For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ and any natural number $n$, the second component of $x^n$ is given by: $$snd(x^n) = \sum_{i=0}^{n-1} r^{n-1-i} \cdot m \cdot r^i$$ where $\cdot$ denotes the left and right actions of $R$ on $M$ respectively.

TrivSqZeroExt.snd_pow_of_smul_comm theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M)
  (n : ℕ) (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • x.fst ^ n.pred •> x.snd

Full source

theorem snd_pow_of_smul_comm [Monoid R] [AddMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ)
    (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • x.fst ^ n.pred •> x.snd := by
  simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]
  match n with
  | 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
  | (Nat.succ n) =>
    simp_rw [Nat.pred_succ]
    refine (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) ?_).trans ?_
    · rintro m hm
      simp_rw [List.mem_map, List.mem_range] at hm
      obtain ⟨i, hi, rfl⟩ := hm
      rw [Nat.sub_add_cancel (Nat.lt_succ_iff.mp hi)]
    · rw [List.length_map, List.length_range]
where
  aux : ∀ n : ℕ, x.snd <• x.fst ^ n = x.fst ^ n •> x.snd := by
    intro n
    induction n with
    | zero => simp
    | succ n ih =>
      rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]

Power of Trivial Square-Zero Extension Element with Commuting Actions

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$ such that the actions commute. For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ and any natural number $n$, if the condition $m \cdot r = r \cdot m$ holds (where $\cdot$ denotes the right and left actions respectively), then the second component of $x^n$ is given by: $$snd(x^n) = n \cdot r^{n-1} \cdot m$$ where $\cdot$ denotes the left action of $R$ on $M$.

TrivSqZeroExt.snd_pow_of_smul_comm' theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M)
  (n : ℕ) (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • (x.snd <• x.fst ^ n.pred)

Full source

theorem snd_pow_of_smul_comm' [Monoid R] [AddMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ)
    (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • (x.snd <• x.fst ^ n.pred) := by
  rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]

Power formula for module component in trivial square-zero extension with commuting actions

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$ such that the actions commute. For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ and any natural number $n$, if the condition $m \cdot r = r \cdot m$ holds (where $\cdot$ denotes the right and left actions respectively), then the second component of $x^n$ is given by: $$snd(x^n) = n \cdot (m \cdot r^{n-1})$$ where $\cdot$ denotes the right action of $R$ on $M$.

TrivSqZeroExt.snd_pow theorem

 [CommMonoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M] (x : tsze R M)
  (n : ℕ) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd

Full source

@[simp]
theorem snd_pow [CommMonoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    [IsCentralScalar R M] (x : tsze R M) (n : ℕ) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd :=
  snd_pow_of_smul_comm _ _ (op_smul_eq_smul _ _)

Power formula for module component in commutative trivial square-zero extension

Informal description

Let $R$ be a commutative monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$ such that the actions are central (i.e., $r \cdot m = m \cdot r$ for all $r \in R$ and $m \in M$). For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ and any natural number $n$, the second component of $x^n$ is given by: $$snd(x^n) = n \cdot r^{n-1} \cdot m$$ where $\cdot$ denotes the scalar multiplication of $R$ on $M$.

TrivSqZeroExt.inl_pow theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (n : ℕ) :
  (inl r ^ n : tsze R M) = inl (r ^ n)

Full source

@[simp]
theorem inl_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R)
    (n : ℕ) : (inl r ^ n : tsze R M) = inl (r ^ n) :=
  ext rfl <| by simp [snd_pow_eq_sum, List.map_const']

Power of Canonical Inclusion in Trivial Square-Zero Extension

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$. For any element $r \in R$ and natural number $n \in \mathbb{N}$, the $n$-th power of the canonical inclusion $\operatorname{inl}(r) \in R \oplus M$ in the trivial square-zero extension equals the canonical inclusion of $r^n$, i.e., $$(\operatorname{inl}(r))^n = \operatorname{inl}(r^n).$$

TrivSqZeroExt.monoid instance

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Monoid (tsze R M)

Full source

instance monoid [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] : Monoid (tsze R M) :=
  { TrivSqZeroExt.mulOneClass with
    mul_assoc := fun x y z =>
      ext (mul_assoc x.1 y.1 z.1) <|
        show
          (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 =
            x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
          by simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
    npow := fun n x => x ^ n
    npow_zero := fun x => ext (pow_zero x.fst) (by simp [snd_pow_eq_sum])
    npow_succ := fun n x =>
      ext (pow_succ _ _)
        (by
          simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]
          cases n
          · simp [List.range_succ]
          rw [List.sum_range_succ']
          simp only [pow_zero, op_one, Nat.sub_zero, one_smul, Nat.succ_sub_succ_eq_sub, fst_pow,
            Nat.pred_succ, List.smul_sum, List.map_map, Function.comp_def]
          simp_rw [← smul_comm (_ : R) (_ : Rᵐᵒᵖ), smul_smul, pow_succ]
          rfl) }

Monoid Structure on Trivial Square-Zero Extension

Informal description

For any monoid $R$ and any $R$-bimodule $M$ with compatible left and right distributive multiplicative actions, the trivial square-zero extension $R \oplus M$ forms a monoid under the multiplication defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, with identity element $(1, 0)$.

TrivSqZeroExt.fst_list_prod theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
  (l : List (tsze R M)) : l.prod.fst = (l.map fst).prod

Full source

theorem fst_list_prod [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) : l.prod.fst = (l.map fst).prod :=
  map_list_prod ({ toFun := fst, map_one' := fst_one, map_mul' := fst_mul } : tszetsze R M →* R) _

First Projection Preserves List Products in Trivial Square-Zero Extension

Informal description

Let $R$ be a monoid and $M$ an additive monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$. For any list $l$ of elements in the trivial square-zero extension $R \oplus M$, the first projection of the product of the list equals the product of the first projections of the elements in the list, i.e., $$\text{fst}\left(\prod_{x \in l} x\right) = \prod_{x \in l} \text{fst}(x).$$

TrivSqZeroExt.semiring instance

[Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Semiring (tsze R M)

Full source

instance semiring [Semiring R] [AddCommMonoid M]
    [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Semiring (tsze R M) :=
  { TrivSqZeroExt.monoid, TrivSqZeroExt.nonAssocSemiring with }

Semiring Structure on Trivial Square-Zero Extensions

Informal description

For any semiring $R$ and any $R$-bimodule $M$ (where $M$ is an additive commutative monoid with compatible left and right $R$-module structures and the actions commute), the trivial square-zero extension $R \oplus M$ forms a semiring. The multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, and the addition is componentwise.

TrivSqZeroExt.snd_list_prod theorem

 [Monoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
  (l : List (tsze R M)) :
  l.prod.snd =
    (l.zipIdx.map fun x : tsze R M × ℕ =>
        ((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum

Full source

/-- The second element of a product $\prod_{i=0}^n (r_i + m_i)$ is a sum of terms of the form
$r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$. -/
theorem snd_list_prod [Monoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) :
    l.prod.snd =
      (l.zipIdx.map fun x : tszetsze R M × ℕ =>
          ((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    rw [List.zipIdx_cons']
    simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
      List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
      List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
    exact add_comm _ _

Decomposition of Module Component in Trivial Square-Zero Extension Product

Informal description

Let $R$ be a monoid and $M$ an additive commutative monoid equipped with compatible left and right distributive multiplicative actions of $R$ on $M$ that commute with each other. For any list $l$ of elements in the trivial square-zero extension $R \oplus M$, the second component of the product of the list is given by the sum of terms of the form: $$(r_1 \cdots r_{i-1}) \cdot m_i \cdot (r_{i+1} \cdots r_n)$$ where for each element $(r_i, m_i)$ in the list (at position $i$), we take the product of the first components before position $i$ to act from the left, the product of the first components after position $i$ to act from the right, and apply these to $m_i$.

TrivSqZeroExt.ring instance

[Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Ring (tsze R M)

Full source

instance ring [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] :
    Ring (tsze R M) :=
  { TrivSqZeroExt.semiring, TrivSqZeroExt.nonAssocRing with }

Ring Structure on Trivial Square-Zero Extensions

Informal description

For any ring $R$ and any $R$-bimodule $M$ (where $M$ is an additive commutative group with compatible left and right $R$-module structures and the actions commute), the trivial square-zero extension $R \oplus M$ forms a ring. The multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, and the addition is componentwise.

TrivSqZeroExt.commMonoid instance

 [CommMonoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M] :
  CommMonoid (tsze R M)

Full source

instance commMonoid [CommMonoid R] [AddCommMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M] : CommMonoid (tsze R M) :=
  { TrivSqZeroExt.monoid with
    mul_comm := fun x₁ x₂ =>
      ext (mul_comm x₁.1 x₂.1) <|
        show x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1 by
          rw [op_smul_eq_smul, op_smul_eq_smul, add_comm] }

Commutative Monoid Structure on Trivial Square-Zero Extension

Informal description

For any commutative monoid $R$ and any $R$-bimodule $M$ with compatible left and right distributive multiplicative actions where the actions are central (i.e., $r \cdot m = m \cdot r$ for all $r \in R$ and $m \in M$), the trivial square-zero extension $R \oplus M$ forms a commutative monoid under the multiplication defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, with identity element $(1, 0)$.

TrivSqZeroExt.commSemiring instance

[CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : CommSemiring (tsze R M)

Full source

instance commSemiring [CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
    [IsCentralScalar R M] : CommSemiring (tsze R M) :=
  { TrivSqZeroExt.commMonoid, TrivSqZeroExt.nonAssocSemiring with }

Commutative Semiring Structure on Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R$ and any $R$-bimodule $M$ with compatible left and right $R$-module structures where the actions are central (i.e., $r \cdot m = m \cdot r$ for all $r \in R$ and $m \in M$), the trivial square-zero extension $R \oplus M$ forms a commutative semiring. The multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, and the addition is componentwise.

TrivSqZeroExt.commRing instance

[CommRing R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : CommRing (tsze R M)

Full source

instance commRing [CommRing R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] :
    CommRing (tsze R M) :=
  { TrivSqZeroExt.nonAssocRing, TrivSqZeroExt.commSemiring with }

Commutative Ring Structure on Trivial Square-Zero Extensions

Informal description

For any commutative ring $R$ and any $R$-bimodule $M$ with compatible left and right $R$-module structures where the actions are central (i.e., $r \cdot m = m \cdot r$ for all $r \in R$ and $m \in M$), the trivial square-zero extension $R \oplus M$ forms a commutative ring. The multiplication is defined by $(r_1, m_1) \cdot (r_2, m_2) = (r_1 r_2, r_1 m_2 + m_1 r_2)$, and the addition is componentwise.

TrivSqZeroExt.inlHom definition

[Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : R →+* tsze R M

Full source

/-- The canonical inclusion of rings `R → TrivSqZeroExt R M`. -/
@[simps apply]
def inlHom [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : R →+* tsze R M where
  toFun := inl
  map_one' := inl_one M
  map_mul' := inl_mul M
  map_zero' := inl_zero M
  map_add' := inl_add M

Canonical inclusion homomorphism into trivial square-zero extension

Informal description

The canonical ring homomorphism from a semiring $R$ to the trivial square-zero extension $R \oplus M$, where $M$ is an $R$-bimodule. This homomorphism maps an element $r \in R$ to $(r, 0) \in R \oplus M$, preserving the additive and multiplicative structures. Specifically: - It maps $1_R$ to $(1, 0)$ - It maps $r_1 \cdot r_2$ to $(r_1 r_2, 0)$ - It maps $0_R$ to $(0, 0)$ - It maps $r_1 + r_2$ to $(r_1 + r_2, 0)$

TrivSqZeroExt.instInv instance

: Inv (tsze R M)

Full source

/-- Inversion of the trivial-square-zero extension, sending $r + m$ to $r^{-1} - r^{-1}mr^{-1}$.

Strictly this is only a _two_-sided inverse when the left and right actions associate. -/
instance instInv : Inv (tsze R M) :=
  ⟨fun b => (b.1⁻¹, -(b.1⁻¹ •> b.2 <• b.1⁻¹))⟩

Inversion in Trivial Square-Zero Extension

Informal description

The trivial square-zero extension $R \oplus M$ of a module $M$ over a ring $R$ has an inversion operation defined by $(r + m)^{-1} = r^{-1} - r^{-1} m r^{-1}$, where $r^{-1}$ is the inverse of $r$ in $R$ and the operations $\cdot$ and $\cdot^{-1}$ are extended to $R \oplus M$ componentwise. This inversion is a two-sided inverse when the left and right actions of $R$ on $M$ associate.

TrivSqZeroExt.fst_inv theorem

(x : tsze R M) : fst x⁻¹ = (fst x)⁻¹

Full source

@[simp] theorem fst_inv (x : tsze R M) : fst x⁻¹ = (fst x)⁻¹ :=
  rfl

First Projection Commutes with Inversion in Trivial Square-Zero Extension

Informal description

For any element $x$ in the trivial square-zero extension $R \oplus M$, the first projection of the inverse of $x$ is equal to the inverse of the first projection of $x$, i.e., $\pi_1(x^{-1}) = (\pi_1(x))^{-1}$.

TrivSqZeroExt.snd_inv theorem

(x : tsze R M) : snd x⁻¹ = -((fst x)⁻¹ •> snd x <• (fst x)⁻¹)

Full source

@[simp] theorem snd_inv (x : tsze R M) : snd x⁻¹ = -((fst x)⁻¹(fst x)⁻¹ •> snd x <• (fst x)⁻¹) :=
  rfl

Second Component of Inverse in Trivial Square-Zero Extension: $snd(x^{-1}) = - (fst(x)^{-1} \cdot snd(x) \cdot fst(x)^{-1})$

Informal description

For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$, the second component of the inverse $x^{-1}$ is given by $- (r^{-1} \cdot m \cdot r^{-1})$, where $r^{-1}$ is the inverse of $r$ in $R$ and $\cdot$ denotes the left and right actions of $R$ on $M$.

TrivSqZeroExt.invertibleFstOfInvertible abbrev

(x : tsze R M) [Invertible x] : Invertible x.fst

Full source

/-- `x.fst : R` is invertible when `x : tzre R M` is. -/
abbrev invertibleFstOfInvertible (x : tsze R M) [Invertible x] : Invertible x.fst where
  invOf := (⅟x).fst
  invOf_mul_self := by rw [← fst_mul, invOf_mul_self, fst_one]
  mul_invOf_self := by rw [← fst_mul, mul_invOf_self, fst_one]

Invertibility of First Projection in Trivial Square-Zero Extension

Informal description

For any element $x$ in the trivial square-zero extension $R \oplus M$, if $x$ is invertible, then its first projection $x.fst$ is also invertible in $R$.

TrivSqZeroExt.fst_invOf theorem

(x : tsze R M) [Invertible x] [Invertible x.fst] : (⅟ x).fst = ⅟ (x.fst)

Full source

theorem fst_invOf (x : tsze R M) [Invertible x] [Invertible x.fst] : (⅟x).fst = ⅟(x.fst) := by
  letI := invertibleFstOfInvertible x
  convert (rfl : _ = ⅟ x.fst)

First Component of Inverse in Trivial Square-Zero Extension: $(\text{⅟ }x)_1 = \text{⅟ }(x_1)$

Informal description

For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$, if $x$ is invertible and its first component $r$ is also invertible in $R$, then the first component of the inverse of $x$ equals the inverse of $r$ in $R$, i.e., $(\text{⅟ }x).\text{fst} = \text{⅟ } r$.

TrivSqZeroExt.mul_left_eq_one theorem

(r : R) (x : tsze R M) (h : r * x.fst = 1) : (inl r + inr (-((r •> x.snd) <• r))) * x = 1

Full source

theorem mul_left_eq_one (r : R) (x : tsze R M) (h : r * x.fst = 1) :
    (inl r + inr (-((r •> x.snd) <• r))) * x = 1 := by
  ext <;> dsimp
  · rw [add_zero, h]
  · rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]

Left multiplication by special element yields identity in trivial square-zero extension

Informal description

Let $R$ be a ring and $M$ an $(R,R)$-bimodule. For any $r \in R$ and $x = (x_1, x_2) \in R \oplus M$ such that $r \cdot x_1 = 1$, the product $(r, -r \cdot x_2 \cdot r) \cdot x$ equals the multiplicative identity $1$ in $R \oplus M$.

TrivSqZeroExt.mul_right_eq_one theorem

(x : tsze R M) (r : R) (h : x.fst * r = 1) : x * (inl r + inr (-(r •> (x.snd <• r)))) = 1

Full source

theorem mul_right_eq_one (x : tsze R M) (r : R) (h : x.fst * r = 1) :
    x * (inl r + inr (-(r •> (x.snd <• r)))) = 1 := by
  ext <;> dsimp
  · rw [add_zero, h]
  · rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]

Right Multiplication by Special Element Yields Identity in Trivial Square-Zero Extension

Informal description

Let $R$ be a ring and $M$ an $(R, R)$-bimodule. For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ and any element $r' \in R$ such that $r \cdot r' = 1$, the product $x \cdot (r', -r' \cdot (m \cdot r'))$ equals the multiplicative identity $1$ in $R \oplus M$.

TrivSqZeroExt.invertibleOfInvertibleFst abbrev

(x : tsze R M) [Invertible x.fst] : Invertible x

Full source

/-- `x : tzre R M` is invertible when `x.fst : R` is. -/
abbrev invertibleOfInvertibleFst (x : tsze R M) [Invertible x.fst] : Invertible x where
  invOf := (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst))
  invOf_mul_self := by
    convert mul_left_eq_one _ _ (invOf_mul_self x.fst)
    ext <;> simp
  mul_invOf_self := by
    convert mul_right_eq_one _ _ (mul_invOf_self x.fst)
    ext <;> simp [smul_comm]

Invertibility in Trivial Square-Zero Extension via First Component

Informal description

Let $R$ be a ring and $M$ an $(R, R)$-bimodule. For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$, if the first component $r$ is invertible in $R$, then $x$ is invertible in $R \oplus M$.

TrivSqZeroExt.snd_invOf theorem

(x : tsze R M) [Invertible x] [Invertible x.fst] : (⅟ x).snd = -(⅟ x.fst •> x.snd <• ⅟ x.fst)

Full source

theorem snd_invOf (x : tsze R M) [Invertible x] [Invertible x.fst] :
    (⅟x).snd = -(⅟x.fst⅟x.fst •> x.snd <• ⅟x.fst) := by
  letI := invertibleOfInvertibleFst x
  convert congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟ x)
  convert rfl

Second Component of Inverse in Trivial Square-Zero Extension: $(⅟x)_2 = -⅟r \cdot m \cdot ⅟r$

Informal description

Let $R$ be a ring and $M$ an $(R, R)$-bimodule. For any invertible element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ with $r$ invertible in $R$, the second component of the inverse $⅟x$ is given by $-⅟r \cdot m \cdot ⅟r$, where $⅟r$ is the inverse of $r$ in $R$.

TrivSqZeroExt.invertibleEquivInvertibleFst definition

(x : tsze R M) : Invertible x ≃ Invertible x.fst

Full source

/-- Together `TrivSqZeroExt.detInvertibleOfInvertible` and `TrivSqZeroExt.invertibleOfDetInvertible`
form an equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def invertibleEquivInvertibleFst (x : tsze R M) : InvertibleInvertible x ≃ Invertible x.fst where
  toFun _ := invertibleFstOfInvertible x
  invFun _ := invertibleOfInvertibleFst x
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence of invertibility in trivial square-zero extension and invertibility of first component

Informal description

For any element $ x $ in the trivial square-zero extension $ R \oplus M $, the property of $ x $ being invertible is equivalent to the property of its first projection $ x.fst $ being invertible in $ R $. This equivalence is given by the functions `invertibleFstOfInvertible` and `invertibleOfInvertibleFst`, which are mutual inverses.

TrivSqZeroExt.isUnit_iff_isUnit_fst theorem

{x : tsze R M} : IsUnit x ↔ IsUnit x.fst

Full source

/-- When lowered to a prop, `Matrix.invertibleEquivInvertibleFst` forms an `iff`. -/
theorem isUnit_iff_isUnit_fst {x : tsze R M} : IsUnitIsUnit x ↔ IsUnit x.fst := by
  simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivInvertibleFst x).nonempty_congr]

Unit Criterion for Trivial Square-Zero Extension: $x$ is a unit if and only if $x.fst$ is a unit

Informal description

An element $x$ of the trivial square-zero extension $R \oplus M$ is a unit if and only if its first component $x.fst$ is a unit in the ring $R$.

TrivSqZeroExt.isUnit_inl_iff theorem

{r : R} : IsUnit (inl r : tsze R M) ↔ IsUnit r

Full source

@[simp]
theorem isUnit_inl_iff {r : R} : IsUnitIsUnit (inl r : tsze R M) ↔ IsUnit r := by
  rw [isUnit_iff_isUnit_fst, fst_inl]

Unit Criterion for Ring Inclusion in Trivial Square-Zero Extension: $(r, 0)$ is a unit if and only if $r$ is a unit

Informal description

For any element $r$ in a ring $R$, the canonical inclusion $(r, 0)$ in the trivial square-zero extension $R \oplus M$ is a unit if and only if $r$ is a unit in $R$.

TrivSqZeroExt.isUnit_inr_iff theorem

{m : M} : IsUnit (inr m : tsze R M) ↔ Subsingleton R

Full source

@[simp]
theorem isUnit_inr_iff {m : M} : IsUnitIsUnit (inr m : tsze R M) ↔ Subsingleton R := by
  simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one]

Unit Criterion for Module Inclusion in Trivial Square-Zero Extension: $(0, m)$ is a unit if and only if $R$ is a subsingleton

Informal description

For any element $m$ in the module $M$, the inclusion $(0, m)$ in the trivial square-zero extension $R \oplus M$ is a unit if and only if the ring $R$ is a subsingleton (i.e., has at most one element).

TrivSqZeroExt.inv_inl theorem

(r : R) : (inl r)⁻¹ = (inl (r⁻¹ : R) : tsze R M)

Full source

protected theorem inv_inl (r : R) :
    (inl r)⁻¹ = (inl (r⁻¹ : R) : tsze R M) := by
  ext
  · rw [fst_inv, fst_inl, fst_inl]
  · rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_zero]

Inverse of Inclusion in Trivial Square-Zero Extension: $(r, 0)^{-1} = (r^{-1}, 0)$

Informal description

For any element $r$ in a ring $R$, the inverse of the canonical inclusion $\mathrm{inl}(r) = (r, 0)$ in the trivial square-zero extension $R \oplus M$ is equal to the inclusion of the inverse of $r$ in $R$, i.e., $(r, 0)^{-1} = (r^{-1}, 0)$.

TrivSqZeroExt.inv_inr theorem

(m : M) : (inr m)⁻¹ = (0 : tsze R M)

Full source

@[simp]
theorem inv_inr (m : M) : (inr m)⁻¹ = (0 : tsze R M) := by
  ext
  · rw [fst_inv, fst_inr, fst_zero, inv_zero]
  · rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_zero]

Inverse of Module Inclusion in Trivial Square-Zero Extension is Zero

Informal description

For any element $m$ in the module $M$, the inverse of the inclusion $\mathrm{inr}(m) = (0, m)$ in the trivial square-zero extension $R \oplus M$ is equal to the zero element $(0, 0)$.

TrivSqZeroExt.inv_zero theorem

: (0 : tsze R M)⁻¹ = (0 : tsze R M)

Full source

@[simp]
protected theorem inv_zero : (0 : tsze R M)⁻¹ = (0 : tsze R M) := by
  rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_zero]

Inverse of Zero in Trivial Square-Zero Extension is Zero

Informal description

The inverse of the zero element $(0, 0)$ in the trivial square-zero extension $R \oplus M$ is itself, i.e., $(0, 0)^{-1} = (0, 0)$.

TrivSqZeroExt.inv_one theorem

: (1 : tsze R M)⁻¹ = (1 : tsze R M)

Full source

@[simp]
protected theorem inv_one : (1 : tsze R M)⁻¹ = (1 : tsze R M) := by
  rw [← inl_one, TrivSqZeroExt.inv_inl, inv_one]

Inverse of Identity in Trivial Square-Zero Extension

Informal description

The inverse of the multiplicative identity $(1, 0)$ in the trivial square-zero extension $R \oplus M$ is itself, i.e., $(1, 0)^{-1} = (1, 0)$.

TrivSqZeroExt.inv_mul_cancel theorem

{x : tsze R M} (hx : fst x ≠ 0) : x⁻¹ * x = 1

Full source

protected theorem inv_mul_cancel {x : tsze R M} (hx : fstfst x ≠ 0) : x⁻¹ * x = 1 := by
  convert mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx) using 2
  ext <;> simp

Left Inverse Property for Nonzero Elements in Trivial Square-Zero Extension

Informal description

For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ where the first component $r$ is nonzero, the product of the inverse of $x$ with $x$ itself equals the multiplicative identity $1$.

TrivSqZeroExt.invOf_eq_inv theorem

(x : tsze R M) [Invertible x] : ⅟ x = x⁻¹

Full source

@[simp] theorem invOf_eq_inv (x : tsze R M) [Invertible x] : ⅟x = x⁻¹ := by
  letI := invertibleFstOfInvertible x
  ext <;> simp [fst_invOf, snd_invOf]

Inverse-of Operator Equals Standard Inverse in Trivial Square-Zero Extension

Informal description

For any invertible element $x$ in the trivial square-zero extension $R \oplus M$, the inverse-of operator $\text{⅟ }x$ coincides with the standard inverse operation $x^{-1}$.

TrivSqZeroExt.mul_inv_cancel theorem

{x : tsze R M} (hx : fst x ≠ 0) : x * x⁻¹ = 1

Full source

protected theorem mul_inv_cancel {x : tsze R M} (hx : fstfst x ≠ 0) : x * x⁻¹ = 1 := by
  have : Invertible x.fst := Units.invertible (.mk0 _ hx)
  have := invertibleOfInvertibleFst x
  rw [← invOf_eq_inv, mul_invOf_self]

Right Inverse Property for Nonzero Elements in Trivial Square-Zero Extension

Informal description

For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ where the first component $r$ is nonzero, the product of $x$ with its inverse $x^{-1}$ equals the multiplicative identity $1$.

TrivSqZeroExt.mul_inv_rev theorem

(a b : tsze R M) : (a * b)⁻¹ = b⁻¹ * a⁻¹

Full source

protected theorem mul_inv_rev (a b : tsze R M) :
    (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  ext
  · rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
  · simp only [snd_inv, snd_mul, fst_mul, fst_inv]
    simp only [neg_smul, smul_neg, smul_add]
    simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]
    obtain ha0 | ha := eq_or_ne (fst a) 0
    · simp [ha0]
    obtain hb0 | hb := eq_or_ne (fst b) 0
    · simp [hb0]
    rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]

Inverse of Product in Trivial Square-Zero Extension: $(ab)^{-1} = b^{-1}a^{-1}$

Informal description

For any two elements $a$ and $b$ in the trivial square-zero extension $R \oplus M$, the inverse of their product equals the product of their inverses in reverse order, i.e., $(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$.

TrivSqZeroExt.inv_inv theorem

{x : tsze R M} (hx : fst x ≠ 0) : x⁻¹⁻¹ = x

Full source

protected theorem inv_inv {x : tsze R M} (hx : fstfst x ≠ 0) : x⁻¹x⁻¹⁻¹ = x :=
  -- adapted from `Matrix.nonsing_inv_nonsing_inv`
  calc
    x⁻¹x⁻¹⁻¹ = 1 * x⁻¹x⁻¹⁻¹ := by rw [one_mul]
    _ = x * x⁻¹ * x⁻¹x⁻¹⁻¹ := by rw [TrivSqZeroExt.mul_inv_cancel hx]
    _ = x := by
      rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]
      rw [fst_inv]
      apply inv_ne_zero hx

Double Inversion in Trivial Square-Zero Extension: $(x^{-1})^{-1} = x$ for $r \neq 0$

Informal description

For any element $x = (r, m)$ in the trivial square-zero extension $R \oplus M$ where the first component $r$ is nonzero, the double inverse of $x$ equals $x$ itself, i.e., $(x^{-1})^{-1} = x$.

TrivSqZeroExt.isUnit_inv_iff theorem

{x : tsze R M} : IsUnit x⁻¹ ↔ IsUnit x

Full source

@[simp]
theorem isUnit_inv_iff {x : tsze R M} : IsUnitIsUnit x⁻¹ ↔ IsUnit x := by
  simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]

Unit Criterion for Inverses in Trivial Square-Zero Extension: $x^{-1}$ is a unit if and only if $x$ is a unit

Informal description

For any element $x$ in the trivial square-zero extension $R \oplus M$, the inverse $x^{-1}$ is a unit if and only if $x$ itself is a unit.

TrivSqZeroExt.inv_neg theorem

{x : tsze R M} : (-x)⁻¹ = -(x⁻¹)

Full source

protected theorem inv_neg {x : tsze R M} : (-x)⁻¹ = -(x⁻¹) := by
  ext <;> simp [inv_neg]

Inverse of Negation in Trivial Square-Zero Extension

Informal description

For any element $x$ in the trivial square-zero extension $R \oplus M$, the inverse of the negation $-x$ is equal to the negation of the inverse $x^{-1}$, i.e., $(-x)^{-1} = -(x^{-1})$.

TrivSqZeroExt.algebra' instance

: Algebra S (tsze R M)

Full source

instance algebra' : Algebra S (tsze R M) where
  algebraMap := (TrivSqZeroExt.inlHom R M).comp (algebraMap S R)
  smul := (· • ·)
  commutes' := fun s x =>
    ext (Algebra.commutes _ _) <|
      show algebraMap S R s •> x.snd + (0 : M) <• x.fst
          = x.fst •> (0 : M) + x.snd <• algebraMap S R s by
        rw [smul_zero, smul_zero, add_zero, zero_add]
        rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
          one_smul, smul_assoc, one_smul]
  smul_def' := fun s x =>
    ext (Algebra.smul_def _ _) <|
      show s • x.snd = algebraMap S R s •> x.snd + (0 : M) <• x.fst by
        rw [smul_zero, add_zero, algebraMap_smul]

$S$-Algebra Structure on Trivial Square-Zero Extensions

Informal description

For any semiring $S$ and any $S$-algebra structure on a ring $R$ with an $(R, R)$-bimodule $M$, the trivial square-zero extension $R \oplus M$ inherits an $S$-algebra structure where the algebra map is given by the composition of the algebra map $S \to R$ with the canonical inclusion $R \to R \oplus M$.

TrivSqZeroExt.instAlgebra instance

: Algebra R' (tsze R' M)

Full source

instance : Algebra R' (tsze R' M) :=
  TrivSqZeroExt.algebra' _ _ _

Canonical $R'$-Algebra Structure on Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R'$ and any $R'$-module $M$ with a symmetric scalar multiplication (i.e., the left and right actions coincide), the trivial square-zero extension $R' \oplus M$ is naturally endowed with an $R'$-algebra structure, where the algebra map is given by the canonical inclusion $R' \to R' \oplus M$.

TrivSqZeroExt.algebraMap_eq_inl theorem

: ⇑(algebraMap R' (tsze R' M)) = inl

Full source

theorem algebraMap_eq_inl : ⇑(algebraMap R' (tsze R' M)) = inl :=
  rfl

Algebra Map as Canonical Inclusion in Trivial Square-Zero Extension

Informal description

The algebra map from a commutative semiring $R'$ to its trivial square-zero extension $R' \oplus M$ is equal to the canonical inclusion map $\text{inl} \colon R' \to R' \oplus M$, which sends $r \in R'$ to $(r, 0) \in R' \oplus M$.

TrivSqZeroExt.algebraMap_eq_inlHom theorem

: algebraMap R' (tsze R' M) = inlHom R' M

Full source

theorem algebraMap_eq_inlHom : algebraMap R' (tsze R' M) = inlHom R' M :=
  rfl

Algebra Map Equals Canonical Inclusion in Trivial Square-Zero Extension

Informal description

The algebra map from a commutative semiring $R'$ to its trivial square-zero extension $R' \oplus M$ is equal to the canonical inclusion homomorphism $\text{inlHom}_{R' M}$.

TrivSqZeroExt.algebraMap_eq_inl' theorem

(s : S) : algebraMap S (tsze R M) s = inl (algebraMap S R s)

Full source

theorem algebraMap_eq_inl' (s : S) : algebraMap S (tsze R M) s = inl (algebraMap S R s) :=
  rfl

Algebra Map Equals Canonical Inclusion in Trivial Square-Zero Extension

Informal description

For any semiring $S$ and any $s \in S$, the algebra map from $S$ to the trivial square-zero extension $R \oplus M$ evaluated at $s$ is equal to the canonical inclusion of the algebra map from $S$ to $R$ evaluated at $s$, i.e., \[ \text{algebraMap}_S(R \oplus M)(s) = \text{inl}(\text{algebraMap}_S R(s)). \]

TrivSqZeroExt.fstHom definition

: tsze R M →ₐ[S] R

Full source

/-- The canonical `S`-algebra projection `TrivSqZeroExt R M → R`. -/
@[simps]
def fstHom : tszetsze R M →ₐ[S] R where
  toFun := fst
  map_one' := fst_one
  map_mul' := fst_mul
  map_zero' := fst_zero (M := M)
  map_add' := fst_add
  commutes' _r := fst_inl M _

First projection algebra homomorphism of trivial square-zero extension

Informal description

The canonical $S$-algebra homomorphism from the trivial square-zero extension $\text{TrivSqZeroExt}\, R\, M$ to $R$, which projects an element $(r, m)$ to its first component $r$.

TrivSqZeroExt.inlAlgHom definition

: R →ₐ[S] tsze R M

Full source

/-- The canonical `S`-algebra inclusion `R → TrivSqZeroExt R M`. -/
@[simps]
def inlAlgHom : R →ₐ[S] tsze R M where
  toFun := inl
  map_one' := inl_one _
  map_mul' := inl_mul _
  map_zero' := inl_zero (M := M)
  map_add' := inl_add _
  commutes' _r := (algebraMap_eq_inl' _ _ _ _).symm

Canonical algebra inclusion into trivial square-zero extension

Informal description

The canonical $S$-algebra homomorphism from $R$ to the trivial square-zero extension $\text{TrivSqZeroExt}\, R\, M$, which maps an element $r \in R$ to $(r, 0) \in R \oplus M$. This homomorphism preserves the multiplicative and additive structures, as well as the algebra structure with respect to $S$.

TrivSqZeroExt.algHom_ext theorem

{A} [Semiring A] [Algebra R' A] ⦃f g : tsze R' M →ₐ[R'] A⦄ (h : ∀ m, f (inr m) = g (inr m)) : f = g

Full source

theorem algHom_ext {A} [Semiring A] [Algebra R' A] ⦃f g : tszetsze R' M →ₐ[R'] A⦄
    (h : ∀ m, f (inr m) = g (inr m)) : f = g :=
  AlgHom.toLinearMap_injective <|
    linearMap_ext (fun _r => (f.commutes _).trans (g.commutes _).symm) h

Extensionality of Algebra Homomorphisms on Trivial Square-Zero Extension via Module Component Equality

Informal description

Let $R'$ be a commutative semiring and $M$ be an $R'$-module with symmetric scalar multiplication. For any $R'$-algebra $A$ and any two $R'$-algebra homomorphisms $f, g \colon R' \oplus M \to A$, if $f$ and $g$ agree on the canonical inclusion of $M$ (i.e., $f(0, m) = g(0, m)$ for all $m \in M$), then $f = g$.

TrivSqZeroExt.algHom_ext' theorem

 {A} [Semiring A] [Algebra S A] ⦃f g : tsze R M →ₐ[S] A⦄ (hinl : f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M))
  (hinr : f.toLinearMap.comp (inrHom R M |>.restrictScalars S) = g.toLinearMap.comp (inrHom R M |>.restrictScalars S)) :
  f = g

Full source

@[ext]
theorem algHom_ext' {A} [Semiring A] [Algebra S A] ⦃f g : tszetsze R M →ₐ[S] A⦄
    (hinl : f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M))
    (hinr : f.toLinearMap.comp (inrHom R M |>.restrictScalars S) =
      g.toLinearMap.comp (inrHom R M |>.restrictScalars S)) : f = g :=
  AlgHom.toLinearMap_injective <|
    linearMap_ext (AlgHom.congr_fun hinl) (LinearMap.congr_fun hinr)

Extensionality of Algebra Homomorphisms on Trivial Square-Zero Extension via Componentwise Agreement

Informal description

Let $S$ be a semiring, $R$ a semiring, and $M$ an $(R, R)$-bimodule. For any $S$-algebra $A$ and any two $S$-algebra homomorphisms $f, g \colon R \oplus M \to A$, if $f$ and $g$ agree on the canonical inclusion of $R$ (i.e., $f \circ \iota_R = g \circ \iota_R$ where $\iota_R \colon R \to R \oplus M$ is the inclusion) and their underlying linear maps agree on the canonical inclusion of $M$ (i.e., $f|_M = g|_M$), then $f = g$.

TrivSqZeroExt.lift definition

 (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
  (hgf : ∀ r x, g (x <• r) = g x * f r) : tsze R M →ₐ[S] A

Full source

/--
Assemble an algebra morphism `TrivSqZeroExt R M →ₐ[S] A` from separate morphisms on `R` and `M`.

Namely, we require that for an algebra morphism `f : R →ₐ[S] A` and a linear map `g : M →ₗ[S] A`,
we have:

* `g x * g y = 0`: the elements of `M` continue to square to zero.
* `g (r •> x) = f r * g x` and `g (x <• r) = g x * f r`: scalar multiplication on the left and
  right is sent to left- and right- multiplication by the image under `f`.

See `TrivSqZeroExt.liftEquiv` for this as an equiv; namely that any such algebra morphism can be
factored in this way.

When `R` is commutative, this can be invoked with `f = Algebra.ofId R A`, which satisfies `hfg` and
`hgf`. This version is captured as an equiv by `TrivSqZeroExt.liftEquivOfComm`. -/
def lift (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r) : tszetsze R M →ₐ[S] A :=
  AlgHom.ofLinearMap
    ((f.comp <| fstHom S R M).toLinearMap + g ∘ₗ (sndHom R M |>.restrictScalars S))
    (show f 1 + g (0 : M) = 1 by rw [map_zero, map_one, add_zero])
    (TrivSqZeroExt.ind fun r₁ m₁ =>
      TrivSqZeroExt.ind fun r₂ m₂ => by
        dsimp
        simp only [add_zero, zero_add, add_mul, mul_add, smul_mul_smul_comm, hg, smul_zero,
          op_smul_eq_smul]
        rw [← map_mul, LinearMap.map_add, add_comm (g _), add_assoc, hfg, hgf])

Universal property of trivial square-zero extension

Informal description

Given an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x) \cdot g(y) = 0$ for all $x, y \in M$ (elements of $M$ square to zero), 2. $g(r \cdot x) = f(r) \cdot g(x)$ for all $r \in R, x \in M$ (left action compatibility), 3. $g(x \cdot r) = g(x) \cdot f(r)$ for all $r \in R, x \in M$ (right action compatibility), there exists a unique $S$-algebra homomorphism $\mathrm{TrivSqZeroExt}(R, M) \to A$ extending $f$ and $g$. This homomorphism is given by $(r, m) \mapsto f(r) + g(m)$.

TrivSqZeroExt.lift_def theorem

 (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r • x) = f r * g x)
  (hgf : ∀ r x, g (op r • x) = g x * f r) (x : tsze R M) : lift f g hg hfg hgf x = f x.fst + g x.snd

Full source

theorem lift_def (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r • x) = f r * g x)
    (hgf : ∀ r x, g (op r • x) = g x * f r) (x : tsze R M) :
    lift f g hg hfg hgf x = f x.fst + g x.snd :=
  rfl

Definition of the lift homomorphism for trivial square-zero extensions

Informal description

Given an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x) \cdot g(y) = 0$ for all $x, y \in M$, 2. $g(r \cdot x) = f(r) \cdot g(x)$ for all $r \in R$, $x \in M$, 3. $g(x \cdot r) = g(x) \cdot f(r)$ for all $r \in R$, $x \in M$, the lift homomorphism $\mathrm{lift}(f, g)$ applied to any element $(r, m) \in R \oplus M$ is given by $f(r) + g(m)$.

TrivSqZeroExt.lift_apply_inl theorem

 (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
  (hgf : ∀ r x, g (x <• r) = g x * f r) (r : R) : lift f g hg hfg hgf (inl r) = f r

Full source

@[simp]
theorem lift_apply_inl (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r)
    (r : R) :
    lift f g hg hfg hgf (inl r) = f r :=
  show f r + g 0 = f r by rw [map_zero, add_zero]

Lift of canonical inclusion in trivial square-zero extension equals algebra homomorphism

Informal description

Let $R$ be a semiring, $M$ an $(R, R)$-bimodule, and $S$ another semiring. Given an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x) \cdot g(y) = 0$ for all $x, y \in M$, 2. $g(r \cdot x) = f(r) \cdot g(x)$ for all $r \in R, x \in M$, 3. $g(x \cdot r) = g(x) \cdot f(r)$ for all $r \in R, x \in M$, then the lift homomorphism $\mathrm{lift}(f, g)$ applied to the canonical inclusion $\mathrm{inl}(r) = (r, 0) \in R \oplus M$ equals $f(r)$. That is, $\mathrm{lift}(f, g)((r, 0)) = f(r)$.

TrivSqZeroExt.lift_apply_inr theorem

 (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
  (hgf : ∀ r x, g (x <• r) = g x * f r) (m : M) : lift f g hg hfg hgf (inr m) = g m

Full source

@[simp]
theorem lift_apply_inr (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r)
    (m : M) :
    lift f g hg hfg hgf (inr m) = g m :=
  show f 0 + g m = g m by rw [map_zero, zero_add]

Evaluation of Lift Homomorphism on Module Elements in Trivial Square-Zero Extension

Informal description

Given an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x)g(y) = 0$ for all $x, y \in M$, 2. $g(r \cdot x) = f(r)g(x)$ for all $r \in R, x \in M$ (left action compatibility), 3. $g(x \cdot r) = g(x)f(r)$ for all $r \in R, x \in M$ (right action compatibility), then for any $m \in M$, the lift homomorphism $\mathrm{lift}(f, g)$ applied to the canonical inclusion $\mathrm{inr}(m) \in \mathrm{TrivSqZeroExt}(R, M)$ equals $g(m)$.

TrivSqZeroExt.lift_comp_inlHom theorem

 (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
  (hgf : ∀ r x, g (x <• r) = g x * f r) : (lift f g hg hfg hgf).comp (inlAlgHom S R M) = f

Full source

@[simp]
theorem lift_comp_inlHom (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r) :
    (lift f g hg hfg hgf).comp (inlAlgHom S R M) = f :=
  AlgHom.ext <| lift_apply_inl f g hg hfg hgf

Composition of Lift with Canonical Inclusion Equals Algebra Homomorphism

Informal description

Let $R$ be a semiring, $M$ an $(R, R)$-bimodule, and $S$ another semiring. Given an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x) \cdot g(y) = 0$ for all $x, y \in M$, 2. $g(r \cdot x) = f(r) \cdot g(x)$ for all $r \in R, x \in M$, 3. $g(x \cdot r) = g(x) \cdot f(r)$ for all $r \in R, x \in M$, then the composition of the lift homomorphism $\mathrm{lift}(f, g) \colon \mathrm{TrivSqZeroExt}(R, M) \to A$ with the canonical inclusion $\mathrm{inlAlgHom} \colon R \to \mathrm{TrivSqZeroExt}(R, M)$ equals $f$. That is, $\mathrm{lift}(f, g) \circ \mathrm{inlAlgHom} = f$.

TrivSqZeroExt.lift_comp_inrHom theorem

 (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
  (hgf : ∀ r x, g (x <• r) = g x * f r) : (lift f g hg hfg hgf).toLinearMap.comp (inrHom R M |>.restrictScalars S) = g

Full source

@[simp]
theorem lift_comp_inrHom (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r) :
    (lift f g hg hfg hgf).toLinearMap.comp (inrHom R M |>.restrictScalars S) = g :=
  LinearMap.ext <| lift_apply_inr f g hg hfg hgf

Compatibility of Lift Homomorphism with Canonical Inclusion in Trivial Square-Zero Extension

Informal description

Given an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x)g(y) = 0$ for all $x, y \in M$, 2. $g(r \cdot x) = f(r)g(x)$ for all $r \in R, x \in M$, 3. $g(x \cdot r) = g(x)f(r)$ for all $r \in R, x \in M$, the composition of the linear map associated to the lift homomorphism $\mathrm{lift}(f, g)$ with the canonical inclusion $\mathrm{inrHom} \colon M \to \mathrm{TrivSqZeroExt}(R, M)$ (restricted to $S$-scalars) equals $g$.

TrivSqZeroExt.lift_inlAlgHom_inrHom theorem

 :
  lift (inlAlgHom _ _ _) (inrHom R M |>.restrictScalars S) (inr_mul_inr R) (fun _ _ => (inl_mul_inr _ _).symm)
      (fun _ _ => (inr_mul_inl _ _).symm) =
    AlgHom.id S (tsze R M)

Full source

/-- When applied to `inr` and `inl` themselves, `lift` is the identity. -/
@[simp]
theorem lift_inlAlgHom_inrHom :
    lift (inlAlgHom _ _ _) (inrHom R M |>.restrictScalars S)
      (inr_mul_inr R) (fun _ _ => (inl_mul_inr _ _).symm) (fun _ _ => (inr_mul_inl _ _).symm) =
    AlgHom.id S (tsze R M) :=
  algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)

Identity Property of Lift Applied to Canonical Inclusions in Trivial Square-Zero Extension

Informal description

The algebra homomorphism obtained by lifting the canonical algebra inclusion $\operatorname{inlAlgHom} \colon R \to R \oplus M$ and the canonical linear inclusion $\operatorname{inrHom} \colon M \to R \oplus M$ (restricted to $S$-scalars) is equal to the identity algebra homomorphism on $R \oplus M$. More precisely, given: 1. The square-zero condition $\operatorname{inr}(m_1) \cdot \operatorname{inr}(m_2) = 0$ for all $m_1, m_2 \in M$, 2. The left action compatibility $\operatorname{inl}(r) \cdot \operatorname{inr}(m) = \operatorname{inr}(r \cdot m)$ for all $r \in R, m \in M$, 3. The right action compatibility $\operatorname{inr}(m) \cdot \operatorname{inl}(r) = \operatorname{inr}(m \cdot r)$ for all $r \in R, m \in M$, the lift homomorphism $\operatorname{lift}(\operatorname{inlAlgHom}, \operatorname{inrHom})$ equals the identity homomorphism on $R \oplus M$.

TrivSqZeroExt.liftEquiv definition

 :
  { fg : (R →ₐ[S] A) × (M →ₗ[S] A) //
      (∀ x y, fg.2 x * fg.2 y = 0) ∧
        (∀ r x, fg.2 (r •> x) = fg.1 r * fg.2 x) ∧ (∀ r x, fg.2 (x <• r) = fg.2 x * fg.1 r) } ≃
    (tsze R M →ₐ[S] A)

Full source

/-- A universal property of the trivial square-zero extension, providing a unique
`TrivSqZeroExt R M →ₐ[R] A` for every pair of maps `f : R →ₐ[S] A` and `g : M →ₗ[S] A`,
where the range of `g` has no non-zero products, and scaling the input to `g` on the left or right
amounts to a corresponding multiplication by `f` in the output.

This isomorphism is named to match the very similar `Complex.lift`. -/
@[simps! apply symm_apply_coe]
def liftEquiv :
    {fg : (R →ₐ[S] A) × (M →ₗ[S] A) //
      (∀ x y, fg.2 x * fg.2 y = 0) ∧
      (∀ r x, fg.2 (r •> x) = fg.1 r * fg.2 x) ∧
      (∀ r x, fg.2 (x <• r) = fg.2 x * fg.1 r)}{fg : (R →ₐ[S] A) × (M →ₗ[S] A) //
      (∀ x y, fg.2 x * fg.2 y = 0) ∧
      (∀ r x, fg.2 (r •> x) = fg.1 r * fg.2 x) ∧
      (∀ r x, fg.2 (x <• r) = fg.2 x * fg.1 r)} ≃ (tsze R M →ₐ[S] A) where
  toFun fg := lift fg.val.1 fg.val.2 fg.prop.1 fg.prop.2.1 fg.prop.2.2
  invFun F :=
    ⟨(F.comp (inlAlgHom _ _ _), F.toLinearMap ∘ₗ (inrHom _ _ |>.restrictScalars _)),
      (fun _x _y =>
        (map_mul F _ _).symm.trans <| (F.congr_arg <| inr_mul_inr _ _ _).trans (map_zero F)),
      (fun _r _x => (F.congr_arg (inl_mul_inr _ _).symm).trans (map_mul F _ _)),
      (fun _r _x => (F.congr_arg (inr_mul_inl _ _).symm).trans (map_mul F _ _))⟩
  left_inv _f := Subtype.ext <| Prod.ext (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
  right_inv _F := algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)

Universal property of trivial square-zero extension as an equivalence

Informal description

The equivalence between pairs $(f, g)$ consisting of an $S$-algebra homomorphism $f \colon R \to A$ and an $S$-linear map $g \colon M \to A$ satisfying: 1. $g(x) \cdot g(y) = 0$ for all $x, y \in M$, 2. $g(r \cdot x) = f(r) \cdot g(x)$ for all $r \in R, x \in M$, 3. $g(x \cdot r) = g(x) \cdot f(r)$ for all $r \in R, x \in M$, and $S$-algebra homomorphisms $\mathrm{TrivSqZeroExt}(R, M) \to A$. The equivalence maps $(f, g)$ to the unique algebra homomorphism extending $f$ and $g$, and conversely extracts $(f, g)$ from any algebra homomorphism by precomposition with the canonical inclusions.

TrivSqZeroExt.liftEquivOfComm definition

: { f : M →ₗ[R'] A // ∀ x y, f x * f y = 0 } ≃ (tsze R' M →ₐ[R'] A)

Full source

/-- A simplified version of `TrivSqZeroExt.liftEquiv` for the commutative case. -/
@[simps! apply symm_apply_coe]
def liftEquivOfComm :
    { f : M →ₗ[R'] A // ∀ x y, f x * f y = 0 }{ f : M →ₗ[R'] A // ∀ x y, f x * f y = 0 } ≃ (tsze R' M →ₐ[R'] A) := by
  refine Equiv.trans ?_ liftEquiv
  exact {
    toFun := fun f => ⟨(Algebra.ofId _ _, f.val), f.prop,
      fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply],
      fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply, Algebra.commutes]⟩
    invFun := fun fg => ⟨fg.val.2, fg.prop.1⟩
    left_inv := fun f => rfl
    right_inv := fun fg => Subtype.ext <|
      Prod.ext (AlgHom.toLinearMap_injective <| LinearMap.ext_ring <| by simp)
      rfl }

Universal property of trivial square-zero extension (commutative case)

Informal description

The equivalence between linear maps $f \colon M \to A$ satisfying $f(x) \cdot f(y) = 0$ for all $x, y \in M$ and $R'$-algebra homomorphisms $\mathrm{TrivSqZeroExt}(R', M) \to A$. This is a simplified version of the universal property for the commutative case, where the algebra homomorphism on $R'$ is fixed to be the canonical inclusion.

TrivSqZeroExt.map definition

(f : M →ₗ[R'] N) : TrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N

Full source

/-- Functoriality of `TrivSqZeroExt` when the ring is commutative: a linear map
`f : M →ₗ[R'] N` induces a morphism of `R'`-algebras from `TrivSqZeroExt R' M` to
`TrivSqZeroExt R' N`.

Note that we cannot neatly state the non-commutative case, as we do not have morphisms of bimodules.
-/
def map (f : M →ₗ[R'] N) : TrivSqZeroExtTrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N :=
  liftEquivOfComm ⟨inrHom R' N ∘ₗ f, fun _ _ => inr_mul_inr _ _ _⟩

Induced algebra homomorphism on trivial square-zero extensions via linear map

Informal description

Given a commutative semiring $R'$ and $R'$-modules $M$ and $N$, any $R'$-linear map $f \colon M \to N$ induces an $R'$-algebra homomorphism $\mathrm{TrivSqZeroExt}(R', M) \to \mathrm{TrivSqZeroExt}(R', N)$ that maps $(r, m)$ to $(r, f(m))$.

TrivSqZeroExt.map_inl theorem

(f : M →ₗ[R'] N) (r : R') : map f (inl r) = inl r

Full source

@[simp]
theorem map_inl (f : M →ₗ[R'] N) (r : R') : map f (inl r) = inl r := by
  rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]

Preservation of Canonical Inclusion under Induced Algebra Homomorphism on Trivial Square-Zero Extensions

Informal description

Let $R'$ be a commutative semiring, and let $M$ and $N$ be $R'$-modules. For any $R'$-linear map $f \colon M \to N$ and any element $r \in R'$, the induced algebra homomorphism $\mathrm{map}(f)$ on the trivial square-zero extensions satisfies $\mathrm{map}(f)((r, 0)) = (r, 0)$.

TrivSqZeroExt.map_inr theorem

(f : M →ₗ[R'] N) (x : M) : map f (inr x) = inr (f x)

Full source

@[simp]
theorem map_inr (f : M →ₗ[R'] N) (x : M) : map f (inr x) = inr (f x) := by
  rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]

Induced homomorphism preserves module elements in trivial square-zero extension

Informal description

Let $R'$ be a commutative semiring, and let $M$ and $N$ be $R'$-modules. For any $R'$-linear map $f \colon M \to N$ and any element $x \in M$, the induced algebra homomorphism $\mathrm{map}(f)$ on the trivial square-zero extensions satisfies $\mathrm{map}(f)(0, x) = (0, f(x))$.

TrivSqZeroExt.fst_map theorem

(f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : fst (map f x) = fst x

Full source

@[simp]
theorem fst_map (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : fst (map f x) = fst x := by
  simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

First Projection Preserved Under Induced Algebra Homomorphism on Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R'$, $R'$-modules $M$ and $N$, and $R'$-linear map $f \colon M \to N$, the first projection of the image of any element $x \in R' \oplus M$ under the induced algebra homomorphism $\mathrm{map}(f)$ equals the first projection of $x$, i.e., $\pi_1(\mathrm{map}(f)(x)) = \pi_1(x)$.

TrivSqZeroExt.snd_map theorem

(f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : snd (map f x) = f (snd x)

Full source

@[simp]
theorem snd_map (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : snd (map f x) = f (snd x) := by
  simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Projection of Induced Algebra Homomorphism on Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R'$ and $R'$-modules $M$ and $N$, given an $R'$-linear map $f \colon M \to N$ and an element $x \in R' \oplus M$, the projection of the image of $x$ under the induced algebra homomorphism $\mathrm{map}\,f$ onto $N$ equals $f$ applied to the projection of $x$ onto $M$. In other words, if $x = (r, m)$, then $\mathrm{snd}(\mathrm{map}\,f\,x) = f(m)$.

TrivSqZeroExt.map_comp_inlAlgHom theorem

(f : M →ₗ[R'] N) : (map f).comp (inlAlgHom R' R' M) = inlAlgHom R' R' N

Full source

@[simp]
theorem map_comp_inlAlgHom (f : M →ₗ[R'] N) :
    (map f).comp (inlAlgHom R' R' M) = inlAlgHom R' R' N :=
  AlgHom.ext <| map_inl _

Compatibility of Induced Algebra Homomorphism with Canonical Inclusion in Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R'$ and $R'$-modules $M$ and $N$, given an $R'$-linear map $f \colon M \to N$, the composition of the induced algebra homomorphism $\mathrm{map}(f) \colon R' \oplus M \to R' \oplus N$ with the canonical inclusion $\mathrm{inlAlgHom}_{R'} \colon R' \to R' \oplus M$ equals the canonical inclusion $\mathrm{inlAlgHom}_{R'} \colon R' \to R' \oplus N$. In other words, the following diagram commutes: \[ \begin{CD} R' @>{\mathrm{inlAlgHom}_{R'}}>> R' \oplus M \\ @V{\mathrm{id}}VV @VV{\mathrm{map}(f)}V \\ R' @>{\mathrm{inlAlgHom}_{R'}}>> R' \oplus N \end{CD} \]

TrivSqZeroExt.map_comp_inrHom theorem

(f : M →ₗ[R'] N) : (map f).toLinearMap ∘ₗ inrHom R' M = inrHom R' N ∘ₗ f

Full source

@[simp]
theorem map_comp_inrHom (f : M →ₗ[R'] N) :
    (map f).toLinearMap ∘ₗ inrHom R' M = inrHominrHom R' N ∘ₗ f :=
  LinearMap.ext <| map_inr _

Commutativity of Induced Homomorphism with Canonical Inclusion in Trivial Square-Zero Extension

Informal description

Given a commutative semiring $R'$ and $R'$-linear maps $f \colon M \to N$, the composition of the linear map induced by the algebra homomorphism $\mathrm{map}(f)$ with the canonical inclusion $\mathrm{inrHom}_{R' M}$ equals the composition of the canonical inclusion $\mathrm{inrHom}_{R' N}$ with $f$. In other words, the following diagram commutes: \[ \begin{tikzcd} M \arrow[r, "f"] \arrow[d, "\mathrm{inrHom}_{R' M}"'] & N \arrow[d, "\mathrm{inrHom}_{R' N}"] \\ \mathrm{TrivSqZeroExt}(R', M) \arrow[r, "\mathrm{map}(f)"] & \mathrm{TrivSqZeroExt}(R', N) \end{tikzcd} \]

TrivSqZeroExt.fstHom_comp_map theorem

(f : M →ₗ[R'] N) : (fstHom R' R' N).comp (map f) = fstHom R' R' M

Full source

@[simp]
theorem fstHom_comp_map (f : M →ₗ[R'] N) :
    (fstHom R' R' N).comp (map f) = fstHom R' R' M :=
  AlgHom.ext <| fst_map _

Compatibility of First Projection with Induced Algebra Homomorphism on Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R'$ and $R'$-modules $M$ and $N$, given an $R'$-linear map $f \colon M \to N$, the composition of the first projection algebra homomorphism $\mathrm{fstHom}_{R' N}$ with the induced algebra homomorphism $\mathrm{map}(f)$ equals the first projection algebra homomorphism $\mathrm{fstHom}_{R' M}$.

TrivSqZeroExt.sndHom_comp_map theorem

(f : M →ₗ[R'] N) : sndHom R' N ∘ₗ (map f).toLinearMap = f ∘ₗ sndHom R' M

Full source

@[simp]
theorem sndHom_comp_map (f : M →ₗ[R'] N) :
    sndHomsndHom R' N ∘ₗ (map f).toLinearMap = f ∘ₗ sndHom R' M :=
  LinearMap.ext <| snd_map _

Commutativity of Projection with Induced Algebra Homomorphism on Trivial Square-Zero Extensions

Informal description

For any commutative semiring $R'$ and $R'$-modules $M$ and $N$, given an $R'$-linear map $f \colon M \to N$, the composition of the projection to $N$ (via `sndHom`) with the algebra homomorphism `map f` equals the composition of $f$ with the projection to $M$ (via `sndHom`). In other words, the following diagram commutes: $$ \begin{CD} \mathrm{TrivSqZeroExt}(R', M) @>{\mathrm{map}\,f}>> \mathrm{TrivSqZeroExt}(R', N) \\ @V{\mathrm{sndHom}_{R', M}}VV @VV{\mathrm{sndHom}_{R', N}}V \\ M @>{f}>> N \end{CD} $$

TrivSqZeroExt.map_id theorem

: map (LinearMap.id : M →ₗ[R'] M) = AlgHom.id R' _

Full source

@[simp]
theorem map_id : map (LinearMap.id : M →ₗ[R'] M) = AlgHom.id R' _ := by
  apply algHom_ext
  simp only [map_inr, LinearMap.id_coe, id_eq, AlgHom.coe_id, forall_const]

Identity Linear Map Induces Identity Algebra Homomorphism on Trivial Square-Zero Extension

Informal description

The algebra homomorphism induced by the identity linear map $\mathrm{id} \colon M \to M$ on the trivial square-zero extension $\mathrm{TrivSqZeroExt}(R', M)$ is equal to the identity algebra homomorphism on $\mathrm{TrivSqZeroExt}(R', M)$.

TrivSqZeroExt.map_comp_map theorem

(f : M →ₗ[R'] N) (g : N →ₗ[R'] P) : map (g.comp f) = (map g).comp (map f)

Full source

theorem map_comp_map (f : M →ₗ[R'] N) (g : N →ₗ[R'] P) :
    map (g.comp f) = (map g).comp (map f) := by
  apply algHom_ext
  simp only [map_inr, LinearMap.coe_comp, Function.comp_apply, AlgHom.coe_comp, forall_const]

Composition of Induced Algebra Homomorphisms on Trivial Square-Zero Extensions

Informal description

Let $R'$ be a commutative semiring and let $M$, $N$, $P$ be $R'$-modules. For any $R'$-linear maps $f \colon M \to N$ and $g \colon N \to P$, the induced algebra homomorphism on trivial square-zero extensions satisfies $\mathrm{map}(g \circ f) = \mathrm{map}(g) \circ \mathrm{map}(f)$.

Main definitions