Ranges of base-change maps for Kähler differentials

This file records two reusable consequences of the Jacobi–Zariski sequence. The base-change map onto Ω[B⁄R] is surjective exactly when Ω[B⁄A] vanishes, and if Ω[A⁄R] is cyclic then its range is generated by the image of a generator. The final linear-algebra lemma identifies generation by one vector with nonvanishing in a one-dimensional vector space.

Main results

• TauCeti.subsingleton_kaehlerDifferential_iff_range_mapBaseChange_eq_top
• TauCeti.range_mapBaseChange_eq_span_singleton
• TauCeti.span_singleton_eq_top_iff_ne_zero_of_finrank_eq_one

theorem TauCeti.subsingleton_kaehlerDifferential_iff_range_mapBaseChange_eq_top (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : Subsingleton Ω[B⁄A] ↔ (KaehlerDifferential.mapBaseChange R A B).range = ⊤

In a tower R → A → B, the first map in the Jacobi–Zariski sequence is surjective exactly when the relative differential module Ω[B⁄A] vanishes.

theorem TauCeti.range_mapBaseChange_eq_span_singleton (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (ω : Ω[A⁄R]) (hω : A ∙ ω = ⊤) : (KaehlerDifferential.mapBaseChange R A B).range = B ∙ (KaehlerDifferential.map R R A B) ω

If Ω[A⁄R] is generated by ω, then the range of the base-change map to Ω[B⁄R] is generated by the image of ω.

theorem TauCeti.span_singleton_eq_top_iff_ne_zero_of_finrank_eq_one {K : Type u_4} {V : Type u_5} [DivisionRing K] [AddCommGroup V] [Module K V] (hfin : Module.finrank K V = 1) (v : V) : K ∙ v = ⊤ ↔ v ≠ 0

In a one-dimensional vector space, a singleton spans exactly when its vector is nonzero.