Smoothness at a point and its affine-local form

Smoothness at a point is Mathlib's: for f : X ⟶ Y locally of finite presentation, x ∈ f.smoothLocus means that the stalk map 𝒪_{Y, f x} → 𝒪_{X, x} is formally smooth (Scheme.Hom.mem_smoothLocus). This agrees with the definition of the sources, "f is smooth at x when its restriction to some open neighbourhood of x is smooth" [TSPA, Tag 01V9], with [TSPA, Tag 00TB] for the affine form; the agreement is mem_smoothLocus_iff_exists_smooth below. Over a field k, indeed over any locally Noetherian base, a morphism locally of finite type is locally of finite presentation (Mathlib's instance in AlgebraicGeometry/Noetherian.lean), so f.smoothLocus makes sense for X locally of finite type over k, the standing hypothesis of the comparison of smooth and regular points in this directory.

The reduction to the affine local statement ("the question is local", as in the proof of [TSPA, Tag 038X]): for f : X ⟶ Spec k and an affine open U ∋ x, the ring of sections S = Γ(X, U) is a k-algebra through k ≅ Γ(Spec k, ⊤) → Γ(X, U) (Scheme.Hom.sectionsAlgebra), of finite type when f is locally of finite type; with 𝔮 = hU.primeIdealOf ⟨x, hx⟩ the prime of x, the point x lies in f.smoothLocus iff S is smooth at 𝔮 over k in Mathlib's sense Algebra.IsSmoothAt k 𝔮 := Algebra.FormallySmooth k (Localization.AtPrime 𝔮) (mem_smoothLocus_iff_isSmoothAt, from Mathlib's formallySmooth_stalkMap_iff applied to the affine open ⊤ of Spec k, and the invariance of formal smoothness under the isomorphism k ≅ Γ(Spec k, ⊤) of base rings). The stalk of Spec k at its unique point is k (isIso_toStalk_Spec_of_field, as in the proof of Mathlib's Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField). The regular half of the reduction is Scheme.isRegularAt_iff_isRegularLocalRing_localization in Hironaka/Algebra/RegularSmooth/Regular.lean.

theorem AlgebraicGeometry.Scheme.Hom.mem_smoothLocus_iff_exists_smooth {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] {x : ↥X} : x ∈ smoothLocus f ↔ ∃ (U : X.Opens), x ∈ U ∧ Smooth (CategoryTheory.CategoryStruct.comp U.ι f)

A point lies in the smooth locus of f iff the restriction of f to some open neighbourhood of the point is smooth: Mathlib's smooth locus agrees with the definition of "smooth at x" of [TSPA, Tag 01V9] (and of [TSPA, Tag 00TB] in the affine case).

theorem AlgebraicGeometry.Scheme.Hom.locallyOfFinitePresentation_of_field {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] : LocallyOfFinitePresentation f

Over a field, a morphism locally of finite type is locally of finite presentation (Mathlib's instance for a locally Noetherian target, in AlgebraicGeometry/Noetherian.lean), so f.smoothLocus is defined for X locally of finite type over k.

theorem RingHom.FormallySmooth.comp_ringEquiv_iff {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (g : S →+* T) (e : R ≃+* S) : (g.comp e.toRingHom).FormallySmooth ↔ g.FormallySmooth

Formal smoothness of a ring map is unchanged by precomposition with a ring isomorphism (the second half of RingHom.FormallySmooth.respectsIso, as an equivalence).

@[instance_reducible]

noncomputable def AlgebraicGeometry.Scheme.Hom.sectionsAlgebra {X : Scheme} {k : Type u} [CommRing k] (f : X ⟶ Spec ↧k) (U : X.Opens) : Algebra k ↑(X.presheaf.obj (Opposite.op U))

For f : X ⟶ Spec k, the k-algebra structure on the sections of X over an open U, by k ≅ Γ(Spec k, ⊤) → Γ(X, U) (Scheme.ΓSpecIso followed by f.appLE ⊤ U): the ring S of an affine open U = Spec S becomes a k-algebra. Not an instance: the structure depends on f.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Hom.algebraMap_sectionsAlgebra {X : Scheme} {k : Type u} [CommRing k] (f : X ⟶ Spec ↧k) (U : X.Opens) : algebraMap k ↑(X.presheaf.obj (Opposite.op U)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧k).inv (appLE f ⊤ U ⋯))

theorem AlgebraicGeometry.Scheme.Hom.finiteType_sectionsAlgebra {X : Scheme} {k : Type u} [CommRing k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] {U : X.Opens} (hU : IsAffineOpen U) : Algebra.FiniteType k ↑(X.presheaf.obj (Opposite.op U))

For f : X ⟶ Spec k locally of finite type and U an affine open, Γ(X, U) is a k-algebra of finite type (for the structure Scheme.Hom.sectionsAlgebra).

theorem AlgebraicGeometry.Scheme.Hom.mem_smoothLocus_iff_isSmoothAt {X : Scheme} {k : Type u} [CommRing k] (f : X ⟶ Spec ↧k) [LocallyOfFinitePresentation f] {U : X.Opens} (hU : IsAffineOpen U) {x : ↥X} (hx : x ∈ U) : x ∈ smoothLocus f ↔ Algebra.IsSmoothAt k (hU.primeIdealOf ⟨x, hx⟩).asIdeal

The affine-local form of smoothness at a point ([TSPA, Tag 00TB]; "the question is local" in the proof of [TSPA, Tag 038X]): for f : X ⟶ Spec k locally of finite presentation and an affine open U ∋ x with 𝔮 = hU.primeIdealOf ⟨x, hx⟩ the prime of x, the point x lies in the smooth locus of f iff Γ(X, U) is smooth at 𝔮 over k: Algebra.IsSmoothAt k 𝔮, i.e. Γ(X, U)_𝔮 is formally smooth over k. Mathlib's formallySmooth_stalkMap_iff for the affine open ⊤ of Spec k, then the base ring Γ(Spec k, ⊤) is replaced by k along Scheme.ΓSpecIso.

theorem AlgebraicGeometry.isIso_toStalk_Spec_of_field {k : Type u} [Field k] (y : ↥(Spec ↧k)) : CategoryTheory.IsIso (StructureSheaf.toStalk k y)

The stalk of Spec k at its point is k (as in the proof of Mathlib's Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField): for a field k, the canonical map k → 𝒪_{Spec k, y} is an isomorphism at the unique point y of Spec k.