theorem conormalExactSeq_exact (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B)

Proposition 35 (Lec 20): exactness in the middle of the conormal sequence I/I² → B ⊗_A Ω_{A/R} → Ω_{B/R} → 0 when A → B is surjective.

theorem conormalExactSeq_mapBaseChange_surjective (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

The right-hand map B ⊗_A Ω_{A/R} → Ω_{B/R} in the conormal sequence is surjective when A → B is surjective.

theorem conormalExactSeq_rightExact (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B) ∧ Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

Right exactness of the conormal sequence: combines the exactness at the middle with the surjectivity on the right.

theorem conormalExactSeq_shortExact_of_formallySmooth (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ∧ Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B) ∧ Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

Under formal smoothness of both A/R and B/R, the conormal sequence is a short exact sequence: the map I/I² → B ⊗_A Ω_{A/R} is also injective.

theorem conormalExactSeq_splitInjection (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B] (h : Function.Surjective ⇑(algebraMap A B)) : ∃ (l : TensorProduct A B Ω[A⁄R] →ₗ[A] (RingHom.ker (algebraMap A B)).Cotangent), l ∘ₗ KaehlerDifferential.kerCotangentToTensor R A B = LinearMap.id

Under formal smoothness, the inclusion I/I² → B ⊗_A Ω_{A/R} admits a left inverse, so the conormal sequence is a split short exact sequence.

theorem conormalExactSeq_finrank {R : Type u} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B] (h : Function.Surjective ⇑(algebraMap A B)) (n m : ℕ) (hΩmid : Module.finrank B (TensorProduct A B Ω[A⁄R]) = n) (hΩB : Module.finrank B Ω[B⁄R] = n - m) : Module.finrank (A ⧸ RingHom.ker (algebraMap A B)) (RingHom.ker (algebraMap A B)).Cotangent = m

Dimension formula from the conormal short exact sequence: if B ⊗_A Ω_{A/R} has dimension n and Ω_{B/R} has dimension n - m, then I/I² has dimension m.

theorem conormalSequence_shortExact_of_smooth (R : Type u) [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ∧ Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B) ∧ Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)

Corollary 26: under formal smoothness, the conormal sequence is short exact.