Documentation

Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Cotangent and localization away #

Let R → S → T be algebras such that T is the localization of S away from one element, where S is generated over R by P : R[X] → S with kernel I and Q : S[Y] → T is the canonical S-presentation of T with kernel K. Denote by J the kernel of the composition R[X,Y] → T.

This file proves J/J² ≃ₗ[T] T ⊗[S] (I/I²) × K/K². For this we establish the exact sequence:

0 → T ⊗[S] (I/I²) → J/J² → K/K² → 0

and use that K/K² is free, so the sequence splits. The first part of the file shows the exactness on the left and the rest of the file deduces the exact sequence and the splitting from the Jacobi Zariski sequence.

Main results #

Algebra.Generators.liftBaseChange_injective: T ⊗[S] (I/I²) → J/J² is injective if T is the localization of S away from an element.
Algebra.Generators.cotangentCompLocalizationAwayEquiv: J/J² ≃ₗ[T] T ⊗[S] (I/I²) × K/K².

theorem Algebra.Generators.comp_localizationAway_ker {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) (f : P.Ring) (h : (algebraMap P.Ring S) f = g) :

((localizationAway T g).comp P).ker = Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔ Ideal.span {(MvPolynomial.rename Sum.inr) f * MvPolynomial.X (Sum.inl ()) - 1}

noncomputable def Algebra.Generators.compLocalizationAwayAlgHom {R : Type u_1} {S : Type u_2} (T : Type u_3) {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) :

((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))

If R[X] → S generates S, T is the localization of S away from g and f is a pre-image of g in R[X], this is the R-algebra map R[X,Y] →ₐ[R] (R[X]/I²)[1/f] defined via mapping Y to 1/f.

Equations

Instances For

@[simp]

theorem Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) (x : P.Ring) :

(compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom x) = (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) x

@[simp]

theorem Algebra.Generators.compLocalizationAwayAlgHom_X_inl {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) :

(compLocalizationAwayAlgHom T g P) (MvPolynomial.X (Sum.inl ())) = IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))

theorem Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) :

(compLocalizationAwayAlgHom T g P) ((MvPolynomial.rename Sum.inr) (P.σ g) * MvPolynomial.X (Sum.inl ()) - 1) = 0

theorem Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) :

((localizationAway T g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)

theorem Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) :

Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway T g).toComp P).toExtensionHom))

Let R → S → T be algebras such that T is the localization of S away from one element, where S is generated over R by P with kernel I and Q is the canonical S-presentation of T. Denote by J the kernel of the composition R[X,Y] → T. Then T ⊗[S] (I/I²) → J/J² is injective.

noncomputable def Algebra.Generators.cotangentCompAwaySec {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) (x : ((localizationAway T g).comp P).toExtension.Cotangent) :

(localizationAway T g).toExtension.Cotangent →ₗ[T] ((localizationAway T g).comp P).toExtension.Cotangent

In the notation of the module docstring: Since T is standard smooth of relative dimension one over S, K/K² is free of rank one generated by the image of g * X - 1. This is the section K/K² → J/J² defined by sending the image of g * X - 1 to x : J/J².

Equations

Instances For

theorem Algebra.Generators.cotangentCompAwaySec_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) (x : ((localizationAway T g).comp P).toExtension.Cotangent) :

(cotangentCompAwaySec g P x) (cMulXSubOneCotangent T g) = x

By construction, the section cotangentCompAwaySec sends g * X - 1 to x.

theorem Algebra.Generators.map_comp_cotangentCompAwaySec {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) :

Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom ∘ₗ cotangentCompAwaySec g P x = LinearMap.id

The section cotangentCompAwaySec is indeed a section of the canonical map J/J² → K/K².

noncomputable def Algebra.Generators.cotangentCompLocalizationAwayEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) :

((localizationAway T g).comp P).toExtension.Cotangent ≃ₗ[T] TensorProduct S T P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent

Let S be generated over R by P : R[X] → S with kernel I and let T be the localization of S away from g generated over S by S[Y] → T with kernel K. Denote by J the kernel of the induced R[X, Y] → T. Then J/J² ≃ₗ[T] T ⊗[S] (I/I²) × (K/K²).

This is the splitting characterised by x ↦ (0, g * X - 1).

Equations

Instances For

theorem Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inr {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) :

(cotangentCompLocalizationAwayEquiv g P hx).symm (0, cMulXSubOneCotangent T g) = x

theorem Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) :

↑(cotangentCompLocalizationAwayEquiv g P hx).symm ∘ₗ LinearMap.inl T (TensorProduct S T P.toExtension.Cotangent) (localizationAway T g).toExtension.Cotangent = LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway T g).toComp P).toExtensionHom)

@[simp]

theorem Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) (a : TensorProduct S T P.toExtension.Cotangent) :

(cotangentCompLocalizationAwayEquiv g P hx).symm (a, 0) = (LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway T g).toComp P).toExtensionHom)) a

theorem Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) :

LinearMap.snd T (TensorProduct S T P.toExtension.Cotangent) (localizationAway T g).toExtension.Cotangent ∘ₗ ↑(cotangentCompLocalizationAwayEquiv g P hx) = Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom

@[simp]

theorem Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Generators R S ι) {x : ((localizationAway T g).comp P).toExtension.Cotangent} (hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g) (a : ((localizationAway T g).comp P).toExtension.Cotangent) :

((cotangentCompLocalizationAwayEquiv g P hx) a).2 = (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) a