Documentation

Hironaka.Algebra.RegularSmooth.Presentation

The localized presentation k[x]_Q โ†’ S_๐”ฎ of a local ring of a finite type algebra #

Mathlib's Jacobian criterion, applied in Hironaka/Algebra/RegularSmooth/RegularImpliesSmooth.lean to show that a regular local ring of a finite type algebra over a field is smooth, is used on the presentation of R = S_๐”ฎ by P = k[x_1, โ€ฆ, x_N]_Q, Q the preimage of ๐”ฎ under a surjection ฯ† : k[x] โ†’ S, as in the proof of [TSPA, Tag 00TS]. This file records what the criterion needs of the presentation: the localized map P โ†’ S_๐”ฎ (Mathlib's Localization.localRingHom) is surjective, its kernel is the ideal generated by ker ฯ† (an element of P maps to zero iff a denominator outside Q clears it into ker ฯ†) and finitely generated since P is Noetherian; P is formally smooth over k (a polynomial ring, then a localization) with ฮฉ[Pโ„k] finite free on the d x_i; and the localized map is a local homomorphism inducing an isomorphism of residue fields. The surjectivity and kernel statements hold for any surjection of commutative rings.

source
theorem Localization.localRingHom_surjective_of_surjective {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] (ฯ† : A โ†’+* S) (๐”ฎ : Ideal S) [๐”ฎ.IsPrime] (hฯ† : Function.Surjective โ‡‘ฯ†) :
Function.Surjective โ‡‘(localRingHom (Ideal.comap ฯ† ๐”ฎ) ๐”ฎ ฯ† โ‹ฏ)

The localization at Q = ฯ†โปยน(๐”ฎ) of a surjection ฯ† : A โ†’ S is a surjection A_Q โ†’ S_๐”ฎ (as in the proof of [TSPA, Tag 00TS]).

source
theorem Localization.ker_localRingHom_of_surjective {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] (ฯ† : A โ†’+* S) (๐”ฎ : Ideal S) [๐”ฎ.IsPrime] (hฯ† : Function.Surjective โ‡‘ฯ†) :
RingHom.ker (localRingHom (Ideal.comap ฯ† ๐”ฎ) ๐”ฎ ฯ† โ‹ฏ) = Ideal.map (algebraMap A (Localization.AtPrime (Ideal.comap ฯ† ๐”ฎ))) (RingHom.ker ฯ†)

The kernel of the localized surjection A_Q โ†’ S_๐”ฎ is the ideal generated by ker ฯ†: a fraction maps to zero iff a denominator outside Q clears its numerator into ker ฯ†.

source
theorem Localization.bijective_residueField_map_localRingHom_of_surjective {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] (ฯ† : A โ†’+* S) (๐”ฎ : Ideal S) [๐”ฎ.IsPrime] (hฯ† : Function.Surjective โ‡‘ฯ†) :
Function.Bijective โ‡‘(IsLocalRing.ResidueField.map (localRingHom (Ideal.comap ฯ† ๐”ฎ) ๐”ฎ ฯ† โ‹ฏ))

The localized surjection A_Q โ†’ S_๐”ฎ induces an isomorphism of residue fields.

source
theorem MvPolynomial.formallySmooth_localization_atPrime {k : Type u} [Field k] {ฮน : Type v} (Q : Ideal (MvPolynomial ฮน k)) [Q.IsPrime] :
Algebra.FormallySmooth k (Localization.AtPrime Q)

k[x]_Q is formally smooth over k (a polynomial ring, then a localization).

source
theorem MvPolynomial.free_kaehlerDifferential_localization_atPrime {k : Type u} [Field k] {ฮน : Type v} (Q : Ideal (MvPolynomial ฮน k)) [Q.IsPrime] :
Module.Free (Localization.AtPrime Q) ฮฉ[Localization.AtPrime Qโ„k]

ฮฉ[k[x]_Q โ„ k] is free, on the d x_i [TSPA, Tags 00RX, 00RT].

source
theorem MvPolynomial.finite_kaehlerDifferential_localization_atPrime {k : Type u} [Field k] {ฮน : Type v} [Finite ฮน] (Q : Ideal (MvPolynomial ฮน k)) [Q.IsPrime] :
Module.Finite (Localization.AtPrime Q) ฮฉ[Localization.AtPrime Qโ„k]

ฮฉ[k[x]_Q โ„ k] is a finite module (finitely many variables).

source
theorem MvPolynomial.fg_of_localization_atPrime {k : Type u} [Field k] {ฮน : Type v} [Finite ฮน] (Q : Ideal (MvPolynomial ฮน k)) [Q.IsPrime] (I : Ideal (Localization.AtPrime Q)) :
I.FG

Every ideal of k[x]_Q is finitely generated (k[x]_Q is Noetherian).