Documentation

Mathlib.RingTheory.Kaehler.TensorProduct

Kaehler differential module under base change #

Main results #

@[reducible, inline]
noncomputable abbrev KaehlerDifferential.mulActionBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] :

(Implementation). A-action on S ⊗[R] Ω[A⁄R].

Equations
Instances For
    @[simp]
    theorem KaehlerDifferential.mulActionBaseChange_smul_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (a : A) (s : S) (x : Ω[AR]) :
    a s ⊗ₜ[R] x = s ⊗ₜ[R] (a x)
    theorem KaehlerDifferential.mulActionBaseChange_smul_zero (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (a : A) :
    a 0 = 0
    theorem KaehlerDifferential.mulActionBaseChange_smul_add (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] (a : A) (x : TensorProduct R S (Ω[AR])) (y : TensorProduct R S (Ω[AR])) :
    a (x + y) = a x + a y
    @[reducible, inline]
    noncomputable abbrev KaehlerDifferential.moduleBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] :

    (Implementation). A-module structure on S ⊗[R] Ω[A⁄R].

    Equations
    Instances For
      instance KaehlerDifferential.instIsScalarTowerTensorProduct (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] :
      Equations
      • =
      instance KaehlerDifferential.instSMulCommClassTensorProduct (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] :
      Equations
      • =
      Equations
      • =
      @[reducible]
      noncomputable def KaehlerDifferential.moduleBaseChange' (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] :

      (Implementation). B = S ⊗[R] A-module structure on S ⊗[R] Ω[A⁄R].

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        instance KaehlerDifferential.instIsScalarTowerTensorProduct_1 (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] :
        Equations
        • =
        instance KaehlerDifferential.instIsScalarTowerTensorProduct_2 (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] :
        Equations
        • =
        theorem KaehlerDifferential.map_liftBaseChange_smul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [h : Algebra.IsPushout R S A B] (b : B) (x : TensorProduct R S (Ω[AR])) :
        noncomputable def KaehlerDifferential.derivationTensorProduct (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [h : Algebra.IsPushout R S A B] :

        (Implementation). The S-derivation B = S ⊗[R] A to S ⊗[R] Ω[A⁄R] sending a ⊗ b to a ⊗ d b.

        Equations
        Instances For
          theorem KaehlerDifferential.derivationTensorProduct_algebraMap (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] (x : A) :
          theorem KaehlerDifferential.tensorKaehlerEquiv_left_inv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] :
          S (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (R (KaehlerDifferential.map R S A B)) = LinearMap.id
          @[simp]
          theorem KaehlerDifferential.tensorKaehlerEquiv_symm_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [h : Algebra.IsPushout R S A B] (a : Ω[BS]) :
          (KaehlerDifferential.tensorKaehlerEquiv R S A B).symm a = (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential a
          noncomputable def KaehlerDifferential.tensorKaehlerEquiv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [h : Algebra.IsPushout R S A B] :

          The canonical isomorphism (S ⊗[R] Ω[A⁄R]) ≃ₗ[S] Ω[B⁄S] for B = S ⊗[R] A.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem KaehlerDifferential.tensorKaehlerEquiv_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] (a : S) (b : Ω[AR]) :
            theorem KaehlerDifferential.isBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [h : Algebra.IsPushout R S A B] :

            If B is the tensor product of S and A over R, then Ω[B⁄S] is the base change of Ω[A⁄R] along R → S.

            instance KaehlerDifferential.isLocalizedModule (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] (p : Submonoid R) [IsLocalization p S] [IsLocalization (Algebra.algebraMapSubmonoid A p) B] :
            Equations
            • =
            instance KaehlerDifferential.isLocalizedModule_of_isLocalizedModule (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] (p : Submonoid R) [IsLocalization p S] [IsLocalizedModule p (IsScalarTower.toAlgHom R A B).toLinearMap] :
            Equations
            • =