Relation of smoothness and Ω[S⁄R]

Main results

• retractionKerToTensorEquivSection: Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I, there is a one-to-one correspondence between P-linear retractions of I →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f.
• retractionKerCotangentToTensorEquivSection: Given a surjective algebra homomorphism f : P →ₐ[R] S with kernel I, there is a one-to-one correspondence between P-linear retractions of I/I² →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f‾ : P/I² → S.

Future projects

• Show that being smooth is local on stalks.
• Show that being formally smooth is Zariski-local (very hard).

References

• https://stacks.math.columbia.edu/tag/00TH
• B. Iversen, Generic Local Structure of the Morphisms in Commutative Algebra

def derivationOfSectionOfKerSqZero {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra R S] (f : P →ₐ[R] S) (hf' : RingHom.ker f ^ 2 = ⊥) (g : S →ₐ[R] P) (hg : f.comp g = AlgHom.id R S) : Derivation R P ↥(RingHom.ker f)

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I, and a section g : S →ₐ[R] P (as an algebra homomorphism), we get an R-derivation P → I via x ↦ x - g (f x).

Equations

• derivationOfSectionOfKerSqZero f hf' g hg = { toFun := fun (x : P) => ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem derivationOfSectionOfKerSqZero_apply_coe {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra R S] (f : P →ₐ[R] S) (hf' : RingHom.ker f ^ 2 = ⊥) (g : S →ₐ[R] P) (hg : f.comp g = AlgHom.id R S) (x : P) : ↑((derivationOfSectionOfKerSqZero f hf' g hg) x) = x - g (f x)

theorem isScalarTower_of_section_of_ker_sqZero {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))

noncomputable def retractionOfSectionOfKerSqZero {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))

Given a surjective algebra hom f : P →ₐ[R] S with square-zero kernel I, and a section g : S →ₐ[R] P (as algebra homs), we get a retraction of the injection I → S ⊗[P] Ω[P/R].

Equations

• retractionOfSectionOfKerSqZero g hf' hg = ↑P (LinearMap.liftBaseChange S (derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential)

@[simp]

theorem retractionOfSectionOfKerSqZero_tmul_D {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) (s : S) (t : P) : ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (KaehlerDifferential.D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

theorem retractionOfSectionOfKerSqZero_comp_kerToTensor {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) : retractionOfSectionOfKerSqZero g hf' hg ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id

theorem sectionOfRetractionKerToTensorAux_prop {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (x y : P) (h : (algebraMap P S) x = (algebraMap P S) y) : x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x)) = y - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) y))

noncomputable def sectionOfRetractionKerToTensorAux {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P) (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) : S →ₐ[R] P

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I. Let σ be an arbitrary (set-theoretic) section of f. Suppose we have a retraction l of the injection I →ₗ[P] S ⊗[P] Ω[P/R], then x ↦ σ x - l (1 ⊗ D (σ x)) is an algebra homomorphism and a section to f.

Equations

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

theorem sectionOfRetractionKerToTensorAux_algebraMap {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P) (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (x : P) : (sectionOfRetractionKerToTensorAux l hl σ hσ hf') ((algebraMap P S) x) = x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x))

theorem toAlgHom_comp_sectionOfRetractionKerToTensorAux {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P) (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id R S

noncomputable def sectionOfRetractionKerToTensor {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : S →ₐ[R] P

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I. Suppose we have a retraction l of the injection I →ₗ[P] S ⊗[P] Ω[P/R], then x ↦ σ x - l (1 ⊗ D (σ x)) is an algebra homomorphism and a section to f, where σ is an arbitrary (set-theoretic) section of f

Equations

• sectionOfRetractionKerToTensor l hl hf' hf = sectionOfRetractionKerToTensorAux l hl (fun (x : S) => ⋯.choose) ⋯ hf'

@[simp]

theorem sectionOfRetractionKerToTensor_algebraMap {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) (x : P) : (sectionOfRetractionKerToTensor l hl hf' hf) ((algebraMap P S) x) = x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x))

@[simp]

theorem toAlgHom_comp_sectionOfRetractionKerToTensor {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensor l hl hf' hf) = AlgHom.id R S

noncomputable def retractionKerToTensorEquivSection {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : { l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)) // l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id } ≃ { g : S →ₐ[R] P // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I, there is a one-to-one correspondence between P-linear retractions of I →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f.

Equations

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

noncomputable def derivationQuotKerSq (R : Type u_1) (P : Type u_2) (S : Type u_3) [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] : Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) (TensorProduct P S Ω[P⁄R])

Given a tower of algebras S/P/R, with I = ker(P → S), this is the R-derivative P/I² → S ⊗[P] Ω[P⁄R] given by [x] ↦ 1 ⊗ D x.

Equations

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

@[simp]

theorem derivationQuotKerSq_mk {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (x : P) : (derivationQuotKerSq R P S) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) x) = 1 ⊗ₜ[P] (KaehlerDifferential.D R P) x

noncomputable def tensorKaehlerQuotKerSqEquiv (R : Type u_1) (P : Type u_2) (S : Type u_3) [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] : TensorProduct (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] ≃ₗ[S] TensorProduct P S Ω[P⁄R]

Given a tower of algebras S/P/R, with I = ker(P → S) and Q := P/I², there is an isomorphism of S-modules S ⊗[Q] Ω[Q/R] ≃ S ⊗[P] Ω[P/R].

Equations

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

@[simp]

theorem tensorKaehlerQuotKerSqEquiv_tmul_D {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (s : S) (t : P) : (tensorKaehlerQuotKerSqEquiv R P S) (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] (KaehlerDifferential.D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) = s ⊗ₜ[P] (KaehlerDifferential.D R P) t

@[simp]

theorem tensorKaehlerQuotKerSqEquiv_symm_tmul_D {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (s : S) (t : P) : (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (KaehlerDifferential.D R P) t) = s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] (KaehlerDifferential.D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)

noncomputable def retractionKerCotangentToTensorEquivSection {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf : Function.Surjective ⇑(algebraMap P S)) : { l : TensorProduct P S Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent // l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P S = LinearMap.id } ≃ { g : S →ₐ[R] P ⧸ RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom ^ 2 // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }

Given a surjective algebra homomorphism f : P →ₐ[R] S with kernel I, there is a one-to-one correspondence between P-linear retractions of I/I² →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f‾ : P/I² → S.

Equations

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

theorem Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Bijective ⇑(CotangentSpace.map P.toInfinitesimal)

theorem Algebra.Extension.Cotangent.map_toInfinitesimal_bijective {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Bijective ⇑(map P.toInfinitesimal)

theorem Algebra.Extension.H1Cotangent.map_toInfinitesimal_bijective {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Bijective ⇑(map P.toInfinitesimal)