Documentation

Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Exactness properties of the difference map on tensor products #

For an R-algebra S, we collect some properties of the R-linear map S →ₗ[R] S ⊗[R] S given by s ↦ s ⊗ₜ 1 - 1 ⊗ₜ s.

Main definitions #

Main results #

source
def Algebra.TensorProduct.includeLeftSubRight (R : Type u_1) [CommSemiring R] (S : Type u_2) [Ring S] [Algebra R S] :
S →ₗ[R] TensorProduct R S S

The R-linear map S →ₗ[R] S ⊗[R] S sending s : S to s ⊗ₜ 1 - 1 ⊗ₜ s.

Equations
Instances For
    source
    @[simp]
    theorem Algebra.TensorProduct.includeLeftSubRight_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] (s : S) :
    (includeLeftSubRight R S) s = s ⊗ₜ[R] 1 - 1 ⊗ₜ[R] s
    source
    theorem Algebra.TensorProduct.includeLeftSubRight_zero_of_mem_range {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] {s : S} (hs : s ∈ Set.range ⇑(algebraMap R S)) :
    (includeLeftSubRight R S) s = 0

    includeLeftSubRight R S vanishes in the range of algebraMap R S.

    source
    theorem Algebra.TensorProduct.includeLeftSubRight_algebraMap_zero {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] (r : R) :
    (includeLeftSubRight R S) ((algebraMap R S) r) = 0

    includeLeftSubRight R S vanishes at algebraMap R S r.

    source
    theorem Algebra.TensorProduct.distribBaseChange_comp_includeLeftSubRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] :
    ↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ LinearMap.lTensor T (includeLeftSubRight R S) = ↑R (includeLeftSubRight T (TensorProduct R T S))

    includeLeftSubRight is compatible with distribBaseChange and lTensor.

    source
    @[simp]
    theorem Algebra.TensorProduct.distribBaseChange_includeLeftSubRight_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (x : TensorProduct R T S) :
    (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S) ((LinearMap.lTensor T (includeLeftSubRight R S)) x) = (includeLeftSubRight T (TensorProduct R T S)) x
    source
    def Algebra.IsEffective (R : Type u_1) [CommSemiring R] (S : Type u_2) [Ring S] [Algebra R S] :
    Prop

    For an R-algebra S, this asserts that the maps algebraMap : R → S and includeLeftSubRight R S : S → S ⊗[R] S form an exact pair. When R and S are commutative rings, this is true if and only if the inclusion im (algebraMap : R → S) → S is an effective monomorphism in the category of commutative rings.

    Equations
    Instances For
      source
      theorem Algebra.IsEffective.eqLocus_includeLeft_includeRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] (h : IsEffective R S) :
      ↑(TensorProduct.includeLeftRingHom.eqLocus TensorProduct.includeRight.toRingHom) = Set.range ⇑(algebraMap R S)

      If IsEffective R S is true, then the equalizer of s ↦ s ⊗ₜ 1 : S →+* S ⊗[R] S and s ↦ 1 ⊗ₜ s : S →+* S ⊗[R] S is the image of algebraMap R S : R →+* S.

      source
      theorem Algebra.IsEffective.of_section {R : Type u_1} [CommSemiring R] {S : Type u_2} [Ring S] [Algebra R S] (g : S →ₐ[R] R) :
      IsEffective R S

      IsEffective is true for any R-algebra S having an R-algebra section of Algebra.ofId _ _ : R →ₐ[R] S.

      source
      theorem Algebra.IsEffective.of_isEffective_tensorProduct_of_faithfullyFlat (R : Type u_3) [CommRing R] (S : Type u_4) (T : Type u_5) [CommRing T] [Algebra R T] [Ring S] [Algebra R S] [Module.FaithfullyFlat R T] (h : IsEffective T (TensorProduct R T S)) :
      IsEffective R S

      IsEffective descends along faithfully flat algebras.

      source
      theorem Algebra.IsEffective.of_faithfullyFlat (R : Type u_3) [CommRing R] (S : Type u_4) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] :
      IsEffective R S

      IsEffective R S is true for any faithfully flat R-algebra S.

      source
      def Algebra.codRestrictEqLocusPushoutCocone (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] :
      R →+* ↑(CommRingCat.equalizerFork (CommRingCat.pushoutCocone R S S).inl (CommRingCat.pushoutCocone R S S).inr).pt

      The canonical ring map from R to the explicit equalizer of includeLeft : S ⟶ S ⊗[R] S and includeRight : S ⟶ S ⊗[R] S.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algebra.codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [FaithfulSMul R S] :
        Function.Injective ⇑(codRestrictEqLocusPushoutCocone R S)

        Injectivity of algebraMap R S implies injectivity of codRestrictEqLocusPushoutCocone.

        source
        theorem Algebra.codRestrictEqLocusPushoutCocone.surjective_of_isEffective (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (hf : IsEffective R S) :
        Function.Surjective ⇑(codRestrictEqLocusPushoutCocone R S)

        Algebra.IsEffective R S implies surjectivity of codRestrictEqLocusPushoutCocone.

        source
        theorem Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] :
        Function.Bijective ⇑(codRestrictEqLocusPushoutCocone R S)

        If S is a faithfully flat R-algebra, codRestrictEqLocusPushoutCocone is bijective.