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 with kernel I and Q is the canonical S-presentation of T. Denote by J the kernel of the composition R[X,Y] → T.

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.

theorem Algebra.Generators.comp_localizationAway_ker {R : Type u_1} {S : Type u_2} {T : Type u_3} [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 g).comp P).ker = Ideal.map ((localizationAway 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) [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 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp {R : Type u_1} {S : Type u_2} {T : Type u_3} [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 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} [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} [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} [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 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} [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 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.

Stacks Tag 08JZ (part of (1))