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:

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

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

variables {R' M : Type*} [CommSemiring R'] [AddCommMonoid M]
variables [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.

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

    The canonical inclusion R → TrivSqZeroExt R M.

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

      The canonical inclusion M → TrivSqZeroExt R M.

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

        The canonical projection TrivSqZeroExt R M → R.

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

          The canonical projection TrivSqZeroExt R M → M.

          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) :
            @[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.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.

            instance TrivSqZeroExt.zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
            instance TrivSqZeroExt.add {R : Type u} {M : Type v} [Add R] [Add M] :
            instance TrivSqZeroExt.sub {R : Type u} {M : Type v} [Sub R] [Sub M] :
            instance TrivSqZeroExt.neg {R : Type u} {M : Type v} [Neg R] [Neg M] :
            instance TrivSqZeroExt.smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S 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] :
            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] :
            instance TrivSqZeroExt.mulAction {S : Type u_2} {R : Type u} {M : Type v} [Monoid S] [MulAction S R] [MulAction S 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] :
            @[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₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_add {R : Type u} {M : Type v} [Add R] [Add M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.fst_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.fst_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[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) :
            @[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) :
            theorem TrivSqZeroExt.fst_sum {R : Type u} {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιTrivSqZeroExt R M) :
            TrivSqZeroExt.fst (Finset.sum s fun i => f i) = Finset.sum s fun i => TrivSqZeroExt.fst (f i)
            theorem TrivSqZeroExt.snd_sum {R : Type u} {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιTrivSqZeroExt R M) :
            TrivSqZeroExt.snd (Finset.sum s fun i => f i) = Finset.sum s fun i => TrivSqZeroExt.snd (f i)
            @[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₂ : R) :
            @[simp]
            @[simp]
            theorem TrivSqZeroExt.inl_sub {R : Type u} (M : Type v) [Sub R] [SubNegZeroMonoid M] (r₁ : 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 (Finset.sum s fun i => f i) = Finset.sum s fun i => 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₂ : M) :
            @[simp]
            @[simp]
            theorem TrivSqZeroExt.inr_sub (R : Type u) {M : Type v} [SubNegZeroMonoid R] [Sub M] (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 (Finset.sum s fun i => f i) = Finset.sum s fun i => TrivSqZeroExt.inr (f i)
            theorem TrivSqZeroExt.ind {R : Type u_3} {M : Type u_4} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R MProp} (h : (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.

            This can be used as induction x using TrivSqZeroExt.ind.

            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 : TrivSqZeroExt R M →ₗ[S] N ⦃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.

            @[simp]
            theorem TrivSqZeroExt.inrHom_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (m : M) :

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

            Instances For
              @[simp]

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

              Instances For

                Multiplicative structure #

                instance TrivSqZeroExt.one {R : Type u} {M : Type v} [One R] [Zero M] :
                instance TrivSqZeroExt.mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] :
                @[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₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
                @[simp]
                theorem TrivSqZeroExt.snd_mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
                @[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₂ : 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₂ : 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₂ : M) :
                @[simp]
                theorem TrivSqZeroExt.fst_nat_cast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                @[simp]
                @[simp]
                theorem TrivSqZeroExt.inl_nat_cast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                @[simp]
                theorem TrivSqZeroExt.fst_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                @[simp]
                theorem TrivSqZeroExt.snd_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                @[simp]
                theorem TrivSqZeroExt.inl_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :

                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.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)) :
                TrivSqZeroExt.snd (List.prod l) = List.sum (List.map (fun x => List.prod (List.take x.fst (List.map TrivSqZeroExt.fst l)) MulOpposite.op (List.prod (List.drop (Nat.succ x.fst) (List.map TrivSqZeroExt.fst l))) TrivSqZeroExt.snd x.snd) (List.enum l))

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

                @[simp]

                The canonical inclusion of rings R → TrivSqZeroExt R M.

                Instances For
                  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 R-algebra projection TrivSqZeroExt R M → R.

                  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 : TrivSqZeroExt R' M →ₐ[R'] A ⦃g : TrivSqZeroExt R' M →ₐ[R'] A (h : ∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) :
                    f = g
                    def TrivSqZeroExt.liftAux {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) (hf : ∀ (x y : M), f x * f y = 0) :

                    There is an alg_hom from the trivial square zero extension to any R-algebra with a submodule whose products are all zero.

                    See TrivSqZeroExt.lift for this as an equiv.

                    Instances For
                      @[simp]
                      theorem TrivSqZeroExt.liftAux_apply_inr {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) (hf : ∀ (x y : M), f x * f y = 0) (m : M) :
                      @[simp]
                      theorem TrivSqZeroExt.liftAux_comp_inrHom {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) (hf : ∀ (x y : M), f x * f y = 0) :
                      @[simp]
                      @[simp]
                      theorem TrivSqZeroExt.lift_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] (F : TrivSqZeroExt R' M →ₐ[R'] A) :
                      ↑(TrivSqZeroExt.lift.symm F) = LinearMap.comp (AlgHom.toLinearMap F) (TrivSqZeroExt.inrHom R' M)
                      @[simp]
                      theorem TrivSqZeroExt.lift_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] (f : { f // ∀ (x y : M), f x * f y = 0 }) :
                      TrivSqZeroExt.lift f = TrivSqZeroExt.liftAux f (_ : ∀ (x y : M), f x * f y = 0)
                      def TrivSqZeroExt.lift {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 // ∀ (x y : M), f x * f y = 0 } (TrivSqZeroExt R' M →ₐ[R'] A)

                      A universal property of the trivial square-zero extension, providing a unique TrivSqZeroExt R M →ₐ[R] A for every linear map M →ₗ[R] A whose range has no non-zero products.

                      This isomorphism is named to match the very similar Complex.lift.

                      Instances For