Spreading out generators of the Kähler differentials from a point

Let k → S be an algebra and v_0, …, v_{n-1} ∈ S. Two Nakayama-type statements used to pass from the stalk at a point to a neighbourhood (the "shrink U" step in producing étale coordinates on a smooth scheme, Hironaka/Scheme/Smooth/EtaleCoordinates.lean):

• exists_smul_mem_span_of_localized: if the d v_i generate Ω[T⁄k] for a localization T of S at a submonoid M, then every ω ∈ Ω[S⁄k] has a multiple s • ω, s ∈ M, in the span of the d v_i (the span of the d v_i localizes to the span of their images, Mathlib's Submodule.localized'_span, and Ω[T⁄k] is the localized module of Ω[S⁄k], KaehlerDifferential.isLocalizedModule_map);
• exists_mem_forall_smul_mem_span: for Ω[S⁄k] finitely generated, one s ∈ M works for all ω (the product of the multipliers of finitely many generators);
• span_eq_top_of_forall_smul_mem: if s • Ω[S⁄k] lies in the span of the d v_i, then the d v_i generate Ω[S'⁄k] for the localization S' = S[1/s];
• span_eq_top_of_basis_tensor: Nakayama at a local ring T: if the classes 1 ⊗ d v_i form a basis of κ ⊗_T Ω[T⁄k], the d v_i generate Ω[T⁄k] (IsLocalRing.span_eq_top_of_tmul_eq_basis).

Routine commutative algebra, not stated as such in the sources (the localization of a finitely generated module, [TSPA, Tag 00DQ], and Nakayama's lemma).

theorem Algebra.map_image_range_D {k S T : Type u} [CommRing k] [CommRing S] [CommRing T] [Algebra k S] [Algebra k T] [Algebra S T] [IsScalarTower k S T] {ι : Type u_1} (v : ι → S) : (⇑(KaehlerDifferential.map k k S T) '' Set.range fun (i : ι) => (KaehlerDifferential.D k S) (v i)) = Set.range fun (i : ι) => (KaehlerDifferential.D k T) ((algebraMap S T) (v i))

The image under Ω[S⁄k] → Ω[T⁄k] of the differentials of the v i are the differentials of their images.

theorem Algebra.exists_smul_mem_span_of_localized {k S T : Type u} [CommRing k] [CommRing S] [CommRing T] [Algebra k S] [Algebra k T] [Algebra S T] [IsScalarTower k S T] (M : Submonoid S) [IsLocalization M T] {ι : Type u_1} (v : ι → S) (h : Submodule.span T (Set.range fun (i : ι) => (KaehlerDifferential.D k T) ((algebraMap S T) (v i))) = ⊤) (ω : Ω[S⁄k]) : ∃ s ∈ M, s • ω ∈ Submodule.span S (Set.range fun (i : ι) => (KaehlerDifferential.D k S) (v i))

If the d v_i generate Ω[T⁄k] for the localization T = S[M⁻¹], every ω ∈ Ω[S⁄k] has a multiple s • ω, s ∈ M, in the span of the d v_i.

theorem Algebra.exists_mem_forall_smul_mem_span {k S T : Type u} [CommRing k] [CommRing S] [CommRing T] [Algebra k S] [Algebra k T] [Algebra S T] [IsScalarTower k S T] (M : Submonoid S) [IsLocalization M T] [Module.Finite S Ω[S⁄k]] {ι : Type u_1} (v : ι → S) (h : Submodule.span T (Set.range fun (i : ι) => (KaehlerDifferential.D k T) ((algebraMap S T) (v i))) = ⊤) : ∃ s ∈ M, ∀ (ω : Ω[S⁄k]), s • ω ∈ Submodule.span S (Set.range fun (i : ι) => (KaehlerDifferential.D k S) (v i))

One multiplier for all of Ω[S⁄k] when it is finitely generated.

theorem Algebra.span_eq_top_of_forall_smul_mem {k S : Type u} [CommRing k] [CommRing S] [Algebra k S] {S' : Type u} [CommRing S'] [Algebra k S'] [Algebra S S'] [IsScalarTower k S S'] (M : Submonoid S) [IsLocalization M S'] {ι : Type u_1} (v : ι → S) {s : S} (hs : s ∈ M) (h : ∀ (ω : Ω[S⁄k]), s • ω ∈ Submodule.span S (Set.range fun (i : ι) => (KaehlerDifferential.D k S) (v i))) : Submodule.span S' (Set.range fun (i : ι) => (KaehlerDifferential.D k S') ((algebraMap S S') (v i))) = ⊤

If s • Ω[S⁄k] lies in the span of the d v_i, the d v_i generate Ω[S'⁄k] for the localization S' = S[1/s] (or any localization at a submonoid containing s).

theorem Algebra.finite_kaehlerDifferential_of_isLocalization {k S T : Type v} [CommRing k] [CommRing S] [CommRing T] [Algebra k S] [Algebra k T] [Algebra S T] [IsScalarTower k S T] (M : Submonoid S) [IsLocalization M T] [Module.Finite S Ω[S⁄k]] : Module.Finite T Ω[T⁄k]

Ω[T⁄k] is a finite T-module when Ω[S⁄k] is a finite S-module and T is a localization of S (it is the base change T ⊗_S Ω[S⁄k]).

theorem Algebra.span_eq_top_of_basis_tensor {k S T : Type v} [CommRing k] [CommRing S] [CommRing T] [Algebra k T] [Algebra S T] [IsLocalRing T] [Module.Finite T Ω[T⁄k]] {ι : Type u_1} (v : ι → S) (b : Module.Basis ι (IsLocalRing.ResidueField T) (TensorProduct T (IsLocalRing.ResidueField T) Ω[T⁄k])) (hb : ∀ (i : ι), b i = 1 ⊗ₜ[T] (KaehlerDifferential.D k T) ((algebraMap S T) (v i))) : Submodule.span T (Set.range fun (i : ι) => (KaehlerDifferential.D k T) ((algebraMap S T) (v i))) = ⊤

Nakayama at a local ring T: if the classes 1 ⊗ d v_i form a basis of κ ⊗_T Ω[T⁄k], the d v_i generate Ω[T⁄k].