Trivial Square-Zero Extension

Given a ring R together with an (R, R)-bimodule M, 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₂ + m₁ r₂.

It is a square-zero extension because M^2 = 0.

Note that expressing this requires bimodules; we write these in general for a not-necessarily-commutative R as:

variable {R M : Type*} [Semiring R] [AddCommMonoid M]
variable [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]

If we instead work with a commutative R' acting symmetrically on M, we write

variable {R' M : Type*} [CommSemiring R'] [AddCommMonoid M]
variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M]

noting that in this context IsCentralScalar R' M implies SMulCommClass R' R'ᵐᵒᵖ M.

Many of the later results in this file are only stated for the commutative R' for simplicity.

Main definitions

• TrivSqZeroExt.inl, TrivSqZeroExt.inr: the canonical inclusions into TrivSqZeroExt R M.
• TrivSqZeroExt.fst, TrivSqZeroExt.snd: the canonical projections from TrivSqZeroExt R M.
• triv_sq_zero_ext.algebra: the associated R-algebra structure.
• TrivSqZeroExt.lift: the universal property of the trivial square-zero extension; algebra morphisms TrivSqZeroExt R M →ₐ[S] A are uniquely defined by an algebra morphism f : R →ₐ[S] A on R and a linear map g : M →ₗ[S] A on M such that:
  • 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: left and right actions are preserved by g.
• TrivSqZeroExt.lift: the universal property of the trivial square-zero extension; algebra morphisms TrivSqZeroExt R M →ₐ[R] A are uniquely defined by linear maps M →ₗ[R] A for which the product of any two elements in the range is zero.

def TrivSqZeroExt (R : Type u) (M : Type v) : Type (max u v)

"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.inl {R : Type u} {M : Type v} [Zero M] (r : R) : TrivSqZeroExt R M

The canonical inclusion R → TrivSqZeroExt R M.

def TrivSqZeroExt.inr {R : Type u} {M : Type v} [Zero R] (m : M) : TrivSqZeroExt R M

The canonical inclusion M → TrivSqZeroExt R M.

def TrivSqZeroExt.fst {R : Type u} {M : Type v} (x : TrivSqZeroExt R M) : R

The canonical projection TrivSqZeroExt R M → R.

def TrivSqZeroExt.snd {R : Type u} {M : Type v} (x : TrivSqZeroExt R M) : M

The canonical projection TrivSqZeroExt R M → M.

@[simp]

theorem TrivSqZeroExt.fst_mk {R : Type u} {M : Type v} (r : R) (m : M) : fst (r, m) = r

@[simp]

theorem TrivSqZeroExt.snd_mk {R : Type u} {M : Type v} (r : R) (m : M) : snd (r, m) = m

theorem TrivSqZeroExt.ext {R : Type u} {M : Type v} {x y : TrivSqZeroExt R M} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y

theorem TrivSqZeroExt.ext_iff {R : Type u} {M : Type v} {x y : TrivSqZeroExt R M} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

@[simp]

theorem TrivSqZeroExt.fst_inl {R : Type u} (M : Type v) [Zero M] (r : R) : (inl r).fst = r

@[simp]

theorem TrivSqZeroExt.snd_inl {R : Type u} (M : Type v) [Zero M] (r : R) : (inl r).snd = 0

@[simp]

theorem TrivSqZeroExt.fst_comp_inl {R : Type u} (M : Type v) [Zero M] : fst ∘ inl = id

@[simp]

theorem TrivSqZeroExt.snd_comp_inl {R : Type u} (M : Type v) [Zero M] : snd ∘ inl = 0

@[simp]

theorem TrivSqZeroExt.fst_inr (R : Type u) {M : Type v} [Zero R] (m : M) : (inr m).fst = 0

@[simp]

theorem TrivSqZeroExt.snd_inr (R : Type u) {M : Type v} [Zero R] (m : M) : (inr m).snd = m

@[simp]

theorem TrivSqZeroExt.fst_comp_inr (R : Type u) {M : Type v} [Zero R] : fst ∘ inr = 0

@[simp]

theorem TrivSqZeroExt.snd_comp_inr (R : Type u) {M : Type v} [Zero R] : snd ∘ inr = id

theorem TrivSqZeroExt.fst_surjective {R : Type u} {M : Type v} [Nonempty M] : Function.Surjective fst

theorem TrivSqZeroExt.snd_surjective {R : Type u} {M : Type v} [Nonempty R] : Function.Surjective snd

theorem TrivSqZeroExt.inl_injective {R : Type u} {M : Type v} [Zero M] : Function.Injective inl

theorem TrivSqZeroExt.inr_injective {R : Type u} {M : Type v} [Zero R] : Function.Injective inr

Structures inherited from Prod

Additive operators and scalar multiplication operate elementwise.

instance TrivSqZeroExt.inhabited {R : Type u} {M : Type v} [Inhabited R] [Inhabited M] : Inhabited (TrivSqZeroExt R M)

instance TrivSqZeroExt.zero {R : Type u} {M : Type v} [Zero R] [Zero M] : Zero (TrivSqZeroExt R M)

instance TrivSqZeroExt.add {R : Type u} {M : Type v} [Add R] [Add M] : Add (TrivSqZeroExt R M)

instance TrivSqZeroExt.sub {R : Type u} {M : Type v} [Sub R] [Sub M] : Sub (TrivSqZeroExt R M)

instance TrivSqZeroExt.neg {R : Type u} {M : Type v} [Neg R] [Neg M] : Neg (TrivSqZeroExt R M)

instance TrivSqZeroExt.addSemigroup {R : Type u} {M : Type v} [AddSemigroup R] [AddSemigroup M] : AddSemigroup (TrivSqZeroExt R M)

instance TrivSqZeroExt.addZeroClass {R : Type u} {M : Type v} [AddZeroClass R] [AddZeroClass M] : AddZeroClass (TrivSqZeroExt R M)

instance TrivSqZeroExt.addMonoid {R : Type u} {M : Type v} [AddMonoid R] [AddMonoid M] : AddMonoid (TrivSqZeroExt R M)

instance TrivSqZeroExt.addGroup {R : Type u} {M : Type v} [AddGroup R] [AddGroup M] : AddGroup (TrivSqZeroExt R M)

instance TrivSqZeroExt.addCommSemigroup {R : Type u} {M : Type v} [AddCommSemigroup R] [AddCommSemigroup M] : AddCommSemigroup (TrivSqZeroExt R M)

instance TrivSqZeroExt.addCommMonoid {R : Type u} {M : Type v} [AddCommMonoid R] [AddCommMonoid M] : AddCommMonoid (TrivSqZeroExt R M)

instance TrivSqZeroExt.addCommGroup {R : Type u} {M : Type v} [AddCommGroup R] [AddCommGroup M] : AddCommGroup (TrivSqZeroExt R M)

instance TrivSqZeroExt.smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] : SMul S (TrivSqZeroExt R M)

instance TrivSqZeroExt.isScalarTower {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [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 (TrivSqZeroExt R M)

instance TrivSqZeroExt.smulCommClass {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMulCommClass T S R] [SMulCommClass T S M] : SMulCommClass T S (TrivSqZeroExt R M)

instance TrivSqZeroExt.isCentralScalar {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsCentralScalar S R] [IsCentralScalar S M] : IsCentralScalar S (TrivSqZeroExt R M)

instance TrivSqZeroExt.mulAction {S : Type u_2} {R : Type u} {M : Type v} [Monoid S] [MulAction S R] [MulAction S M] : MulAction S (TrivSqZeroExt R M)

instance TrivSqZeroExt.distribMulAction {S : Type u_2} {R : Type u} {M : Type v} [Monoid S] [AddMonoid R] [AddMonoid M] [DistribMulAction S R] [DistribMulAction S M] : DistribMulAction S (TrivSqZeroExt R M)

instance TrivSqZeroExt.module {S : Type u_2} {R : Type u} {M : Type v} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [Module S R] [Module S M] : Module S (TrivSqZeroExt R M)

instance TrivSqZeroExt.instNontrivial_of_left {R : Type u_3} {M : Type u_4} [Nontrivial R] [Nonempty M] : Nontrivial (TrivSqZeroExt R M)

The trivial square-zero extension is nontrivial if it is over a nontrivial ring.

instance TrivSqZeroExt.instNontrivial_of_right {R : Type u_3} {M : Type u_4} [Nonempty R] [Nontrivial M] : Nontrivial (TrivSqZeroExt R M)

The trivial square-zero extension is nontrivial if it is over a nontrivial module.

@[simp]

theorem TrivSqZeroExt.fst_zero {R : Type u} {M : Type v} [Zero R] [Zero M] : fst 0 = 0

@[simp]

theorem TrivSqZeroExt.snd_zero {R : Type u} {M : Type v} [Zero R] [Zero M] : snd 0 = 0

@[simp]

theorem TrivSqZeroExt.fst_add {R : Type u} {M : Type v} [Add R] [Add M] (x₁ x₂ : TrivSqZeroExt R M) : (x₁ + x₂).fst = x₁.fst + x₂.fst

@[simp]

theorem TrivSqZeroExt.snd_add {R : Type u} {M : Type v} [Add R] [Add M] (x₁ x₂ : TrivSqZeroExt R M) : (x₁ + x₂).snd = x₁.snd + x₂.snd

@[simp]

theorem TrivSqZeroExt.fst_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : TrivSqZeroExt R M) : (-x).fst = -x.fst

@[simp]

theorem TrivSqZeroExt.snd_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : TrivSqZeroExt R M) : (-x).snd = -x.snd

@[simp]

theorem TrivSqZeroExt.fst_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ x₂ : TrivSqZeroExt R M) : (x₁ - x₂).fst = x₁.fst - x₂.fst

@[simp]

theorem TrivSqZeroExt.snd_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ x₂ : TrivSqZeroExt R M) : (x₁ - x₂).snd = x₁.snd - x₂.snd

@[simp]

theorem TrivSqZeroExt.fst_smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] (s : S) (x : TrivSqZeroExt R M) : (s • x).fst = s • x.fst

@[simp]

theorem TrivSqZeroExt.snd_smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] (s : S) (x : TrivSqZeroExt R M) : (s • x).snd = s • x.snd

theorem TrivSqZeroExt.fst_sum {R : Type u} {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → TrivSqZeroExt R M) : (∑ i ∈ s, f i).fst = ∑ i ∈ s, (f i).fst

theorem TrivSqZeroExt.snd_sum {R : Type u} {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → TrivSqZeroExt R M) : (∑ i ∈ s, f i).snd = ∑ i ∈ s, (f i).snd

@[simp]

theorem TrivSqZeroExt.inl_zero {R : Type u} (M : Type v) [Zero R] [Zero M] : inl 0 = 0

@[simp]

theorem TrivSqZeroExt.inl_add {R : Type u} (M : Type v) [Add R] [AddZeroClass M] (r₁ r₂ : R) : inl (r₁ + r₂) = inl r₁ + inl r₂

@[simp]

theorem TrivSqZeroExt.inl_neg {R : Type u} (M : Type v) [Neg R] [NegZeroClass M] (r : R) : inl (-r) = -inl r

@[simp]

theorem TrivSqZeroExt.inl_sub {R : Type u} (M : Type v) [Sub R] [SubNegZeroMonoid M] (r₁ r₂ : R) : inl (r₁ - r₂) = inl r₁ - inl r₂

@[simp]

theorem TrivSqZeroExt.inl_smul {S : Type u_2} {R : Type u} (M : Type v) [Monoid S] [AddMonoid M] [SMul S R] [DistribMulAction S M] (s : S) (r : R) : inl (s • r) = s • inl r

theorem TrivSqZeroExt.inl_sum {R : Type u} (M : Type v) {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → R) : inl (∑ i ∈ s, f i) = ∑ i ∈ s, inl (f i)

@[simp]

theorem TrivSqZeroExt.inr_zero (R : Type u) {M : Type v} [Zero R] [Zero M] : inr 0 = 0

@[simp]

theorem TrivSqZeroExt.inr_add (R : Type u) {M : Type v} [AddZeroClass R] [Add M] (m₁ m₂ : M) : inr (m₁ + m₂) = inr m₁ + inr m₂

@[simp]

theorem TrivSqZeroExt.inr_neg (R : Type u) {M : Type v} [NegZeroClass R] [Neg M] (m : M) : inr (-m) = -inr m

@[simp]

theorem TrivSqZeroExt.inr_sub (R : Type u) {M : Type v} [SubNegZeroMonoid R] [Sub M] (m₁ m₂ : M) : inr (m₁ - m₂) = inr m₁ - inr m₂

@[simp]

theorem TrivSqZeroExt.inr_smul {S : Type u_2} (R : Type u) {M : Type v} [Zero R] [SMulZeroClass S R] [SMul S M] (r : S) (m : M) : inr (r • m) = r • inr m

theorem TrivSqZeroExt.inr_sum (R : Type u) {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → M) : inr (∑ i ∈ s, f i) = ∑ i ∈ s, inr (f i)

theorem TrivSqZeroExt.inl_fst_add_inr_snd_eq {R : Type u} {M : Type v} [AddZeroClass R] [AddZeroClass M] (x : TrivSqZeroExt R M) : inl x.fst + inr x.snd = x

theorem TrivSqZeroExt.ind {R : Type u_3} {M : Type u_4} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R M → Prop} (inl_add_inr : ∀ (r : R) (m : M), P (inl r + inr m)) (x : TrivSqZeroExt R M) : P x

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.

theorem TrivSqZeroExt.linearMap_ext {S : Type u_2} {R : Type u} {M : Type v} {N : Type u_3} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [AddCommMonoid N] [Module S R] [Module S M] [Module S N] ⦃f g : TrivSqZeroExt R M →ₗ[S] N⦄ (hl : ∀ (r : R), f (inl r) = g (inl r)) (hr : ∀ (m : M), f (inr m) = g (inr m)) : f = g

This cannot be marked @[ext] as it ends up being used instead of LinearMap.prod_ext when working with R × M.

def TrivSqZeroExt.inrHom (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] TrivSqZeroExt R M

The canonical R-linear inclusion M → TrivSqZeroExt R M.

@[simp]

theorem TrivSqZeroExt.inrHom_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (m : M) : (inrHom R M) m = inr m

def TrivSqZeroExt.sndHom (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : TrivSqZeroExt R M →ₗ[R] M

The canonical R-linear projection TrivSqZeroExt R M → M.

@[simp]

theorem TrivSqZeroExt.sndHom_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (x : TrivSqZeroExt R M) : (sndHom R M) x = x.snd

Multiplicative structure

instance TrivSqZeroExt.one {R : Type u} {M : Type v} [One R] [Zero M] : One (TrivSqZeroExt R M)

instance TrivSqZeroExt.mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] : Mul (TrivSqZeroExt R M)

@[simp]

theorem TrivSqZeroExt.fst_one {R : Type u} {M : Type v} [One R] [Zero M] : fst 1 = 1

@[simp]

theorem TrivSqZeroExt.snd_one {R : Type u} {M : Type v} [One R] [Zero M] : snd 1 = 0

@[simp]

theorem TrivSqZeroExt.fst_mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : TrivSqZeroExt R M) : (x₁ * x₂).fst = x₁.fst * x₂.fst

@[simp]

theorem TrivSqZeroExt.snd_mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : TrivSqZeroExt R M) : (x₁ * x₂).snd = x₁.fst • x₂.snd + MulOpposite.op x₂.fst • x₁.snd

@[simp]

theorem TrivSqZeroExt.inl_one {R : Type u} (M : Type v) [One R] [Zero M] : inl 1 = 1

@[simp]

theorem TrivSqZeroExt.inl_mul {R : Type u} (M : Type v) [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R) : inl (r₁ * r₂) = inl r₁ * inl r₂

theorem TrivSqZeroExt.inl_mul_inl {R : Type u} (M : Type v) [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R) : inl r₁ * inl r₂ = inl (r₁ * r₂)

@[simp]

theorem TrivSqZeroExt.inr_mul_inr (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ m₂ : M) : inr m₁ * inr m₂ = 0

theorem TrivSqZeroExt.inl_mul_inr {R : Type u} {M : Type v} [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) : inl r * inr m = inr (r • m)

theorem TrivSqZeroExt.inr_mul_inl {R : Type u} {M : Type v} [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) : inr m * inl r = inr (MulOpposite.op r • m)

theorem TrivSqZeroExt.inl_mul_eq_smul {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (x : TrivSqZeroExt R M) : inl r * x = r • x

theorem TrivSqZeroExt.mul_inl_eq_op_smul {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (r : R) : x * inl r = MulOpposite.op r • x

instance TrivSqZeroExt.mulOneClass {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] : MulOneClass (TrivSqZeroExt R M)

instance TrivSqZeroExt.addMonoidWithOne {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] : AddMonoidWithOne (TrivSqZeroExt R M)

@[simp]

theorem TrivSqZeroExt.fst_natCast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (↑n).fst = ↑n

@[simp]

theorem TrivSqZeroExt.snd_natCast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : (↑n).snd = 0

@[simp]

theorem TrivSqZeroExt.inl_natCast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ℕ) : inl ↑n = ↑n

instance TrivSqZeroExt.addGroupWithOne {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] : AddGroupWithOne (TrivSqZeroExt R M)

@[simp]

theorem TrivSqZeroExt.fst_intCast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ℤ) : (↑z).fst = ↑z

@[simp]

theorem TrivSqZeroExt.snd_intCast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ℤ) : (↑z).snd = 0

@[simp]

theorem TrivSqZeroExt.inl_intCast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ℤ) : inl ↑z = ↑z

instance TrivSqZeroExt.nonAssocSemiring {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : NonAssocSemiring (TrivSqZeroExt R M)

instance TrivSqZeroExt.nonAssocRing {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] : NonAssocRing (TrivSqZeroExt R M)

instance TrivSqZeroExt.instPowNatOfDistribMulActionMulOpposite {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] : Pow (TrivSqZeroExt R M) ℕ

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$.

@[simp]

theorem TrivSqZeroExt.fst_pow {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ) : (x ^ n).fst = x.fst ^ n

theorem TrivSqZeroExt.snd_pow_eq_sum {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ) : (x ^ n).snd = (List.map (fun (i : ℕ) => MulOpposite.op (x.fst ^ i) • x.fst ^ (n.pred - i) • x.snd) (List.range n)).sum

theorem TrivSqZeroExt.snd_pow_of_smul_comm {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ) (h : MulOpposite.op x.fst • x.snd = x.fst • x.snd) : (x ^ n).snd = n • x.fst ^ n.pred • x.snd

theorem TrivSqZeroExt.snd_pow_of_smul_comm.aux {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (h : MulOpposite.op x.fst • x.snd = x.fst • x.snd) (n : ℕ) : MulOpposite.op (x.fst ^ n) • x.snd = x.fst ^ n • x.snd

theorem TrivSqZeroExt.snd_pow_of_smul_comm' {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ) (h : MulOpposite.op x.fst • x.snd = x.fst • x.snd) : (x ^ n).snd = n • MulOpposite.op (x.fst ^ n.pred) • x.snd

@[simp]

theorem TrivSqZeroExt.snd_pow {R : Type u} {M : Type v} [CommMonoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M] (x : TrivSqZeroExt R M) (n : ℕ) : (x ^ n).snd = n • x.fst ^ n.pred • x.snd

@[simp]

theorem TrivSqZeroExt.inl_pow {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (n : ℕ) : inl r ^ n = inl (r ^ n)

instance TrivSqZeroExt.monoid {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Monoid (TrivSqZeroExt R M)

theorem TrivSqZeroExt.fst_list_prod {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (l : List (TrivSqZeroExt R M)) : l.prod.fst = (List.map fst l).prod

instance TrivSqZeroExt.semiring {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Semiring (TrivSqZeroExt R M)

theorem TrivSqZeroExt.snd_list_prod {R : Type u} {M : Type v} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (l : List (TrivSqZeroExt R M)) : l.prod.snd = (List.map (fun (x : TrivSqZeroExt R M × ℕ) => MulOpposite.op (List.drop x.2.succ (List.map fst l)).prod • (List.take x.2 (List.map fst l)).prod • x.1.snd) l.zipIdx).sum

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$.

instance TrivSqZeroExt.ring {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : Ring (TrivSqZeroExt R M)

instance TrivSqZeroExt.commMonoid {R : Type u} {M : Type v} [CommMonoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M] : CommMonoid (TrivSqZeroExt R M)

instance TrivSqZeroExt.commSemiring {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : CommSemiring (TrivSqZeroExt R M)

instance TrivSqZeroExt.commRing {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : CommRing (TrivSqZeroExt R M)

def TrivSqZeroExt.inlHom (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : R →+* TrivSqZeroExt R M

The canonical inclusion of rings R → TrivSqZeroExt R M.

@[simp]

theorem TrivSqZeroExt.inlHom_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (r : R) : (inlHom R M) r = inl r

instance TrivSqZeroExt.instInv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] : Inv (TrivSqZeroExt R M)

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.

@[simp]

theorem TrivSqZeroExt.fst_inv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] (x : TrivSqZeroExt R M) : x⁻¹.fst = x.fst⁻¹

@[simp]

theorem TrivSqZeroExt.snd_inv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] (x : TrivSqZeroExt R M) : x⁻¹.snd = -(MulOpposite.op x.fst⁻¹ • x.fst⁻¹ • x.snd)

This section is heavily inspired by analogous results about matrices.

@[reducible, inline]

abbrev TrivSqZeroExt.invertibleFstOfInvertible {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] (x : TrivSqZeroExt R M) [Invertible x] : Invertible x.fst

x.fst : R is invertible when x : tzre R M is.

theorem TrivSqZeroExt.fst_invOf {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] (x : TrivSqZeroExt R M) [Invertible x] [Invertible x.fst] : (⅟x).fst = ⅟x.fst

theorem TrivSqZeroExt.mul_left_eq_one {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] (r : R) (x : TrivSqZeroExt R M) (h : r * x.fst = 1) : (inl r + inr (-(MulOpposite.op r • r • x.snd))) * x = 1

theorem TrivSqZeroExt.mul_right_eq_one {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] (x : TrivSqZeroExt R M) (r : R) (h : x.fst * r = 1) : x * (inl r + inr (-(r • MulOpposite.op r • x.snd))) = 1

@[reducible, inline]

abbrev TrivSqZeroExt.invertibleOfInvertibleFst {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) [Invertible x.fst] : Invertible x

x : tzre R M is invertible when x.fst : R is.

theorem TrivSqZeroExt.snd_invOf {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) [Invertible x] [Invertible x.fst] : (⅟x).snd = -(MulOpposite.op ⅟x.fst • ⅟x.fst • x.snd)

def TrivSqZeroExt.invertibleEquivInvertibleFst {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) : Invertible x ≃ Invertible x.fst

Together TrivSqZeroExt.detInvertibleOfInvertible and TrivSqZeroExt.invertibleOfDetInvertible form an equivalence, although both sides of the equiv are subsingleton anyway.

@[simp]

theorem TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (x✝ : Invertible x) : ⅟x.fst = (⅟x).fst

@[simp]

theorem TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (x✝ : Invertible x.fst) : ⅟x = (⅟x.fst, -(MulOpposite.op ⅟x.fst • ⅟x.fst • x.snd))

theorem TrivSqZeroExt.isUnit_iff_isUnit_fst {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M} : IsUnit x ↔ IsUnit x.fst

When lowered to a prop, Matrix.invertibleEquivInvertibleFst forms an iff.

@[simp]

theorem TrivSqZeroExt.isUnit_inl_iff {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] {r : R} : IsUnit (inl r) ↔ IsUnit r

@[simp]

theorem TrivSqZeroExt.isUnit_inr_iff {R : Type u} {M : Type v} [AddCommGroup M] [Semiring R] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] {m : M} : IsUnit (inr m) ↔ Subsingleton R

theorem TrivSqZeroExt.inv_inl {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] (r : R) : (inl r)⁻¹ = inl r⁻¹

@[simp]

theorem TrivSqZeroExt.inv_inr {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] (m : M) : (inr m)⁻¹ = 0

@[simp]

theorem TrivSqZeroExt.inv_zero {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] : 0⁻¹ = 0

@[simp]

theorem TrivSqZeroExt.inv_one {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] : 1⁻¹ = 1

theorem TrivSqZeroExt.inv_mul_cancel {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] {x : TrivSqZeroExt R M} (hx : x.fst ≠ 0) : x⁻¹ * x = 1

@[simp]

theorem TrivSqZeroExt.invOf_eq_inv {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) [Invertible x] : ⅟x = x⁻¹

theorem TrivSqZeroExt.mul_inv_cancel {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M} (hx : x.fst ≠ 0) : x * x⁻¹ = 1

theorem TrivSqZeroExt.mul_inv_rev {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] (a b : TrivSqZeroExt R M) : (a * b)⁻¹ = b⁻¹ * a⁻¹

theorem TrivSqZeroExt.inv_inv {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M} (hx : x.fst ≠ 0) : x⁻¹⁻¹ = x

@[simp]

theorem TrivSqZeroExt.isUnit_inv_iff {R : Type u} {M : Type v} [DivisionSemiring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M} : IsUnit x⁻¹ ↔ IsUnit x

theorem TrivSqZeroExt.inv_neg {R : Type u} {M : Type v} [DivisionRing R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] {x : TrivSqZeroExt R M} : (-x)⁻¹ = -x⁻¹

instance TrivSqZeroExt.algebra' (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] : Algebra S (TrivSqZeroExt R M)

instance TrivSqZeroExt.instAlgebra (R' : Type u) (M : Type v) [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] : Algebra R' (TrivSqZeroExt R' M)

theorem TrivSqZeroExt.algebraMap_eq_inl (R' : Type u) (M : Type v) [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] : ⇑(algebraMap R' (TrivSqZeroExt R' M)) = inl

theorem TrivSqZeroExt.algebraMap_eq_inlHom (R' : Type u) (M : Type v) [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] : algebraMap R' (TrivSqZeroExt R' M) = inlHom R' M

theorem TrivSqZeroExt.algebraMap_eq_inl' (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] (s : S) : (algebraMap S (TrivSqZeroExt R M)) s = inl ((algebraMap S R) s)

def TrivSqZeroExt.fstHom (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] : TrivSqZeroExt R M →ₐ[S] R

The canonical S-algebra projection TrivSqZeroExt R M → R.

@[simp]

theorem TrivSqZeroExt.fstHom_apply (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) : (fstHom S R M) x = x.fst

def TrivSqZeroExt.inlAlgHom (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] : R →ₐ[S] TrivSqZeroExt R M

The canonical S-algebra inclusion R → TrivSqZeroExt R M.

@[simp]

theorem TrivSqZeroExt.inlAlgHom_apply (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] (r : R) : (inlAlgHom S R M) r = inl r

theorem TrivSqZeroExt.algHom_ext {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] ⦃f g : TrivSqZeroExt R' M →ₐ[R'] A⦄ (h : ∀ (m : M), f (inr m) = g (inr m)) : f = g

theorem TrivSqZeroExt.algHom_ext' {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] ⦃f g : TrivSqZeroExt R M →ₐ[S] A⦄ (hinl : f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M)) (hinr : f.toLinearMap ∘ₗ ↑S (inrHom R M) = g.toLinearMap ∘ₗ ↑S (inrHom R M)) : f = g

theorem TrivSqZeroExt.algHom_ext'_iff {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] {f g : TrivSqZeroExt R M →ₐ[S] A} : f = g ↔ f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M) ∧ f.toLinearMap ∘ₗ ↑S (inrHom R M) = g.toLinearMap ∘ₗ ↑S (inrHom R M)

def TrivSqZeroExt.lift {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) : TrivSqZeroExt R M →ₐ[S] A

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.

theorem TrivSqZeroExt.lift_def {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) (x : TrivSqZeroExt R M) : (lift f g hg hfg hgf) x = f x.fst + g x.snd

@[simp]

theorem TrivSqZeroExt.lift_apply_inl {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) (r : R) : (lift f g hg hfg hgf) (inl r) = f r

@[simp]

theorem TrivSqZeroExt.lift_apply_inr {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) (m : M) : (lift f g hg hfg hgf) (inr m) = g m

@[simp]

theorem TrivSqZeroExt.lift_comp_inlHom {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) : (lift f g hg hfg hgf).comp (inlAlgHom S R M) = f

@[simp]

theorem TrivSqZeroExt.lift_comp_inrHom {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) : (lift f g hg hfg hgf).toLinearMap ∘ₗ ↑S (inrHom R M) = g

@[simp]

theorem TrivSqZeroExt.lift_inlAlgHom_inrHom {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] : lift (inlAlgHom S R M) (↑S (inrHom R M)) ⋯ ⋯ ⋯ = AlgHom.id S (TrivSqZeroExt R M)

When applied to inr and inl themselves, lift is the identity.

@[simp]

theorem TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] : (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr) = ⊤

@[simp]

theorem TrivSqZeroExt.range_liftAux {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) : (lift f g hg hfg hgf).range = f.range ⊔ Algebra.adjoin S (Set.range ⇑g)

def TrivSqZeroExt.liftEquiv {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] : { fg : (R →ₐ[S] A) × (M →ₗ[S] A) // (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧ (∀ (r : R) (x : M), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r : R) (x : M), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r } ≃ (TrivSqZeroExt R M →ₐ[S] A)

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.

@[simp]

theorem TrivSqZeroExt.liftEquiv_symm_apply_coe {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (F : TrivSqZeroExt R M →ₐ[S] A) : ↑(liftEquiv.symm F) = (F.comp (inlAlgHom S R M), F.toLinearMap ∘ₗ ↑S (inrHom R M))

@[simp]

theorem TrivSqZeroExt.liftEquiv_apply {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (fg : { fg : (R →ₐ[S] A) × (M →ₗ[S] A) // (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧ (∀ (r : R) (x : M), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r : R) (x : M), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }) : liftEquiv fg = lift (↑fg).1 (↑fg).2 ⋯ ⋯ ⋯

def TrivSqZeroExt.liftEquivOfComm {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] : { f : M →ₗ[R'] A // ∀ (x y : M), f x * f y = 0 } ≃ (TrivSqZeroExt R' M →ₐ[R'] A)

A simplified version of TrivSqZeroExt.liftEquiv for the commutative case.

@[simp]

theorem TrivSqZeroExt.liftEquivOfComm_apply {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] (a✝ : { f : M →ₗ[R'] A // ∀ (x y : M), f x * f y = 0 }) : liftEquivOfComm a✝ = lift (Algebra.ofId R' A) ↑a✝ ⋯ ⋯ ⋯

@[simp]

theorem TrivSqZeroExt.liftEquivOfComm_symm_apply_coe {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] (a✝ : TrivSqZeroExt R' M →ₐ[R'] A) : ↑(liftEquivOfComm.symm a✝) = a✝.toLinearMap ∘ₗ ↑R' (inrHom R' M)

def TrivSqZeroExt.map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) : TrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N

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.

@[simp]

theorem TrivSqZeroExt.map_inl {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (r : R') : (map f) (inl r) = inl r

@[simp]

theorem TrivSqZeroExt.map_inr {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (x : M) : (map f) (inr x) = inr (f x)

@[simp]

theorem TrivSqZeroExt.fst_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : ((map f) x).fst = x.fst

@[simp]

theorem TrivSqZeroExt.snd_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : ((map f) x).snd = f x.snd

@[simp]

theorem TrivSqZeroExt.map_comp_inlAlgHom {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) : (map f).comp (inlAlgHom R' R' M) = inlAlgHom R' R' N

@[simp]

theorem TrivSqZeroExt.map_comp_inrHom {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) : (map f).toLinearMap ∘ₗ inrHom R' M = inrHom R' N ∘ₗ f

@[simp]

theorem TrivSqZeroExt.fstHom_comp_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) : (fstHom R' R' N).comp (map f) = fstHom R' R' M

@[simp]

theorem TrivSqZeroExt.sndHom_comp_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) : sndHom R' N ∘ₗ (map f).toLinearMap = f ∘ₗ sndHom R' M

@[simp]

theorem TrivSqZeroExt.map_id {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] : map LinearMap.id = AlgHom.id R' (TrivSqZeroExt R' M)

theorem TrivSqZeroExt.map_comp_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] [AddCommMonoid P] [Module R' P] [Module R'ᵐᵒᵖ P] [IsCentralScalar R' P] (f : M →ₗ[R'] N) (g : N →ₗ[R'] P) : map (g ∘ₗ f) = (map g).comp (map f)