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.

Future projects

• Show that relative smooth iff H¹(L_{S/R}) = 0 and Ω[S/R] is projective.
• Show that being smooth is local on stalks.
• Show that being formally smooth is Zariski-local (very hard).

@[simp]

theorem derivationOfSectionOfKerSqZero_apply_coe {R : Type u} {P : Type u} {S : Type u} [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)

def derivationOfSectionOfKerSqZero {R : Type u} {P : Type u} {S : Type u} [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 { x : P // x ∈ 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' := ⋯ }

theorem isScalarTower_of_section_of_ker_sqZero {R : Type u} {P : Type u} {S : Type u} [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 { x : P // x ∈ RingHom.ker (algebraMap P S) }

noncomputable def retractionOfSectionOfKerSqZero {R : Type u} {P : Type u} {S : Type u} [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] { x : P // x ∈ 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} {P : Type u} {S : Type u} [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} {P : Type u} {S : Type u} [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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ RingHom.ker (algebraMap P S) }) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (x : P) (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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ 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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ 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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ 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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ 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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ 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} {P : Type u} {S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] { x : P // x ∈ 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} {P : Type u} {S : Type u} [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] { x : P // x ∈ 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.