Documentation

Mathlib.Algebra.TrivSqZeroExt

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 #

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.

Equations
Instances For
    def TrivSqZeroExt.inl {R : Type u} {M : Type v} [Zero M] (r : R) :

    The canonical inclusion R → TrivSqZeroExt R M.

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

      The canonical inclusion M → TrivSqZeroExt R M.

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

        The canonical projection TrivSqZeroExt R M → R.

        Equations
        • x.fst = x.1
        Instances For
          def TrivSqZeroExt.snd {R : Type u} {M : Type v} (x : TrivSqZeroExt R M) :
          M

          The canonical projection TrivSqZeroExt R M → M.

          Equations
          • x.snd = x.2
          Instances For
            @[simp]
            theorem TrivSqZeroExt.fst_mk {R : Type u} {M : Type v} (r : R) (m : M) :
            @[simp]
            theorem TrivSqZeroExt.snd_mk {R : Type u} {M : Type v} (r : 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
            @[simp]
            theorem TrivSqZeroExt.fst_inl {R : Type u} (M : Type v) [Zero M] (r : R) :
            @[simp]
            theorem TrivSqZeroExt.snd_inl {R : Type u} (M : Type v) [Zero M] (r : R) :
            @[simp]
            theorem TrivSqZeroExt.fst_comp_inl {R : Type u} (M : Type v) [Zero M] :
            TrivSqZeroExt.fst TrivSqZeroExt.inl = id
            @[simp]
            theorem TrivSqZeroExt.snd_comp_inl {R : Type u} (M : Type v) [Zero M] :
            TrivSqZeroExt.snd TrivSqZeroExt.inl = 0
            @[simp]
            theorem TrivSqZeroExt.fst_inr (R : Type u) {M : Type v} [Zero R] (m : M) :
            @[simp]
            theorem TrivSqZeroExt.snd_inr (R : Type u) {M : Type v} [Zero R] (m : M) :
            @[simp]
            theorem TrivSqZeroExt.fst_comp_inr (R : Type u) {M : Type v} [Zero R] :
            TrivSqZeroExt.fst TrivSqZeroExt.inr = 0
            @[simp]
            theorem TrivSqZeroExt.snd_comp_inr (R : Type u) {M : Type v} [Zero R] :
            TrivSqZeroExt.snd TrivSqZeroExt.inr = id
            theorem TrivSqZeroExt.fst_surjective {R : Type u} {M : Type v} [Nonempty M] :
            Function.Surjective TrivSqZeroExt.fst
            theorem TrivSqZeroExt.snd_surjective {R : Type u} {M : Type v} [Nonempty R] :
            Function.Surjective TrivSqZeroExt.snd
            theorem TrivSqZeroExt.inl_injective {R : Type u} {M : Type v} [Zero M] :
            Function.Injective TrivSqZeroExt.inl
            theorem TrivSqZeroExt.inr_injective {R : Type u} {M : Type v} [Zero R] :
            Function.Injective TrivSqZeroExt.inr

            Structures inherited from Prod #

            Additive operators and scalar multiplication operate elementwise.

            Equations
            • TrivSqZeroExt.inhabited = instInhabitedProd
            instance TrivSqZeroExt.zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
            Equations
            • TrivSqZeroExt.zero = Prod.instZero
            instance TrivSqZeroExt.add {R : Type u} {M : Type v} [Add R] [Add M] :
            Equations
            • TrivSqZeroExt.add = Prod.instAdd
            instance TrivSqZeroExt.sub {R : Type u} {M : Type v} [Sub R] [Sub M] :
            Equations
            • TrivSqZeroExt.sub = Prod.instSub
            instance TrivSqZeroExt.neg {R : Type u} {M : Type v} [Neg R] [Neg M] :
            Equations
            • TrivSqZeroExt.neg = Prod.instNeg
            Equations
            • TrivSqZeroExt.addSemigroup = Prod.instAddSemigroup
            Equations
            • TrivSqZeroExt.addZeroClass = Prod.instAddZeroClass
            Equations
            • TrivSqZeroExt.addMonoid = Prod.instAddMonoid
            instance TrivSqZeroExt.addGroup {R : Type u} {M : Type v} [AddGroup R] [AddGroup M] :
            Equations
            • TrivSqZeroExt.addGroup = Prod.instAddGroup
            Equations
            • TrivSqZeroExt.addCommSemigroup = Prod.instAddCommSemigroup
            Equations
            • TrivSqZeroExt.addCommMonoid = Prod.instAddCommMonoid
            Equations
            • TrivSqZeroExt.addCommGroup = Prod.instAddCommGroup
            instance TrivSqZeroExt.smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] :
            Equations
            • TrivSqZeroExt.smul = Prod.smul
            theorem 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] :
            theorem 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] :
            instance TrivSqZeroExt.mulAction {S : Type u_2} {R : Type u} {M : Type v} [Monoid S] [MulAction S R] [MulAction S M] :
            Equations
            • TrivSqZeroExt.mulAction = Prod.mulAction
            Equations
            • TrivSqZeroExt.distribMulAction = Prod.distribMulAction
            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] :
            Equations
            • TrivSqZeroExt.module = Prod.instModule

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

            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] :
            @[simp]
            theorem TrivSqZeroExt.snd_zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
            @[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) :
            (∑ is, f i).fst = is, (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) :
            (∑ is, f i).snd = is, (f i).snd
            @[simp]
            theorem TrivSqZeroExt.inl_zero {R : Type u} (M : Type v) [Zero R] [Zero M] :
            @[simp]
            theorem TrivSqZeroExt.inl_add {R : Type u} (M : Type v) [Add R] [AddZeroClass M] (r₁ r₂ : R) :
            @[simp]
            @[simp]
            theorem TrivSqZeroExt.inl_sub {R : Type u} (M : Type v) [Sub R] [SubNegZeroMonoid M] (r₁ r₂ : 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) :
            theorem TrivSqZeroExt.inl_sum {R : Type u} (M : Type v) {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιR) :
            TrivSqZeroExt.inl (∑ is, f i) = is, TrivSqZeroExt.inl (f i)
            @[simp]
            theorem TrivSqZeroExt.inr_zero (R : Type u) {M : Type v} [Zero R] [Zero M] :
            @[simp]
            theorem TrivSqZeroExt.inr_add (R : Type u) {M : Type v} [AddZeroClass R] [AddZeroClass M] (m₁ m₂ : M) :
            @[simp]
            @[simp]
            theorem TrivSqZeroExt.inr_sub (R : Type u) {M : Type v} [SubNegZeroMonoid R] [Sub M] (m₁ m₂ : M) :
            @[simp]
            theorem TrivSqZeroExt.inr_smul {S : Type u_2} (R : Type u) {M : Type v} [Zero R] [Zero S] [SMulWithZero S R] [SMul S M] (r : S) (m : M) :
            theorem TrivSqZeroExt.inr_sum (R : Type u) {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιM) :
            TrivSqZeroExt.inr (∑ is, f i) = is, TrivSqZeroExt.inr (f i)
            theorem TrivSqZeroExt.ind {R : Type u_3} {M : Type u_4} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R MProp} (inl_add_inr : ∀ (r : R) (m : M), P (TrivSqZeroExt.inl r + TrivSqZeroExt.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 (TrivSqZeroExt.inl r) = g (TrivSqZeroExt.inl r)) (hr : ∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.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.

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

            Equations
            Instances For
              @[simp]

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

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

                Multiplicative structure #

                instance TrivSqZeroExt.one {R : Type u} {M : Type v} [One R] [Zero M] :
                Equations
                • TrivSqZeroExt.one = { one := (1, 0) }
                instance TrivSqZeroExt.mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] :
                Equations
                @[simp]
                theorem TrivSqZeroExt.fst_one {R : Type u} {M : Type v} [One R] [Zero M] :
                @[simp]
                theorem TrivSqZeroExt.snd_one {R : Type u} {M : Type v} [One R] [Zero M] :
                @[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] :
                @[simp]
                theorem TrivSqZeroExt.inl_mul {R : Type u} (M : Type v) [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ 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) :
                theorem TrivSqZeroExt.inl_mul_eq_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (r : R) (x : TrivSqZeroExt R M) :
                Equations
                Equations
                @[simp]
                theorem TrivSqZeroExt.fst_natCast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                (↑n).fst = n
                @[deprecated TrivSqZeroExt.fst_natCast]
                theorem TrivSqZeroExt.fst_nat_cast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                (↑n).fst = n

                Alias of TrivSqZeroExt.fst_natCast.

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

                Alias of TrivSqZeroExt.snd_natCast.

                @[simp]
                theorem TrivSqZeroExt.inl_natCast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                @[deprecated TrivSqZeroExt.inl_natCast]
                theorem TrivSqZeroExt.inl_nat_cast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :

                Alias of TrivSqZeroExt.inl_natCast.

                Equations
                • TrivSqZeroExt.addGroupWithOne = AddGroupWithOne.mk SubNegMonoid.zsmul
                @[simp]
                theorem TrivSqZeroExt.fst_intCast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                (↑z).fst = z
                @[deprecated TrivSqZeroExt.fst_intCast]
                theorem TrivSqZeroExt.fst_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                (↑z).fst = z

                Alias of TrivSqZeroExt.fst_intCast.

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

                Alias of TrivSqZeroExt.snd_intCast.

                @[simp]
                theorem TrivSqZeroExt.inl_intCast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                @[deprecated TrivSqZeroExt.inl_intCast]
                theorem TrivSqZeroExt.inl_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :

                Alias of TrivSqZeroExt.inl_intCast.

                Equations
                Equations

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

                Equations
                • One or more equations did not get rendered due to their size.
                @[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]
                Equations
                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 TrivSqZeroExt.fst l).prod
                Equations
                • TrivSqZeroExt.semiring = Semiring.mk Monoid.npow
                theorem TrivSqZeroExt.snd_list_prod {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module 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.1.succ (List.map TrivSqZeroExt.fst l)).prod (List.take x.1 (List.map TrivSqZeroExt.fst l)).prod x.2.snd) l.enum).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] :
                Equations
                • TrivSqZeroExt.ring = Ring.mk SubNegMonoid.zsmul
                Equations
                Equations
                Equations

                The canonical inclusion of rings R → TrivSqZeroExt R M.

                Equations
                • TrivSqZeroExt.inlHom R M = { toFun := TrivSqZeroExt.inl, map_one' := , map_mul' := , map_zero' := , map_add' := }
                Instances For
                  @[simp]
                  instance TrivSqZeroExt.instInv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul 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.

                  Equations
                  @[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]

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

                  Equations
                  • x.invertibleFstOfInvertible = { invOf := (x).fst, invOf_mul_self := , mul_invOf_self := }
                  Instances For
                    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) :
                    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) :
                    @[reducible, inline]

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

                    Equations
                    Instances For
                      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)

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]

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

                        @[simp]
                        @[simp]
                        @[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
                        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.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) :
                        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] :
                        Equations
                        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)) = TrivSqZeroExt.inl

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

                        Equations
                        • TrivSqZeroExt.fstHom S R M = { toFun := TrivSqZeroExt.fst, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                        Instances For
                          @[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) :
                          (TrivSqZeroExt.fstHom S R M) x = x.fst

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

                          Equations
                          • TrivSqZeroExt.inlAlgHom S R M = { toFun := TrivSqZeroExt.inl, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                          Instances For
                            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 (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.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 (TrivSqZeroExt.inlAlgHom S R M) = g.comp (TrivSqZeroExt.inlAlgHom S R M)) (hinr : f.toLinearMap ∘ₗ S (TrivSqZeroExt.inrHom R M) = g.toLinearMap ∘ₗ S (TrivSqZeroExt.inrHom R M)) :
                            f = g
                            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) :

                            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.

                            Equations
                            Instances For
                              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) :
                              (TrivSqZeroExt.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) :
                              (TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.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) :
                              (TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.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) :
                              (TrivSqZeroExt.lift f g hg hfg hgf).comp (TrivSqZeroExt.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) :
                              (TrivSqZeroExt.lift f g hg hfg hgf).toLinearMap ∘ₗ S (TrivSqZeroExt.inrHom R M) = g
                              @[simp]

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

                              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.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[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) :
                                (TrivSqZeroExt.liftEquiv.symm F) = (F.comp (TrivSqZeroExt.inlAlgHom S R M), F.toLinearMap ∘ₗ S (TrivSqZeroExt.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 }) :
                                TrivSqZeroExt.liftEquiv fg = TrivSqZeroExt.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.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[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 }) :
                                  TrivSqZeroExt.liftEquivOfComm a✝ = TrivSqZeroExt.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) :
                                  (TrivSqZeroExt.liftEquivOfComm.symm a✝) = a✝.toLinearMap ∘ₗ R' (TrivSqZeroExt.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) :

                                  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.

                                  Equations
                                  Instances For
                                    @[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') :
                                    @[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) :
                                    @[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) :
                                    ((TrivSqZeroExt.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) :
                                    ((TrivSqZeroExt.map f) x).snd = f x.snd
                                    @[simp]
                                    @[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) :
                                    (TrivSqZeroExt.map f).toLinearMap ∘ₗ TrivSqZeroExt.inrHom R' M = TrivSqZeroExt.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) :
                                    @[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) :
                                    TrivSqZeroExt.sndHom R' N ∘ₗ (TrivSqZeroExt.map f).toLinearMap = f ∘ₗ TrivSqZeroExt.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] :
                                    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) :