37.28 Connected components of… to 37.45 Applications of Zariski's…
Section37.28 Connected components of fibres#
Section 37.28 of the Stacks Project, Tag 055C. 7 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 055D, a lemma
Tag 055D in the Stacks Project.
AlgebraicGeometry.exists_open_natCard_connectedComponents_fiber_ge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FibreConnectedComponents/LowerBound.lean, line 208. References: EGA IV (9.7.1), “connected components”.
Stacks Project, Tag 055D. For a finite type morphism to a scheme with a chosen dense generic point, the number of connected components of the fibres is at least the number for the generic fibre on a nonempty open subset of the base.
theorem exists_open_natCard_connectedComponents_fiber_ge {X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFiniteType f] [QuasiCompact f] (η : Y) (hη : IsGenericPoint η Set.univ) (n : ℕ)
(hcomp : Nat.card (ConnectedComponents (f.fiber η)) = n) :
∃ V : Set Y, IsOpen V ∧ V.Nonempty ∧
∀ y ∈ V, n ≤ Nat.card (ConnectedComponents (f.fiber y))
Tag 055E, a lemma
Tag 055E in the Stacks Project.
AlgebraicGeometry.geometricallyConnected_fiber_locus_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ConnectedComponents.lean, line 60.
Stacks Project, Tag 055E. Formation of the locus where the fibres of a scheme morphism are geometrically connected commutes with arbitrary base change.
theorem geometricallyConnected_fiber_locus_pullback
{X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y) :
{y' : Y' |
GeometricallyConnected ((pullback.snd f g).fiberToSpecResidueField y')} =
g ⁻¹' {y : Y | GeometricallyConnected (f.fiberToSpecResidueField y)}
Tag 055F, a lemma
Tag 055F in the Stacks Project.
AlgebraicGeometry.numGeometricConnectedComponents, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ConnectedComponents.lean, line 171. The attribute's comment: “the function”. References: EGA III (4.3.4), “geom. # of components”; EGA IV (15.5.3); EGA IV (4.5.2), “more general”.
The number of geometric connected components of each fibre of a morphism of schemes.
def numGeometricConnectedComponents (f : X ⟶ Y) : Y → ℕ∞
AlgebraicGeometry.enatCard_connectedComponents_fiberBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ConnectedComponents.lean, line 178. The attribute's comment: “well-definedness”. References: EGA IV (15.5.3), “more general”.
Computing the number of connected components after extending a fibre to any separably closed extension gives the canonical number of geometric connected components.
theorem enatCard_connectedComponents_fiberBaseChange (f : X ⟶ Y) (y : Y)
(K : Type u) [Field K] [Algebra (Y.residueField y) K] [IsSepClosed K] :
ENat.card (ConnectedComponents (geometricFiber f y K)) =
numGeometricConnectedComponents f y
AlgebraicGeometry.numGeometricConnectedComponents_eq_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ConnectedComponents.lean, line 202. The attribute's comment: “base change”.
The number of geometric connected components of fibres is preserved by arbitrary base change.
theorem numGeometricConnectedComponents_eq_of_isPullback
{X' Y' : Scheme.{u}} (f : X ⟶ Y) (f' : X' ⟶ Y') (i : X' ⟶ X) (g : Y' ⟶ Y)
(h : IsPullback i f' f g) :
numGeometricConnectedComponents f' = numGeometricConnectedComponents f ∘ g
Declarations registered for the tag:
geometricFiberregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ConnectedComponents.lean, line 84 (StacksFrontier): “geometric fibre”.
Tag 055G, a lemma
Tag 055G in the Stacks Project.
AlgebraicGeometry.geometricallyConnectedAfterShrinking, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 80.
Stacks Project, Tag 055G. A finite type morphism onto an irreducible base whose fibre over the generic point is geometrically connected has geometrically connected fibres over a nonempty open subscheme of the base.
theorem geometricallyConnectedAfterShrinking : GeometricallyConnectedAfterShrinking.{u}
Tag 055H, a lemma
Tag 055H in the Stacks Project.
AlgebraicGeometry.exists_open_numGeometricConnectedComponents_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FibreConnectedComponents/GenericConstancy.lean, line 701.
Stacks Project, Tag 055H. For a finite type morphism of schemes, the number of geometric connected components of the fibres is constant on some nonempty open subset of the closure of any prescribed point of the base.
theorem exists_open_numGeometricConnectedComponents_eq {X Y : Scheme.{u}} (f : X ⟶ Y)
[LocallyOfFiniteType f] [QuasiCompact f] (y : Y) :
∃ V : TopologicalSpace.Opens (↑(closure ({y} : Set Y))), Nonempty V ∧
∃ n : ℕ∞, ∀ z : V, numGeometricConnectedComponents f z.1.1 = n
Tag 055I, a lemma
Tag 055I in the Stacks Project.
AlgebraicGeometry.isLocallyConstructible_numGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FibreConnectedComponents/Constructible.lean, line 81. References: EGA IV (9.7.9), “n'(s) (connected)”.
Stacks Project, Tag 055I. Every level set of the number of geometrically connected components of the fibres of a morphism of finite presentation is locally constructible.
theorem isLocallyConstructible_numGeometricConnectedComponents {X Y : Scheme.{u}} (f : X ⟶ Y)
(hf : AlgebraicGeometry.FinitePresentation f) (n : ℕ∞) :
IsLocallyConstructible {y : Y | numGeometricConnectedComponents f y = n}
Tag 055J, a lemma
Tag 055J in the Stacks Project.
AlgebraicGeometry.connectedSpace_fiber_bot_of_isReduced_fiber_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ConnectedGenericFibre.lean, line 234. References: EGA IV (15.5.6), “more general”; EGA IV (18.9.7), “special case”.
Stacks Project, Tag 055J. A flat degeneration of a disconnected scheme is either disconnected or nonreduced: if a flat scheme over a discrete valuation ring is connected and its closed fibre is reduced, then its generic fibre is connected.
theorem connectedSpace_fiber_bot_of_isReduced_fiber_closedPoint
{R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
{X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [Flat f] [ConnectedSpace X]
[IsReduced (f.fiber (IsLocalRing.closedPoint R))] :
ConnectedSpace (f.fiber (⟨⊥, inferInstance⟩ : PrimeSpectrum R))
Sources
Section37.29 Connected components meeting a section#
Section 37.29 of the Stacks Project, Tag 055K. 7 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 055K, the section
Tag 055K in the Stacks Project.
AlgebraicGeometry.ConnectedAlongSection.mem_locus_iff_asFiber_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/GroupScheme.lean, line 57. The attribute's comment: “Situation 055L: X⁰ = ⋃_y X⁰_y, pointwise”.
For a morphism
f : X ⟶ Ywith a sections, the subsetX⁰ = ⋃_y X⁰_yofXconsists of the pointsxwhich, viewed as points of their own fibreX_{f(x)}, lie in the connected componentX⁰_{f(x)}of that fibre containings(f(x)).
theorem mem_locus_iff_asFiber_mem (D : ConnectedAlongSection.{u}) (x : D.X) :
x ∈ D.locus ↔ D.f.asFiber x ∈ D.fiberComponent (D.f x)
AlgebraicGeometry.ConnectedAlongSection.ofGrpObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/GroupScheme.lean, line 67. The attribute's comment: “a group scheme G → S with its neutral section e : S → G”.
A group scheme
G ⟶ Stogether with its neutral sectione : S ⟶ G, as a morphism of schemes with a section. The neutral section is the morphism of schemes underlying the unitη[G] : 𝟙_ (Over S) ⟶ Gof the group objectG.
noncomputable def ofGrpObj : ConnectedAlongSection.{u}
AlgebraicGeometry.GroupScheme.neutralLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/GroupScheme.lean, line 98. The attribute's comment: “G⁰ = ⋃_s G⁰_s for the neutral section”. References: EGA IV (15.6.8), “special case”; EGA IV (9.7.12), “special case”; SGA 3 XIX (5.10).
For a group scheme
G ⟶ Swith neutral sectione, the subsetG⁰ ⊆ G: the union overs : Sof the connected componentsG⁰_sof the fibresG_scontaininge(s), that is, the locusX⁰forf = (G ⟶ S)and the sectione.
noncomputable def neutralLocus : Set G.left
AlgebraicGeometry.GroupScheme.fiberι_preimage_neutralLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/GroupScheme.lean, line 104. The attribute's comment: “the trace of G⁰ on G_s is the component of G_s containing e(s)”.
For a group scheme
G ⟶ Swith neutral sectioneand a points : S, the trace ofG⁰on the fibreG_sis the connected component ofG_scontaining the pointe(s).
theorem fiberι_preimage_neutralLocus (s : S) (z : G.hom.fiber s)
(hz : G.hom.fiberι s z = η[G].left s) :
(G.hom.fiberι s) ⁻¹' neutralLocus G = connectedComponent z
Tag 055L, a situation
Tag 055L in the Stacks Project.
AlgebraicGeometry.ConnectedAlongSection, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Section.lean, line 55. The attribute's comment: “the sectioned morphism”.
Stacks Project, Tag 055L (standing data). A morphism of schemes together with a specified section.
structure ConnectedAlongSection
AlgebraicGeometry.ConnectedAlongSection.fiberComponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Section.lean, line 79. The attribute's comment: “the component X⁰_y”. References: EGA IV (15.6.5); EGA IV (15.6.8).
Stacks Project, Tag 055L (the fibrewise component). The connected component of the fibre over
ywhich contains the point supplied by the section.
noncomputable def fiberComponent (D : ConnectedAlongSection) (y : D.Y) : Set (D.f.fiber y)
AlgebraicGeometry.ConnectedAlongSection.locus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Section.lean, line 85. The attribute's comment: “the union X⁰”. References: EGA IV (15.6.4).
Stacks Project, Tag 055L (the union). The subset
X⁰ ⊆ Xobtained by taking, for everyy : Y, the image inXof the connected componentX⁰_y.
noncomputable def locus (D : ConnectedAlongSection) : Set D.X
Tag 055M, a lemma
Tag 055M in the Stacks Project.
AlgebraicGeometry.ConnectedAlongSection.locus_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedComponentSection/BaseChange.lean, line 287.
Stacks Project, Tag 055M. In a cartesian square of sectioned morphisms, where the sections are compatible with the horizontal maps, the union of the connected components of the fibres containing the section pulls back to the corresponding union upstairs.
theorem locus_eq_preimage_of_isPullback
(D D' : ConnectedAlongSection.{u})
(g' : D'.X ⟶ D.X) (g : D'.Y ⟶ D.Y)
(h : IsPullback g' D'.f D.f g)
(hs : D'.s ≫ g' = g ≫ D.s) :
D'.locus = g' ⁻¹' D.locus
Tag 055N, a lemma
Tag 055N in the Stacks Project.
AlgebraicGeometry.ConnectedAlongSection.clopenLocusAfterShrinking, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 90.
Stacks Project, Tag 055N. For a finite type morphism with a section and a point
yof the target, the locusX⁰is open and closed in the inverse image of a nonempty open subset of the closure ofy.
theorem clopenLocusAfterShrinking : ClopenLocusAfterShrinking.{u}
Tag 055P, a lemma
Tag 055P in the Stacks Project.
AlgebraicGeometry.ConnectedAlongSection.isLocallyConstructible_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 96. References: EGA IV (9.7.12).
Stacks Project, Tag 055P. For a morphism of finite presentation with a section, the locus
X⁰is locally constructible in the source.
theorem isLocallyConstructible_locus : Statement055P.{u}
Tag 055Q, a lemma
Tag 055Q in the Stacks Project.
AlgebraicGeometry.locus_mem_nhds_of_isDiscreteValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/SectionLocusDVR.lean, line 328. The attribute's comment: “the case of a discrete valuation ring base; the source's reduction to this case, and hence the statement for a general base, is not proved here”. References: EGA IV (15.6.5), “DVR base”.
Stacks 055Q over a discrete valuation ring base. The locus
X⁰is a neighbourhood of every point of the connected component of the closed fibre containing the section.
theorem locus_mem_nhds_of_isDiscreteValuationRing
{X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (sec : Spec (.of R) ⟶ X)
(hsec : sec ≫ f = 𝟙 _) [Flat f] [LocallyOfFiniteType f]
[IsReduced (f.fiber (IsLocalRing.closedPoint R))]
{x : X} (hx : x ∈ connectedComponentIn (f ⁻¹' {IsLocalRing.closedPoint R} : Set X)
(sec (IsLocalRing.closedPoint R))) :
ConnectedAlongSection.locus ⟨X, Spec (.of R), f, sec, hsec⟩ ∈ nhds x
AlgebraicGeometry.ConnectedAlongSection.locus_mem_nhds_of_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/SectionLocusReduction.lean, line 253. The attribute's comment: “the topological reduction to the discrete valuation ring case, for a Noetherian source”. References: EGA IV (15.6.5), “Noeth. source”.
Stacks 055Q for a Noetherian source. If
Xis a Noetherian scheme,fis flat and locally of finite type and the fibre offthroughx ∈ X⁰is geometrically reduced, thenX⁰is a neighbourhood ofx.Quantified over the points
xofX⁰lying over a pointyofY, this is the conclusion of the source:X⁰is a neighbourhood ofX⁰_y.
theorem locus_mem_nhds_of_isConstructible (D : ConnectedAlongSection.{u})
[AlgebraicGeometry.IsNoetherian D.X] [Flat D.f] [LocallyOfFiniteType D.f]
{x : D.X} (hx : x ∈ D.locus)
(hred : GeometricallyReduced (D.f.fiberToSpecResidueField (D.f x))) :
D.locus ∈ nhds x
AlgebraicGeometry.ConnectedAlongSection.locus_mem_nhdsSet_fiberComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 103. References: EGA IV (15.6.5), “nbhd of X⁰_y”; EGA IV (15.6.4), “special case”.
Stacks Project, Tag 055Q. For a flat morphism of finite presentation with a section whose fibre over
yis geometrically reduced, the locusX⁰is a neighbourhood of the connected component of that fibre meeting the section.
theorem locus_mem_nhdsSet_fiberComponent (D : ConnectedAlongSection.{u})
(hfp : FinitePresentation D.f) [Flat D.f] (y : D.Y)
(hgr : GeometricallyReduced (D.f.fiberToSpecResidueField y)) :
D.locus ∈ nhdsSet (D.f.fiberι y '' D.fiberComponent y)
Tag 055R, a lemma
Tag 055R in the Stacks Project.
AlgebraicGeometry.isOpen_locus_of_isDiscreteValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/SectionLocusDVR.lean, line 302. The attribute's comment: “the case of a discrete valuation ring base; the source's reduction to this case, and hence the statement for a general base, is not proved here”. References: EGA IV (15.6.5), “DVR base”.
Stacks 055R over a discrete valuation ring base. The locus
X⁰of connected components of fibres meeting the section is open. Only reducedness of the closed fibre is needed; the source's hypothesis that all fibres be geometrically reduced is not used, and the two reductions of the source that pass from a general base to this one are not proved here.
theorem isOpen_locus_of_isDiscreteValuationRing
{X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (sec : Spec (.of R) ⟶ X)
(hsec : sec ≫ f = 𝟙 _) [Flat f] [LocallyOfFiniteType f]
[IsReduced (f.fiber (IsLocalRing.closedPoint R))] :
IsOpen (ConnectedAlongSection.locus ⟨X, Spec (.of R), f, sec, hsec⟩)
AlgebraicGeometry.ConnectedAlongSection.isOpen_locus_of_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/SectionLocusReduction.lean, line 270. The attribute's comment: “the topological reduction to the discrete valuation ring case, for a Noetherian source”. References: EGA IV (15.6.5), “Noeth. source”.
Stacks 055R for a Noetherian source. If
Xis a Noetherian scheme andfis flat and locally of finite type with geometrically reduced fibres, thenX⁰is open.
theorem isOpen_locus_of_isConstructible (D : ConnectedAlongSection.{u})
[AlgebraicGeometry.IsNoetherian D.X] [Flat D.f] [LocallyOfFiniteType D.f]
[GeometricallyReduced D.f] :
IsOpen D.locus
AlgebraicGeometry.ConnectedAlongSection.isOpen_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 112. References: EGA IV (15.6.5), “In particular: X⁰ open”.
Stacks Project, Tag 055R. For a flat morphism of finite presentation with a section and geometrically reduced fibres, the locus
X⁰is open in the source.
theorem isOpen_locus : Statement055R.{u}
Sources
Section37.30 Dimension of fibres#
Section 37.30 of the Stacks Project, Tag 05F6. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05F7, a lemma
Tag 05F7 in the Stacks Project.
AlgebraicGeometry.exists_nonempty_open_fiberDimension_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/GenericConstancy.lean, line 232. References: EGA IV (9.5.6), “dim X_s = n near η”.
Stacks Project, Tag 05F7. Let
f : X ⟶ Ybe a morphism of finite type withYirreducible with generic pointη. If the generic fibre has dimensionn, then the fibres over some nonempty open subset ofYall have dimensionn.
public theorem exists_nonempty_open_fiberDimension_eq {X Y : Scheme.{u}} (f : X ⟶ Y)
[IrreducibleSpace Y] [LocallyOfFiniteType f] [QuasiCompact f] (n : ℕ) (η : Y)
(hη : IsGenericPoint η Set.univ) (hdim : f.fiberDimension η = (n : WithBot ℕ∞)) :
∃ V : Y.Opens, (V : Set Y).Nonempty ∧ ∀ y ∈ V, f.fiberDimension y = (n : WithBot ℕ∞)
Tag 05F8, a lemma
Tag 05F8 in the Stacks Project.
AlgebraicGeometry.Scheme.Hom.fiberDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Basic.lean, line 74. The attribute's comment: “the function n_{X/Y}”. References: EGA IV (14.2.4).
The dimension-of-fibres function of a morphism of schemes assigns to a point of the target the dimension of the scheme-theoretic fibre over it. Points outside the image of the morphism have empty fibre, hence dimension
⊥.
public noncomputable def fiberDimension (f : X ⟶ Y) : Y → WithBot ℕ∞
AlgebraicGeometry.Scheme.Hom.fiberDimension_eq_of_isPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Basic.lean, line 152. The attribute's comment: “the base-change formula n_{X'/Y'} = n_{X/Y} ∘ g”.
Stacks Project, Tag 05F8. The dimension-of-fibres function of a morphism locally of finite type is unchanged by base change: for a pullback square with
flocally of finite type, the dimension-of-fibres function of the base change is the composite of that offwith the morphism of bases.
public lemma fiberDimension_eq_of_isPullback {X' Y' : Scheme.{u}} {g' : X' ⟶ X} {f' : X' ⟶ Y'}
{f : X ⟶ Y} {g : Y' ⟶ Y} (hsq : IsPullback g' f' f g) [LocallyOfFiniteType f] :
f'.fiberDimension = f.fiberDimension ∘ g
Tag 05F9, a lemma
Tag 05F9 in the Stacks Project.
AlgebraicGeometry.isLocallyConstructible_fiberDimension_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Constructible.lean, line 257. References: EGA IV (9.2.6.1); EGA IV (9.5.5), “Z = X, max dimension”; SGA 3 VIB (4.1), “(ii)”.
Stacks Project, Tag 05F9. For a morphism of schemes of finite presentation, every level set of the dimension-of-fibres function is locally constructible in the target.
public theorem isLocallyConstructible_fiberDimension_eq {X Y : Scheme.{u}} (f : X ⟶ Y)
(hf : FinitePresentation f) (n : WithBot ℕ∞) :
IsLocallyConstructible {y : Y | f.fiberDimension y = n}
Tag 0D4H, a lemma
Tag 0D4H in the Stacks Project.
AlgebraicGeometry.lowerSemicontinuous_fiberDimension, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/LowerSemicontinuity.lean, line 112.
Stacks Project, Tag 0D4H. The dimension-of-fibres function of a flat morphism of finite presentation is lower semicontinuous.
public lemma lowerSemicontinuous_fiberDimension {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f]
(hf : FinitePresentation f) : LowerSemicontinuous f.fiberDimension
Tag 0D4I, a lemma
Tag 0D4I in the Stacks Project.
AlgebraicGeometry.upperSemicontinuous_fiberDimension, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UpperSemicontinuity.lean, line 102. References: EGA IV (13.1.5), “universally closed”.
Stacks Project, Tag 0D4I. The dimension-of-fibres function of a universally closed morphism of schemes locally of finite type is upper semicontinuous. In particular this holds for a proper morphism, which is the source's statement.
public lemma upperSemicontinuous_fiberDimension {X Y : Scheme.{u}} (f : X ⟶ Y)
[UniversallyClosed f] [LocallyOfFiniteType f] :
UpperSemicontinuous f.fiberDimension
Tag 0D4J, a lemma
Tag 0D4J in the Stacks Project.
AlgebraicGeometry.isLocallyConstant_fiberDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/LocallyConstant.lean, line 95. References: EGA IV (14.2.5), “flat fin. pres. case”; EGA IV (13.2.12), “(ii), special case”; SGA 3 VIB (4.3), “special case”.
Stacks Project, Tag 0D4J. The dimension-of-fibres function of a proper, flat morphism of schemes of finite presentation is locally constant.
public theorem isLocallyConstant_fiberDimension {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
[Flat f] (hfp : FinitePresentation f) : IsLocallyConstant f.fiberDimension
Sources
Section37.31 Weak relative Noether normalization#
Section 37.31 of the Stacks Project, Tag 0GTD. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GTE, a lemma
Tag 0GTE in the Stacks Project.
Ideal.exists_mem_ideal_transcendental_residue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/NoetherNormalization.lean, line 34.
An ideal avoiding finitely many incomparable prime ideals contains an element whose image is transcendental over each of the prescribed subfields of the residue fields.
theorem exists_mem_ideal_transcendental_residue
(R : Type*) [CommRing R] (ι : Type*) [Finite ι]
(p : ι → PrimeSpectrum R)
(k : ∀ i, Subfield (p i).asIdeal.ResidueField)
(hinc : ∀ i j, i ≠ j → ¬ (p i).asIdeal ≤ (p j).asIdeal)
(htrans : ∀ i, ¬ Algebra.IsAlgebraic (k i) (p i).asIdeal.ResidueField)
(J : Ideal R) (hJ : ∀ i, ¬ J ≤ (p i).asIdeal) :
∃ x ∈ J, ∀ i, Transcendental (k i)
(algebraMap R (p i).asIdeal.ResidueField x)
Tag 0GTF, a lemma
Tag 0GTF in the Stacks Project.
AlgebraicGeometry.eventually_topologicalKrullDim_fiber_specMapAeval_pow_add_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/EventualFibreDimension.lean, line 2905.
Stacks Project, Tag 0GTF. If the morphism to the affine line determined by
ahas fibres of dimension at mostd, then so does the morphism determined bya ^ n + b, for every sufficiently large exponentn.
public theorem eventually_topologicalKrullDim_fiber_specMapAeval_pow_add_le
{R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
[Algebra.FiniteType R S] (d : ℕ) (a b : S)
(ha : ∀ q : Spec (.of (Polynomial R)),
topologicalKrullDim ((specMapAeval a).fiber q) ≤ (d : WithBot ℕ∞)) :
∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
∀ q : Spec (.of (Polynomial R)),
topologicalKrullDim ((specMapAeval (a ^ n + b)).fiber q) ≤
(d : WithBot ℕ∞)
Tag 0GTG, a lemma
Tag 0GTG in the Stacks Project.
Algebra.exists_quasiFinite_mvPolynomial_of_relativeDimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/WeakRelativeNoetherNormalization.lean, line 1145. The attribute's comment: “The maximum of the dimensions of the fibres is Algebra.relativeDimension R S (Tag 00QD) and is bounded by, rather than equal to, the natural number d; the two are equivalent, and the inequality is what covers Spec S = ∅, where the maximum is ⊥. Quasi-finiteness is Mathlib's RingHom.QuasiFinite, which asks only for finite fibres, so the finite type of the map is a separate conjunct.”.
Stacks Project, Tag 0GTG. Let
R → Sbe a finite type ring map and letdbound the maximumAlgebra.relativeDimension R Sof the dimensions of the fibres ofSpec S → Spec R. Then there is a quasi-finiteR-algebra mapR[t_1, …, t_d] → S.
public theorem exists_quasiFinite_mvPolynomial_of_relativeDimension_le
{R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
[Algebra.FiniteType R S] (d : ℕ)
(hd : Algebra.relativeDimension R S ≤ (d : WithBot ℕ∞)) :
∃ φ : MvPolynomial (Fin d) R →ₐ[R] S,
φ.toRingHom.FiniteType ∧ φ.toRingHom.QuasiFinite
Algebra.exists_quasiFinite_mvPolynomial_of_relativeDimension_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/WeakRelativeNoetherNormalization.lean, line 1160. The attribute's comment: “The source's form, with d equal to the maximum Algebra.relativeDimension R S (Tag 00QD) of the dimensions of the fibres. Quasi-finiteness is Mathlib's RingHom.QuasiFinite, which asks only for finite fibres, so the finite type of the map is a separate conjunct.”.
Stacks Project, Tag 0GTG, in the source's form:
dis the maximum of the dimensions of the fibres ofSpec S → Spec R.
public theorem exists_quasiFinite_mvPolynomial_of_relativeDimension_eq
{R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
[Algebra.FiniteType R S] (d : ℕ)
(hd : Algebra.relativeDimension R S = (d : WithBot ℕ∞)) :
∃ φ : MvPolynomial (Fin d) R →ₐ[R] S,
φ.toRingHom.FiniteType ∧ φ.toRingHom.QuasiFinite
Sources
Section37.32 Bertini theorems#
Section 37.32 of the Stacks Project, Tag 0G4C. 4 tags here are carried by 43 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0G4D, a lemma
Tag 0G4D in the Stacks Project.
Algebra.isGeometricallyIrreducible_adjoin_linearCombination, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/Bertini.lean, line 821.
Let
K/kbe a finitely generated geometrically irreducible extension and letΩbe generated overKby algebraically independent elementsx₁, …, xₙ. Ifx₁, …, xₙ,∑ gᵢxᵢand∑ cᵢgᵢare algebraically independent overk, thenΩis geometrically irreducible over the subfield generated overkby thexᵢand∑ gᵢxᵢ.
theorem isGeometricallyIrreducible_adjoin_linearCombination
(k K Ω : Type u) [Field k] [Field K] [Field Ω]
[Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
(n : ℕ) (_hn : 0 < n) (x : Fin n → Ω) (g : Fin n → K)
(hgen : IntermediateField.adjoin K (Set.range x) = ⊤)
(hx : AlgebraicIndependent K x)
(hK : Algebra.IsGeometricallyIrreducible k K)
(hfg : (⊤ : IntermediateField k K).FG)
(c : Fin n → k)
(hind : AlgebraicIndependent k
(Sum.elim x (Bool.rec
(∑ i, algebraMap K Ω (g i) * x i)
(∑ i, algebraMap K Ω ((algebraMap k K (c i)) * g i))))) :
let ξ : Ω := ∑ i, algebraMap K Ω (g i) * x i
let F : IntermediateField k Ω :=
IntermediateField.adjoin k (Set.range x ∪ {ξ})
letI : Algebra F Ω := F.toSubalgebra.toAlgebra
Algebra.IsGeometricallyIrreducible F Ω
Tag 0G4E, a lemma
Tag 0G4E in the Stacks Project.
Algebra.exists_algebraicIndependent_linearCombinations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniAlgebraicIndependence.lean, line 333.
Let
Abe a domain of finite type over a fieldk, letn ≥ 2and letg : Fin n → A. If the common zero locus ofg 0andg 1has an irreducible component of dimensiondim A - 2, then there arec : Fin n → kfor which the variablesx₁, …, xₙ, the linear combination∑ gᵢxᵢand the constant∑ cᵢgᵢare algebraically independent overk.
public theorem exists_algebraicIndependent_linearCombinations
(k : Type u) (A : Type v) [Field k] [CommRing A] [IsDomain A] [Algebra k A]
[Algebra.FiniteType k A] {n : ℕ} (hn : 2 ≤ n) (g : Fin n → A)
(hcodim : ∃ p : Ideal A,
p ∈ (Ideal.span {g ⟨0, by omega⟩, g ⟨1, by omega⟩}).minimalPrimes ∧
ringKrullDim (A ⧸ p) + 2 = ringKrullDim A) :
∃ c : Fin n → k,
AlgebraicIndependent k
(Sum.elim (MvPolynomial.X : Fin n → MvPolynomial (Fin n) A)
(fun j : Fin 2 =>
if j = 0 then
∑ i : Fin n, MvPolynomial.C (g i) * MvPolynomial.X i
else
MvPolynomial.C (∑ i : Fin n, algebraMap k A (c i) * g i)))
Algebra.algebraicIndependent_linearCombination_of_codimTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniLinearCombinationCodimTwo.lean, line 90. The attribute's comment: “the variables and their linear combination, read in the ambient field”.
The variables and their linear combination are algebraically independent over the base field. Let
Abe a domain of finite type overk,n ≥ 2andg : Fin n → Asuch thatV(g₁, g₂)has an irreducible component of codimension two inSpec A. Then then + 1elementsx₁, …, xₙandξ = ∑ gᵢxᵢofΩare algebraically independent overk.
theorem algebraicIndependent_linearCombination_of_codimTwo
[IsDomain A] [Algebra.FiniteType k A] [IsFractionRing A K]
{n : ℕ} (hn : 2 ≤ n) (x : Fin n → Ω) (hx : AlgebraicIndependent K x) (g : Fin n → A)
(hcodim : ∃ p : Ideal A,
p ∈ (Ideal.span {g ⟨0, by omega⟩, g ⟨1, by omega⟩}).minimalPrimes ∧
ringKrullDim (A ⧸ p) + 2 = ringKrullDim A) :
AlgebraicIndependent k
(Sum.elim x fun _ : Unit => ∑ i, algebraMap K Ω (algebraMap A K (g i)) * x i)
Tag 0G4F, a lemma
Tag 0G4F in the Stacks Project.
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_ringKrullDim_quotient_add_two_eq_reducedChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartAlgebra.lean, line 126. The attribute's comment: “hypothesis (3) as the codimension datum of the chart statements”.
On a trivializing affine chart meeting
Z, the reduced chart ringAis a domain of finite type overk, and some minimal primepover the ideal generated by the images of the functions ofv₂andv₃satisfiesdim (A ⧸ p) + 2 = dim A.
theorem exists_ringKrullDim_quotient_add_two_eq_reducedChart (c : D.Chart)
(hZ : ((c.U : Set D.X) ∩ (h.Z : Set D.X)).Nonempty) :
letI := reducedChartAlgebra c.U
∃ p : Ideal (reducedChartRing c.U),
p ∈ (Ideal.span {Ideal.Quotient.mk _ (chartFunction c.triv h.v₂),
Ideal.Quotient.mk _ (chartFunction c.triv h.v₃)}).minimalPrimes ∧
ringKrullDim (reducedChartRing c.U ⧸ p) + 2 = ringKrullDim (reducedChartRing c.U)
Algebra.isGeometricallyIrreducible_universalDivisorChart_of_linearSubst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartChangeOfBasis.lean, line 326. The attribute's comment: “the generic fibre over a chart, for distinguished vectors of an arbitrary basis”.
The function field of the universal divisor over a chart is geometrically irreducible over the field generated by the parameters. This is
Algebra.isGeometricallyIrreducible_universalDivisorChartwith the parameters indexed by an arbitrary finite setσand its hypotheses imposed not onfitself but on the imagegoffunder an invertiblek-linear transformationbof the parameters.
theorem isGeometricallyIrreducible_universalDivisorChart_of_linearSubst (hn : 2 ≤ n)
(g : Fin (n + 1) → A) (hg : ∀ i, g i = ∑ j, algebraMap k A (b i j) * f j)
{w : A} (hw : w * g 0 = 1)
(hcompat : ∀ a : A, algebraMap K Ω (algebraMap A K a) =
universalDivisorChartMap A Ω f (C a))
(hK : Algebra.IsGeometricallyIrreducible k K)
(hcodim : ∃ p : Ideal A,
p ∈ (Ideal.span {g ⟨1, by omega⟩, g ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (A ⧸ p) + 2 = ringKrullDim A) :
letI F : IntermediateField k Ω :=
IntermediateField.adjoin k
(Set.range fun j : σ => universalDivisorChartMap A Ω f (X j))
letI : Algebra F Ω := F.toSubalgebra.toAlgebra
Algebra.IsGeometricallyIrreducible F Ω
Algebra.algebraicIndependent_universalDivisorChartMap_X_of_linearSubst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartChangeOfBasis.lean, line 360. The attribute's comment: “the dominance over the parameter space, for an arbitrary basis”.
The parameters of a chart are algebraically independent over the base field. This is
Algebra.algebraicIndependent_universalDivisorChartMap_Xwith the parameters indexed by an arbitrary finite set and its hypotheses imposed on the image offunder an invertiblek-linear transformation of the parameters.
theorem algebraicIndependent_universalDivisorChartMap_X_of_linearSubst (hn : 2 ≤ n)
(g : Fin (n + 1) → A) (hg : ∀ i, g i = ∑ j, algebraMap k A (b i j) * f j)
{w : A} (hw : w * g 0 = 1)
(hcompat : ∀ a : A, algebraMap K Ω (algebraMap A K a) =
universalDivisorChartMap A Ω f (C a))
(hcodim : ∃ p : Ideal A,
p ∈ (Ideal.span {g ⟨1, by omega⟩, g ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (A ⧸ p) + 2 = ringKrullDim A) :
AlgebraicIndependent k fun j : σ => universalDivisorChartMap A Ω f (X j)
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_mem_minimalPrimes_height_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartCodimension.lean, line 64. The attribute's comment: “hypothesis (3) read on a chart meeting Z, as an exact height”.
On a trivializing affine chart
Uthat meetsZ, the prime ofΓ(U, ⊤)cutting outZ ∩ Uis a minimal prime over the ideal generated by the functionsg₂, g₃ofv₂, v₃, and its height is exactly two.
theorem exists_mem_minimalPrimes_height_eq_two (c : D.Chart)
(hZ : ((c.U : Set D.X) ∩ (h.Z : Set D.X)).Nonempty) :
∃ p : Ideal Γ(c.U.toScheme, ⊤),
p ∈ (Ideal.span {chartFunction c.triv h.v₂, chartFunction c.triv h.v₃}).minimalPrimes ∧
p.height = 2
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_chart_isUnit_and_height_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartCodimension.lean, line 81. The attribute's comment: “hypothesis (3) on a single chart: an invertible first function and an exact height”.
There is a trivializing affine chart on which the function of
v₁is a unit and on which some minimal prime over the ideal generated by the functions ofv₂andv₃has height exactly two.
theorem exists_chart_isUnit_and_height_eq_two :
∃ c : D.Chart, IsUnit (chartFunction c.triv h.v₁) ∧
∃ p : Ideal Γ(c.U.toScheme, ⊤),
p ∈ (Ideal.span {chartFunction c.triv h.v₂, chartFunction c.triv h.v₃}).minimalPrimes ∧
p.height = 2
Stacks.Bertini.FamilyDivisors.Hypotheses.v₁_notMem_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartCodimension.lean, line 111. The attribute's comment: “v₁ is independent from v₂ and v₃”.
The vector
v₁is not in the span ofv₂andv₃.
theorem v₁_notMem_span : h.v₁ ∉ Submodule.span D.k {h.v₂, h.v₃}
Stacks.Bertini.FamilyDivisors.Hypotheses.linearIndependent_v₂_v₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartCodimension.lean, line 129. The attribute's comment: “v₂ and v₃ are independent”.
The vectors
v₂andv₃are linearly independent.
theorem linearIndependent_v₂_v₃ : LinearIndependent D.k ![h.v₂, h.v₃]
Stacks.Bertini.FamilyDivisors.Hypotheses.linearIndependent_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartCodimension.lean, line 151. The attribute's comment: “the three distinguished vectors are linearly independent”.
The three distinguished vectors
v₁, v₂, v₃of hypothesis (3) are linearly independent.
theorem linearIndependent_distinguished : LinearIndependent D.k ![h.v₁, h.v₂, h.v₃]
Stacks.Bertini.FamilyDivisors.Hypotheses.isGeometricallyIrreducible_chartRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartFractionField.lean, line 75. The attribute's comment: “hypothesis (2) read on a trivializing affine chart”.
The chart ring
Γ(U, ⊤)of a trivializing affine chart is geometrically irreducible overk.
theorem isGeometricallyIrreducible_chartRing (c : D.Chart) :
letI := chartAlgebra c.U
Algebra.IsGeometricallyIrreducible D.k Γ(c.U.toScheme, ⊤)
Stacks.Bertini.FamilyDivisors.Hypotheses.isGeometricallyIrreducible_reducedChartRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartFractionField.lean, line 95. The attribute's comment: “hypothesis (2) read on the reduced ring of a trivializing affine chart”.
The reduced chart ring
Γ(U, ⊤) ⧸ √0of a trivializing affine chart is geometrically irreducible overk.
theorem isGeometricallyIrreducible_reducedChartRing (c : D.Chart) :
letI := reducedChartAlgebra c.U
Algebra.IsGeometricallyIrreducible D.k (reducedChartRing c.U)
Stacks.Bertini.FamilyDivisors.Hypotheses.isGeometricallyIrreducible_reducedChartFractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartFractionField.lean, line 107. The attribute's comment: “hypothesis (2) as geometric irreducibility of the chart's fraction field”.
The fraction field of the reduced chart ring of a trivializing affine chart is geometrically irreducible over
k.
theorem isGeometricallyIrreducible_reducedChartFractionRing (c : D.Chart) :
letI := reducedChartAlgebra c.U
Algebra.IsGeometricallyIrreducible D.k (reducedChartFractionRing c.U)
Algebra.isGeometricallyIrreducible_universalDivisorChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartFunctionField.lean, line 432. The attribute's comment: “the generic fibre over a trivializing affine chart, in field-theoretic form”.
The function field of the universal divisor over a trivializing chart is geometrically irreducible over the field generated by the parameters.
Let
Abe a domain of finite type over a fieldkwith fraction fieldKgeometrically irreducible overk, letn ≥ 2and letf₀, …, fₙ ∈ Awithf₀invertible. If the common zero locus off₁andf₂has an irreducible component of codimension two inSpec A, then a fraction fieldΩof the chart ringA[x₀, …, xₙ]/(x₀f₀ + ⋯ + xₙfₙ)of the universal divisor is geometrically irreducible over the subfield generated overkby the images of the coordinatesx₀, …, xₙ. The hypothesishcompatsays that the two mapsA → K → ΩandA → A[x₀, …, xₙ] → Ωagree.
theorem isGeometricallyIrreducible_universalDivisorChart
(k A K Ω : Type u) [Field k] [CommRing A] [IsDomain A] [Algebra k A]
[Algebra.FiniteType k A] [Field K] [Algebra A K] [IsFractionRing A K] [Algebra k K]
[IsScalarTower k A K] [Field Ω] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
{n : ℕ} (hn : 2 ≤ n) (f : Fin (n + 1) → A) {u : A} (hu : u * f 0 = 1)
[Algebra (MvPolynomial (Fin (n + 1)) A ⧸ Ideal.span {universalLinearForm f}) Ω]
[IsFractionRing (MvPolynomial (Fin (n + 1)) A ⧸ Ideal.span {universalLinearForm f}) Ω]
(hcompat : ∀ a : A, algebraMap K Ω (algebraMap A K a) =
universalDivisorChartMap A Ω f (C a))
(hK : Algebra.IsGeometricallyIrreducible k K)
(hcodim : ∃ p : Ideal A,
p ∈ (Ideal.span {f ⟨1, by omega⟩, f ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (A ⧸ p) + 2 = ringKrullDim A) :
letI F : IntermediateField k Ω :=
IntermediateField.adjoin k
(Set.range fun j : Fin (n + 1) => universalDivisorChartMap A Ω f (X j))
letI : Algebra F Ω := F.toSubalgebra.toAlgebra
Algebra.IsGeometricallyIrreducible F Ω
Algebra.algebraicIndependent_universalDivisorChartMap_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartFunctionField.lean, line 463. The attribute's comment: “the dominance over the parameter space, read on a trivializing affine chart”.
The parameters of the chart are algebraically independent over the base field. In the situation of
Algebra.isGeometricallyIrreducible_universalDivisorChartthen + 1images of the coordinatesx₀, …, xₙin a fraction fieldΩof the chart ringA[x₀, …, xₙ]/(x₀f₀ + ⋯ + xₙfₙ)are algebraically independent overk; equivalently, the polynomial ringk[x₀, …, xₙ]injects intoΩ.
theorem algebraicIndependent_universalDivisorChartMap_X
(k A K Ω : Type u) [Field k] [CommRing A] [IsDomain A] [Algebra k A]
[Algebra.FiniteType k A] [Field K] [Algebra A K] [IsFractionRing A K] [Algebra k K]
[IsScalarTower k A K] [Field Ω] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
{n : ℕ} (hn : 2 ≤ n) (f : Fin (n + 1) → A) {u : A} (hu : u * f 0 = 1)
[Algebra (MvPolynomial (Fin (n + 1)) A ⧸ Ideal.span {universalLinearForm f}) Ω]
[IsFractionRing (MvPolynomial (Fin (n + 1)) A ⧸ Ideal.span {universalLinearForm f}) Ω]
(hcompat : ∀ a : A, algebraMap K Ω (algebraMap A K a) =
universalDivisorChartMap A Ω f (C a))
(hcodim : ∃ p : Ideal A,
p ∈ (Ideal.span {f ⟨1, by omega⟩, f ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (A ⧸ p) + 2 = ringKrullDim A) :
AlgebraicIndependent k fun j : Fin (n + 1) => universalDivisorChartMap A Ω f (X j)
Stacks.Bertini.FamilyDivisors.Hypotheses.isGeometricallyIrreducible_reducedChartDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartGenericFibre.lean, line 88. The attribute's comment: “the generic fibre over a chart, from the tag's own hypotheses”.
Let
Ωbe a fraction field of the chart ring of the universal divisor over the reduced chart ring of a trivializing affine chart, compatibly with the fraction fieldKof the chart's own domain. If an invertiblek-linear substitution of the parameters carries the chart equations to a tuplegwhose zeroth entry is a unit and whose first two entries carry the codimension datum, thenΩis geometrically irreducible over the subfield generated overkby the images of the parameters.
theorem isGeometricallyIrreducible_reducedChartDivisor (c : D.Chart) {m : ℕ}
(b : Matrix (Fin (m + 3)) D.basisIndex D.k) (b' : Matrix D.basisIndex (Fin (m + 3)) D.k)
(hbb' : b * b' = 1) (hb'b : b' * b = 1) (Ω : Type u) [Field Ω] [Algebra D.k Ω] :
letI := reducedChartAlgebra c.U
∀ [Algebra (reducedChartFractionRing c.U) Ω]
[IsScalarTower D.k (reducedChartFractionRing c.U) Ω]
[Algebra (reducedChartDivisorRing c) Ω] [IsFractionRing (reducedChartDivisorRing c) Ω]
(g : Fin (m + 3) → reducedChartRing c.U) (w : reducedChartRing c.U),
(∀ i, g i = ∑ j : D.basisIndex,
algebraMap D.k (reducedChartRing c.U) (b i j) * reducedChartEquation c j) →
w * g ⟨0, by omega⟩ = 1 →
(∃ q : Ideal (reducedChartRing c.U),
q ∈ (Ideal.span {g ⟨1, by omega⟩, g ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (reducedChartRing c.U ⧸ q) + 2 = ringKrullDim (reducedChartRing c.U)) →
(∀ a : reducedChartRing c.U,
algebraMap (reducedChartFractionRing c.U) Ω
(algebraMap (reducedChartRing c.U) (reducedChartFractionRing c.U) a) =
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.C a)) →
letI F : IntermediateField D.k Ω :=
IntermediateField.adjoin D.k
(Set.range fun j : D.basisIndex =>
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.X j))
letI : Algebra F Ω := F.toSubalgebra.toAlgebra
Algebra.IsGeometricallyIrreducible F Ω
Stacks.Bertini.FamilyDivisors.Hypotheses.algebraicIndependent_reducedChartDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartGenericFibre.lean, line 128. The attribute's comment: “the dominance over the parameter space, from the tag's own hypotheses”.
In the situation of
Stacks.Bertini.FamilyDivisors.Hypotheses.isGeometricallyIrreducible_reducedChartDivisorthe images of the parameters of the family inΩare algebraically independent overk.
theorem algebraicIndependent_reducedChartDivisor (c : D.Chart) {m : ℕ}
(b : Matrix (Fin (m + 3)) D.basisIndex D.k) (b' : Matrix D.basisIndex (Fin (m + 3)) D.k)
(hbb' : b * b' = 1) (hb'b : b' * b = 1) (Ω : Type u) [Field Ω] [Algebra D.k Ω] :
letI := reducedChartAlgebra c.U
∀ [Algebra (reducedChartFractionRing c.U) Ω]
[IsScalarTower D.k (reducedChartFractionRing c.U) Ω]
[Algebra (reducedChartDivisorRing c) Ω] [IsFractionRing (reducedChartDivisorRing c) Ω]
(g : Fin (m + 3) → reducedChartRing c.U) (w : reducedChartRing c.U),
(∀ i, g i = ∑ j : D.basisIndex,
algebraMap D.k (reducedChartRing c.U) (b i j) * reducedChartEquation c j) →
w * g ⟨0, by omega⟩ = 1 →
(∃ q : Ideal (reducedChartRing c.U),
q ∈ (Ideal.span {g ⟨1, by omega⟩, g ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (reducedChartRing c.U ⧸ q) + 2 = ringKrullDim (reducedChartRing c.U)) →
(∀ a : reducedChartRing c.U,
algebraMap (reducedChartFractionRing c.U) Ω
(algebraMap (reducedChartRing c.U) (reducedChartFractionRing c.U) a) =
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.C a)) →
AlgebraicIndependent D.k fun j : D.basisIndex =>
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.X j)
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_chart_generic_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartGenericFibre.lean, line 182. The attribute's comment: “the generic fibre and the dominance on a chart, from the tag's own hypotheses”.
There is a trivializing affine chart whose chart ring of the universal divisor is a domain and on which, for every fraction field
Ωof that ring compatible with the chart's own fraction field, the function field of the universal divisor is geometrically irreducible over the subfield generated by the parameters and the parameters are algebraically independent overk.
theorem exists_chart_generic_fibre :
∃ c : D.Chart,
IsDomain (reducedChartDivisorRing c) ∧
letI := reducedChartAlgebra c.U
∀ (Ω : Type u) [Field Ω] [Algebra D.k Ω] [Algebra (reducedChartFractionRing c.U) Ω]
[IsScalarTower D.k (reducedChartFractionRing c.U) Ω]
[Algebra (reducedChartDivisorRing c) Ω] [IsFractionRing (reducedChartDivisorRing c) Ω],
(∀ a : reducedChartRing c.U,
algebraMap (reducedChartFractionRing c.U) Ω
(algebraMap (reducedChartRing c.U) (reducedChartFractionRing c.U) a) =
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.C a)) →
(AlgebraicIndependent D.k fun j : D.basisIndex =>
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.X j)) ∧
letI F : IntermediateField D.k Ω :=
IntermediateField.adjoin D.k
(Set.range fun j : D.basisIndex =>
Algebra.universalDivisorChartMap (reducedChartRing c.U) Ω (reducedChartEquation c)
(MvPolynomial.X j))
letI : Algebra F Ω := F.toSubalgebra.toAlgebra
Algebra.IsGeometricallyIrreducible F Ω
Stacks.Bertini.FamilyDivisors.exists_surjective_ker_le_nilradical_reducedChartDivisorRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartReduction.lean, line 141. The attribute's comment: “the reduced chart ring of the universal divisor as the reduction of its chart ring”.
The reduced chart ring of the universal divisor is the reduction of its chart ring: there is a surjection from the chart ring onto the reduced chart ring with kernel inside the nilradical.
theorem exists_surjective_ker_le_nilradical_reducedChartDivisorRing (c : D.Chart) :
∃ Φ : chartDivisorRing c →+* reducedChartDivisorRing c,
Function.Surjective Φ ∧ RingHom.ker Φ ≤ nilradical (chartDivisorRing c)
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_chart_substitution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartSubstitution.lean, line 115. The attribute's comment: “hypothesis (3) as the substitution datum of the chart statements”.
There is a trivializing affine chart, an invertible pair of
k-matrices between the parameter index set of the family and{0, …, m + 2}, and a tuplegof elements of the reduced chart ring which is the image of the chart equations under that substitution, whose zeroth entry is invertible and whose first and second entries carry the codimension datum.
theorem exists_chart_substitution :
∃ (c : D.Chart) (m : ℕ) (b : Matrix (Fin (m + 3)) D.basisIndex D.k)
(b' : Matrix D.basisIndex (Fin (m + 3)) D.k),
b * b' = 1 ∧ b' * b = 1 ∧
letI := reducedChartAlgebra c.U
∃ (g : Fin (m + 3) → reducedChartRing c.U) (w : reducedChartRing c.U),
(∀ i, g i = ∑ j : D.basisIndex,
algebraMap D.k (reducedChartRing c.U) (b i j) * reducedChartEquation c j) ∧
w * g ⟨0, by omega⟩ = 1 ∧
∃ q : Ideal (reducedChartRing c.U),
q ∈ (Ideal.span {g ⟨1, by omega⟩, g ⟨2, by omega⟩}).minimalPrimes ∧
ringKrullDim (reducedChartRing c.U ⧸ q) + 2 =
ringKrullDim (reducedChartRing c.U)
Stacks.Bertini.FamilyDivisors.isIrreducible_supportSet_universalDivisor_of_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniChartSupport.lean, line 314. The attribute's comment: “the passage from the trivializing charts to the universal divisor”.
The universal divisor is irreducible, for a cover closed under refining intersections. Same as
Stacks.Bertini.FamilyDivisors.isIrreducible_supportSet_universalDivisor, but with the two topological hypotheses replaced by the requirement that the intersection of any two members of the cover contain a member: the parts ofH_univover the charts are then automatically nonempty, because each is irreducible, and the part over a member insideUᵢ ∩ Uⱼwitnesses that the parts overUᵢand overUⱼmeet.This is the shape in which the union argument of [Stacks, Tag 0G4F] is run: the cover is the family of all affine opens of
XtrivializingLon which the hypotheses hold, which is closed under passing to a smaller affine open.
theorem isIrreducible_supportSet_universalDivisor_of_directed {ι : Sort*} [Nonempty ι]
(W : ι → D.X.Opens) (hW : ⨆ i, W i = ⊤) (hdir : ∀ i j, ∃ k, W k ≤ W i ⊓ W j)
[∀ i, IsAffine (W i).toScheme] [∀ i, IsNoetherianRing Γ((W i).toScheme, ⊤)]
(hnil : ∀ i, (nilradical Γ((W i).toScheme, ⊤)).IsPrime)
(eW : ∀ i, D.restrictedModule (W i) ≅ SheafOfModules.unit (W i).toScheme.ringCatSheaf)
(hf : ∀ i, ∃ j, ¬ IsNilpotent (D.chartEquation (eW i) j))
(hcodim : ∀ i, ∀ p ∈ (Ideal.span (Set.range (D.chartEquation (eW i)))).minimalPrimes,
2 ≤ p.height) :
IsIrreducible D.universalDivisor.supportSet
Stacks.Bertini.FamilyDivisors.commonZeroSet, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniCommonZeroSet.lean, line 102. The attribute's comment: “the common zero locus of the linear system”.
The common zero locus
Z = ⋂_{v ∈ V} H_vof the linear system. This is the closed set on which hypothesis (4) of [Stacks, Tag 0G4F] imposes a codimension bound.
def commonZeroSet : Set D.X
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_basis_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniDistinguishedBasis.lean, line 52. The attribute's comment: “the three distinguished vectors as the first members of a basis”.
The linear system has a basis indexed by
Fin (m + 3), for somem, whose members at0, 1, 2are the three distinguished vectorsv₁, v₂, v₃of hypothesis (3).
theorem exists_basis_distinguished :
∃ (m : ℕ) (W : Module.Basis (Fin (m + 3)) D.k D.V),
W ⟨0, by omega⟩ = h.v₁ ∧ W ⟨1, by omega⟩ = h.v₂ ∧ W ⟨2, by omega⟩ = h.v₃
Stacks.Bertini.FamilyDivisors.Hypotheses, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniHypotheses.lean, line 131. The attribute's comment: “the hypotheses”.
The hypotheses of the Bertini irreducibility theorem on the standing situation of the Bertini theorems:
Xof finite type and geometrically irreducible overk, an irreducible componentZofH_{v₂} ∩ H_{v₃}of codimension exactly two not contained inH_{v₁}, and a codimension-two condition on the common zero locus of the linear system.
structure Hypotheses (D : FamilyDivisors.{u, v})
Stacks.Bertini.FamilyDivisors.Hypotheses.two_le_height_chartEquation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniHypotheses.lean, line 183. The attribute's comment: “hypothesis (4) read on a trivializing affine chart”.
Hypothesis (4), read on a chart. Every minimal prime over the ideal
(f₁, …, f_r)generated by the functions representing the sectionsψ(vᵢ)on a trivializing affine chart has height at least two.
theorem two_le_height_chartEquation (c : D.Chart)
{q : Ideal Γ(c.U.toScheme, ⊤)}
(hq : q ∈ (Ideal.span (Set.range (D.chartEquation c.triv))).minimalPrimes) :
2 ≤ q.height
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_not_isNilpotent_chartEquation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniHypotheses.lean, line 193. The attribute's comment: “hypothesis (3) read on a trivializing affine chart”.
Hypothesis (3), read on a chart. On every trivializing affine chart some basis vector is represented by a function that is not nilpotent.
theorem exists_not_isNilpotent_chartEquation (c : D.Chart) :
∃ j, ¬ IsNilpotent (D.chartEquation c.triv j)
Stacks.Bertini.FamilyDivisors.Hypotheses.isIrreducible_supportSet_universalDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniHypotheses.lean, line 221. The attribute's comment: “the irreducibility of the universal divisor, from the tag's own hypotheses”.
H_univis irreducible under the hypotheses of the Bertini irreducibility theorem.
theorem isIrreducible_supportSet_universalDivisor :
IsIrreducible D.universalDivisor.supportSet
Stacks.Bertini.FamilyDivisors.Hypotheses.irreducibleSpace_universalDivisorScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniHypotheses.lean, line 233. The attribute's comment: “the universal divisor as an irreducible scheme, from the tag's own hypotheses”.
H_univis an irreducible scheme under the hypotheses of the Bertini irreducibility theorem.
theorem irreducibleSpace_universalDivisorScheme :
IrreducibleSpace D.universalDivisor.subscheme
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_chart_isUnit_chartFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniInvertibleChart.lean, line 81. The attribute's comment: “hypothesis (3) as an invertible section on a chart meeting Z”.
There is a trivializing affine chart meeting
Zon which the function ofv₁is invertible.
theorem exists_chart_isUnit_chartFunction :
∃ c : D.Chart, ((c.U : Set D.X) ∩ (h.Z : Set D.X)).Nonempty ∧
IsUnit (chartFunction c.triv h.v₁)
Stacks.Bertini.FamilyDivisors.isFractionRing_parameterBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniParameterFunctionField.lean, line 105. The attribute's comment: “the residue field at the generic point of the parameter space”.
The function field
κ(η)of the parameter space𝔸^r_kis a fraction field of the polynomial ring in the parameters.
theorem isFractionRing_parameterBase :
letI := D.parameterBaseFunctionFieldAlgebra
IsFractionRing (MvPolynomial D.basisIndex D.k) D.parameterBase.functionField
Stacks.Bertini.FamilyDivisors.adjoin_range_coord_parameterBase_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniParameterFunctionField.lean, line 123. The attribute's comment: “the generic point of the parameter space generates the residue field”.
The residue field
κ(η)at the generic point of𝔸^r_kis generated overkas a field by the images of the coordinates.
theorem adjoin_range_coord_parameterBase_eq_top :
letI := D.parameterBaseFunctionFieldAlgebra
letI := D.parameterBaseFunctionFieldBaseAlgebra
IntermediateField.adjoin D.k
(Set.range fun i : D.basisIndex =>
algebraMap (MvPolynomial D.basisIndex D.k) D.parameterBase.functionField
(MvPolynomial.X i)) = ⊤
Stacks.Bertini.FamilyDivisors.Hypotheses.exists_chart_isFractionRing_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorFunctionField.lean, line 116. The attribute's comment: “the residue field of the universal divisor at its generic point”.
Under the hypotheses of the family,
H_univis irreducible and there is a chartc, whose part ofH_univcontains the generic point, such that the residue field ofH_univat its generic point is a fraction field of the chart ring of the universal divisor overc, with structure map sending the reduction of a sectionaover the chart to the value ofaat the generic point.
theorem exists_chart_isFractionRing_residueField :
haveI := h.irreducibleSpace_universalDivisorScheme
∃ (c : D.Chart) (hξ : genericPoint D.universalDivisorScheme ∈ D.chartDivisorOpen c.U),
∃ _ : Algebra (reducedChartDivisorRing c)
(D.universalDivisorScheme.residueField (genericPoint D.universalDivisorScheme)),
IsFractionRing (reducedChartDivisorRing c)
(D.universalDivisorScheme.residueField
(genericPoint D.universalDivisorScheme)) ∧
∀ a : Γ(D.universalDivisorScheme, D.chartDivisorOpen c.U),
algebraMap (reducedChartDivisorRing c)
(D.universalDivisorScheme.residueField (genericPoint D.universalDivisorScheme))
(reducedChartDivisorReduction c (D.chartSubschemeΓEquiv c.U c.triv a)) =
D.universalDivisorScheme.evaluation (D.chartDivisorOpen c.U)
(genericPoint D.universalDivisorScheme) hξ a
Stacks.Bertini.FamilyDivisors.isFractionRing_parameterSpecResidueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorGenericFibre.lean, line 120. The attribute's comment: “the residue field at the generic point of the parameter space, on Spec Γ”.
The residue field of
Spec Γ(𝔸^r_k, ⊤)at its generic point is a fraction field of the polynomial ring in the parameters:κ(η) = k(xⱼ).
theorem isFractionRing_parameterSpecResidueField :
letI := D.parameterSpecResidueFieldAlgebra
IsFractionRing (MvPolynomial D.basisIndex D.k) D.parameterSpecResidueField
Stacks.Bertini.FamilyDivisors.adjoin_range_parameterSpecResidueField_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorGenericFibre.lean, line 140. The attribute's comment: “the coordinates generate the residue field at the generic point of 𝔸^r_k”.
κ(η)is generated overkby the images of the coordinates.
theorem adjoin_range_parameterSpecResidueField_eq_top :
letI := D.parameterSpecResidueFieldAlgebra
letI := D.parameterSpecResidueFieldBaseAlgebra
IntermediateField.adjoin D.k
(Set.range fun j : D.basisIndex =>
algebraMap (MvPolynomial D.basisIndex D.k) D.parameterSpecResidueField
(MvPolynomial.X j)) = ⊤
Stacks.Bertini.FamilyDivisors.Hypotheses.isGeometricallyIrreducible_residueField_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorGenericFibre.lean, line 231. The attribute's comment: “the generic fibre, read on the residue field of the universal divisor”.
The residue field of
H_univat its generic point is geometrically irreducible overκ(η).
theorem isGeometricallyIrreducible_residueField_genericPoint :
haveI := h.irreducibleSpace_universalDivisorScheme
letI := residueFieldAlgebraOfEq (D.universalFamily ≫ D.parameterBase.isoSpec.hom)
(comp_isoSpec_genericPoint_eq D.universalFamily h.base_genericPoint_universalFamily)
Algebra.IsGeometricallyIrreducible D.parameterSpecResidueField
(D.universalDivisorScheme.residueField (genericPoint D.universalDivisorScheme))
Stacks.Bertini.FamilyDivisors.Hypotheses.geometricallyIrreducible_fiber_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorGenericFibre.lean, line 315. The attribute's comment: “the generic fibre of the universal family”. References: SGA 7 XVIII (6.1.6.1), “Case s = 1 of 6.1.6.1”.
The generic fibre of the universal family is geometrically irreducible.
theorem geometricallyIrreducible_fiber_genericPoint :
haveI := h.irreducibleSpace_universalDivisorScheme
GeometricallyIrreducible
(D.universalFamily.fiberToSpecResidueField (genericPoint D.parameterBase))
Stacks.Bertini.FamilyDivisors.Hypotheses.forGeneral_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorGenericFibre.lean, line 335. References: SGA 7 XVIII (6.1.6.1), “special case”.
Let
Xbe a scheme of finite type over a fieldk, geometrically irreducible overk, letLbe an invertible module onXand letV ⊂ Γ(X, L)be a finite dimensional linear system. Assume there arev₁, v₂, v₃ ∈ Vand an irreducible componentZofH_{v₂} ∩ H_{v₃}withZ ⊄ H_{v₁}andcodim(Z, X) = 2, and assume every irreducible closed subset of the common zero locus ofVhas codimension at least two inX. Then for generalv ∈ V ⊗_k k'the divisorH_vis geometrically irreducible overk': there is one nonempty openU ⊂ 𝔸^r_k, defined overk, such thatH_vis geometrically irreducible overk'for every field extensionk'/kand everyk'-point ofU.
theorem forGeneral_geometricallyIrreducible :
D.ForGeneral (fun K _ _ w =>
∀ a : Fin (Module.finrank D.k D.V) → K,
w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
GeometricallyIrreducible
((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))
Algebra.isIrreducible_zeroLocus_universalLinearForm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorIrreducible.lean, line 747. The attribute's comment: “irreducibility of the universal divisor over an affine chart”.
The universal divisor over an affine chart is irreducible. Let
Abe a Noetherian domain andf₁, …, f_r ∈ Awithf₁ ≠ 0. If every irreducible component ofV(f₁, …, f_r)has codimension at least two inSpec A, then the zero locus ofx₁f₁ + ⋯ + x_rf_rinSpec A[x₁, …, x_r]is irreducible.This is the irreducibility of
H_Uin the proof of [Stacks, Tag 0G4F]; see the module docstring for what the source deduces from it and what is not formalized here.
theorem isIrreducible_zeroLocus_universalLinearForm (hf : f 0 ≠ 0)
(hcodim : ∀ p ∈ (Ideal.span (Set.range f)).minimalPrimes, 2 ≤ p.height) :
IsIrreducible (PrimeSpectrum.zeroLocus {universalLinearForm f} :
Set (PrimeSpectrum (MvPolynomial (Fin (n + 1)) A)))
Algebra.isIrreducible_zeroLocus_linearForm_of_isPrime_nilradical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalDivisorIrreducible.lean, line 855. The attribute's comment: “the reduction step and the irreducibility of the universal divisor over a chart”.
The universal divisor over an affine chart is irreducible, without a reducedness hypothesis. Let
Abe a Noetherian ring whose nilradical is prime — equivalently, withSpec Airreducible — letσbe a finite index set and letf : σ → Abe a family withf i₀not nilpotent for some indexi₀. If every irreducible component of the common zero locusV(f)has codimension at least two inSpec A, then the zero locus of∑ᵢ fᵢxᵢinSpec A[xᵢ : i ∈ σ]is irreducible.This is the reduction step at the beginning of the proof of [Stacks, Tag 0G4F], carried out on a chart: the source replaces
Xby its reduction, which changes neither the topology ofXnor that of the universal divisor. HereAis replaced byA / √0, which is a Noetherian domain, andAlgebra.isIrreducible_zeroLocus_linearFormis applied there; the comparison mapSpec (A/√0)[xᵢ] → Spec A[xᵢ]is surjective because its kernel consists of nilpotents, so the two zero loci are homeomorphic, and heights and minimal primes are unchanged byIdeal.le_height_of_mem_minimalPrimes_map_quotientMk.
theorem isIrreducible_zeroLocus_linearForm_of_isPrime_nilradical
(hnil : (nilradical A).IsPrime) {σ : Type v} [Fintype σ] (f : σ → A) {i₀ : σ}
(hf : ¬ IsNilpotent (f i₀))
(hcodim : ∀ p ∈ (Ideal.span (Set.range f)).minimalPrimes, 2 ≤ p.height) :
IsIrreducible (PrimeSpectrum.zeroLocus {∑ i, C (f i) * X i} :
Set (PrimeSpectrum (MvPolynomial σ A)))
Stacks.Bertini.FamilyDivisors.Hypotheses.isDominant_universalFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniUniversalFamilyDominance.lean, line 153. The attribute's comment: “the dominance of the universal family over the parameter space”.
Under the hypotheses of the family, the universal family
H_univ → 𝔸^r_kis dominant.
theorem isDominant_universalFamily : IsDominant D.universalFamily
Tag 0G4G, a remark
Tag 0G4G in the Stacks Project.
Stacks.Bertini.FamilyDivisors.exists_smooth_irreducibleSpace_specializedDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniSmoothIrreducibleMember.lean, line 425. The attribute's comment: “for an arbitrary finite dimensional linear system with phi_(L, psi) a closed immersion: the hyperplane section is H_v over k itself”.
[Stacks, Tag 0G4G] for an arbitrary linear system. Let
kbe an algebraically closed field and letX ⊂ 𝐏^n_kbe smooth and irreducible of dimension≥ 2. Then there is a hyperplaneH ⊂ 𝐏^n_ksuch thatX ∩ His smooth and irreducible. The tag as the source states it, for a closed subscheme ofℙⁿ_k, isStacks.Bertini.ProjectiveSubscheme.exists_hyperplane_smooth_irreducibleSpace.The remark works in the standing situation of [Stacks, Tag 0G47] with
V = k T_0 ⊕ … ⊕ k T_n,L = 𝒪_X(1)andψthe restriction of the coordinates toX; the hyperplane attached tov ∈ VisH_vandX ∩ H_vis the divisorZ(ψ(v)), which overkitself isStacks.Bertini.FamilyDivisors.specializedDivisorat the coordinate tuple ofv. The inclusionX ⊂ 𝐏^n_kis read as the remark reads it when it invokes [Stacks, Tag 0FD6]:ψgeneratesL(hypothesis (2) there) and the morphismφ_{L,ψ} : X → 𝐏(V)it determines is an immersion (hypothesis (3) there, at every basis, equivalently at one byStacks.Bertini.FamilyDivisors.isImmersive_congr_basis'), together with properness ofXoverk, which says that the immersion is a closed one. This is a generalization:Vmay be any finite dimensional linear system,ψneed not be injective. Nothing else about the embedding is assumed: ampleness ofL, which Enriques–Severi–Zariski needs, is derived byStacks.Bertini.FamilyDivisors.isAmple_of_isImmersive. "Of dimension≥ 2" is2 ≤ dim X, the Krull dimension of the underlying space.The conclusion asserts in addition
ψ(v) ≠ 0, that isX ⊄ H_v: the hyperplane is honest andX ∩ H_vis a genuine hyperplane section, not the whole ofX.The proof is the remark's: smoothness of the general member is [Stacks, Tag 0FD6], connectedness is Enriques–Severi–Zariski in the form [Stacks, Tag 0FD9], and a connected scheme smooth over a field is irreducible.
theorem exists_smooth_irreducibleSpace_specializedDivisor [IsAlgClosed D.k] [Smooth D.toBase]
[IsProper D.toBase] [IrreducibleSpace D.X] (hgen : D.Generates)
(himm : ∀ (m : ℕ) (b : Module.Basis (Fin (m + 1)) D.k D.V),
D.IsImmersive b (D.generatesBy_basis hgen b))
(hdim : (2 : WithBot ℕ∞) ≤ topologicalKrullDim D.X) :
∃ c : Fin (Module.finrank D.k D.V) → D.k,
D.sectionOf (∑ i, c i • D.basis i) ≠ 0 ∧
Smooth ((D.specializedDivisor D.k c).subschemeι ≫ D.baseChangeToSpec D.k) ∧
IrreducibleSpace (D.specializedDivisor D.k c).subscheme
Stacks.Bertini.ProjectiveSubscheme.exists_hyperplane_smooth_irreducibleSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniSmoothIrreducibleMember.lean, line 617.
[Stacks, Tag 0G4G]. Let
kbe an algebraically closed field and letX ⊂ 𝐏^n_kbe smooth and irreducible of dimension≥ 2. Then there is a hyperplaneH ⊂ 𝐏^n_ksuch thatX ∩ His smooth and irreducible.
X ⊂ 𝐏^n_kis a closed immersioni : X → ℙⁿ_k, andXis smooth overkthrough it. A hyperplane isH = Z(∑ⱼ cⱼ Tⱼ)for a nonzeroc ∈ kⁿ⁺¹, the zero scheme of a nonzero linear form in the homogeneous coordinatesT_0, …, T_nof𝒪(1)(Stacks.AlgebraicGeometry.ProjectiveSpaceSectionMultiplication.hyperplane), andX ∩ His its scheme-theoretic inverse imageH.comap i. "Of dimension≥ 2" is2 ≤ dim X.The proof is the remark's: smoothness of the general hyperplane section is [Stacks, Tag 0FD6], connectedness is Enriques–Severi–Zariski in the form [Stacks, Tag 0FD9], and a connected scheme smooth over a field is irreducible (
Stacks.Bertini.FamilyDivisors.exists_smooth_irreducibleSpace_divisor, applied to the standing situationStacks.Bertini.ProjectiveSubscheme.familyof the remark).
theorem exists_hyperplane_smooth_irreducibleSpace [IsAlgClosed k] [IsClosedImmersion i]
[Smooth (i ≫ pullback.fst (terminal.from (Spec (.of k)))
(terminal.from (projectiveSpaceAtUniverse.{u} n)))]
[IrreducibleSpace X] (hdim : (2 : WithBot ℕ∞) ≤ topologicalKrullDim X) :
∃ c : Fin (n + 1) → k, c ≠ 0 ∧
let H := Stacks.AlgebraicGeometry.ProjectiveSpaceSectionMultiplication.hyperplane n
(Spec (.of k))
(Stacks.Divisors.sectionsOfTop (projectiveSpaceTwistingSheaf n (Spec (.of k)))
(∑ j, (pullback.fst (terminal.from (Spec (.of k)))
(terminal.from (projectiveSpaceAtUniverse.{u} n))).appTop
((Scheme.ΓSpecIso (.of k)).inv (c j)) •
pullbackGlobalSections (projectiveSpaceOver.toIntegralAtUniverse n (Spec (.of k)))
(twistingSheafAtUniverse.{u} n)
(Stacks.TwistPullbackPinned.coordGlobalSection.{u} n j)))
Smooth ((H.comap i).subschemeι ≫ i ≫ pullback.fst (terminal.from (Spec (.of k)))
(terminal.from (projectiveSpaceAtUniverse.{u} n))) ∧
IrreducibleSpace (H.comap i).subscheme
Sources
Section37.33 Theorem of the cube#
Section 37.33 of the Stacks Project, Tag 0BEZ. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BDP, a lemma
Tag 0BDP in the Stacks Project.
AlgebraicGeometry.hasDescentLocus_of_flat_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DescentLocusRepresentable.lean, line 47.
Stacks Tag 0BDP. Let
f : X ⟶ Sbe a flat, proper morphism of finite presentation andEa finite locally free𝒪_X-module. Assume that𝒪_T ⟶ p_*𝒪_{X_T}is an isomorphism for everyg : T ⟶ S, wherep : X_T = X ×_S T ⟶ T. Then there is an immersion of finite presentationj : Z ⟶ Ssuch thatg : T ⟶ Sfactors throughZif and only if there is a finite locally free𝒪_T-moduleNwithp^*N ≅ q^*E,q : X_T ⟶ Xthe projection.
theorem hasDescentLocus_of_flat_of_isProper {X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [IsProper f]
(hfp : FinitePresentation f)
(hO : ∀ {T : Scheme.{u}} (g : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f g).toLRSHom.toShHom))
(E : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
[hE : SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] :
HasDescentLocus f E
Tag 0EX7, a lemma
Tag 0EX7 in the Stacks Project.
AlgebraicGeometry.exists_finiteLocallyFree_iso_of_fiberwiseFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FiberwiseFreeReducedBase.lean, line 218. The attribute's comment: “assuming the representability of the descent locus of Tag 0BDP”.
Stacks Tag 0EX7, reduced to representability of the descent condition. A finite locally free module on
Xwhose restriction to every fibre offis free of finite rank is the pullback of a finite locally free module on the reduced baseS, provided the descent condition for it is represented — that is, provided the conclusion of Stacks Tag 0BDP holds forfandE.Tag 0BDP's hypotheses on
f— flatness, properness, finite presentation, and invariance of the structure sheaf under pushforward along every base change — enter only through that representability, and so do not appear.
theorem exists_finiteLocallyFree_iso_of_fiberwiseFree {X S : Scheme.{u}} (f : X ⟶ S)
(E : _root_.SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
(h0BDP : HasDescentLocus f E) [IsReduced S]
(hfiber : ∀ s : S, ∃ r : ℕ,
Nonempty ((modulePullback
(pullback.fst f (S.fromSpecResidueField s)).toLRSHom.toShHom).obj E ≅
_root_.SheafOfModules.free (ULift.{u} (Fin r)))) :
∃ N : _root_.SheafOfModules.{u} (structureSheafRing S.toRingedSpace),
SheafOfModules.IsFiniteLocallyFree.{u, u, u} N ∧
Nonempty ((modulePullback f.toLRSHom.toShHom).obj N ≅ E)
AlgebraicGeometry.exists_finiteLocallyFree_iso_of_fiberwiseFree_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FiberwiseFreeReducedBaseUnconditional.lean, line 39.
Stacks Tag 0EX7. Let
f : X ⟶ Sbe a flat, proper morphism of finite presentation such that𝒪_S ⟶ f_*𝒪_Xis an isomorphism and remains so after arbitrary base change. LetEbe a finite locally free𝒪_X-module such that (1)E|_{X_s} ≅ 𝒪_{X_s}^{⊕ r_s}for everys ∈ S, and (2)Sis reduced. ThenE ≅ f^*Nfor a finite locally free𝒪_S-moduleN.
theorem exists_finiteLocallyFree_iso_of_fiberwiseFree_of_isReduced {X S : Scheme.{u}}
(f : X ⟶ S) [Flat f] [IsProper f] (hfp : FinitePresentation f)
(hO : ∀ {T : Scheme.{u}} (g : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f g).toLRSHom.toShHom))
(E : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
[SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
(hfiber : ∀ s : S, ∃ r : ℕ,
Nonempty ((modulePullback
(pullback.fst f (S.fromSpecResidueField s)).toLRSHom.toShHom).obj E ≅
SheafOfModules.free (ULift.{u} (Fin r))))
[IsReduced S] :
∃ N : SheafOfModules.{u} (structureSheafRing S.toRingedSpace),
SheafOfModules.IsFiniteLocallyFree.{u, u, u} N ∧
Nonempty ((modulePullback f.toLRSHom.toShHom).obj N ≅ E)
Tag 0EX8, a lemma
Tag 0EX8 in the Stacks Project.
AlgebraicGeometry.ValuativeTriviality.isTrivial_of_isTrivial_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DescentLocusValuationRing.lean, line 828.
[Stacks, Tag 0EX8]. Let
f : X ⟶ Spec Abe a proper flat morphism of finite presentation over a valuation ringAwith fraction fieldK, and letLbe an invertible𝒪_X-module. Assume thatLis trivial on the generic fibreX_K, that the closed fibre is integral, and thatK = H⁰(X_K, 𝒪_{X_K}). ThenLis trivial.
theorem isTrivial_of_isTrivial_genericFiber
[ValuationRing A] (K : Type u) [Field K] [Algebra A K] [IsFractionRing A K]
[IsProper f] [Flat f] [LocallyOfFinitePresentation f]
(L : X.Modules) [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
(hgen : SheafOfModules.IsTrivial
(pullback f (Spec.map (CommRingCat.ofHom (algebraMap A K)))).presheaf
(pullback f (Spec.map (CommRingCat.ofHom (algebraMap A K)))).ringCatSheaf.2
((modulePullback (pullback.fst f
(Spec.map (CommRingCat.ofHom (algebraMap A K)))).toLRSHom.toShHom).obj L))
[IsIntegral (f.fiber (IsLocalRing.closedPoint A))]
(hΓ : Function.Bijective
(pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A K)))).appTop.hom) :
SheafOfModules.IsTrivial X.presheaf X.ringCatSheaf.2 L
Tag 0BF0, a lemma
Tag 0BF0 in the Stacks Project.
AlgebraicGeometry.IsDescentLocus.isClosedImmersion_hom_of_geometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DescentLocusClosedness.lean, line 167.
[Stacks, Tag 0BF0]. Let
f : X ⟶ Sbe flat, proper and of finite presentation, with𝒪_T ⟶ f_{T,*}𝒪_{X_T}an isomorphism for every base changeT ⟶ S, letEbe an invertible𝒪_X-module, and let the geometric fibres offbe integral (hgeom:X ×_S Spec kis integral for every algebraically closed fieldkandSpec k ⟶ S). Then every descent locusZofEoverf(Tag 0BDP) is closed inS: its structure morphism is a closed immersion.
theorem IsDescentLocus.isClosedImmersion_hom_of_geometricallyIntegral
{X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
(hO : ∀ {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f a).toLRSHom.toShHom))
(E : X.Modules) [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 E]
(hgeom : ∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (.of k) ⟶ S),
IsIntegral (pullback f s))
{Z : Over S} (hZ : IsDescentLocus f E Z) :
IsClosedImmersion Z.hom
Tag 0BF1, a lemma
Tag 0BF1 in the Stacks Project.
AlgebraicGeometry.exists_open_descendsFromBase_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescentLocusComparison0BF1.lean, line 253.
Stacks Tag 0BF1. Let
f : X ⟶ Sandf' : X' ⟶ Ssatisfy the hypotheses of [Stacks, Tag 0BDP] — flat, proper, of finite presentation, with𝒪_T ⟶ p_* 𝒪_{X_T}an isomorphism after every base changeT ⟶ S— and leti : X' ⟶ Xbe a morphism overS,Lan invertible𝒪_X-module andL' = i^* L. Lets ∈ Sbe a point of the descent locusZof(f, L)at whichH¹(X_s, 𝒪) → H¹(X'_s, 𝒪)is injective. ThenZ ∩ U = Z' ∩ Ufor an open neighbourhoodUofs, whereZ'is the descent locus of(f', L').Rendering. The locus
Zof Tag 0BDP is the subscheme representing the descent conditionAlgebraicGeometry.DescendsFromBase f L(a morphismg : T ⟶ Sfactors throughZexactly whenLpulled back toX ×_S Tcomes from a finite locally free module onT), and likewiseZ'for(f', L'). The statement is written through the functors these subschemes represent, which determine them:s ∈ ZisDescendsFromBase f L (S.fromSpecResidueField s), andZ ∩ U = Z' ∩ Uis the equivalence of the two descent conditions for everyg : T ⟶ Swith image inU. The fibre mapX'_s ⟶ X_sispullback.mapofi, and the map onH¹is the pullback map of [Stacks, Tag 01FA] on the structure sheaf, read inH¹(X'_s, 𝒪_{X'_s})through the canonical(X'_s ⟶ X_s)^* 𝒪_{X_s} ≅ 𝒪_{X'_s}. The containmentZ ⊆ Z'isdescendsFromBase_modulePullback_of_comp; the same statement for given representing objectsZ,Z'isAlgebraicGeometry.IsDescentLocus.exists_open_factorsThrough_iff.
theorem exists_open_descendsFromBase_iff {X X' S : Scheme.{u}} (f : X ⟶ S) (f' : X' ⟶ S)
(i : X' ⟶ X) (hi : i ≫ f = f')
[Flat f] [IsProper f] (hfp : FinitePresentation f)
(hfO : ∀ {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f a).toLRSHom.toShHom))
[Flat f'] [IsProper f'] (hfp' : FinitePresentation f')
(hfO' : ∀ {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f' a).toLRSHom.toShHom))
(L : X.Modules) [Stacks.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
(s : S) (hs : DescendsFromBase f L (S.fromSpecResidueField s))
(hH1 : Function.Injective (Stacks.Cohomology.moduleCohomologyPullbackMap
(pullback.map f' (S.fromSpecResidueField s) f (S.fromSpecResidueField s) i (𝟙 _) (𝟙 _)
(by rw [Category.comp_id, hi])
(by rw [Category.comp_id, Category.id_comp])).toLRSHom.toShHom
1 (SheafOfModules.unit (pullback f (S.fromSpecResidueField s)).ringCatSheaf) ≫
(Stacks.Cohomology.moduleCohomologyAlong
(pullback.map f' (S.fromSpecResidueField s) f (S.fromSpecResidueField s) i (𝟙 _) (𝟙 _)
(by rw [Category.comp_id, hi])
(by rw [Category.comp_id, Category.id_comp])).toLRSHom.toShHom 1).map
(Scheme.Modules.pullbackUnitIso
(pullback.map f' (S.fromSpecResidueField s) f (S.fromSpecResidueField s) i (𝟙 _)
(𝟙 _) (by rw [Category.comp_id, hi])
(by rw [Category.comp_id, Category.id_comp]))).hom)) :
∃ U : S.Opens, s ∈ U ∧ ∀ {T : Scheme.{u}} (g : T ⟶ S), Set.range g.base ⊆ U →
(DescendsFromBase f L g ↔ DescendsFromBase f' ((Scheme.Modules.pullback i).obj L) g)
Tag 0BF2, a lemma
Tag 0BF2 in the Stacks Project.
AlgebraicGeometry.IsDescentLocus.exists_factorsThrough_iff_forall_of_injective_H1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DescentLocusIntersection.lean, line 407.
[Stacks, Tag 0BF2]. Let
f : X ⟶ Sand thei k ≫ f : Y k ⟶ S(kin a finite type) be flat, proper and of finite presentation with𝒪_T ⟶ p_{T,*}𝒪an isomorphism after every base changeT ⟶ S, the hypotheses of Tag 0BDP. Letℒbe an invertible𝒪_X-module,ℒ_kits pullback toY k, andZ,Z_kdescent loci (Tag 0BDP) ofℒoverfand ofℒ_koveri k ≫ f. Ifs ∈ ZandH¹(X_s, 𝒪) ⟶ ⊕_k H¹(Y_{k,s}, 𝒪)is injective, thenZ ∩ U = (⋂_k Z_k) ∩ U(scheme theoretic intersection) for an open neighbourhoodUofs: a morphismg : T ⟶ Swith image inUfactors throughZif and only if it factors through everyZ_k.
H¹(X_s, 𝒪)is the degree-1cohomology of theκ(s)-linear derived global sections of𝒪_{X_s}, and thek-th component of the map isStacks.Cohomology.GlobalKunneth.sectionsPullbackMapalong the base changeY_{k,s} ⟶ X_sofi k.
theorem IsDescentLocus.exists_factorsThrough_iff_forall_of_injective_H1
[Flat f] [IsProper f] (hfp : FinitePresentation f)
(hO : ∀ {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f a).toLRSHom.toShHom))
{ι : Type u} [Finite ι] (Y : ι → Scheme.{u}) (i : ∀ k, Y k ⟶ X)
(hflat : ∀ k, Flat (i k ≫ f)) (hprop : ∀ k, IsProper (i k ≫ f))
(hfpk : ∀ k, FinitePresentation (i k ≫ f))
(hOk : ∀ k {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd (i k ≫ f) a).toLRSHom.toShHom))
(L : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
[hL : IsInvertible X.presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) X.IsSheaf) L]
{Z : Over S} (hZ : IsDescentLocus f L Z) {Zk : ι → Over S}
(hZk : ∀ k, IsDescentLocus (i k ≫ f) ((modulePullback (i k).toLRSHom.toShHom).obj L) (Zk k))
(s : S) (hs : s ∈ Set.range Z.hom)
(hinj : ∀ c : (DerivedCategory.homologyFunctor
(ModuleCat.{u} (baseRing (Spec (S.residueField s)).toRingedSpace)) 1).obj
((sectionsOverBase (pullback.snd f (S.fromSpecResidueField s)).toLRSHom.toShHom).obj
(DerivedCategory.Q.obj ((HomologicalComplex.single _ (ComplexShape.up ℤ) 0).obj
(SheafOfModules.unit (structureSheafRing
(pullback f (S.fromSpecResidueField s)).toRingedSpace))))),
(∀ k, ((DerivedCategory.homologyFunctor _ 1).map
(sectionsPullbackMap (pullback.snd f (S.fromSpecResidueField s)).toLRSHom.toShHom
(pullback.map (i k ≫ f) (S.fromSpecResidueField s) f (S.fromSpecResidueField s)
(i k) (𝟙 _) (𝟙 _) (by simp) (by simp)).toLRSHom.toShHom
(DerivedCategory.Q.obj ((HomologicalComplex.single _ (ComplexShape.up ℤ) 0).obj
(SheafOfModules.unit (structureSheafRing
(pullback f (S.fromSpecResidueField s)).toRingedSpace)))))).hom c = 0) →
c = 0) :
∃ U : S.Opens, s ∈ U ∧ ∀ {T : Scheme.{u}} (g : T ⟶ S), Set.range g ⊆ (U : Set S) →
((∃ h : T ⟶ Z.left, h ≫ Z.hom = g) ↔
∀ k, ∃ h : T ⟶ (Zk k).left, h ≫ (Zk k).hom = g)
Tag 0BF3, a lemma
Tag 0BF3 in the Stacks Project.
AlgebraicGeometry.SheafOfModules.exists_isTrivial_on_open_of_isTrivial_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/DescentLocusTrivialityKunneth.lean, line 59.
Let
f : X ⟶ Sandg : Y ⟶ Sbe flat, proper and of finite presentation with𝒪_T ≅ f_{T,*}𝒪and𝒪_T ≅ g_{T,*}𝒪after every base change, with sectionsσoffandτofg, and letLbe invertible onX ×_S Y. IfLis trivial on the two faces(1, τ ∘ f) : X ⟶ X ×_S Yand(σ ∘ g, 1) : Y ⟶ X ×_S Yand on the fibre overs, thenLis trivial overU ×_S (X ×_S Y)for an open neighbourhoodUofs.
theorem exists_isTrivial_on_open_of_isTrivial_faces
{S X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
[Flat f] [IsProper f] (hfp : FinitePresentation f)
(hfO : ∀ {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd f a).toLRSHom.toShHom))
[Flat g] [IsProper g] (hgp : FinitePresentation g)
(hgO : ∀ {T : Scheme.{u}} (a : T ⟶ S),
IsIso (structureSheafHom (pullback.snd g a).toLRSHom.toShHom))
(σ : S ⟶ X) (hσ : σ ≫ f = 𝟙 S)
(τ : S ⟶ Y) (hτ : τ ≫ g = 𝟙 S)
(s : S)
(L : _root_.SheafOfModules.{u} (structureSheafRing (pullback f g).toRingedSpace))
[IsInvertible (pullback f g).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback f g).IsSheaf) L]
(hfaceX :
let i : X ⟶ pullback f g :=
pullback.lift (𝟙 X) (f ≫ τ) (by simp [Category.assoc, hτ])
IsTrivial X.presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) X.IsSheaf)
((modulePullback i.toLRSHom.toShHom).obj L))
(hfaceY :
let i : Y ⟶ pullback f g :=
pullback.lift (g ≫ σ) (𝟙 Y) (by simp [Category.assoc, hσ])
IsTrivial Y.presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) Y.IsSheaf)
((modulePullback i.toLRSHom.toShHom).obj L))
(hfiber :
let P := pullback f g
let p : P ⟶ S := pullback.fst f g ≫ f
let W := pullback p (S.fromSpecResidueField s)
IsTrivial W.presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) W.IsSheaf)
((modulePullback (pullback.fst p (S.fromSpecResidueField s)).toLRSHom.toShHom).obj L)) :
∃ U : S.Opens, s ∈ U ∧
(let P := pullback f g
let p : P ⟶ S := pullback.fst f g ≫ f
let W := pullback p U.ι
IsTrivial W.presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) W.IsSheaf)
((modulePullback (pullback.fst p U.ι).toLRSHom.toShHom).obj L))
Tag 0BF4, a theorem
Tag 0BF4 in the Stacks Project.
AlgebraicGeometry.SheafOfModules.isTrivial_of_isTrivial_faces_and_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/TheoremOfTheCube0BF4.lean, line 46.
The theorem of the cube. Let
f : X ⟶ S,g : Y ⟶ Sandh : Z ⟶ Sbe morphisms of schemes, withfandgflat, proper, of finite presentation and with geometrically integral fibres, letxandybe sections offandg, and letLbe an invertible module onX ×_S Y ×_S Zwhose pullbacks along the facesx × 1 × 1and1 × y × 1are trivial and whose restriction to one fibreX ×_S Y ×_S zis trivial. IfZis connected, thenLis trivial.The fibre over
zis the base change of the projectionX ×_S Y ×_S Z ⟶ ZalongZ.fromSpecResidueField z.
theorem isTrivial_of_isTrivial_faces_and_fiber {S X Y Z : Scheme.{u}}
(f : X ⟶ S) (g : Y ⟶ S) (h : Z ⟶ S)
(x : S ⟶ X) (hx : x ≫ f = 𝟙 S) (y : S ⟶ Y) (hy : y ≫ g = 𝟙 S)
[Flat f] [IsProper f] (hfp : FinitePresentation f) [GeometricallyIntegral f]
[Flat g] [IsProper g] (hgp : FinitePresentation g) [GeometricallyIntegral g]
[ConnectedSpace Z]
(L : _root_.SheafOfModules.{u}
(structureSheafRing (pullback (pullback.fst f g ≫ f) h).toRingedSpace))
[IsInvertible (pullback (pullback.fst f g ≫ f) h).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback (pullback.fst f g ≫ f) h).IsSheaf) L]
(hfaceX :
let i : pullback g h ⟶ pullback (pullback.fst f g ≫ f) h :=
pullback.lift
(pullback.lift (pullback.fst g h ≫ g ≫ x) (pullback.fst g h)
(by simp only [Category.assoc, hx, Category.comp_id]))
(pullback.snd g h)
(by rw [pullback.lift_fst_assoc]
simp only [Category.assoc, hx, Category.comp_id, pullback.condition])
IsTrivial (pullback g h).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback g h).IsSheaf)
((modulePullback i.toLRSHom.toShHom).obj L))
(hfaceY :
let i : pullback f h ⟶ pullback (pullback.fst f g ≫ f) h :=
pullback.lift
(pullback.lift (pullback.fst f h) (pullback.fst f h ≫ f ≫ y)
(by simp only [Category.assoc, hy, Category.comp_id]))
(pullback.snd f h)
(by rw [pullback.lift_fst_assoc, pullback.condition])
IsTrivial (pullback f h).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback f h).IsSheaf)
((modulePullback i.toLRSHom.toShHom).obj L))
(hfiber : ∃ z : Z,
IsTrivial (pullback (pullback.snd (pullback.fst f g ≫ f) h)
(Z.fromSpecResidueField z)).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback (pullback.snd (pullback.fst f g ≫ f) h)
(Z.fromSpecResidueField z)).IsSheaf)
((modulePullback (pullback.fst (pullback.snd (pullback.fst f g ≫ f) h)
(Z.fromSpecResidueField z)).toLRSHom.toShHom).obj L)) :
IsTrivial (pullback (pullback.fst f g ≫ f) h).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback (pullback.fst f g ≫ f) h).IsSheaf) L
AlgebraicGeometry.SheafOfModules.isTrivial_of_isTrivial_face_and_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/TheoremOfTheCube.lean, line 223. The attribute's comment: “assuming the conclusions of Tags 0BDP, 0BF0 and 0BF3 for the descent locus”.
The theorem of the cube. Let
f : X ⟶ S,g : Y ⟶ Sandh : Z ⟶ Sbe morphisms of schemes, letxandybe sections offandg, and letLbe a sheaf of modules onX ×_S Y ×_S Zwhose pullback along the facex × 1 × 1is trivial and whose restriction to one fibreX ×_S Y ×_S zis trivial. IfZis connected andDis a descent locus forLalong the projection toZwhich is a closed immersion and contains a neighbourhood of each of its points, thenLis trivial.
theorem isTrivial_of_isTrivial_face_and_fiber {S X Y Z : Scheme.{u}} {D : Over Z}
(f : X ⟶ S) (g : Y ⟶ S) (h : Z ⟶ S)
(x : S ⟶ X) (hx : x ≫ f = 𝟙 S) (y : S ⟶ Y) (hy : y ≫ g = 𝟙 S) [ConnectedSpace Z]
(L : _root_.SheafOfModules.{u}
(structureSheafRing (pullback (pullback.fst f g ≫ f) h).toRingedSpace))
(hD : IsDescentLocus (pullback.snd (pullback.fst f g ≫ f) h) L D)
(hclosed : _root_.AlgebraicGeometry.IsClosedImmersion D.hom)
(hnbhd : ∀ z ∈ Set.range D.hom, ∃ U : Z.Opens, z ∈ U ∧
DescendsFromBase (pullback.snd (pullback.fst f g ≫ f) h) L U.ι)
(hfaceX :
let i : pullback g h ⟶ pullback (pullback.fst f g ≫ f) h :=
pullback.lift
(pullback.lift (pullback.fst g h ≫ g ≫ x) (pullback.fst g h)
(by simp only [Category.assoc, hx, Category.comp_id]))
(pullback.snd g h)
(by rw [pullback.lift_fst_assoc]
simp only [Category.assoc, hx, Category.comp_id, pullback.condition])
IsTrivial (pullback g h).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback g h).IsSheaf)
((modulePullback i.toLRSHom.toShHom).obj L))
(hfiber : ∃ z : Z,
IsTrivial (pullback (pullback.snd (pullback.fst f g ≫ f) h)
(Z.fromSpecResidueField z)).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback (pullback.snd (pullback.fst f g ≫ f) h)
(Z.fromSpecResidueField z)).IsSheaf)
((modulePullback (pullback.fst (pullback.snd (pullback.fst f g ≫ f) h)
(Z.fromSpecResidueField z)).toLRSHom.toShHom).obj L)) :
IsTrivial (pullback (pullback.fst f g ≫ f) h).presheaf
(Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat)
(pullback (pullback.fst f g ≫ f) h).IsSheaf) L
Sources
Section37.34 Limit arguments#
Section 37.34 of the Stacks Project, Tag 05FA. 11 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05FB, a lemma
Tag 05FB in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximation.lean, line 99.
Stacks Project, Tag 05FB. An affine morphism of finite presentation between affine schemes admits an affine finite-type model over a base of finite type over
ℤ.
theorem exists_finiteTypeAffineModel {X S : Scheme.{u}} [IsAffine X] [IsAffine S]
(f : X ⟶ S) (hf : FinitePresentation f) :
Nonempty (FiniteTypeAffineModel ⊤ f)
Tag 05FC, a lemma
Tag 05FC in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximationModule.lean, line 228.
Stacks Project, Tag 05FC. A quasi-coherent module of finite presentation on the source of a morphism of affine schemes of finite presentation descends to a coherent module on an affine finite-type model of that morphism over a base of finite type over
ℤ.
theorem exists_finiteTypeAffineModel_isCoherent
{X S : Scheme.{u}} [IsAffine X] [IsAffine S]
(f : X ⟶ S) (hf : FinitePresentation f)
(F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation] :
∃ (m : FiniteTypeAffineModel ⊤ f) (F₀ : m.X₀.Modules),
F₀.IsCoherent ∧ Nonempty ((Scheme.Modules.pullback m.toSource).obj F₀ ≅ F)
Tag 05FD, a lemma
Tag 05FD in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_isCoherent_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximationModule.lean, line 266.
Stacks Project, Tag 05FD. A quasi-coherent module of finite presentation on the source of a morphism of affine schemes of finite presentation which is moreover flat over the target descends to a coherent module, flat over the base, on an affine finite-type model of that morphism over a base of finite type over
ℤ.
theorem exists_finiteTypeAffineModel_isCoherent_isFlatOver
{X S : Scheme.{u}} [IsAffine X] [IsAffine S]
(f : X ⟶ S) (hf : FinitePresentation f)
(F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation]
(hF : IsFlatOver f.toLRSHom.toShHom F) :
∃ (m : FiniteTypeAffineModel ⊤ f) (F₀ : m.X₀.Modules),
F₀.IsCoherent ∧ Nonempty ((Scheme.Modules.pullback m.toSource).obj F₀ ≅ F) ∧
IsFlatOver m.f₀.toLRSHom.toShHom F₀
Tag 05FE, a lemma
Tag 05FE in the Stacks Project.
AlgebraicGeometry.exists_flat_finiteTypeAffineModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximation.lean, line 160.
Stacks Project, Tag 05FE. A flat morphism of finite presentation between affine schemes admits an affine finite-type model whose modeled morphism is flat.
theorem exists_flat_finiteTypeAffineModel
{X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S)
(hf : FinitePresentation f) [Flat f] :
Nonempty (FiniteTypeAffineModel @Flat f)
Tag 05FF, a lemma
Tag 05FF in the Stacks Project.
AlgebraicGeometry.exists_smooth_finiteTypeAffineModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximation.lean, line 222.
Stacks Project, Tag 05FF. A smooth morphism between affine schemes admits an affine finite-type model whose modeled morphism is smooth.
theorem exists_smooth_finiteTypeAffineModel
{X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S) [Smooth f] :
Nonempty (FiniteTypeAffineModel @Smooth f)
Tag 05FG, a lemma
Tag 05FG in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_geometricallyReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximationFibre.lean, line 182. References: EGA IV (8.9.1), “(i), special case”.
Stacks Project, Tag 05FG. A morphism of affine schemes of finite presentation with geometrically reduced fibres admits an affine finite-type model over a base of finite type over
ℤwhose fibres are geometrically reduced as well.The limit argument is
AlgebraicGeometry.exists_finiteTypeAffineModel_fiberwise, applied to the locus of geometrically reduced fibres. Its compatibility with base change is Tag 0576,AlgebraicGeometry.geometricallyReduced_fiber_set_eq_preimage_of_isPullback, and its local constructibility over an affine Noetherian base is Tag 0579,AlgebraicGeometry.isLocallyConstructible_geometricallyReduced_fiber_of_isAffine.
theorem exists_finiteTypeAffineModel_geometricallyReduced
{X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S)
(hf : FinitePresentation f) (hfib : GeometricallyReduced f) :
Nonempty (FiniteTypeAffineModel @GeometricallyReduced f)
Tag 05FH, a lemma
Tag 05FH in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximationFibre.lean, line 127.
Stacks Project, Tag 05FH. A morphism of affine schemes of finite presentation with geometrically irreducible fibres admits an affine finite-type model over a base of finite type over
ℤwhose fibres are geometrically irreducible as well.
theorem exists_finiteTypeAffineModel_geometricallyIrreducible
{X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S)
(hf : FinitePresentation f) (hfib : GeometricallyIrreducible f) :
Nonempty (FiniteTypeAffineModel @GeometricallyIrreducible f)
Tag 05FI, a lemma
Tag 05FI in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_geometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximationFibre.lean, line 163.
Stacks Project, Tag 05FI. A morphism of affine schemes of finite presentation with geometrically connected fibres admits an affine finite-type model over a base of finite type over
ℤwhose fibres are geometrically connected as well.
theorem exists_finiteTypeAffineModel_geometricallyConnected
{X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S)
(hf : FinitePresentation f) (hfib : GeometricallyConnected f) :
Nonempty (FiniteTypeAffineModel @GeometricallyConnected f)
Tag 05FJ, a lemma
Tag 05FJ in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_fiberDimension_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/Approximation.lean, line 327.
Stacks Project, Tag 05FJ. An affine morphism of finite presentation all of whose fibres have dimension
dadmits an affine finite-type model all of whose fibres have dimensiond.
public theorem exists_finiteTypeAffineModel_fiberDimension_eq {X S : Scheme.{u}} [IsAffine X]
[IsAffine S] (f : X ⟶ S) (hf : FinitePresentation f) (d : ℕ)
(hd : ∀ s : S, f.fiberDimension s = (d : WithBot ℕ∞)) :
∃ m : FiniteTypeAffineModel ⊤ f,
∀ s₀ : m.S₀, m.f₀.fiberDimension s₀ = (d : WithBot ℕ∞)
Tag 05FK, a lemma
Tag 05FK in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_standardSyntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineApproximation.lean, line 371.
Stacks Project, Tag 05FK. A standard syntomic morphism of affine schemes admits an affine finite-type model whose modeled morphism is standard syntomic.
theorem exists_finiteTypeAffineModel_standardSyntomic
{X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S)
(hf : IsStandardSyntomic f) :
Nonempty {m : FiniteTypeAffineModel ⊤ f //
letI : IsAffine m.X₀ := m.source_affine
letI : IsAffine m.S₀ := m.base_affine
IsStandardSyntomic m.f₀}
Tag 05FL, a lemma
Tag 05FL in the Stacks Project.
AlgebraicGeometry.exists_finiteTypeAffineModel_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AffineModel.lean, line 443.
Two finite-type affine models of an affine morphism of finite presentation, for properties stable under base change, can be combined into one model on which both properties hold.
theorem exists_finiteTypeAffineModel_inf
(P Q : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange]
[Q.IsStableUnderBaseChange] {X S : Scheme.{u}} [IsAffine X] [IsAffine S]
(f : X ⟶ S) [LocallyOfFinitePresentation f] [QuasiCompact f]
(hP : FiniteTypeAffineModel P f) (hQ : FiniteTypeAffineModel Q f) :
Nonempty (FiniteTypeAffineModel (P ⊓ Q) f)
Sources
Section37.35 Étale neighbourhoods#
Section 37.35 of the Stacks Project, Tag 02LD. 6 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02LE, a definition
Tag 02LE in the Stacks Project.
AlgebraicGeometry.EtaleNeighborhood, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleNeighborhood.lean, line 62. The attribute's comment: “part (1)”.
An étale neighbourhood of a scheme
Sat a pointsis a scheme which is étale overS, together with a distinguished point lying overs.
structure EtaleNeighborhood (S : Scheme.{u}) (s : S)
AlgebraicGeometry.EtaleNeighborhood.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleNeighborhood.lean, line 82. The attribute's comment: “part (2)”.
A morphism of étale neighbourhoods of
(S, s)is a morphism of schemes overSwhich carries the distinguished point to the distinguished point.
structure Hom (U V : EtaleNeighborhood S s)
AlgebraicGeometry.EtaleNeighborhood.IsElementary, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleNeighborhood.lean, line 127. The attribute's comment: “part (3)”.
An étale neighbourhood is elementary if the induced extension of residue fields is trivial.
abbrev IsElementary (U : EtaleNeighborhood S s) : Prop
Tag 02LF, a lemma
Tag 02LF in the Stacks Project.
AlgebraicGeometry.exists_etaleNeighborhood_residueField_algEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/ResidueField.lean, line 133. References: EGA IV (18.8.6), “more general”; SGA 2 XIV (3.4).
Stacks Project, Tag 02LF. Every finite separable extension of the residue field at a point is realized by the residue field at the chosen point of an étale neighborhood.
theorem exists_etaleNeighborhood_residueField_algEquiv
(S : Scheme.{u}) (s : S) (k : Type v) [Field k]
[Algebra (S.residueField s) k]
[Module.Finite (S.residueField s) k]
[Algebra.IsSeparable (S.residueField s) k] :
∃ U : EtaleNeighborhood S s,
letI := U.residueFieldMap.hom.toAlgebra
Nonempty (U.scheme.residueField U.point ≃ₐ[S.residueField s] k)
Tag 057A, a lemma
Tag 057A in the Stacks Project.
AlgebraicGeometry.exists_common_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Refinement.lean, line 68. The attribute's comment: “part (1)”.
Stacks Project, Tag 057A, part (1). Two étale neighborhoods of a point admit a common refinement.
theorem exists_common_refinement {S : Scheme.{u}} {s : S}
(U V : EtaleNeighborhood S s) :
∃ W : EtaleNeighborhood S s, Nonempty ((W ⟶ U) × (W ⟶ V))
AlgebraicGeometry.exists_equalizing_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Refinement.lean, line 144. The attribute's comment: “part (2)”.
Stacks Project, Tag 057A, part (2). Two neighborhood maps which induce the same map on residue fields become equal after a refinement.
theorem exists_equalizing_refinement (f g : U ⟶ V)
(hκ : (V.scheme.residueFieldCongr f.map_point).inv ≫
f.hom.residueFieldMap U.point =
(V.scheme.residueFieldCongr g.map_point).inv ≫
g.hom.residueFieldMap U.point) :
∃ W : EtaleNeighborhood S s, ∃ h : W ⟶ U, h ≫ f = h ≫ g
Tag 057B, a lemma
Tag 057B in the Stacks Project.
Stacks.EtaleCohomology.isCofiltered_elementaryEtaleNeighborhood, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleStalk/ElementaryFiber.lean, line 288.
Stacks 057B. The category of elementary étale neighbourhoods of a point of a scheme is cofiltered: two neighbourhoods are dominated by their fibre product and two morphisms of elementary neighbourhoods are equalized after a refinement, both by Tag 057A.
public instance isCofiltered_elementaryEtaleNeighborhood (X : Scheme.{u}) (x : X) :
IsCofiltered (ElementaryEtaleNeighborhood X x)
Tag 05KS, a lemma
Tag 05KS in the Stacks Project.
AlgebraicGeometry.instIsFilteredOppositeElementaryEtaleNeighborhood, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Henselization.lean, line 1253. The attribute's comment: “the indexing category is filtered”. References: EGA IV (18.6.3), “more general”.
Stacks Project, Tag 05KS. The opposite of the category of elementary étale neighborhoods of a point is filtered.
instance instIsFilteredOppositeElementaryEtaleNeighborhood
(S : Scheme.{u}) (s : S) :
IsFiltered (ElementaryEtaleNeighborhood S s)ᵒᵖ
AlgebraicGeometry.isColimit_globalSections, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Henselization.lean, line 1354. The attribute's comment: “the henselization is the colimit”.
Stacks Project, Tag 05KS. A henselization of the local ring of a scheme at a point is a colimit of the rings of global sections of its elementary étale neighborhoods.
lemma isColimit_globalSections (S : Scheme.{u}) (s : S)
(Rh : Type u) [CommRing Rh] [IsLocalRing Rh]
[Algebra (S.presheaf.stalk s) Rh]
[IsLocalRing.IsHenselization (S.presheaf.stalk s)
(IsLocalRing.ResidueField (S.presheaf.stalk s)) Rh] :
∃ ι : globalSections S s ⟶
(Functor.const _).obj (CommRingCat.of Rh),
(∀ U x, IsLocalRing.residue Rh ((ι.app U).hom x) =
henselizationResidueFieldMap S s Rh
(elementaryEtaleAugmentation S s U.unop x)) ∧
(∀ U : (ElementaryEtaleNeighborhood S s)ᵒᵖ,
IsOverStalk S s Rh U.unop (ι.app U).hom) ∧
(∀ ι' : globalSections S s ⟶ (Functor.const _).obj (CommRingCat.of Rh),
(∀ U x, IsLocalRing.residue Rh ((ι'.app U).hom x) =
henselizationResidueFieldMap S s Rh
(elementaryEtaleAugmentation S s U.unop x)) →
(∀ U : (ElementaryEtaleNeighborhood S s)ᵒᵖ,
IsOverStalk S s Rh U.unop (ι'.app U).hom) → ι' = ι) ∧
Nonempty (IsColimit (Cocone.mk _ ι))
Tag 0CAS, a lemma
Tag 0CAS in the Stacks Project.
AlgebraicGeometry.exists_etaleNeighborhood_fiber_openImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/FiberLifting.lean, line 455.
Stacks Project, Tag 0CAS. An étale neighborhood on a fiber can be refined by an open immersion from the fiber of an étale neighborhood on the total space.
public theorem exists_etaleNeighborhood_fiber_openImmersion
{X S : Scheme.{u}} (f : X ⟶ S) (x : X)
(V : EtaleNeighborhood (f.fiber (f x)) (f.asFiber x)) :
∃ (U : EtaleNeighborhood X x)
(u : (U.toBase ≫ f).fiber (f x))
(p : (U.toBase ≫ f).fiber (f x) ⟶ f.fiber (f x))
(h : (U.toBase ≫ f).fiber (f x) ⟶ V.scheme),
(U.toBase ≫ f).fiberι (f x) u = U.point ∧
p ≫ f.fiberι (f x) = (U.toBase ≫ f).fiberι (f x) ≫ U.toBase ∧
Etale p ∧
p u = f.asFiber x ∧
h ≫ V.toBase = p ∧
h u = V.point ∧
IsOpenImmersion h
Sources
Section37.36 Étale neighbourhoods and branches#
Section 37.36 of the Stacks Project, Tag 0CB2. 4 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0CB3, a lemma
Tag 0CB3 in the Stacks Project.
encard_minimalPrimes_directLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/MinimalPrimesDirectLimit.lean, line 166.
Stacks Project, Tag 0CB3. For a directed system of rings with faithfully flat transition maps, the number of minimal primes of the direct limit is the supremum of the numbers of minimal primes at the individual stages.
theorem encard_minimalPrimes_directLimit
{ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
(R : ι → Type v) [(i : ι) → CommRing (R i)]
(f : (i j : ι) → i ≤ j → R i →+* R j)
[DirectedSystem R (fun i j h => (f i j h : R i → R j))]
(hff : ∀ i j (h : i ≤ j), (f i j h).FaithfullyFlat) :
Set.encard (minimalPrimes (Ring.DirectLimit R
(fun i j h => (f i j h : R i → R j)))) =
⨆ i, Set.encard (minimalPrimes (R i))
Tag 0CB4, a lemma
Tag 0CB4 in the Stacks Project.
AlgebraicGeometry.numberOfGeometricBranches_eq_iSup_encard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Branches.lean, line 568. The attribute's comment: “geometric_branches_supremum”.
Stacks Project, Tag 0CB4. The number of geometric branches at a point is the supremum, over all étale neighborhoods of that point, of the number of irreducible components of the neighborhood passing through its distinguished point.
theorem numberOfGeometricBranches_eq_iSup_encard
(X : AlgebraicGeometry.Scheme.{u}) (x : X) :
numberOfGeometricBranches X x =
⨆ U : EtaleNeighborhood X x,
Set.encard {Z ∈ irreducibleComponents U.scheme | U.point ∈ Z}
AlgebraicGeometry.numberOfBranches_eq_iSup_encard_irreducibleComponentsThrough, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Branches.lean, line 1093. The attribute's comment: “branches_supremum”.
Stacks Project, Tag 0CB4. The number of branches at a point is the supremum, over elementary étale neighborhoods, of the number of irreducible components passing through the distinguished point.
theorem numberOfBranches_eq_iSup_encard_irreducibleComponentsThrough
(X : Scheme.{u}) (x : X) :
numberOfBranches X x =
⨆ (U : EtaleNeighborhood X x) (_ : U.IsElementary),
Set.encard {Z ∈ irreducibleComponents U.scheme | U.point ∈ Z}
AlgebraicGeometry.isUnibranchAt_iff_existsUnique_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/UnibranchEtaleCriterion.lean, line 70. The attribute's comment: “unibranch_iff”.
Stacks Project, Tag 0CB4. A scheme is unibranch at a point if and only if every elementary étale neighbourhood of that point has exactly one irreducible component passing through its distinguished point.
theorem isUnibranchAt_iff_existsUnique_irreducibleComponent (X : Scheme.{u}) (x : X) :
IsUnibranchAt X x ↔
∀ U : EtaleNeighborhood X x, U.IsElementary →
∃! Z : irreducibleComponents U.scheme, U.point ∈ (Z : Set U.scheme)
AlgebraicGeometry.isGeometricallyUnibranchAt_iff_existsUnique_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/UnibranchEtaleCriterion.lean, line 89. The attribute's comment: “geometrically_unibranch_iff”. References: EGA IV (7.9.10), “more general”; SGA 3 X (5.14.0), “partial”.
Stacks Project, Tag 0CB4. A scheme is geometrically unibranch at a point if and only if every étale neighbourhood of that point has exactly one irreducible component passing through its distinguished point.
theorem isGeometricallyUnibranchAt_iff_existsUnique_irreducibleComponent
(X : Scheme.{u}) (x : X) :
IsGeometricallyUnibranchAt X x ↔
∀ U : EtaleNeighborhood X x,
∃! Z : irreducibleComponents U.scheme, U.point ∈ (Z : Set U.scheme)
Tag 0CB5, a lemma
Tag 0CB5 in the Stacks Project.
AlgebraicGeometry.numberOfBranches_fiber_eq_iSup_encard_irreducibleComponentsThrough, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/FiberBranches.lean, line 273. The attribute's comment: “fibre_branches”.
Stacks Project, Tag 0CB5. The branches of a fibre are counted by irreducible components through the distinguished points of fibres of elementary étale neighborhoods.
public theorem numberOfBranches_fiber_eq_iSup_encard_irreducibleComponentsThrough
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
numberOfBranches (f.fiber (f x)) (f.asFiber x) =
⨆ (U : EtaleNeighborhood X x) (_ : U.IsElementary),
Set.encard
{Z ∈ irreducibleComponents ((U.toBase ≫ f).fiber (f x)) |
((U.toBase ≫ f).fiberHomeo (f x)).symm
⟨U.point, by simp [U.map_point]⟩ ∈ Z}
AlgebraicGeometry.numberOfGeometricBranches_fiber_eq_iSup_encard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/FiberBranches.lean, line 299. The attribute's comment: “fibre_geometric_branches”.
Stacks Project, Tag 0CB5. Geometric branches of a fibre are counted by irreducible components through the distinguished points of fibres of étale neighbourhoods.
public theorem numberOfGeometricBranches_fiber_eq_iSup_encard
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
numberOfGeometricBranches (f.fiber (f x)) (f.asFiber x) =
⨆ U : EtaleNeighborhood X x,
Set.encard
{Z ∈ irreducibleComponents ((U.toBase ≫ f).fiber (f x)) |
((U.toBase ≫ f).fiberHomeo (f x)).symm
⟨U.point, by simp [U.map_point]⟩ ∈ Z}
AlgebraicGeometry.isUnibranchAt_fiber_iff_existsUnique_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/FiberBranches.lean, line 324. The attribute's comment: “fibre_unibranch_iff”.
Stacks Project, Tag 0CB5. The fibre is unibranch at the point if and only if for every elementary étale neighbourhood of the point in the total space there is exactly one irreducible component of its fibre passing through the distinguished point.
public theorem isUnibranchAt_fiber_iff_existsUnique_irreducibleComponent
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
IsUnibranchAt (f.fiber (f x)) (f.asFiber x) ↔
∀ U : EtaleNeighborhood X x, U.IsElementary →
∃! Z : irreducibleComponents ((U.toBase ≫ f).fiber (f x)),
((U.toBase ≫ f).fiberHomeo (f x)).symm ⟨U.point, by simp [U.map_point]⟩ ∈
(Z : Set ((U.toBase ≫ f).fiber (f x)))
AlgebraicGeometry.isGeometricallyUnibranchAt_fiber_iff_existsUnique_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/FiberBranches.lean, line 358. The attribute's comment: “fibre_geometrically_unibranch_iff”.
Stacks Project, Tag 0CB5, part (4), stated about the fibre. The fibre is geometrically unibranch at the point if and only if for every étale neighbourhood of the point in the total space there is exactly one irreducible component of its fibre passing through the distinguished point.
The source states part (4) as "
Xis geometrically unibranch atx", notX_s, while its right-hand side is about the irreducible components of the fibreU_s. That pairing ofXwithU_sis the asymmetry: parts (1), (2) and (3) are all aboutX_s, part (4) is the geometric counterpart of part (3), and the cited proof (Tags 0CB4 and 0CAS) yields the statement about the fibre. The fibre statement is what is proved here; the deviation from the literal text of part (4) is recorded rather than silently adopted.The deviation is not a choice between two defensible readings:
AlgebraicGeometry.not_forall_isGeometricallyUnibranchAt_iff_existsUnique_irreducibleComponentrefutes the literal statement aboutX, so the reading about the fibre proved here is the only true one.
public theorem isGeometricallyUnibranchAt_fiber_iff_existsUnique_irreducibleComponent
{X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
IsGeometricallyUnibranchAt (f.fiber (f x)) (f.asFiber x) ↔
∀ U : EtaleNeighborhood X x,
∃! Z : irreducibleComponents ((U.toBase ≫ f).fiber (f x)),
((U.toBase ≫ f).fiberHomeo (f x)).symm ⟨U.point, by simp [U.map_point]⟩ ∈
(Z : Set ((U.toBase ≫ f).fiber (f x)))
AlgebraicGeometry.not_forall_isGeometricallyUnibranchAt_iff_existsUnique_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/FiberBranchesLiteralForm.lean, line 155. The attribute's comment: “part (4) as printed, about X rather than X_s, is FALSE: counterexample”.
It is not true that for every morphism
f : X ⟶ Sand every pointxofX,Xis geometrically unibranch atxif and only if for every étale neighbourhood(U, u)of(X, x)there is exactly one irreducible component of the fibre ofU ⟶ Soverf xthroughu.
theorem not_forall_isGeometricallyUnibranchAt_iff_existsUnique_irreducibleComponent :
¬ ∀ (X S : Scheme.{u}) (f : X ⟶ S) (x : X),
IsGeometricallyUnibranchAt X x ↔
∀ U : EtaleNeighborhood X x,
∃! Z : irreducibleComponents ((U.toBase ≫ f).fiber (f x)),
((U.toBase ≫ f).fiberHomeo (f x)).symm ⟨U.point, by simp [U.map_point]⟩ ∈
(Z : Set ((U.toBase ≫ f).fiber (f x)))
Tag 0DQ2, a lemma
Tag 0DQ2 in the Stacks Project.
AlgebraicGeometry.numberOfGeometricBranches_eq_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/SmoothBranches.lean, line 220. The attribute's comment: “geometric_branches”.
Stacks Project, Tag 0DQ2. A smooth morphism of schemes preserves the number of geometric branches at a point.
public theorem numberOfGeometricBranches_eq_of_smooth {X S : Scheme.{u}} (f : X ⟶ S) [Smooth f]
(x : X) :
numberOfGeometricBranches X x = numberOfGeometricBranches S (f.base x)
AlgebraicGeometry.numberOfBranches_eq_of_smooth_of_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleNeighbourhood/SmoothBranches.lean, line 229. The attribute's comment: “branches_purely_inseparable”.
Stacks Project, Tag 0DQ2. A smooth morphism of schemes preserves the number of branches at a point whose residue field is a purely inseparable extension of the residue field of its image.
public theorem numberOfBranches_eq_of_smooth_of_isPurelyInseparable {X S : Scheme.{u}}
(f : X ⟶ S) [Smooth f] (x : X)
(h : (f.residueFieldMap x).hom.IsPurelyInseparable) :
numberOfBranches X x = numberOfBranches S (f.base x)
Sources
Section37.37 Unramified and étale morphisms#
Section 37.37 of the Stacks Project, Tag 0GS7. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GS8, a lemma
Tag 0GS8 in the Stacks Project.
AlgebraicGeometry.etaleAt_of_unramifiedAt_of_specializes_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/Unibranch.lean, line 41. References: EGA IV (18.10.1), “suff.; generic pt in”.
Let
f : X ⟶ Ybe locally of finite type withYintegral, and letx : Xbe a point whose image is a point whereYis geometrically unibranch. Iffis unramified atxandxis a specialization of a point lying over the generic point ofY, thenfis étale atx.
theorem etaleAt_of_unramifiedAt_of_specializes_genericPoint
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral Y] [LocallyOfFiniteType f] {x x' : X}
(hy : IsGeometricallyUnibranchAt Y (f x))
(hxx' : x' ⤳ x) (hx' : f x' = genericPoint Y)
(hunramified : UnramifiedAt f x) :
EtaleAt f x
Tag 0GS9, a lemma
Tag 0GS9 in the Stacks Project.
AlgebraicGeometry.etale_of_unramified_of_dominant_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/UnibranchConnected.lean, line 156. The attribute's comment: “etaleness”. References: EGA IV (18.10.3), “f étale”; SGA 1 I (9.11), “f étale”.
An unramified morphism from a connected scheme to an integral geometrically unibranch scheme is étale as soon as one irreducible component of its source dominates the target.
theorem etale_of_unramified_of_dominant_component
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral Y] [Unramified f] [ConnectedSpace X]
(hY : IsGeometricallyUnibranch Y)
(hdom : ∃ Z : irreducibleComponents X, closure (f '' (Z : Set X)) = Set.univ) :
Etale f
AlgebraicGeometry.irreducibleSpace_of_unramified_of_dominant_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/UnibranchConnected.lean, line 169. The attribute's comment: “irreducibility”. References: EGA IV (18.10.3), “X irreducible”; SGA 1 I (9.11), “X irreducible”.
The source of an unramified morphism from a connected scheme to an integral geometrically unibranch scheme is irreducible as soon as one of its irreducible components dominates the target.
theorem irreducibleSpace_of_unramified_of_dominant_component
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral Y] [Unramified f] [ConnectedSpace X]
(hY : IsGeometricallyUnibranch Y)
(hdom : ∃ Z : irreducibleComponents X, closure (f '' (Z : Set X)) = Set.univ) :
IrreducibleSpace X
Tag 0GSA, a lemma
Tag 0GSA in the Stacks Project.
AlgebraicGeometry.etaleAt_left_of_comp_etaleAt_of_specializes_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/UnibranchComposition.lean, line 51. The attribute's comment: “first factor”.
If a composite
f ≫ gis étale atx, the intermediate scheme is integral and geometrically unibranch atf x, andxis a specialization of a point whose image underfis the generic point, thenfis étale atx.
theorem etaleAt_left_of_comp_etaleAt_of_specializes_genericPoint
{X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegral Y] {x x' : X}
(hy : IsGeometricallyUnibranchAt Y (f x)) (hcomp : EtaleAt (f ≫ g) x)
(hxx' : x' ⤳ x) (hx' : f x' = genericPoint Y) :
EtaleAt f x
AlgebraicGeometry.etaleAt_right_of_comp_etaleAt_of_specializes_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/UnibranchComposition.lean, line 79. The attribute's comment: “second factor”.
Under the hypotheses of
AlgebraicGeometry.etaleAt_left_of_comp_etaleAt_of_specializes_genericPoint, the second factor is étale at the image ofx.
theorem etaleAt_right_of_comp_etaleAt_of_specializes_genericPoint
{X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegral Y] {x x' : X}
(hy : IsGeometricallyUnibranchAt Y (f x)) (hcomp : EtaleAt (f ≫ g) x)
(hxx' : x' ⤳ x) (hx' : f x' = genericPoint Y) :
EtaleAt g (f x)
Tag 0GSB, a lemma
Tag 0GSB in the Stacks Project.
AlgebraicGeometry.etale_left_of_comp_etale_of_dominant_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/UnibranchComposition.lean, line 133. The attribute's comment: “first factor”.
If a composite
f ≫ gis étale, the intermediate scheme is integral and geometrically unibranch, and every irreducible component of the source dominates it, thenfis étale.
theorem etale_left_of_comp_etale_of_dominant_components
{X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegral Y]
(hY : IsGeometricallyUnibranch Y) (hcomp : Etale (f ≫ g))
(hdom : ∀ C : irreducibleComponents X, closure (f '' (C : Set X)) = Set.univ) :
Etale f
AlgebraicGeometry.etaleAt_right_of_comp_etale_of_dominant_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/UnibranchComposition.lean, line 148. The attribute's comment: “second factor”.
Under the hypotheses of
AlgebraicGeometry.etale_left_of_comp_etale_of_dominant_components, the second factor is étale at every point in the image of the first.
theorem etaleAt_right_of_comp_etale_of_dominant_components
{X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegral Y]
(hY : IsGeometricallyUnibranch Y) (hcomp : Etale (f ≫ g))
(hdom : ∀ C : irreducibleComponents X, closure (f '' (C : Set X)) = Set.univ) :
∀ y ∈ Set.range f, EtaleAt g y
Sources
Section37.38 Slicing smooth morphisms#
Section 37.38 of the Stacks Project, Tag 055S. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 057C, a lemma
Tag 057C in the Stacks Project.
Stacks.AlgebraicGeometry.exists_smooth_effectiveCartierDivisor_of_nonzero_differential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/SmoothSlice/SmoothDivisor.lean, line 693. References: SGA 1 II (4.12), “dF(x)≠0 ⇒ Y smooth”.
Stacks Project, Tag 057C. A local equation with nonzero relative differential cuts out a smooth effective Cartier divisor near the point.
public theorem exists_smooth_effectiveCartierDivisor_of_nonzero_differential
{X S : Scheme.{u}} (f : X ⟶ S) (x : X)
(h : X.presheaf.stalk x)
(hh : h ∈ IsLocalRing.maximalIdeal (X.presheaf.stalk x))
(hf : InfinitesimalLifting.SmoothAt f x)
(hdh : HasNonzeroRelativeDifferential f x h) :
∃ (U : X.Opens) (_hU : IsAffineOpen U) (hxU : x ∈ U)
(a : Γ(X, U)) (I : U.toScheme.IdealSheafData),
((TopCat.Presheaf.germ X.presheaf U x hxU).hom a = h) ∧
(∀ V : U.toScheme.affineOpens,
I.ideal V = Ideal.span
{((U.toScheme.presheaf.map (homOfLE le_top).op).hom
(U.topIso.inv.hom a))}) ∧
Stacks.Divisors.IsEffectiveCartierDivisor I ∧
(⟨x, hxU⟩ : U.toScheme) ∈ I.support ∧
Smooth (I.subschemeι ≫ U.ι ≫ f)
Tag 057D, a lemma
Tag 057D in the Stacks Project.
Stacks.AlgebraicGeometry.exists_smooth_divisor_of_nonzero_differential_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/SmoothSliceCriteria.lean, line 267.
Stacks Project, Tag 057D. Let
f : X ⟶ Sbe smooth atx, with images = f x. If the mapΩ_{X_s/s,x} ⊗_{𝒪_{X_s,x}} κ(x) ⟶ Ω_{κ(x)/κ(s)}has a nonzero kernel, then there is an affine open neighbourhoodUofxand an effective Cartier divisorD ⊆ UcontainingxwithD ⟶ Ssmooth.
public theorem exists_smooth_divisor_of_nonzero_differential_kernel
(hf : InfinitesimalLifting.SmoothAt f x)
(hker :
letI := algebraResidueFiber f x
letI := algebraFiberResidue f x
letI := algebraTargetResidueResidueField f x
letI := isScalarTower_targetResidue_fiberStalk_residueField f x
¬ Function.Injective (KaehlerDifferential.mapBaseChange (targetResidue f x)
(ToType ((f.fiber (f x)).sheaf.presheaf.stalk (fiberPoint f x)))
(ToType (X.residueField x)))) :
∃ (U : X.Opens) (_hU : IsAffineOpen U) (hxU : x ∈ U)
(I : U.toScheme.IdealSheafData),
Stacks.Divisors.IsEffectiveCartierDivisor I ∧
(⟨x, hxU⟩ : U.toScheme) ∈ I.support ∧
Smooth (I.subschemeι ≫ U.ι ≫ f)
Tag 057E, a remark
Tag 057E in the Stacks Project.
Stacks.AlgebraicGeometry.not_exists_etale_lift_through_inseparableClosedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/InseparableSliceObstruction.lean, line 297.
No étale lift through an inseparable closed point. Let
kbe a field of characteristicp > 0and leta ∈ knot be ap-th power, so thatkis imperfect. For the closed pointwofX = 𝐀²_kgiven by the maximal ideal(x, y^p - a)and the projectionf : X ⟶ S = 𝐀¹_k, there is no commutative diagramh : S' ⟶ X,g : S' ⟶ Swithh ≫ f = g,gétale, andwin the image ofh.
theorem not_exists_etale_lift_through_inseparableClosedPoint {k : Type u} [Field k] {p : ℕ}
[Fact p.Prime] [CharP k p] (a : k) (ha : ∀ b : k, b ^ p ≠ a) :
¬ ∃ (S' : Scheme.{u}) (g : S' ⟶ affineLine k) (h : S' ⟶ affinePlane k),
Etale g ∧ h ≫ projection k = g ∧ closedPoint a ha ∈ Set.range h.base
Tag 057F, a lemma
Tag 057F in the Stacks Project.
Stacks.AlgebraicGeometry.exists_smooth_divisor_of_separable_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/SmoothSliceCriteria.lean, line 465.
Stacks Project, Tag 057F. Let
f : X ⟶ Sbe smooth atx, with images = f x. If the residue field extensionκ(x)/κ(s)is separable andxis not a generic point of the fibreX_s, then there is an affine open neighbourhoodUofxand an effective Cartier divisorD ⊆ UcontainingxwithD ⟶ Ssmooth.
public theorem exists_smooth_divisor_of_separable_residueField
(hf : InfinitesimalLifting.SmoothAt f x)
(hsep : letI := (f.residueFieldMap x).hom.toAlgebra
Algebra.IsSeparableExtension (ToType (S.residueField (f x)))
(ToType (X.residueField x)))
(hngen : f.asFiber x ∉ genericPoints (f.fiber (f x))) :
∃ (U : X.Opens) (_hU : IsAffineOpen U) (hxU : x ∈ U)
(I : U.toScheme.IdealSheafData),
Stacks.Divisors.IsEffectiveCartierDivisor I ∧
(⟨x, hxU⟩ : U.toScheme) ∈ I.support ∧
Smooth (I.subschemeι ≫ U.ι ≫ f)
Tag 057G, a lemma
Tag 057G in the Stacks Project.
Stacks.AlgebraicGeometry.exists_etale_immersion_with_singleton_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CohenMacaulaySlice/EtaleSlice.lean, line 504. References: EGA IV (17.16.3), “Clause (i)”; SGA 3 XI (1.10), “more general”.
Stacks Project, Tag 057G. Let
f : X ⟶ Sbe a morphism of schemes,x : Xa point with images = f x. Iffis smooth atx, ifxis a closed point of the fibreX_s, and if the residue field extensionκ(x)/κ(s)is separable, then there is an immersioni : Z ⟶ Xwhose image containsxsuch thatZ ⟶ Sis étale andZ_s = {x}set theoretically.
public theorem exists_etale_immersion_with_singleton_fiber
{X S : Scheme.{u}} (f : X ⟶ S) (x : X)
(hsmooth : InfinitesimalLifting.SmoothAt f x)
(hclosed : IsClosed ({f.asFiber x} : Set (f.fiber (f x))))
(hsep : letI := (f.residueFieldMap x).hom.toAlgebra
Algebra.IsSeparableExtension (S.residueField (f x)) (X.residueField x)) :
∃ (Z : Scheme.{u}) (i : Z ⟶ X) (z : Z),
IsImmersion i ∧ i z = x ∧ Etale (i ≫ f) ∧
{z' : Z | (i ≫ f) z' = f x} = {z}
Tag 055U, a lemma
Tag 055U in the Stacks Project.
AlgebraicGeometry.exists_etaleNeighborhood_lift_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/EtaleLocalSection.lean, line 241.
Stacks Project, Tag 055U. A smooth morphism admits an étale local section through any point of its image.
theorem exists_etaleNeighborhood_lift_of_smooth {X S : Scheme.{u}}
(f : X ⟶ S) [Smooth f] (s : S) (hs : s ∈ Set.range f.base) :
∃ (W : EtaleNeighborhood S s) (g : W.scheme ⟶ X), g ≫ f = W.toBase
Tag 055V, a lemma
Tag 055V in the Stacks Project.
AlgebraicGeometry.exists_etale_cover_refining_smooth_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmoothRefinement.lean, line 49.
Stacks Project, Tag 055V. Every smooth covering of a scheme is refined by an étale covering.
public theorem exists_etale_cover_refining_smooth_cover {S : Scheme.{u}}
(𝒰 : S.Cover.{v} (Scheme.precoverage (@Smooth.{u}))) :
∃ 𝒱 : S.Cover.{u} (Scheme.precoverage (@Etale.{u})),
Nonempty (𝒱.toPreZeroHypercover.Hom 𝒰.toPreZeroHypercover)
Tag 0EY4, a lemma
Tag 0EY4 in the Stacks Project.
AlgebraicGeometry.exists_etaleCover_factors_affine_smooth_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SlicingSmooth/AffineConnectedCover.lean, line 176.
A smooth morphism of schemes admits an étale covering of its source each member of which maps to the base through an étale morphism, the first factor being a smooth morphism of affine schemes which has a section and has geometrically connected fibres.
theorem exists_etaleCover_factors_affine_smooth_section {X S : Scheme.{u}} (f : X ⟶ S)
[Smooth f] :
∃ 𝒰 : X.Cover.{u} Scheme.etalePrecoverage, ∀ i : 𝒰.I₀,
∃ (Bᵢ : Scheme.{u}) (h : Bᵢ ⟶ S) (g : 𝒰.X i ⟶ Bᵢ) (σ : Bᵢ ⟶ 𝒰.X i),
Etale h ∧ IsAffine (𝒰.X i) ∧ IsAffine Bᵢ ∧ Smooth g ∧ σ ≫ g = 𝟙 Bᵢ ∧
GeometricallyConnected g ∧ g ≫ h = 𝒰.f i ≫ f
Sources
Section37.39 Étale neighbourhoods and Artin approximation#
Section 37.39 of the Stacks Project, Tag 0CAT. 9 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0CAU, a lemma
Tag 0CAU in the Stacks Project.
StacksDraft.ArtinApproximation.exists_elementaryEtaleNeighborhood_approximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/ArtinApproximationScheme.lean, line 509. The attribute's comment: “the full scheme-level statement, with the congruence in the completed local ring of the neighbourhood. The hypotheses are exactly the source's own: S locally Noetherian, f and g locally of finite type, x and y over the same point, 𝒪_{S, s} a G-ring, and the local 𝒪_{S, s}-algebra map φ : 𝒪_{Y, y} → 𝒪^∧_{X, x}. The affine case enters through the unconditional Stacks 0CAR StacksDraft.ArtinApproximation.artinApproximationGRing. The source's own proof of 37.39.1 is the reduction to the affine case, and that reduction is what is PROVED here on top of the affine case StacksDraft.ArtinApproximation.exists_etaleApproximation: the affine charts, the chart descriptions of the three local rings, the elementariness of the neighbourhood from the ring-level residue field equality, and the transport of the congruence. The source states the conclusion for a diagram; here it is the single congruence that the diagram expresses.”.
Stacks Project, Tag 0CAU (More on Morphisms, Lemma 37.39.1). Let
Sbe a locally Noetherian scheme, letf : X ⟶ Sandg : Y ⟶ Sbe locally of finite type, and letx ∈ Xandy ∈ Ylie over the same points = f x = g yofS. Assume𝒪_{S, s}is a G-ring, and letφ : 𝒪_{Y, y} → 𝒪^∧_{X, x}be a local homomorphism of𝒪_{S, s}-algebras. Then for everyN ≥ 1there are an elementary étale neighbourhood(U, u)of(X, x)and a morphismF : U ⟶ YoverSwithF u = ysuch that the square formed byφ, the map𝒪^∧_{X, x} → 𝒪^∧_{U, u}, the mapF^♯_u : 𝒪_{Y, y} → 𝒪_{U, u}and𝒪_{U, u} → 𝒪^∧_{U, u}commutes modulo𝔪_u^N.The proof reduces to the affine case
StacksDraft.ArtinApproximation.exists_etaleApproximation, which rests on Stacks 0CARStacksDraft.ArtinApproximation.artinApproximationGRing: it chooses affine charts, transportsφto the charts, and readsSpec A'as an elementary étale neighbourhood of(X, x)with a morphism toYoverS.
theorem exists_elementaryEtaleNeighborhood_approximation
{S X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
[IsLocallyNoetherian S] [LocallyOfFiniteType f] [LocallyOfFiniteType g]
(x : X) (y : Y) (hxy : f x = g y)
(hG : IsGRing (S.presheaf.stalk (f x)))
(N : ℕ) (hN : 1 ≤ N)
(φ : Y.presheaf.stalk y →+*
AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))
(hφ : IsLocalHom φ)
(hbase : φ.comp ((S.presheaf.stalkCongr (.of_eq hxy)).hom ≫ g.stalkMap y).hom =
(algebraMap (X.presheaf.stalk x)
(AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))).comp
(f.stalkMap x).hom) :
∃ U : EtaleNeighborhood X x, U.IsElementary ∧
∃ (F : U.scheme ⟶ Y) (hF : F U.point = y), F ≫ g = U.toBase ≫ f ∧
∀ a : Y.presheaf.stalk y,
adicCompletionMap
(((X.presheaf.stalkCongr (.of_eq U.map_point.symm)).hom ≫
U.toBase.stalkMap U.point).hom)
(maximalIdeal (X.presheaf.stalk x))
(maximalIdeal (U.scheme.presheaf.stalk U.point))
(map_maximalIdeal_le_etaleNeighborhood U) (φ a) -
algebraMap (U.scheme.presheaf.stalk U.point)
(AdicCompletion (maximalIdeal (U.scheme.presheaf.stalk U.point))
(U.scheme.presheaf.stalk U.point))
(((Y.presheaf.stalkCongr (.of_eq hF.symm)).hom ≫ F.stalkMap U.point).hom a) ∈
Ideal.map
(algebraMap (U.scheme.presheaf.stalk U.point)
(AdicCompletion (maximalIdeal (U.scheme.presheaf.stalk U.point))
(U.scheme.presheaf.stalk U.point)))
(maximalIdeal (U.scheme.presheaf.stalk U.point) ^ N)
Tag 0CAV, a lemma
Tag 0CAV in the Stacks Project.
StacksDraft.ArtinApproximation.exists_common_elementaryEtaleNeighborhood_of_adicCompletion_ringEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/IsomorphismApproximation.lean, line 391. The attribute's comment: “with NO carried hypotheses, exactly as Tag 0CAU it rests on: the only hypotheses are the source's own. Everything in the source's own proof of 37.39.2 is proved here. The congruence is stated on the whole completed local ring of the neighbourhood rather than only on the image of the local ring, which is what the source's diagram of complete local rings asserts”.
Stacks Project, Tag 0CAV (More on Morphisms, Lemma 37.39.2). Let
Sbe a locally Noetherian scheme, letf : X ⟶ Sandg : Y ⟶ Sbe locally of finite type, and letx ∈ Xandy ∈ Ylie over a common pointsofSwhose local ring is a G-ring. Suppose given an isomorphismΦ : 𝒪^∧_{Y, y} ≅ 𝒪^∧_{X, x}which is compatible with the two maps from𝒪_{S, s}. Then for everyN ≥ 1there is a single pointed scheme(U, u)sitting in a diagram(X, x) ← (U, u) → (Y, y)overSin which both legs are elementary étale neighbourhoods, and over which the triangle of completed local rings commutes modulo𝔪_u ^ N: for everyz ∈ 𝒪^∧_{Y, y}, the two images ofzin𝒪^∧_{U, u}— one obtained by transportingzthroughΦand then along the first leg, the other by going directly along the second leg — differ by an element of𝔪_u ^ N · 𝒪^∧_{U, u}.Tag 0CAU already produces the neighbourhood
(U₀, u₀)of(X, x)and a morphismF : U₀ ⟶ YoverSwhose congruence holds on the image of𝒪_{Y, y}. The content added here is thatFis étale atu₀, which is extracted from the congruence itself: it forces the induced map𝒪^∧_{Y, y} → 𝒪^∧_{U₀, u₀}to be bijective, and a bijection of completions upgrades to étaleness of local rings by Tag 039M. ShrinkingU₀to an open on whichFis étale gives the required(U, u).The difference of the two completion maps is written with an explicit
HSubinstance because the two completions are only definitionally, not reducibly, the same ring: the second is indexed by the scheme ofEtaleNeighborhood.along, whoseschemefield is the first one byrfl. The term is the ordinary_ - _.
theorem exists_common_elementaryEtaleNeighborhood_of_adicCompletion_ringEquiv
{S X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
[IsLocallyNoetherian S] [LocallyOfFiniteType f] [LocallyOfFiniteType g]
(x : X) (y : Y) (hxy : f x = g y)
(hG : IsGRing (S.presheaf.stalk (f x)))
(N : ℕ) (hN : 1 ≤ N)
(Φ : AdicCompletion (maximalIdeal (Y.presheaf.stalk y)) (Y.presheaf.stalk y) ≃+*
AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))
(hΦ : Φ.toRingHom.comp ((algebraMap (Y.presheaf.stalk y)
(AdicCompletion (maximalIdeal (Y.presheaf.stalk y)) (Y.presheaf.stalk y))).comp
((S.presheaf.stalkCongr (.of_eq hxy)).hom ≫ g.stalkMap y).hom) =
(algebraMap (X.presheaf.stalk x)
(AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))).comp
(f.stalkMap x).hom) :
∃ (U : EtaleNeighborhood X x) (q : U.scheme ⟶ Y) (hqEt : Etale q) (hq : q U.point = y),
U.IsElementary ∧ (U.along q hqEt hq).IsElementary ∧ q ≫ g = U.toBase ≫ f ∧
∀ z : AdicCompletion (maximalIdeal (Y.presheaf.stalk y)) (Y.presheaf.stalk y),
@HSub.hSub _ _ _ instHSub (U.completionMap (Φ z))
((U.along q hqEt hq).completionMap z) ∈
Ideal.map (algebraMap (U.scheme.presheaf.stalk U.point)
(AdicCompletion (maximalIdeal (U.scheme.presheaf.stalk U.point))
(U.scheme.presheaf.stalk U.point)))
(maximalIdeal (U.scheme.presheaf.stalk U.point) ^ N)
Tag 0GDX, a lemma
Tag 0GDX in the Stacks Project.
AlgebraicGeometry.exists_elementaryEtaleNeighborhood_absoluteApproximation_full_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/AbsoluteApproximationFull.lean, line 92. The attribute's comment: “clauses (1), (2), (3) and (4) of the conclusion, together with the commutativity of the source's diagram: (1) the elementary étale neighbourhood (V, v) of (S, s); (2) the morphism F : W ⟶ X with F(w) = x, étale and trivial on residue fields at w, i.e. an elementary étale neighbourhood (W, w) → (X, x); (3) τ(v) = t; and (4) the elementary étale neighbourhood (W, w) → (Y ×_{T, τ} V, y_τ). HOW y_τ IS SPECIFIED -- the one part of the source's sentence that is NOT proved: the source takes for y_τ the point corresponding to y_σ under the identification (Y_σ)_s = (Y ×_T V)_v. Here y_τ is specified by lying over y and over v, together with the equality of the two morphisms Spec κ(s) ⟶ T -- one through Spec 𝒪^∧_{S, s} and σ, one through V and τ -- which IS that identification of the two fibres as one and the same scheme. That y_τ and y_σ are the same point OF that common fibre is not established. NO hypothesis beyond the source's is carried: Theorem 07QZ in particular is not, being proved as StacksDraft.ArtinApproximation.localApproximationProperty, so Tags 0CAU, 0CAV, 07GC, 07PS, 01ZC, 01ZM, 07RP and 057G that this rests on are unconditional. Two of the source's hypotheses are WEAKENED, so what is proved is stronger there: T of finite type over Spec ℤ is only required to be LOCALLY of finite type, and φ is only required to be a map of 𝒪_{S, s}-algebras rather than of 𝒪^∧_{S, s}-algebras”.
Stacks Tag 0GDX, clauses (1)–(4), with the two morphisms
Spec κ(s) ⟶ Tidentified. LetfX : X ⟶ Sbe locally of finite type withSlocally Noetherian, letgY : Y ⟶ Tbe locally of finite type withTof finite type overℤ, letx ∈ Xlie overs ∈ Swith𝒪_{S, s}a G-ring, and letσ : 𝒪_{T, t} → 𝒪^∧_{S, s}be a local homomorphism. Letyσbe a point ofY ×_T Spec 𝒪^∧_{S, s}lying overy ∈ Yand over the closed point, and letφ : 𝒪^∧_{X, x} ≅ 𝒪^∧_{Y ×_T Spec 𝒪^∧_{S, s}, yσ}be an isomorphism of𝒪_{S, s}-algebras. Then there are an elementary étale neighbourhoodVof(S, s), a morphismτ : V ⟶ Tcarrying the marked point tot, a pointyτofY ×_{T, τ} Voveryand over the marked point ofV, and an elementary étale neighbourhoodWof(Y ×_{T, τ} V, yτ)together with a morphismF : W ⟶ Xcarrying the marked point toxwhich is étale, trivial on residue fields, and compatible with the structure morphisms toS; moreover the canonical sectionSpec κ(s) ⟶ Spec 𝒪^∧_{S, s}followed bySpec 𝒪^∧_{S, s} ⟶ Tagrees with the canonical sectionSpec κ(s) ⟶ Vfollowed byτ.
public theorem exists_elementaryEtaleNeighborhood_absoluteApproximation_full_section
{S T X Y : Scheme.{u}} [IsLocallyNoetherian S]
(fX : X ⟶ S) (gY : Y ⟶ T) [LocallyOfFiniteType fX] [LocallyOfFiniteType gY]
(hT : LocallyOfFiniteType (specULiftZIsTerminal.{u}.from T))
(x : X) (s : S) (hfx : fX x = s) (t : T) (y : Y)
(hG : IsGRing (S.presheaf.stalk s))
(σ : T.presheaf.stalk t →+* AdicCompletion (maximalIdeal (S.presheaf.stalk s))
(S.presheaf.stalk s))
(hσ : IsLocalHom σ)
(yσ : ↥(pullback gY (Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t)))
(hyσ₁ : pullback.fst gY (Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t) yσ = y)
(hyσ₂ : pullback.snd gY (Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t) yσ =
closedPoint _)
(φ : AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x) ≃+*
AdicCompletion (maximalIdeal ((pullback gY (Spec.map (CommRingCat.ofHom σ) ≫
T.fromSpecStalk t)).presheaf.stalk yσ))
((pullback gY (Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t)).presheaf.stalk yσ))
(hbase : (pullback.snd gY (Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t) ≫
Spec.map (CommRingCat.ofHom (algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)))) ≫
S.fromSpecStalk s) yσ = s)
(hφ : φ.toRingHom.comp ((algebraMap (X.presheaf.stalk x)
(AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))).comp
(fX.stalkHomAt hfx)) =
(algebraMap ((pullback gY (Spec.map (CommRingCat.ofHom σ) ≫
T.fromSpecStalk t)).presheaf.stalk yσ)
(AdicCompletion (maximalIdeal ((pullback gY (Spec.map (CommRingCat.ofHom σ) ≫
T.fromSpecStalk t)).presheaf.stalk yσ))
((pullback gY (Spec.map (CommRingCat.ofHom σ) ≫
T.fromSpecStalk t)).presheaf.stalk yσ))).comp
((pullback.snd gY (Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t) ≫
Spec.map (CommRingCat.ofHom (algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)))) ≫
S.fromSpecStalk s).stalkHomAt hbase)) :
∃ V : EtaleNeighborhood S s, ∃ hVel : V.IsElementary,
∃ (τ : V.scheme ⟶ T) (_ : τ V.point = t),
specResidueFieldSection (Spec.map (CommRingCat.ofHom (algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)))) ≫
S.fromSpecStalk s) (specCompletedStalkToBase_closedPoint s)
(isIso_residueFieldMap_specCompletedStalkToBase s) ≫
(Spec.map (CommRingCat.ofHom σ) ≫ T.fromSpecStalk t) =
specResidueFieldSection V.toBase V.map_point
((EtaleNeighborhood.isElementary_iff V).mp hVel) ≫ τ ∧
∃ yτ : ↥(pullback gY τ),
pullback.fst gY τ yτ = y ∧ pullback.snd gY τ yτ = V.point ∧
∃ W : EtaleNeighborhood (pullback gY τ) yτ, W.IsElementary ∧
∃ (F : W.scheme ⟶ X) (_ : F W.point = x),
Etale F ∧ IsIso (F.residueFieldMap W.point) ∧
F ≫ fX = W.toBase ≫ pullback.snd gY τ ≫ V.toBase
StacksDraft.ArtinApproximation.exists_elementaryEtaleNeighborhood_absoluteApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteTypeBaseApproximation.lean, line 280. The attribute's comment: “clauses (1) and (3) of the conclusion: the elementary étale neighbourhood (V, v) of (S, s) and the morphism τ : V ⟶ T with τ(v) = t. What is proved is STRONGER than those two clauses: it carries in addition the congruence that Tag 0CAW records as its clause (3), namely that the square relating σ to τ^♯_v commutes modulo 𝔪_v ^ N, which is why this registration is kept; and the source's T of finite type over Spec ℤ is weakened to LOCALLY of finite type. None of X, Y, φ, y_σ enters this statement, so it says nothing about clauses (2) and (4) — the elementary étale neighbourhood (W, w) of (X, x) which is simultaneously one of (Y ×_{T, τ} V, y_τ). THOSE ARE PROVED ELSEWHERE, twice over and independently, and both of those statements carry a registration for the whole conclusion: all four clauses are AlgebraicGeometry.exists_elementaryEtaleNeighborhood_absoluteApproximation_full_section in StacksFrontier.AlgebraicGeometry.Morphisms.EtaleNeighbourhood.AbsoluteApproximationFull, and also StacksDraft.ArtinApproximation.exists_common_elementaryEtaleNeighborhood_absoluteApproximation in StacksFrontier.AlgebraicGeometry.Morphisms.EtaleNeighbourhood.RelativeMapApproximation. NO hypothesis beyond the source's is carried: the library's Tag 0CAU behind this deduction is unconditional, Theorem 07QZ being proved as StacksDraft.ArtinApproximation.localApproximationProperty”.
Stacks Project, Tag 0GDX, clauses (1) and (3). Let
Sbe a locally Noetherian scheme, letTbe locally of finite type overSpec ℤ, lett ∈ Tands ∈ S, assume𝒪_{S, s}is a G-ring, and letσ : 𝒪_{T, t} → 𝒪^∧_{S, s}be a local homomorphism. Then for everyN ≥ 1there are an elementary étale neighbourhood(V, v)of(S, s)and a morphismτ : V ⟶ Twithτ v = t; moreover the square relatingσtoτ^♯_vcommutes modulo𝔪_v ^ N, which is the extra conclusion that Tag 0CAW records as its clause (3).
theorem exists_elementaryEtaleNeighborhood_absoluteApproximation
{S T : Scheme.{u}} [IsLocallyNoetherian S]
(hT : LocallyOfFiniteType (specULiftZIsTerminal.{u}.from T))
(t : T) (s : S) (hG : IsGRing (S.presheaf.stalk s))
(N : ℕ) (hN : 1 ≤ N)
(σ : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))
(hσ : IsLocalHom σ) :
∃ V : EtaleNeighborhood S s, V.IsElementary ∧
∃ (τ : V.scheme ⟶ T) (hτ : τ V.point = t),
∀ a : T.presheaf.stalk t,
V.completionMap (σ a) -
algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)) (τ.stalkHomAt hτ a) ∈
Ideal.map
(algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)))
(maximalIdeal (V.scheme.presheaf.stalk V.point) ^ N)
StacksDraft.ArtinApproximation.exists_common_elementaryEtaleNeighborhood_absoluteApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/RelativeMapApproximation.lean, line 4440. The attribute's comment: “What is proved is STRONGER than the source in two respects, both inherited from the first stage of Tag 0CAW which replaces the étale slice of Tag 057G here: the pair (V, τ) satisfies in addition the congruence that Tag 0CAW records as its clause (3), namely that the square relating σ to τ^♯_v commutes modulo 𝔪_v ^ N for the given N ≥ 1; and the source's T of finite type over Spec ℤ is weakened to LOCALLY of finite type”.
Stacks Project, Tag 0GDX. Let
Sbe a locally Noetherian scheme, lets ∈ Shave a G-ring local ring, letTbe locally of finite type overSpec ℤ, letp : X ⟶ Sandq : Y ⟶ Tbe locally of finite type, letx ∈ Xlie oversandy ∈ Yovert ∈ T, and letσ : 𝒪_{T, t} → 𝒪^∧_{S, s}be a local homomorphism. WriteY_σ = Y ×_{T, σ} Spec 𝒪^∧_{S, s}and lety_σ ∈ Y_σlie overyand over the closed point. An isomorphismφ : 𝒪^∧_{X, x} ≅ 𝒪^∧_{Y_σ, y_σ}of𝒪_{S, s}-algebras is then induced, after elementary étale changes, by a morphism of schemes: there are an elementary étale neighbourhood(V, v)of(S, s), a morphismτ : V ⟶ Twithτ v = t, and an elementary étale neighbourhood(W, w)of(X, x)which is simultaneously an elementary étale neighbourhood of(Y ×_{T, τ} V, y_τ), wherey_τcorresponds toy_σunder the identification of the closed fibres(Y_σ)_s = (Y ×_T V)_v.The identification of the closed fibres is given explicitly: an isomorphism
eof the residue fields of the two bases compatible with their maps toSand toT, and an isomorphism of the scheme-theoretic fibres compatible with the two maps toYand withe, carrying the point abovey_σto the point abovey_τ.
theorem exists_common_elementaryEtaleNeighborhood_absoluteApproximation
{X S Y T : Scheme.{u}} [IsLocallyNoetherian S] (p : X ⟶ S) (q : Y ⟶ T)
[LocallyOfFiniteType p] [LocallyOfFiniteType q]
(hT : LocallyOfFiniteType (specULiftZIsTerminal.{u}.from T))
{x : X} {s : S} {y : Y} {t : T} (hx : p x = s) (hy : q y = t)
(hG : IsGRing (S.presheaf.stalk s)) (N : ℕ) (hN : 1 ≤ N)
(σ : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))
(hσ : IsLocalHom σ)
(yσ : (pullback q (relativeBaseChangeMorphism s σ) : Scheme.{u}))
(hyσY : pullback.fst q (relativeBaseChangeMorphism s σ) yσ = y)
(hyσZ : pullback.snd q (relativeBaseChangeMorphism s σ) yσ =
specCompletedStalkPoint S s)
(φ : AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x) ≃+*
AdicCompletion
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
(hφ : φ.toRingHom.comp ((algebraMap (X.presheaf.stalk x)
(AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))).comp
(p.stalkHomAt hx)) =
(algebraMap ((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ)
(AdicCompletion
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))).comp
(((pullback.snd q (relativeBaseChangeMorphism s σ)).stalkHomAt hyσZ).comp
((specCompletedStalkTo S s).stalkHomAt
(specCompletedStalkTo_specCompletedStalkPoint S s)))) :
∃ (V : EtaleNeighborhood S s) (τ : V.scheme ⟶ T) (hτ : τ V.point = t)
(yτ : (pullback q τ : Scheme.{u}))
(_ : pullback.fst q τ yτ = y) (hyτV : pullback.snd q τ yτ = V.point)
(W : EtaleNeighborhood X x) (g : W.scheme ⟶ pullback q τ)
(hgPoint : g W.point = yτ) (_ : Etale g),
V.IsElementary ∧ W.IsElementary ∧
IsIso (((pullback q τ).residueFieldCongr hgPoint).inv ≫
g.residueFieldMap W.point) ∧
g ≫ pullback.snd q τ ≫ V.toBase = W.toBase ≫ p ∧
(∀ b : T.presheaf.stalk t,
V.completionMap (σ b) -
algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)) (τ.stalkHomAt hτ b) ∈
Ideal.map
(algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)))
(maximalIdeal (V.scheme.presheaf.stalk V.point) ^ N)) ∧
∃ (eBase : (specCompletedStalk S s).residueField (specCompletedStalkPoint S s) ≅
V.scheme.residueField V.point)
(eFiber : (pullback.snd q (relativeBaseChangeMorphism s σ)).fiber
(specCompletedStalkPoint S s) ≅
(pullback.snd q τ).fiber V.point),
(Spec.map eBase.inv ≫ V.scheme.fromSpecResidueField V.point ≫ V.toBase =
(specCompletedStalk S s).fromSpecResidueField (specCompletedStalkPoint S s) ≫
specCompletedStalkTo S s) ∧
(Spec.map eBase.inv ≫ V.scheme.fromSpecResidueField V.point ≫ τ =
(specCompletedStalk S s).fromSpecResidueField (specCompletedStalkPoint S s) ≫
relativeBaseChangeMorphism s σ) ∧
(eFiber.hom ≫ (pullback.snd q τ).fiberι V.point ≫ pullback.fst q τ =
(pullback.snd q (relativeBaseChangeMorphism s σ)).fiberι
(specCompletedStalkPoint S s) ≫
pullback.fst q (relativeBaseChangeMorphism s σ)) ∧
(eFiber.hom ≫ (pullback.snd q τ).fiberToSpecResidueField V.point =
(pullback.snd q (relativeBaseChangeMorphism s σ)).fiberToSpecResidueField
(specCompletedStalkPoint S s) ≫ Spec.map eBase.inv) ∧
(eFiber.hom (((pullback.snd q (relativeBaseChangeMorphism s σ)).fiberHomeo
(specCompletedStalkPoint S s)).symm ⟨yσ, hyσZ⟩) =
((pullback.snd q τ).fiberHomeo V.point).symm ⟨yτ, hyτV⟩)
Tag 0CAW, a lemma
Tag 0CAW in the Stacks Project.
StacksDraft.ArtinApproximation.exists_elementaryEtaleNeighborhood_baseApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/BaseChangeApproximation.lean, line 131. The attribute's comment: “the FIRST STAGE of the conclusion: clause (1) for v and τ (v ↦ s and τ(v) = t), clause (2) ((V, v) → (S, s) is an elementary étale neighbourhood) and clause (3) (the square relating σ to τ^♯_v commutes modulo 𝔪_v ^ N), with τ a morphism over S. This is the source's own last step, Tag 0CAU applied to (S, s) ← (S, s), (T, t) → (S, s) and σ. Clauses (4) and (5) are NOT established by this declaration; see StacksDraft.ArtinApproximation.exists_elementaryEtaleNeighborhood_relativeApproximation. There is NO hypothesis beyond the source's: the Tag 0CAU used here is unconditional, Theorem 07QZ being proved as StacksDraft.ArtinApproximation.localApproximationProperty”.
Stacks Project, Tag 0CAW, first stage: clauses (1) for
(v, τ), (2) and (3). LetSbe a locally Noetherian scheme, leth : T ⟶ Sbe locally of finite type, lett ∈ Tlie overs ∈ S, assume𝒪_{S, s}is a G-ring, and letσ : 𝒪_{T, t} → 𝒪^∧_{S, s}be a local homomorphism of𝒪_{S, s}-algebras. Then for everyN ≥ 1there are an elementary étale neighbourhood(V, v)of(S, s)and a morphismτ : V ⟶ ToverSwithτ v = tsuch that the squarecommutes modulo𝒪^∧_{S, s} ⟶ 𝒪^∧_{V, v} ↑σ ↑ 𝒪_{T, t} —τ^♯—→ 𝒪_{V, v}𝔪_v ^ N.This is Tag 0CAU for the pointed diagram
(S, s) ← (S, s),(T, t) → (S, s)and the mapσ: the source's own proof of 0CAW ends by applying 0CAU "one more time toSpec CandSpec RoverSpec Rand the mapC → R^∧", and that application is this statement.
theorem exists_elementaryEtaleNeighborhood_baseApproximation
{S T : Scheme.{u}} (h : T ⟶ S)
[IsLocallyNoetherian S] [LocallyOfFiniteType h]
(t : T) (s : S) (hts : h t = s)
(hG : IsGRing (S.presheaf.stalk s))
(N : ℕ) (hN : 1 ≤ N)
(σ : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))
(hσ : IsLocalHom σ)
(hσbase : σ.comp (h.stalkHomAt hts) =
algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))) :
∃ V : EtaleNeighborhood S s, V.IsElementary ∧
∃ (τ : V.scheme ⟶ T) (hτ : τ V.point = t), τ ≫ h = V.toBase ∧
∀ a : T.presheaf.stalk t,
V.completionMap (σ a) -
algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)) (τ.stalkHomAt hτ a) ∈
Ideal.map
(algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)))
(maximalIdeal (V.scheme.presheaf.stalk V.point) ^ N)
StacksDraft.ArtinApproximation.exists_elementaryEtaleNeighborhood_relativeApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/BaseChangeApproximation.lean, line 201. The attribute's comment: “the SECOND STAGE of the conclusion, for a first stage supplied as hypotheses: the remaining part of clause (1) — w ↦ (y, v), which is W.map_point, and the morphism f : W ⟶ X ×_S V with f(w) = (x, v), delivered as the two projection identities of f together with F w = x and the hypothesis placing y_τ over v — clause (4) ((W, w) → (Y ×_{T, τ} V, (y, v)) is an elementary étale neighbourhood), and clause (5) in the form of the congruence modulo 𝔪_w ^ N in 𝒪^∧_{W, w} that the source's square expresses once the identification 𝒪_{Y_σ, y_σ}/𝔪^N = 𝒪_{Y ×_{T, τ} V, (y, v)}/𝔪^N is removed from both sides. HYPOTHESES BEYOND THE SOURCE'S, all stated explicitly — Theorem 07QZ is NOT among them, the Tag 0CAU used here being unconditional: (a) the first stage itself, i.e. the elementary étale neighbourhood (V, v) of (S, s) with the morphism τ : V ⟶ T, which StacksDraft.ArtinApproximation.exists_elementaryEtaleNeighborhood_baseApproximation produces from the source's hypotheses; (b) the point y_τ of Y ×_{T, τ} V over v; (c) the local 𝒪_{S, s}-algebra map φ : 𝒪_{X, x} → 𝒪^∧_{Y ×_{T, τ} V, y_τ} in place of the source's φ : 𝒪_{X, x} → 𝒪^∧_{Y_σ, y_σ}, the bridge between the two being the canonical isomorphism of Y_σ with Y ×_{T, τ} V over 𝒪_{V, v}/𝔪_v ^ N = 𝒪_{S, s}/𝔪_s ^ N which clauses (2) and (3) make available. That identification IS constructed, as StacksDraft.ArtinApproximation.exists_truncationEquiv_stalk_relativeBaseChange, but only as an isomorphism of the local rings TRUNCATED at 𝔪 ^ N, which is the shape clause (5) uses it in; it does not produce a map into the COMPLETED local ring 𝒪^∧_{Y ×_{T, τ} V, (y, v)} out of the source's φ, and no isomorphism of the completions exists, so hypothesis (c) is not discharged by it”.
Stacks Project, Tag 0CAW, second stage: the rest of clause (1), clause (4), and clause (5) in the form of a congruence in
𝒪^∧_{W, w}. Given the first stage — an elementary étale neighbourhood(V, v)of(S, s)and a morphismτ : V ⟶ T— a pointy_τofY ×_{T, τ} Vlying overv, and a local𝒪_{S, s}-algebra mapφ : 𝒪_{X, x} → 𝒪^∧_{Y ×_{T, τ} V, y_τ}, there are for everyN ≥ 1an elementary étale neighbourhood(W, w)of(Y ×_{T, τ} V, y_τ)and a morphismF : W ⟶ XoverSwithF w = x, hence a morphismW ⟶ X ×_S Vcarryingwto(x, v), such thatφfollowed by the map𝒪^∧_{Y ×_{T, τ} V, y_τ} → 𝒪^∧_{W, w}agrees modulo𝔪_w ^ Nwith the map𝒪_{X, x} → 𝒪_{W, w}induced byF.This is Tag 0CAU for the pointed diagram
(Y ×_{T, τ} V, y_τ) → (S, s),(X, x) → (S, s), the first leg being read overSthroughV ⟶ S.
theorem exists_elementaryEtaleNeighborhood_relativeApproximation
{S T X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ T)
[IsLocallyNoetherian S] [LocallyOfFiniteType f] [LocallyOfFiniteType g]
(x : X) (hG : IsGRing (S.presheaf.stalk (f x)))
(V : EtaleNeighborhood S (f x)) (τ : V.scheme ⟶ T)
(yτ : ↥(pullback g τ)) (hyτ : pullback.snd g τ yτ = V.point)
(N : ℕ) (hN : 1 ≤ N)
(φ : X.presheaf.stalk x →+*
AdicCompletion (maximalIdeal ((pullback g τ).presheaf.stalk yτ))
((pullback g τ).presheaf.stalk yτ))
(hφ : IsLocalHom φ)
(hφbase : φ.comp (f.stalkMap x).hom =
(algebraMap ((pullback g τ).presheaf.stalk yτ)
(AdicCompletion (maximalIdeal ((pullback g τ).presheaf.stalk yτ))
((pullback g τ).presheaf.stalk yτ))).comp
(((pullback.snd g τ).stalkHomAt hyτ).comp V.stalkHom)) :
∃ W : EtaleNeighborhood (pullback g τ) yτ, W.IsElementary ∧
∃ (F : W.scheme ⟶ X) (hF : F W.point = x),
F ≫ f = W.toBase ≫ pullback.snd g τ ≫ V.toBase ∧
(∃ fW : W.scheme ⟶ pullback f V.toBase,
fW ≫ pullback.fst f V.toBase = F ∧
fW ≫ pullback.snd f V.toBase = W.toBase ≫ pullback.snd g τ) ∧
∀ a : X.presheaf.stalk x,
W.completionMap (φ a) -
algebraMap (W.scheme.presheaf.stalk W.point)
(AdicCompletion (maximalIdeal (W.scheme.presheaf.stalk W.point))
(W.scheme.presheaf.stalk W.point)) (F.stalkHomAt hF a) ∈
Ideal.map
(algebraMap (W.scheme.presheaf.stalk W.point)
(AdicCompletion (maximalIdeal (W.scheme.presheaf.stalk W.point))
(W.scheme.presheaf.stalk W.point)))
(maximalIdeal (W.scheme.presheaf.stalk W.point) ^ N)
StacksDraft.ArtinApproximation.exists_relativeMapApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/CompletedBaseChangeMapApproximation.lean, line 344. The attribute's comment: “the source's own hypotheses, with nothing beyond them: h : T ⟶ S locally of finite type, a G-ring 𝒪_{S, s}, a local 𝒪_{S, s}-algebra map σ : 𝒪_{T, t} → 𝒪^∧_{S, s}, the base change Y_σ = Y ×_{T, σ} Spec 𝒪^∧_{S, s}, a point y_σ of Y_σ over y (the source's the point: lying over y forces it over the closed point, by StacksDraft.ArtinApproximation.snd_eq_closedPoint_of_fst_eq, so no second hypothesis places it there) and a local 𝒪_{S, s}-algebra map φ : 𝒪_{X, x} → 𝒪^∧_{Y_σ, y_σ}. Theorem 07QZ is discharged, not an input: the LocalApproximationProperty hypothesis of Tag 0CAU behind both stages is supplied by StacksDraft.ArtinApproximation.localApproximationProperty, which rests on the unconditional Tag 07QZ Stacks.Smoothing.exists_localEtaleSolution_of_isGRing and hence on the unconditional Popescu Theorem 07GC Stacks.Smoothing.indSmooth_of_isRegularRingMap. The conclusion is the source's whole diagram: clause (1) — v ↦ s, τ(v) = t, f(w) = (x, v) as the two projection identities of f with F w = x, and w ↦ (y, v) as W.map_point with the point of Y ×_{T, τ} V lying over y and v; clause (2); clause (3); clause (4); and clause (5), the commuting square, whose = between 𝒪_{Y_σ, y_σ}/𝔪^N and 𝒪_{Y ×_{T, τ} V, (y, v)}/𝔪^N is exhibited as the ring isomorphism θ together with the two compatibilities that characterise it as the source's canonical identification over 𝒪_{V, v}/𝔪_v ^ N = 𝒪_{S, s}/𝔪_s ^ N: it matches the two maps from 𝒪_{Y, y} and the two maps from 𝒪_{S, s}. Only the truncations are identified; the completions need not be isomorphic, as the cusp-versus-node example in the module docstring of StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteTypeBaseApproximation.lean shows. The route is the source's own: Tag 0CAU over Spec 𝒪^∧_{S, s} replaces φ by a morphism to X out of an elementary étale neighbourhood of (Y_σ, y_σ), that pointed span descends to a smooth stage of Popescu's presentation of 𝒪^∧_{S, s}, and Tag 0CAU applied one more time to Spec 𝒪_{T, t} and Spec 𝒪_{S, s} over Spec 𝒪_{S, s} replaces the stage by (V, v); θ is the order-N comparison of the two base changes of the stage object, along Spec 𝒪^∧_{S, s} ⟶ D and along V ⟶ D, read through the two étale legs. The identification of the closed fibres (Y_σ)_s ≅ (Y ×_T V)_v of Tag 0GDX is recorded as well”.
Stacks Project, Tag 0CAW (More on Morphisms, Lemma 37.39.6). Let
Sbe a locally Noetherian scheme, letp : X ⟶ S,q : Y ⟶ Tandh : T ⟶ Sbe locally of finite type, letx ∈ Xlie overs ∈ Sandy ∈ Yovert ∈ Twithh t = s, and assume𝒪_{S, s}is a G-ring. Letσ : 𝒪_{T, t} → 𝒪^∧_{S, s}be a local𝒪_{S, s}-algebra map, writeY_σ = Y ×_{T, σ} Spec 𝒪^∧_{S, s}, lety_σbe a point ofY_σovery— the only one, since such a point lies over the closed point byStacksDraft.ArtinApproximation.snd_eq_closedPoint_of_fst_eq— and letφ : 𝒪_{X, x} → 𝒪^∧_{Y_σ, y_σ}be a local𝒪_{S, s}-algebra map.Then for every
N ≥ 1there is a commutative diagramof schemes overX ← X ×_S V ←—f— W —→ Y ×_{T, τ} V → Y ↓ ↓ ↓ S ←——————————— V ———τ——————————————→ TSwith pointsw ∈ Wandv ∈ Vsuch that 1.v ↦ s,τ v = t,f w = (x, v)andw ↦ (y, v); 2.(V, v) → (S, s)is an elementary étale neighbourhood; 3. the square relatingσtoτ^♯_vcommutes modulo𝔪_v ^ N; 4.(W, w) → (Y ×_{T, τ} V, (y, v))is an elementary étale neighbourhood; 5. the squarecommutes, where𝒪_{X, x} —φ→ 𝒪^∧_{Y_σ, y_σ} → 𝒪_{Y_σ, y_σ}/𝔪^N —θ→ 𝒪_{Y ×_{T, τ} V, (y, v)}/𝔪^N ‖ ↓ 𝒪_{X, x} → 𝒪_{X ×_S V, (x, v)} —f^♯_w→ 𝒪_{W, w} ———————→ 𝒪_{W, w}/𝔪^Nθis the canonical isomorphism ofY_σwithY ×_{T, τ} Vover𝒪_{V, v}/𝔪_v ^ N = 𝒪_{S, s}/𝔪_s ^ Nthat clauses (2) and (3) provide.The isomorphism
θis exhibited, together with the compatibilities which characterise it: it matches the two maps from𝒪_{Y, y}and the two maps from𝒪_{S, s}. Only the𝔪 ^ Ntruncations are identified; the completions𝒪^∧_{Y_σ, y_σ}and𝒪^∧_{Y ×_{T, τ} V, (y, v)}need not be isomorphic, as the cusp-versus-node example in the module docstring ofStacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteTypeBaseApproximation.leanshows. The correspondence of(y, v)withy_σon the closed fibres is recorded in addition, as in Tag 0GDX.
theorem exists_relativeMapApproximation
{X S Y T : Scheme.{u}} [IsLocallyNoetherian S] (p : X ⟶ S) (q : Y ⟶ T) (h : T ⟶ S)
[LocallyOfFiniteType p] [LocallyOfFiniteType q] [LocallyOfFiniteType h]
{x : X} {s : S} {y : Y} {t : T} (hx : p x = s) (hy : q y = t) (hts : h t = s)
(hG : IsGRing (S.presheaf.stalk s)) (N : ℕ) (hN : 1 ≤ N)
(σ : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))
(hσ : IsLocalHom σ)
(hσbase : σ.comp (h.stalkHomAt hts) =
algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)))
(yσ : (pullback q (relativeBaseChangeMorphism s σ) : Scheme.{u}))
(hyσY : pullback.fst q (relativeBaseChangeMorphism s σ) yσ = y)
(φ : X.presheaf.stalk x →+*
AdicCompletion
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
(hφ : IsLocalHom φ)
(hφbase : φ.comp (p.stalkHomAt hx) =
(algebraMap ((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ)
(AdicCompletion
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))).comp
(((pullback.snd q (relativeBaseChangeMorphism s σ)).stalkHomAt
(snd_eq_closedPoint_of_fst_eq h q hy hts σ hσbase
(relativeBaseChangeMorphism s σ) rfl yσ hyσY)).comp
((specCompletedStalkTo S s).stalkHomAt
(specCompletedStalkTo_specCompletedStalkPoint S s)))) :
∃ (V : EtaleNeighborhood S s) (τ : V.scheme ⟶ T) (hτ : τ V.point = t)
(yτ : (pullback q τ : Scheme.{u}))
(hyτY : pullback.fst q τ yτ = y) (hyτV : pullback.snd q τ yτ = V.point)
(W : EtaleNeighborhood (pullback q τ) yτ) (F : W.scheme ⟶ X) (hF : F W.point = x)
(f : W.scheme ⟶ pullback p V.toBase),
V.IsElementary ∧ W.IsElementary ∧ τ ≫ h = V.toBase ∧
f ≫ pullback.fst p V.toBase = F ∧
f ≫ pullback.snd p V.toBase = W.toBase ≫ pullback.snd q τ ∧
F ≫ p = W.toBase ≫ pullback.snd q τ ≫ V.toBase ∧
(∀ b : T.presheaf.stalk t,
V.completionMap (σ b) -
algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)) (τ.stalkHomAt hτ b) ∈
Ideal.map
(algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)))
(maximalIdeal (V.scheme.presheaf.stalk V.point) ^ N)) ∧
(∃ θ : ((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ ⧸
maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ^ N) ≃+*
((pullback q τ).presheaf.stalk yτ ⧸
maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N),
(∀ b : Y.presheaf.stalk y,
θ (Ideal.Quotient.mk (maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ^ N)
((pullback.fst q (relativeBaseChangeMorphism s σ)).stalkHomAt hyσY b)) =
Ideal.Quotient.mk (maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N)
((pullback.fst q τ).stalkHomAt hyτY b)) ∧
(∀ c : S.presheaf.stalk s,
θ (Ideal.Quotient.mk (maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ^ N)
((pullback.snd q (relativeBaseChangeMorphism s σ)).stalkHomAt
(snd_eq_closedPoint_of_fst_eq h q hy hts σ hσbase
(relativeBaseChangeMorphism s σ) rfl yσ hyσY)
((specCompletedStalkTo S s).stalkHomAt
(specCompletedStalkTo_specCompletedStalkPoint S s) c))) =
Ideal.Quotient.mk (maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N)
((pullback.snd q τ).stalkHomAt hyτV (V.stalkHom c))) ∧
∀ (α : X.presheaf.stalk x) (z : (pullback q τ).presheaf.stalk yτ),
θ (AdicCompletion.evalₐ (maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ)) N
(φ α)) =
Ideal.Quotient.mk (maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N) z →
Ideal.Quotient.mk (maximalIdeal (W.scheme.presheaf.stalk W.point) ^ N)
(W.stalkHom z) =
Ideal.Quotient.mk (maximalIdeal (W.scheme.presheaf.stalk W.point) ^ N)
(F.stalkHomAt hF α)) ∧
∃ (eBase : (specCompletedStalk S s).residueField (specCompletedStalkPoint S s) ≅
V.scheme.residueField V.point)
(eFiber : (pullback.snd q (relativeBaseChangeMorphism s σ)).fiber
(specCompletedStalkPoint S s) ≅
(pullback.snd q τ).fiber V.point),
(Spec.map eBase.inv ≫ V.scheme.fromSpecResidueField V.point ≫ V.toBase =
(specCompletedStalk S s).fromSpecResidueField (specCompletedStalkPoint S s) ≫
specCompletedStalkTo S s) ∧
(Spec.map eBase.inv ≫ V.scheme.fromSpecResidueField V.point ≫ τ =
(specCompletedStalk S s).fromSpecResidueField (specCompletedStalkPoint S s) ≫
relativeBaseChangeMorphism s σ) ∧
(eFiber.hom ≫ (pullback.snd q τ).fiberι V.point ≫ pullback.fst q τ =
(pullback.snd q (relativeBaseChangeMorphism s σ)).fiberι
(specCompletedStalkPoint S s) ≫
pullback.fst q (relativeBaseChangeMorphism s σ)) ∧
(eFiber.hom ≫ (pullback.snd q τ).fiberToSpecResidueField V.point =
(pullback.snd q (relativeBaseChangeMorphism s σ)).fiberToSpecResidueField
(specCompletedStalkPoint S s) ≫ Spec.map eBase.inv) ∧
(eFiber.hom (((pullback.snd q (relativeBaseChangeMorphism s σ)).fiberHomeo
(specCompletedStalkPoint S s)).symm
⟨yσ, snd_eq_closedPoint_of_fst_eq h q hy hts σ hσbase
(relativeBaseChangeMorphism s σ) rfl yσ hyσY⟩) =
((pullback.snd q τ).fiberHomeo V.point).symm ⟨yτ, hyτV⟩)
Tag 0CAX, a lemma
Tag 0CAX in the Stacks Project.
AlgebraicGeometry.exists_finiteType_pointed_extension_agree_mod_maximalIdeal_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/ArtinApproximation.lean, line 814.
A local map from the stalk of a finite-type Noetherian scheme to the completed local ring of its base can be made rigid modulo any positive power of the base maximal ideal after a pointed finite-type extension.
This is the source's statement, in which the comparison maps
σ'are required to be local. It isAlgebraicGeometry.exists_finiteType_pointed_extension_agree_mod_maximalIdeal_pow_of_factors, which proves the agreement clause for everyσ'factoring through the extension.
theorem exists_finiteType_pointed_extension_agree_mod_maximalIdeal_pow
{S T : Scheme.{u}} (f : T ⟶ S)
[IsNoetherian S] [IsNoetherian T]
[LocallyOfFiniteType f] [QuasiCompact f]
(s : S) (t : T) (ht : f t = s)
(sigma : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))
(hsigma : IsLocalHom sigma)
(hsigma_base :
sigma.comp ((f.stalkMap t).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) ht).symm).hom) =
algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)))
(N : ℕ) (hN : 1 ≤ N) :
∃ (T' : Scheme.{u}) (g : T' ⟶ T) (t' : T') (hgt : g t' = t)
(_ : LocallyOfFiniteType g) (_ : QuasiCompact g),
∃ tau : T'.presheaf.stalk t' →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s),
IsLocalHom tau ∧
sigma = tau.comp ((g.stalkMap t').hom.comp
(eqToHom (congrArg (fun z ↦ T.presheaf.stalk z) hgt).symm).hom) ∧
tau.comp ((g.stalkMap t').hom.comp
((eqToHom (congrArg (fun z ↦ T.presheaf.stalk z) hgt).symm).hom.comp
((f.stalkMap t).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) ht).symm).hom))) =
algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)) ∧
(∀ (sigma' : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)),
IsLocalHom sigma' →
sigma'.comp ((f.stalkMap t).hom.comp
(eqToHom (congrArg (fun z ↦ S.presheaf.stalk z) ht).symm).hom) =
algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s))
(S.presheaf.stalk s)) →
(∃ tau' : T'.presheaf.stalk t' →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s),
sigma' = tau'.comp ((g.stalkMap t').hom.comp
(eqToHom (congrArg (fun z ↦ T.presheaf.stalk z) hgt).symm).hom)) →
∀ a : T.presheaf.stalk t,
sigma a - sigma' a ∈
Ideal.map
(algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s))
(S.presheaf.stalk s)))
(maximalIdeal (S.presheaf.stalk s) ^ N))
Tag 0CAY, a lemma
Tag 0CAY in the Stacks Project.
Stacks.ConormalApproximation.exists_finiteType_pointed_extension_conormalAlgebra_iso_of_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/ConormalApproximationSubFamily.lean, line 698.
Stacks 0CAY. Let
Y → T → Sbe finite type morphisms of Noetherian schemes, lett ∈ Tlie overs ∈ Sand letσ : 𝒪_{T,t} → 𝒪^∧_{S,s}be a local𝒪_{S,s}-algebra map. Then there is a finite type morphism of pointed schemes(T', t') → (T, t)through whichσfactors by a local homomorphism, such that for every local𝒪_{S,s}-algebra mapσ' : 𝒪_{T,t} → 𝒪^∧_{S,s}factoring through𝒪_{T',t'}the two closed immersionsY_σ ← Y_t → Y_{σ'}of the fibre into the two base changes exist and have isomorphic conormal algebras.The hypotheses are the source's and nothing more:
σis assumed local because the source assumes it ("letσ : 𝒪_{T,t} → 𝒪_{S,s}^∧be a local𝒪_{S,s}-algebra map"), and it is in any case forced — a factorisation ofσthrough a local homomorphism out of the stalk of an extension makesσlocal.This is
Stacks.ConormalApproximation.exists_finiteType_pointed_extension_conormalAlgebra_iso_of_boundwith its comparison hypothesis discharged byStacks.ConormalApproximation.hasConormalBoundAlongExtension_of_isLocalHom. The two facts that discharge it are the locality of the identity-induced comparison (Stacks.ArtinRees.sameDenominator_iff_exists_isInducedByIdentitytogether withStacks.ConormalApproximation.sameDenominator_of_presentationsandStacks.ConormalApproximation.sameDenominator_of_localization), which lets the chart-local comparison be propagated from a chart to the basic opens inside it, and the compactness of the fibre, which makes finitely many charts enough — so the per-presentation Artin-Rees bound of the affine core suffices, which is exactly the source's "coverYby finitely many affines and glue by uniqueness".
theorem exists_finiteType_pointed_extension_conormalAlgebra_iso_of_isLocalHom
{S T Y : Scheme.{u}} (f : T ⟶ S) (p : Y ⟶ T)
[IsNoetherian S] [IsNoetherian T] [IsNoetherian Y]
[LocallyOfFiniteType f] [QuasiCompact f]
[LocallyOfFiniteType p] [QuasiCompact p]
(s : S) (t : T) (ht : f t = s)
(sigma : T.presheaf.stalk t →+* completedStalk S s) (hsigma : IsLocalHom sigma)
(hsigma_base : sigma.comp (pointedStalkMap f ht) =
algebraMap (S.presheaf.stalk s) (completedStalk S s)) :
∃ (T' : Scheme.{u}) (g : T' ⟶ T) (t' : T') (hgt : g t' = t)
(_ : LocallyOfFiniteType g) (_ : QuasiCompact g),
∃ tau : T'.presheaf.stalk t' →+* completedStalk S s,
IsLocalHom tau ∧
sigma = tau.comp (pointedStalkMap g hgt) ∧
∀ sigma' : T.presheaf.stalk t →+* completedStalk S s,
IsLocalHom sigma' →
sigma'.comp (pointedStalkMap f ht) =
algebraMap (S.presheaf.stalk s) (completedStalk S s) →
(∃ tau' : T'.presheaf.stalk t' →+* completedStalk S s,
sigma' = tau'.comp (pointedStalkMap g hgt)) →
HasIsoConormalFibreImmersions p t
(Spec.map (CommRingCat.ofHom sigma) ≫ T.fromSpecStalk t)
(Spec.map (CommRingCat.ofHom sigma') ≫ T.fromSpecStalk t)
Tag 0CAZ, an equation
Tag 0CAZ in the Stacks Project.
Stacks.SyzygyCoefficients.exact_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FiniteType/SyzygyCoefficients.lean, line 131.
Let
PpresentBasC[x_1, …, x_n]/(f_1, …, f_m), letσ : C → DmakeDaC-algebra and leta_{kj} ∈ D[x_1, …, x_n],k = 1, …, K, generate the module of relations among theσ(f_j). ThenD[x]^{⊕K} → D[x]^{⊕m} → D[x] → B ⊗_{C, σ} D → 0is exact.
theorem exact_resolution
{C : Type u} {B : Type v} {D : Type w}
[CommRing C] [CommRing B] [CommRing D] [Algebra C B] [Algebra C D]
{n m K : ℕ} (P : Algebra.Presentation C B (Fin n) (Fin m))
(a : Fin K → Fin m → MvPolynomial (Fin n) D)
(ha : ∀ k, ∑ j, a k j * MvPolynomial.map (algebraMap C D) (P.relation j) = 0)
(hgen : ∀ v : Fin m → MvPolynomial (Fin n) D,
(∑ j, v j * MvPolynomial.map (algebraMap C D) (P.relation j) = 0) →
∃ w : Fin K → MvPolynomial (Fin n) D, ∀ j, v j = ∑ k, w k * a k j) :
LinearMap.ker (relationMap D P) = LinearMap.range (syzygyMap a) ∧
LinearMap.range (relationMap D P) =
RingHom.ker (aeval (R := D) (S₁ := D ⊗[C] B) (P.baseChange D).val) ∧
Function.Surjective (aeval (R := D) (S₁ := D ⊗[C] B) (P.baseChange D).val)
Tag 0CB0, an equation
Tag 0CB0 in the Stacks Project.
Stacks.SyzygyCoefficients.exists_finiteType_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FiniteType/SyzygyCoefficients.lean, line 190.
Let
PpresentBasC[x_1, …, x_n]/(f_1, …, f_m), letDbe aC-algebra, and leta_{kj} ∈ D[x_1, …, x_n],k = 1, …, K, be syzygies∑_j a_{kj} f_j = 0generating all syzygies among the images of thef_j. Then there are aC-algebraC'of finite type, aC-algebra mapτ : C' → Dand polynomialst_{kj} ∈ C'[x_1, …, x_n]with∑_j t_{kj} f_j = 0, such thatτcarries thet_{kj}to thea_{kj}and the four-term complex overC'[x_1, …, x_n]built from thet_{kj}and thef_jis exact atC'[x_1, …, x_n]and atB ⊗_C C'.
theorem exists_finiteType_resolution
{C : Type u} {B : Type v} {D : Type w}
[CommRing C] [CommRing B] [CommRing D] [Algebra C B] [Algebra C D]
{n m K : ℕ} (P : Algebra.Presentation C B (Fin n) (Fin m))
(a : Fin K → Fin m → MvPolynomial (Fin n) D)
(ha : ∀ k, ∑ j, a k j * MvPolynomial.map (algebraMap C D) (P.relation j) = 0)
(_hgen : ∀ v : Fin m → MvPolynomial (Fin n) D,
(∑ j, v j * MvPolynomial.map (algebraMap C D) (P.relation j) = 0) →
∃ w : Fin K → MvPolynomial (Fin n) D, ∀ j, v j = ∑ k, w k * a k j) :
∃ (C' : Type u) (_ : CommRing C') (_ : Algebra C C') (_ : Algebra.FiniteType C C')
(τ : C' →ₐ[C] D) (t : Fin K → Fin m → MvPolynomial (Fin n) C'),
(∀ k, ∑ j, t k j * MvPolynomial.map (algebraMap C C') (P.relation j) = 0) ∧
(∀ k j, MvPolynomial.map (τ : C' →+* D) (t k j) = a k j) ∧
(∀ j, MvPolynomial.map (τ : C' →+* D)
(MvPolynomial.map (algebraMap C C') (P.relation j)) =
MvPolynomial.map (algebraMap C D) (P.relation j)) ∧
Ideal.span (Set.range fun j : Fin m =>
MvPolynomial.map (algebraMap C C') (P.relation j)) =
RingHom.ker (aeval (R := C') (S₁ := C' ⊗[C] B) (P.baseChange C').val) ∧
Function.Surjective (aeval (R := C') (S₁ := C' ⊗[C] B) (P.baseChange C').val)
Tag 0CB1, a lemma
Tag 0CB1 in the Stacks Project.
StacksDraft.ArtinApproximation.exists_etale_relativeIsomorphismApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/RelativeMapApproximation.lean, line 4580. The attribute's comment: “the source's own hypotheses, with nothing beyond them: h : T ⟶ S locally of finite type, σ : 𝒪_{T, t} → 𝒪^∧_{S, s} a local 𝒪_{S, s}-algebra map for h, the base change Y_σ = Y ×_{T, σ} Spec 𝒪^∧_{S, s}, a point y_σ of Y_σ over y and the closed point, and the isomorphism φ : 𝒪^∧_{X, x} ≅ 𝒪^∧_{Y_σ, y_σ} of 𝒪_{S, s}-algebras which is what 0CB1 adds to Tag 0CAW. Theorem 07QZ is NOT carried: the LocalApproximationProperty hypothesis of Tag 0CAU behind Tag 0CAV and behind the first stage of Tag 0CAW is discharged with StacksDraft.ArtinApproximation.localApproximationProperty, which rests on the unconditional Tag 07QZ Stacks.Smoothing.exists_localEtaleSolution_of_isGRing and hence on the unconditional Popescu Theorem 07GC Stacks.Smoothing.indSmooth_of_isRegularRingMap. The conclusion is the source's whole diagram: clauses (1), (2), (3), (4) and (5) of Tag 0CAW together with the étaleness of f : W ⟶ X ×_S V, which is the content of 0CB1. Clause (5) is the ring isomorphism θ : 𝒪_{Y_σ, y_σ}/𝔪^N ≅ 𝒪_{Y ×_{T, τ} V, (y, v)}/𝔪^N which the conclusion exhibits, compatible with the two maps from 𝒪_{Y, y} and with the two maps from 𝒪_{S, s} — the compatibilities which characterise the source's canonical identification over 𝒪_{V, v}/𝔪_v ^ N = 𝒪_{S, s}/𝔪_s ^ N — together with the source's commuting square: φ read on 𝒪_{X, x} through θ and then through W ⟶ Y ×_{T, τ} V is F^♯_w modulo 𝔪_w ^ N. Only the 𝔪 ^ N-truncations are identified; the completions 𝒪^∧_{Y_σ, y_σ} and 𝒪^∧_{Y ×_{T, τ} V, y_τ} need not be isomorphic, as the cusp-versus-node example in the module docstring of StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteTypeBaseApproximation.lean shows. The identification of the closed fibres (Y_σ)_s ≅ (Y ×_T V)_v of Tag 0GDX is recorded as well. The route to étaleness is Tag 0CAV over Spec 𝒪^∧_{S, s} followed by the descent of Tag 0GDX, which delivers W ⟶ X étale directly, in place of the source's comparison of associated graded rings through Tag 0CAY; clause (5) comes from the congruence modulo 𝔪 ^ N that Tag 0CAV supplies upstairs, transported to W by the order-N comparison of the two base changes of the stage object along Spec 𝒪^∧_{S, s} ⟶ D and along V ⟶ D”.
Stacks Project, Tag 0CB1 (More on Morphisms, Lemma 37.39.7). With the notation and assumptions of Tag 0CAW — a locally Noetherian
S, morphismsp : X ⟶ S,q : Y ⟶ Tandh : T ⟶ Slocally of finite type, pointsx ↦ sandy ↦ t ↦ s, a G-ring𝒪_{S, s}, a local𝒪_{S, s}-algebra mapσ : 𝒪_{T, t} → 𝒪^∧_{S, s}, the base changeY_σ = Y ×_{T, σ} Spec 𝒪^∧_{S, s}and a pointy_σof it overyand over the closed point — assume moreover thatφinduces an isomorphism𝒪^∧_{X, x} ≅ 𝒪^∧_{Y_σ, y_σ}of𝒪_{S, s}-algebras on completions. Then for everyN ≥ 1the diagram of Tag 0CAW can be chosen withfétale: there are an elementary étale neighbourhood(V, v)of(S, s), a morphismτ : V ⟶ ToverSwithτ v = twhose square withσcommutes modulo𝔪_v ^ N, a pointy_τofY ×_{T, τ} Voveryandvwhich corresponds toy_σon the closed fibres, an elementary étale neighbourhood(W, w)of(Y ×_{T, τ} V, y_τ), a morphismF : W ⟶ XoverScarryingwtox, and an étalef : W ⟶ X ×_S Vwithf ≫ pr₁ = Fandf ≫ pr₂ = W ⟶ Y ×_{T, τ} V ⟶ V, so thatf w = (x, v).Clause (5) of Tag 0CAW is the ring isomorphism
θ : 𝒪_{Y_σ, y_σ}/𝔪_{y_σ} ^ N ≅ 𝒪_{Y ×_{T, τ} V, (y, v)}/𝔪_{(y, v)} ^ Nwhich the conclusion exhibits, compatible with the two maps from𝒪_{Y, y}and with the two maps from𝒪_{S, s}— the compatibilities which makeθthe source's canonical identification of the two base changes over𝒪_{V, v}/𝔪_v ^ N = 𝒪_{S, s}/𝔪_s ^ N— together with the commutativity of the source's square:φread on𝒪_{X, x}throughθand then through the elementary étale neighbourhoodW ⟶ Y ×_{T, τ} VisF^♯_wmodulo𝔪_w ^ N. No isomorphism of the completions𝒪^∧_{Y_σ, y_σ}and𝒪^∧_{Y ×_{T, τ} V, y_τ}is asserted: only the𝔪 ^ N-truncations are identified, and for a pair(V, τ)satisfying clauses (2) and (3) alone the completions can be a cusp and a node.The correspondence of
y_τwithy_σis recorded in addition, as in Tag 0GDX: an isomorphismeBaseof the residue fields of the two bases compatible with their maps toSand toT, and an isomorphismeFiberof the scheme-theoretic closed fibres compatible with the two maps toYand witheBase, carrying the point abovey_σto the point abovey_τ.
theorem exists_etale_relativeIsomorphismApproximation
{X S Y T : Scheme.{u}} [IsLocallyNoetherian S] (p : X ⟶ S) (q : Y ⟶ T) (h : T ⟶ S)
[LocallyOfFiniteType p] [LocallyOfFiniteType q] [LocallyOfFiniteType h]
{x : X} {s : S} {y : Y} {t : T} (hx : p x = s) (hy : q y = t) (hts : h t = s)
(hG : IsGRing (S.presheaf.stalk s)) (N : ℕ) (hN : 1 ≤ N)
(σ : T.presheaf.stalk t →+*
AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s))
(hσ : IsLocalHom σ)
(hσbase : σ.comp (h.stalkHomAt hts) =
algebraMap (S.presheaf.stalk s)
(AdicCompletion (maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)))
(yσ : (pullback q (relativeBaseChangeMorphism s σ) : Scheme.{u}))
(hyσY : pullback.fst q (relativeBaseChangeMorphism s σ) yσ = y)
(hyσZ : pullback.snd q (relativeBaseChangeMorphism s σ) yσ =
specCompletedStalkPoint S s)
(φ : AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x) ≃+*
AdicCompletion
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
(hφ : φ.toRingHom.comp ((algebraMap (X.presheaf.stalk x)
(AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))).comp
(p.stalkHomAt hx)) =
(algebraMap ((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ)
(AdicCompletion
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ))).comp
(((pullback.snd q (relativeBaseChangeMorphism s σ)).stalkHomAt hyσZ).comp
((specCompletedStalkTo S s).stalkHomAt
(specCompletedStalkTo_specCompletedStalkPoint S s)))) :
∃ (V : EtaleNeighborhood S s) (τ : V.scheme ⟶ T) (hτ : τ V.point = t)
(yτ : (pullback q τ : Scheme.{u}))
(hyτY : pullback.fst q τ yτ = y) (hyτV : pullback.snd q τ yτ = V.point)
(W : EtaleNeighborhood (pullback q τ) yτ) (F : W.scheme ⟶ X) (hF : F W.point = x)
(f : W.scheme ⟶ pullback p V.toBase),
V.IsElementary ∧ W.IsElementary ∧ τ ≫ h = V.toBase ∧ Etale f ∧
f ≫ pullback.fst p V.toBase = F ∧
f ≫ pullback.snd p V.toBase = W.toBase ≫ pullback.snd q τ ∧
F ≫ p = W.toBase ≫ pullback.snd q τ ≫ V.toBase ∧
(∀ b : T.presheaf.stalk t,
V.completionMap (σ b) -
algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)) (τ.stalkHomAt hτ b) ∈
Ideal.map
(algebraMap (V.scheme.presheaf.stalk V.point)
(AdicCompletion (maximalIdeal (V.scheme.presheaf.stalk V.point))
(V.scheme.presheaf.stalk V.point)))
(maximalIdeal (V.scheme.presheaf.stalk V.point) ^ N)) ∧
(∃ θ : ((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ⧸
(maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ^ N) ≃+*
((pullback q τ).presheaf.stalk yτ) ⧸
(maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N),
(∀ b : Y.presheaf.stalk y,
θ (Ideal.Quotient.mk (maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ^ N)
((pullback.fst q (relativeBaseChangeMorphism s σ)).stalkHomAt hyσY b)) =
Ideal.Quotient.mk (maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N)
((pullback.fst q τ).stalkHomAt hyτY b)) ∧
(∀ c : S.presheaf.stalk s,
θ (Ideal.Quotient.mk (maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ) ^ N)
((pullback.snd q (relativeBaseChangeMorphism s σ)).stalkHomAt hyσZ
((specCompletedStalkTo S s).stalkHomAt
(specCompletedStalkTo_specCompletedStalkPoint S s) c))) =
Ideal.Quotient.mk (maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N)
((pullback.snd q τ).stalkHomAt hyτV (V.stalkHom c))) ∧
∀ (α : X.presheaf.stalk x) (z : (pullback q τ).presheaf.stalk yτ),
θ (AdicCompletion.evalₐ (maximalIdeal
((pullback q (relativeBaseChangeMorphism s σ)).presheaf.stalk yσ)) N
(φ (algebraMap (X.presheaf.stalk x)
(AdicCompletion (maximalIdeal (X.presheaf.stalk x))
(X.presheaf.stalk x)) α))) =
Ideal.Quotient.mk (maximalIdeal ((pullback q τ).presheaf.stalk yτ) ^ N) z →
Ideal.Quotient.mk (maximalIdeal (W.scheme.presheaf.stalk W.point) ^ N)
(W.stalkHom z) =
Ideal.Quotient.mk (maximalIdeal (W.scheme.presheaf.stalk W.point) ^ N)
(F.stalkHomAt hF α)) ∧
∃ (eBase : (specCompletedStalk S s).residueField (specCompletedStalkPoint S s) ≅
V.scheme.residueField V.point)
(eFiber : (pullback.snd q (relativeBaseChangeMorphism s σ)).fiber
(specCompletedStalkPoint S s) ≅
(pullback.snd q τ).fiber V.point),
(Spec.map eBase.inv ≫ V.scheme.fromSpecResidueField V.point ≫ V.toBase =
(specCompletedStalk S s).fromSpecResidueField (specCompletedStalkPoint S s) ≫
specCompletedStalkTo S s) ∧
(Spec.map eBase.inv ≫ V.scheme.fromSpecResidueField V.point ≫ τ =
(specCompletedStalk S s).fromSpecResidueField (specCompletedStalkPoint S s) ≫
relativeBaseChangeMorphism s σ) ∧
(eFiber.hom ≫ (pullback.snd q τ).fiberι V.point ≫ pullback.fst q τ =
(pullback.snd q (relativeBaseChangeMorphism s σ)).fiberι
(specCompletedStalkPoint S s) ≫
pullback.fst q (relativeBaseChangeMorphism s σ)) ∧
(eFiber.hom ≫ (pullback.snd q τ).fiberToSpecResidueField V.point =
(pullback.snd q (relativeBaseChangeMorphism s σ)).fiberToSpecResidueField
(specCompletedStalkPoint S s) ≫ Spec.map eBase.inv) ∧
(eFiber.hom (((pullback.snd q (relativeBaseChangeMorphism s σ)).fiberHomeo
(specCompletedStalkPoint S s)).symm ⟨yσ, hyσZ⟩) =
((pullback.snd q τ).fiberHomeo V.point).symm ⟨yτ, hyτV⟩)
Sources
Section37.40 Finite free locally dominates étale#
Section 37.40 of the Stacks Project, Tag 04HE. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02LG, a lemma
Tag 02LG in the Stacks Project.
Stacks.Topologies.Etale.exists_isFiniteLocallyFree_surjective_locally_lift_etaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/FiniteFreeDominationNeighborhood.lean, line 238.
Stacks Project, Tag 02LG. After restricting the base to an affine open neighbourhood of the point, an étale neighbourhood is locally dominated, at every point above the distinguished point, by a surjective finite locally free morphism.
theorem exists_isFiniteLocallyFree_surjective_locally_lift_etaleNeighborhood
{S : Scheme.{u}} {s : S} (U : EtaleNeighborhood S s) :
∃ (V : S.affineOpens) (hs : s ∈ V.1) (T : Scheme.{u}) (π : T ⟶ V.1)
(_ : Surjective π) (_ : Stacks.Morphisms.IsFiniteLocallyFree π),
∀ (t : T) (_ : π t = ⟨s, hs⟩),
∃ (W : T.Opens) (ht : t ∈ W) (h : (W : Scheme.{u}) ⟶ U.scheme),
W.ι ≫ π ≫ V.1.ι = h ≫ U.toBase ∧ h ⟨t, ht⟩ = U.point
Tag 02LH, a lemma
Tag 02LH in the Stacks Project.
Stacks.Topologies.Etale.exists_isFiniteLocallyFree_surjective_finite_openCover_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/FiniteFreeDominationAffine.lean, line 103.
Stacks Project, Tag 02LH. A surjective étale morphism of affine schemes is dominated by a surjective finite locally free morphism whose source has a finite open covering lifting to the given étale cover.
theorem exists_isFiniteLocallyFree_surjective_finite_openCover_lift
{U S : Scheme.{u}} [IsAffine U] [IsAffine S] (f : U ⟶ S) [Etale f] [Surjective f] :
∃ (T : Scheme.{u}) (p : T ⟶ S),
Stacks.Morphisms.IsFiniteLocallyFree p ∧ Surjective p ∧
∃ 𝒯 : T.OpenCover.{u}, Finite 𝒯.I₀ ∧
∃ g : ∀ i, 𝒯.X i ⟶ U, ∀ i, 𝒯.f i ≫ p = g i ≫ f
Tag 02LI, a remark
Tag 02LI in the Stacks Project.
Stacks.Topologies.Etale.exists_zariski_finiteLocallyFree_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/FiniteFreeDomination.lean, line 168.
An étale covering is refined, after a Zariski covering of the base, by Zariski coverings of schemes which are finite locally free and surjective over the corresponding members of the base covering.
theorem exists_zariski_finiteLocallyFree_refinement {S : Scheme.{u}}
(E : PreZeroHypercover.{w} S) (hE : E.presieve₀ ∈ Scheme.etalePrecoverage S) :
∃ (V : S.OpenCover.{u}) (W : V.I₀ → Scheme.{u}) (p : ∀ j, W j ⟶ V.X j),
(∀ j, Stacks.Morphisms.IsFiniteLocallyFree (p j)) ∧
(∀ j, Surjective (p j)) ∧
∃ U : ∀ j, (W j).OpenCover.{u},
Nonempty
((V.toPreZeroHypercover.bind fun j ↦
(U j).toPreZeroHypercover.pushforward (p j)).Hom E)
Sources
Section37.41 Étale localization of quasi-finite morphisms#
Section 37.41 of the Stacks Project, Tag 04HF. 7 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02LJ, an equation
Tag 02LJ in the Stacks Project.
Declarations registered for the tag:
CategoryTheory.IsPullback.of_hasPullbackregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch37.lean, line 69 (StacksFrontier): “the cartesian square X_U = U ×_S X of the basic diagram”.
Tag 02LK, a lemma
Tag 02LK in the Stacks Project.
Stacks.Flatness.exists_etaleNeighborhood_finiteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteNeighborhood.lean, line 392. The attribute's comment: “existence”. References: EGA IV (18.12.1).
A locally finite type morphism becomes finite near a point isolated in its fibre after an elementary étale base change.
theorem exists_etaleNeighborhood_finiteAt {X S : Scheme.{u}} (f : X ⟶ S)
[LocallyOfFiniteType f] (x : X) (hx : IsIsolatedPoint (f.asFiber x)) :
Nonempty (FiniteNeighborhoodAt f x)
Stacks.Flatness.isFiniteNeighborhoodAt_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteNeighborhood.lean, line 578. The attribute's comment: “elementary étale refinement”.
The pullback of a finite neighbourhood along any further elementary étale neighbourhood is again a finite neighbourhood: finite over the new base, with a unique distinguished-fibre point having the same residue field as the original point.
theorem isFiniteNeighborhoodAt_baseChange {X S : Scheme.{u}} (f : X ⟶ S) (x : X)
(U : EtaleNeighborhood S (f x))
(V : (pullback f U.toBase).Opens) (hV : IsFiniteNeighborhoodAt f x U V)
(U' : EtaleNeighborhood U.scheme U.point) (hU' : U'.IsElementary) :
IsFiniteNeighborhoodAt f x
{ scheme := U'.scheme
point := U'.point
toBase := U'.toBase ≫ U.toBase
map_point := by simp [U'.map_point, U.map_point] }
((pullback.map f (U'.toBase ≫ U.toBase) f U.toBase
(𝟙 X) U'.toBase (𝟙 S) (by simp) (by simp)) ⁻¹ᵁ V)
Tag 02LL, a lemma
Tag 02LL in the Stacks Project.
Stacks.Flatness.exists_etaleNeighborhood_finite_opens_of_isolated_fiber_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/IsolatedPointsDecomposition.lean, line 147.
Stacks Project, Tag 02LL. Several isolated points of one fibre can simultaneously be made finite over a single elementary étale neighbourhood of the base point.
theorem exists_etaleNeighborhood_finite_opens_of_isolated_fiber_points
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(s : S) (n : ℕ) (x : Fin n → X) (hx : ∀ i, f (x i) = s)
(hx_isolated : ∀ i, IsIsolatedPoint (f.asFiber (x i))) :
∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
(V : Fin n → (pullback f U.toBase).Opens)
(v : ∀ i, V i),
(∀ i, IsFinite ((V i).ι ≫ pullback.snd f U.toBase)) ∧
(∀ i, {y : V i | ((V i).ι ≫ pullback.snd f U.toBase) y = U.point} = {v i}) ∧
(∀ i, ((V i).ι ≫ pullback.fst f U.toBase) (v i) = x i) ∧
(∀ i, IsIso (((V i).ι ≫ pullback.fst f U.toBase).residueFieldMap (v i)))
AlgebraicGeometry.exists_elementaryEtaleNeighborhood_finite_opens_of_isolated_fiber_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleLocalizationQuasiFinite/FiniteNeighborhood.lean, line 297.
Stacks Project, Tag 02LL. Several isolated points in one fibre can simultaneously be made finite over an elementary étale neighborhood.
public theorem exists_elementaryEtaleNeighborhood_finite_opens_of_isolated_fiber_points
(f : X ⟶ S) [LocallyOfFiniteType f] (s : S) (n : ℕ) (x : Fin n → X) (hx : ∀ i, f (x i) = s)
(hx_isolated : ∀ i, IsIsolatedPoint (f.asFiber (x i))) :
∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
(V : Fin n → (pullback f U.toBase).Opens)
(v : ∀ i, V i),
(∀ i, IsFinite ((V i).ι ≫ pullback.snd f U.toBase)) ∧
(∀ i, {y : V i | ((V i).ι ≫ pullback.snd f U.toBase) y = U.point} = {v i}) ∧
(∀ i, ((V i).ι ≫ pullback.fst f U.toBase) (v i) = x i) ∧
(∀ i, IsIso (((V i).ι ≫ pullback.fst f U.toBase).residueFieldMap (v i)))
Tag 02LM, a lemma
Tag 02LM in the Stacks Project.
AlgebraicGeometry.exists_etale_finite_opens_of_isolated_fiber_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/QuasiFiniteEtaleLocalisation.lean, line 318. References: EGA IV (18.12.1), “more general”.
Stacks Project, Tag 02LM. Finitely many distinct isolated points of a fibre of a morphism locally of finite type have, after a single étale base change, finite open neighbourhoods meeting the distinguished fibre in exactly one point, with finite purely inseparable residue extension, and these points exhaust the base change of the chosen points.
theorem exists_etale_finite_opens_of_isolated_fiber_points
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
(n : ℕ) (s : S) (x : Fin n → X) (hx : ∀ i, f (x i) = s)
(hx_injective : Function.Injective x)
(hx_isolated : ∀ i, IsIsolatedPoint (f.asFiber (x i))) :
∃ (U : EtaleNeighborhood S s)
(m : Fin n → ℕ)
(V : ∀ i, Fin (m i) → (pullback f U.toBase).Opens)
(v : ∀ i j, V i j),
(∀ i j,
let g := (V i j).ι ≫ pullback.snd f U.toBase
IsFinite g ∧
g ⁻¹' {U.point} = {v i j} ∧
((V i j).ι ≫ pullback.fst f U.toBase) (v i j) = x i ∧
∃ hvu : g (v i j) = U.point,
RingHom.Finite (((U.scheme.residueFieldCongr hvu).inv ≫
g.residueFieldMap (v i j)).hom) ∧
((U.scheme.residueFieldCongr hvu).inv ≫
g.residueFieldMap (v i j)).hom.IsPurelyInseparable) ∧
Function.Injective (fun p : Σ i, Fin (m i) ↦ (V p.1 p.2).ι (v p.1 p.2)) ∧
(∀ i (y : ↥(pullback f U.toBase)),
(pullback.snd f U.toBase) y = U.point →
(pullback.fst f U.toBase) y = x i →
∃ j, (V i j).ι (v i j) = y)
Tag 02LN, a lemma
Tag 02LN in the Stacks Project.
Stacks.Flatness.exists_etaleNeighborhood_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/IsolatedPointsDecomposition.lean, line 329. References: EGA IV (18.12.1), “separated case”; EGA IV (18.12.3), “more general”.
Stacks Project, Tag 02LN. Finitely many distinct isolated points of a fibre of a separated morphism locally of finite type split into separate finite open-and-closed pieces after an elementary étale base change.
theorem exists_etaleNeighborhood_decomposition
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f]
(s : S) (n : ℕ) (x : Fin n → X) (hx : ∀ i, f (x i) = s)
(hx_injective : Function.Injective x)
(hx_isolated : ∀ i, IsOpen {f.asFiber (x i)}) :
∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
(P : Option (Fin n) → Scheme.{u})
(j : ∀ a, P a ⟶ pullback f U.toBase)
(_ : ∀ a, IsOpenImmersion (j a))
(_ : ∀ a, IsClosedImmersion (j a))
(_ : IsIso (Sigma.desc j))
(v : ∀ i, P (some i))
(_ : ∀ i, IsFinite (j (some i) ≫ pullback.snd f U.toBase)),
(∀ i, (j (some i) ≫ pullback.fst f U.toBase) (v i) = x i) ∧
(∀ i, {y : P (some i) |
(j (some i) ≫ pullback.snd f U.toBase) y = U.point} = {v i}) ∧
(∀ i, IsIso ((j (some i) ≫ pullback.fst f U.toBase).residueFieldMap (v i))) ∧
(∀ y : P none,
(j none ≫ pullback.snd f U.toBase) y = U.point →
∀ i, (j none ≫ pullback.fst f U.toBase) y ≠ x i)
AlgebraicGeometry.exists_elementaryEtaleNeighborhood_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleLocalizationQuasiFinite/Decomposition.lean, line 239. References: EGA IV (18.12.1), “separated case”; EGA IV (18.12.3), “more general”.
Stacks Project, Tag 02LN. Finitely many distinct isolated points of a fibre of a separated morphism locally of finite type split into separate finite open-and-closed pieces after an elementary étale base change.
public theorem exists_elementaryEtaleNeighborhood_decomposition
(f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f]
(s : S) (n : ℕ) (x : Fin n → X) (hx : ∀ i, f (x i) = s)
(hx_injective : Function.Injective x)
(hx_isolated : ∀ i, IsOpen {f.asFiber (x i)}) :
∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
(P : Option (Fin n) → Scheme.{u})
(j : ∀ a, P a ⟶ pullback f U.toBase)
(_ : ∀ a, IsOpenImmersion (j a))
(_ : ∀ a, IsClosedImmersion (j a))
(_ : IsIso (Sigma.desc j))
(v : ∀ i, P (some i))
(_ : ∀ i, IsFinite (j (some i) ≫ pullback.snd f U.toBase)),
(∀ i, (j (some i) ≫ pullback.fst f U.toBase) (v i) = x i) ∧
(∀ i, {y : P (some i) |
(j (some i) ≫ pullback.snd f U.toBase) y = U.point} = {v i}) ∧
(∀ i, IsIso ((j (some i) ≫ pullback.fst f U.toBase).residueFieldMap (v i))) ∧
(∀ y : P none,
(j none ≫ pullback.snd f U.toBase) y = U.point →
∀ i, (j none ≫ pullback.fst f U.toBase) y ≠ x i)
Tag 02LO, a lemma
Tag 02LO in the Stacks Project.
AlgebraicGeometry.exists_etaleNeighborhood_purelyInseparable_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleLocalizationQuasiFinite/PurelyInseparableDecomposition.lean, line 65. References: EGA IV (18.12.1), “separated case”; EGA IV (18.12.3), “partial”.
Stacks Project, Tag 02LO. Finitely many pairwise distinct isolated points of a fibre of a separated morphism locally of finite type split into finite open-and-closed pieces after an étale base change. Each distinguished piece has singleton fibre and purely inseparable residue-field extension, and the residual piece contains none of the specified points.
public theorem exists_etaleNeighborhood_purelyInseparable_decomposition
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f]
(n : ℕ) (s : S) (x : Fin n → f.fiber s) (hx : Function.Injective x)
(hxi : ∀ i, IsIsolatedPoint (x i)) :
∃ (U : EtaleNeighborhood S s)
(m : Fin n → ℕ)
(D : Option (Σ i, Fin (m i)) → (pullback f U.toBase).Opens)
(v : ∀ i j, D (some ⟨i, j⟩)),
Set.PairwiseDisjoint Set.univ (fun k ↦ (D k).1) ∧
(⋃ k, (D k).1) = Set.univ ∧
(∀ k, IsClopen (D k).1) ∧
(∀ i j,
let V := D (some ⟨i, j⟩)
let g := V.ι ≫ pullback.snd f U.toBase
IsFinite g ∧
g ⁻¹' {U.point} = {v i j} ∧
(V.ι ≫ pullback.fst f U.toBase) (v i j) = f.fiberι s (x i) ∧
∃ hvu : g (v i j) = U.point,
((U.scheme.residueFieldCongr hvu).inv ≫
g.residueFieldMap (v i j)).hom.IsPurelyInseparable) ∧
(∀ w : D none,
((D none).ι ≫ pullback.snd f U.toBase) w = U.point →
∀ i, ((D none).ι ≫ pullback.fst f U.toBase) w ≠ f.fiberι s (x i))
Tag 02LP, a lemma
Tag 02LP in the Stacks Project.
AlgebraicGeometry.exists_elementaryEtaleNeighborhood_isCompl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/EtaleLocalizationQuasiFinite/Decomposition.lean, line 461. References: EGA IV (18.12.1), “separated case”; EGA IV (18.12.3).
Stacks Project, Tag 02LP. After an elementary étale base change, the isolated part of a fibre of a separated morphism locally of finite type splits off as a finite open-and-closed subscheme. The complementary fibre has no isolated points and is empty when the original set-theoretic fibre is finite.
public theorem exists_elementaryEtaleNeighborhood_isCompl
(f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f] (s : S)
(hfinite : {x : f.fiber s | IsIsolatedPoint x}.Finite) :
∃ (U : EtaleNeighborhood S s),
U.IsElementary ∧
∃ (W V : (pullback f U.toBase).Opens),
IsCompl W V ∧
IsFinite (V.ι ≫ pullback.snd f U.toBase) ∧
(∀ x : (W.ι ≫ pullback.snd f U.toBase).fiber U.point,
¬ IsIsolatedPoint x) ∧
((f ⁻¹' {s}).Finite →
IsEmpty ((W.ι ≫ pullback.snd f U.toBase).fiber U.point))
AlgebraicGeometry.exists_elementaryEtale_isCompl_not_quasiFiniteAt_of_finite_isolatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/SplitFiniteFibre.lean, line 251. The attribute's comment: “the main assertion: V ⟶ U is finite and W_u has no isolated point”. References: EGA IV (18.12.1), “separated case”; EGA IV (18.12.3).
Stacks Project, Tag 02LP, the main assertion. Let
f : X ⟶ Sbe separated and locally of finite type and lets : Sbe such that the fibreX_shas only finitely many isolated points, i.e. only finitely many points ofXoversat whichfis quasi-finite. Then there is an elementary étale neighbourhood(U, u)ofs— an étaleg : U ⟶ Swithg u = sinducing an isomorphism of residue fields — and a decomposition ofU ×_S Xinto two complementary open-and-closed piecesVandWsuch thatV ⟶ Uis finite and the fibreW_ucontains no isolated point, i.e. the second projection is quasi-finite at no point ofWoveru.
theorem exists_elementaryEtale_isCompl_not_quasiFiniteAt_of_finite_isolatedPoints
{X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f] {s : S}
(hfin : {x : X | f.base x = s ∧ f.QuasiFiniteAt x}.Finite) :
∃ (U : Scheme.{u}) (g : U ⟶ S) (u : U), Etale g ∧ g.base u = s ∧
IsIso (g.residueFieldMap u) ∧
∃ V W : (pullback f g).Opens, IsCompl V W ∧
IsFinite (V.ι ≫ pullback.snd f g) ∧
∀ w : W, (pullback.snd f g).base (W.ι.base w) = u →
¬ (pullback.snd f g).QuasiFiniteAt (W.ι.base w)
AlgebraicGeometry.exists_elementaryEtale_isCompl_isEmpty_fiber_of_finite_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/SplitFiniteFibre.lean, line 296. The attribute's comment: “the final assertion: W_u = ∅ when the fibre over s is finite”. References: EGA IV (18.12.1), “separated, finite fibre”; EGA IV (18.12.3).
Stacks Project, Tag 02LP, the final assertion. Let
f : X ⟶ Sbe separated and locally of finite type with finite fibre overs : S. Then there is an elementary étale neighbourhood(U, u)ofsand a decomposition ofU ×_S Xinto two complementary open-and-closed piecesVandWsuch thatV ⟶ Uis finite andWhas no point overuat all.
theorem exists_elementaryEtale_isCompl_isEmpty_fiber_of_finite_fiber {X S : Scheme.{u}}
(f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f] {s : S}
(hfin : (f.base ⁻¹' {s}).Finite) :
∃ (U : Scheme.{u}) (g : U ⟶ S) (u : U), Etale g ∧ g.base u = s ∧
IsIso (g.residueFieldMap u) ∧
∃ V W : (pullback f g).Opens, IsCompl V W ∧
IsFinite (V.ι ≫ pullback.snd f g) ∧
∀ w : W, (pullback.snd f g).base (W.ι.base w) ≠ u
Sources
Section37.42 Étale localization of integral morphisms#
Section 37.42 of the Stacks Project, Tag 0BUH. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BSR, a lemma
Tag 0BSR in the Stacks Project.
Algebra.exists_etale_completeOrthogonalIdempotents_integral_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/IntegralSplitting.lean, line 1285.
Splitting an integral algebra after an étale extension. If an integral
R-algebraShas finitely many primes overp, and the maximal separable subextension of every corresponding residue-field extension is finite, then after an étale base change the algebra splits into integral factors having one prime over the chosen prime and purely inseparable residue-field extensions.
public theorem exists_etale_completeOrthogonalIdempotents_integral_isPurelyInseparable
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
[Algebra.IsIntegral R S] (p : Ideal R) [p.IsPrime]
(hfinite : Set.Finite {q : Ideal S | q.IsPrime ∧ q.LiesOver p})
(hseparable : ∀ (q : Ideal S) (hq : q.IsPrime) (hqover : q.LiesOver p),
letI := hq
letI := hqover
letI := Localization.AtPrime.algebraOfLiesOver p q
Module.Finite p.ResidueField
(separableClosure p.ResidueField q.ResidueField)) :
∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
(p' : Ideal R') (_ : p'.IsPrime) (_ : p'.LiesOver p) (n : ℕ)
(e : Fin n → R' ⊗[R] S) (_ : CompleteOrthogonalIdempotents e)
(r : (i : Fin n) → Ideal (Localization.Away (e i)))
(_ : ∀ i, (r i).IsPrime) (_ : ∀ i, (r i).LiesOver p'),
(∀ i : Fin n, Algebra.IsIntegral R' (Localization.Away (e i))) ∧
(∀ (i : Fin n) (q : Ideal (Localization.Away (e i))),
q.IsPrime → q.LiesOver p' → q = r i) ∧
∀ i : Fin n,
letI := Localization.AtPrime.algebraOfLiesOver p' (r i)
IsPurelyInseparable p'.ResidueField (r i).ResidueField
Sources
Section37.43 Zariski's Main Theorem#
Section 37.43 of the Stacks Project, Tag 02LQ. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02LR, a lemma
Tag 02LR in the Stacks Project.
AlgebraicGeometry.isOpenImmersion_toNormalization_and_isIntegralHom_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineQuasiFinite.lean, line 113. The attribute's comment: “the factorization”. References: EGA IV (8.12.11), “sufficiency”.
Stacks Project, Tag 02LR, the factorization. Let
f : X ⟶ Sbe a separated quasi-finite morphism of schemes. Then the morphism fromXto the normalization ofSinXis a quasi-compact open immersion, and the normalization is integral overS.Both clauses are Mathlib instances; the open immersion is Mathlib's form of Stacks 03GW.
theorem isOpenImmersion_toNormalization_and_isIntegralHom_fromNormalization [IsSeparated f]
[LocallyQuasiFinite f] [LocallyOfFiniteType f] [QuasiCompact f] :
IsOpenImmersion f.toNormalization ∧ QuasiCompact f.toNormalization ∧
IsIntegralHom f.fromNormalization
AlgebraicGeometry.isQuasiAffineHom_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineQuasiFinite.lean, line 132. The attribute's comment: “quasi-affineness”. References: EGA IV (18.12.12); EGA II (6.2.7), “more general”; EGA III (4.4.12), “(i) quasi-affine”; EGA IV (8.11.2), “more general”; SGA 1 VIII (6.2), “more general”.
Stacks Project, Tag 02LR, quasi-affineness. A separated quasi-finite morphism of schemes is quasi-affine.
It factors as the morphism to the normalization of the target in the source, which is a quasi-compact open immersion and hence quasi-affine, followed by the normalization, which is integral and hence affine and hence quasi-affine; quasi-affine morphisms are stable under composition by Stacks 01SN.
theorem isQuasiAffineHom_of_locallyQuasiFinite [IsSeparated f] [LocallyQuasiFinite f]
[LocallyOfFiniteType f] [QuasiCompact f] : IsQuasiAffineHom f
AlgebraicGeometry.isSeparated_inf_quasiFinite_le_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineQuasiFinite.lean, line 153. The attribute's comment: “containment of properties”. References: EGA IV (18.12.12); EGA II (6.2.7); EGA III (4.4.12), “(i) quasi-affine”; EGA IV (8.11.2), “more general”; SGA 1 VIII (6.2), “more general”; SGA 3 X (5.4), “more general”.
Stacks Project, Tag 02LR as a containment of morphism properties: the separated quasi-finite morphisms of schemes — separated, locally quasi-finite, locally of finite type and quasi-compact — are quasi-affine.
This is the shape in which
AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isSeparated_inf_quasiFinitetakes Stacks 02LR as a hypothesis.
theorem isSeparated_inf_quasiFinite_le_isQuasiAffineHom :
(@IsSeparated.{u} ⊓ @LocallyQuasiFinite ⊓ @LocallyOfFiniteType ⊓ @QuasiCompact :
MorphismProperty Scheme.{u}) ≤ @IsQuasiAffineHom
Tag 05K0, a lemma
Tag 05K0 in the Stacks Project.
Stacks.FiniteFactorization.exists_isOpenImmersion_isFinite_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteFactorization/Basic.lean, line 102. References: EGA III (4.4.12), “Quasi-finite case”; EGA III (4.4.3), “more general”; EGA III (4.4.5), “special case”; EGA IV (18.12.13).
Zariski's Main Theorem (Stacks Project, Tag 05K0). A quasi-finite separated morphism
f : X ⟶ Sonto a quasi-compact quasi-separated scheme factors as a quasi-compact open immersionj : X ⟶ Tfollowed by a finite morphismπ : T ⟶ S.Quasi-finiteness is Stacks 02NG, that is, locally quasi-finite and of finite type, which in Mathlib's vocabulary is
AlgebraicGeometry.LocallyQuasiFinite,AlgebraicGeometry.LocallyOfFiniteTypeandAlgebraicGeometry.QuasiCompacttogether.The affine case of the factorization, [Stacks, Tag 03GU], is
AlgebraicGeometry.exists_isOpenImmersion_isFinite_factorization; it is a different statement and is not used here.
theorem exists_isOpenImmersion_isFinite_factorization {X S : Scheme.{u}} (f : X ⟶ S)
[IsSeparated f] [LocallyQuasiFinite f] [LocallyOfFiniteType f] [QuasiCompact f]
[CompactSpace S] [QuasiSeparatedSpace S] :
∃ (T : Scheme.{u}) (j : X ⟶ T) (π : T ⟶ S),
IsOpenImmersion j ∧ QuasiCompact j ∧ IsFinite π ∧ f = j ≫ π
Tag 0F2N, a lemma
Tag 0F2N in the Stacks Project.
Stacks.FiniteFactorization.exists_isOpenImmersion_isFinite_finitePresentation_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteFactorization/Basic.lean, line 181. References: EGA III (4.4.12), “Quasi-finite case”; EGA III (4.4.3), “more general”; EGA III (4.4.5), “special case”; EGA IV (18.12.13), “special case”; EGA IV (8.12.6).
Zariski's Main Theorem with finite presentation (Stacks Project, Tag 0F2N). Let
f : X ⟶ Sbe a quasi-finite separated morphism onto a quasi-compact quasi-separated scheme, and assume in addition thatfis locally of finite presentation. Then the factorization of [Stacks, Tag 05K0] into a quasi-compact open immersionj : X ⟶ Tfollowed by a finite morphismπ : T ⟶ Smay be chosen withπof finite presentation as well.Quasi-finiteness is Stacks 02NG, as for Tag 05K0:
AlgebraicGeometry.LocallyQuasiFinite,AlgebraicGeometry.LocallyOfFiniteTypeandAlgebraicGeometry.QuasiCompacttogether. Finite presentation ofπisAlgebraicGeometry.FinitePresentation, part (3) of [Stacks, Tag 01TP]; for a finite, hence affine, morphism it is the same as being locally of finite presentation, so this is the tag's "finite and of finite presentation overS".
theorem exists_isOpenImmersion_isFinite_finitePresentation_factorization
{X S : Scheme.{u}} (f : X ⟶ S)
[IsSeparated f] [LocallyQuasiFinite f] [LocallyOfFiniteType f] [QuasiCompact f]
[LocallyOfFinitePresentation f] [CompactSpace S] [QuasiSeparatedSpace S] :
∃ (T : Scheme.{u}) (j : X ⟶ T) (π : T ⟶ S),
IsOpenImmersion j ∧ QuasiCompact j ∧ IsFinite π ∧ FinitePresentation π ∧ f = j ≫ π
Sources
Section37.44 Applications of Zariski's Main Theorem, I#
Section 37.44 of the Stacks Project, Tag 0F2P. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02LS, a lemma
Tag 02LS in the Stacks Project.
AlgebraicGeometry.IsFinite.tfae_isProper_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/FiniteIffQuasiFinite.lean, line 51. References: EGA III (4.4.11), “more general”; EGA IV (18.12.4).
For a morphism of schemes
f : X ⟶ Sthe following are equivalent:fis finite;fis proper with finite fibres;fis proper and locally quasi-finite;fis universally closed, separated, locally of finite type and has finite fibres. The fibre oversis its underlying setf ⁻¹' {s}.
theorem IsFinite.tfae_isProper_locallyQuasiFinite {X S : Scheme.{u}} (f : X ⟶ S) :
List.TFAE
[IsFinite f,
IsProper f ∧ ∀ s : S, (f ⁻¹' {s}).Finite,
IsProper f ∧ LocallyQuasiFinite f,
UniversallyClosed f ∧ IsSeparated f ∧ LocallyOfFiniteType f ∧
∀ s : S, (f ⁻¹' {s}).Finite]
AlgebraicGeometry.isFinite_iff_isProper_and_forall_finite_preimage_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/ProperFiniteFibre.lean, line 86. The attribute's comment: “condition (1) <=> condition (2): a morphism of schemes is finite exactly when it is proper with finite fibres. PROVED outright, with no hypothesis beyond the two sides of the equivalence: Mathlib's IsFinite.iff_isProper_and_locallyQuasiFinite is the tag's own (1) <=> (3), and locallyQuasiFinite_iff_finite_preimage_singleton turns local quasi-finiteness into finiteness of the fibres. Properness in Mathlib's sense contains universal closedness and therefore quasi-compactness, so the source's finite-type requirement is met.”. References: EGA III (4.4.11), “more general”; EGA III (4.4.2), “more general”; EGA IV (18.12.4).
[Stacks, Tag 02LS], condition (1) ⟺ condition (2). A morphism of schemes is finite exactly when it is proper and all of its fibres are finite.
The source's properness is
AlgebraicGeometry.IsProper, which containsAlgebraicGeometry.UniversallyClosedand henceAlgebraicGeometry.QuasiCompact, so no further hypothesis is needed to pass between finiteness of the fibres and local quasi-finiteness.
theorem isFinite_iff_isProper_and_forall_finite_preimage_singleton {X S : Scheme.{u}}
(f : X ⟶ S) :
IsFinite f ↔ IsProper f ∧ ∀ s : S, (f ⁻¹' {s}).Finite
AlgebraicGeometry.isFinite_iff_isSeparated_universallyClosed_locallyOfFiniteType_and_finite_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/ProperFiniteFibre.lean, line 100. The attribute's comment: “condition (1) <=> condition (4): a morphism of schemes is finite exactly when it is separated, universally closed, locally of finite type and has finite fibres. PROVED outright from condition (1) <=> condition (2) by unfolding Mathlib's IsProper into its three parents.”. References: EGA III (4.4.2), “more general”.
[Stacks, Tag 02LS], condition (1) ⟺ condition (4). A morphism of schemes is finite exactly when it is separated, universally closed, locally of finite type and has finite fibres. This is the previous equivalence with
AlgebraicGeometry.IsProperunfolded into its three parents.
theorem isFinite_iff_isSeparated_universallyClosed_locallyOfFiniteType_and_finite_fibres
{X S : Scheme.{u}} (f : X ⟶ S) :
IsFinite f ↔ (IsSeparated f ∧ UniversallyClosed f ∧ LocallyOfFiniteType f) ∧
∀ s : S, (f ⁻¹' {s}).Finite
Sources
Section37.45 Applications of Zariski's Main Theorem, II#
Section 37.45 of the Stacks Project, Tag 0F2Q. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07S0, a lemma
Tag 07S0 in the Stacks Project.
AlgebraicGeometry.exists_isAffineOpen_containing_finite_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Affine/QuasiAffineQuasiFinite.lean, line 168.
Stacks Project, Tag 07S0. Let
f : X ⟶ Sbe a separated quasi-finite morphism of schemes with affine target. Then every finite set of points ofXis contained in a single affine open ofX.Cover the finite set by finitely many affine opens and let
Ube their union. ThenUis quasi-compact, soU.ι ≫ fis quasi-compact, and it is still separated and quasi-finite; hence it is quasi-affine by Stacks 02LR. Taking the affine open⊤ofSshows thatUitself is a quasi-affine scheme, and Stacks 01ZY part (1) puts the finite set into an affine open ofU.
theorem exists_isAffineOpen_containing_finite_of_locallyQuasiFinite [IsSeparated f]
[LocallyQuasiFinite f] [LocallyOfFiniteType f] [IsAffine S] {E : Set X} (hE : E.Finite) :
∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ U
Tag 03I1, a lemma
Tag 03I1 in the Stacks Project.
AlgebraicGeometry.exists_dense_open_isFinite_of_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteOverDenseOpen.lean, line 208.
Stacks Project, Tag 03I1. A quasi-finite morphism of schemes is finite over a dense open subscheme of its target. This is also the statement of [Stacks Project, Tag 03HZ], the remark offering it as an alternative to [Stacks Project, Tag 02NW] and deferring its proof to here.
theorem exists_dense_open_isFinite_of_quasiFinite {Y X : Scheme.{u}} (f : Y ⟶ X)
[LocallyOfFiniteType f] [LocallyQuasiFinite f] [QuasiCompact f] :
∃ U : X.Opens, Dense (U : Set X) ∧ IsFinite (f ∣_ U)
Tag 07RY, a lemma
Tag 07RY in the Stacks Project.
AlgebraicGeometry.exists_closed_filtration_characterizing_finiteLocallyFree_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/DegreeStratification.lean, line 760.
Stacks Project, Tag 07RY. A separated, flat, locally finitely presented, locally quasi-finite morphism with universally bounded fibres admits a finite closed filtration whose strata universally characterize finite locally free base changes of each degree.
public theorem exists_closed_filtration_characterizing_finiteLocallyFree_rank
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
[IsSeparated f] [LocallyQuasiFinite f] (hbounded : HasUniversallyBoundedFibers f) :
∃ (n : ℕ) (Z : Fin (n + 2) → Set S),
(∀ i, IsClosed (Z i)) ∧
Z 0 = ∅ ∧
Z (Fin.last (n + 1)) = Set.univ ∧
(∀ i : Fin (n + 1), Z i.castSucc ⊆ Z i.succ) ∧
∀ (r : Fin (n + 1)) (T : Scheme.{u}) (g : T ⟶ S),
IsFiniteLocallyFreeOfRank (pullback.snd f g) r.val ↔
Set.range g.base ⊆ Z r.succ \ Z r.castSucc
Tag 07RZ, a lemma
Tag 07RZ in the Stacks Project.
AlgebraicGeometry.exists_quasiCompact_stratification_of_finiteLocallyFree_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/DegreeStratification.lean, line 1181.
Stacks Project, Tag 07RZ. A flat, locally finitely presented, separated and quasi-finite morphism admits an increasing sequence of closed subsets of its target whose successive differences are quasi-compactly immersed and are characterised by the degree of the finite locally free base changes of the morphism.
public theorem exists_quasiCompact_stratification_of_finiteLocallyFree_rank
{X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f] [IsSeparated f]
[LocallyQuasiFinite f] [QuasiCompact f] :
∃ (Z : ℕ → Set S) (Y : ℕ → Scheme.{u}) (i : (r : ℕ) → Y r ⟶ S),
(∀ r, IsClosed (Z r)) ∧
Z 0 = ∅ ∧
(∀ r, Z r ⊆ Z (r + 1)) ∧
(⋃ r, Z r) = Set.univ ∧
(∀ r, IsImmersion (i r)) ∧
(∀ r, QuasiCompact (i r)) ∧
(∀ r, Set.range (i r).base = Z (r + 1) \ Z r) ∧
∀ (r : ℕ) (T : Scheme.{u}) (g : T ⟶ S),
IsFiniteLocallyFreeOfRank (pullback.snd f g) r ↔
Set.range g.base ⊆ Z (r + 1) \ Z r
Tag 086R, a lemma
Tag 086R in the Stacks Project.
AlgebraicGeometry.exists_antitone_opens_iff_fiber_degree_ge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/DegreeOpenness.lean, line 443.
A flat, locally finitely presented, separated and locally quasi-finite morphism of schemes has a decreasing sequence of open subschemes of its target through which a field-valued point factors exactly when the corresponding fibre has degree at least the index; a fibre which is not finite counts as having infinite degree.
public theorem exists_antitone_opens_iff_fiber_degree_ge {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
[LocallyOfFinitePresentation f] [IsSeparated f] [LocallyQuasiFinite f] :
∃ U : ℕ → S.Opens,
U 0 = ⊤ ∧ Antitone U ∧
∀ (d : ℕ) (k : Type u) [Field k] (g : Spec (.of k) ⟶ S),
(∃ h : Spec (.of k) ⟶ (U d).toScheme, h ≫ (U d).ι = g) ↔
(¬ IsFinite (pullback.fst g f) ∨
∃ r : ℕ, d ≤ r ∧ IsFiniteLocallyFreeOfRank (pullback.fst g f) r)
Tag 082V, a lemma
Tag 082V in the Stacks Project.
AlgebraicGeometry.exists_open_injective_ideal_sum_with_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/SectionIdealSumCapture.lean, line 1471.
Stacks 082V. For
f : X ⟶ Sflat, locally of finite presentation and locally quasi-finite andga nonzero global function onX, there are opensV ⊆ f ⁻¹ Uon whichgstays nonzero and a quasi-coherent ideal sheafF ⊆ 𝒪_Usuch that a finite direct sum ofr > 0copies ofFinjects intof_* 𝒪_Vwithg|_Vin the image.
public theorem exists_open_injective_ideal_sum_with_section
{X S : Scheme.{u}} (f : X ⟶ S)
[Flat f] [LocallyOfFinitePresentation f] [LocallyQuasiFinite f]
(g : Γ(X, ⊤)) (hg : g ≠ 0) :
∃ (U : S.Opens) (V : X.Opens) (hVU : V ≤ f ⁻¹ᵁ U)
(F : (SheafOfModules.unit U.toScheme.ringCatSheaf).Submodule),
F.toSheafOfModules.IsQuasicoherent ∧
∃ (r : ℕ) (_hr : 0 < r)
(φ : (∐ fun _ : Fin r => F.toSheafOfModules) ⟶
(Scheme.Modules.pushforward (f.resLE U V hVU)).obj (SheafOfModules.unit _)),
Mono φ ∧
∃ t : Γ((∐ fun _ : Fin r => F.toSheafOfModules), ⊤),
Scheme.Modules.Hom.app φ ⊤ t =
(show Γ((Scheme.Modules.pushforward (f.resLE U V hVU)).obj
(SheafOfModules.unit _), ⊤) from (V.ι.appTop).hom g) ∧
(V.ι.appTop).hom g ≠ 0
Tag 09Z0, a lemma
Tag 09Z0 in the Stacks Project.
Stacks.MoreMorphisms.exists_isIntegralHom_surjective_zariskiLocallyFactors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IntegralRefinement.lean, line 907. The attribute's comment: “the existence assertion: a surjective étale covering of a quasi-compact and quasi-separated scheme is refined by a surjective integral morphism factoring through it Zariski-locally. The closing sentence, that the refinement may be taken finite and of finite presentation, is Stacks.MoreMorphisms.exists_isFinite_finitePresentation_surjective_zariskiLocallyFactors”.
Stacks, Tag 09Z0: a surjective étale covering is refined by a surjective integral morphism which factors through it Zariski-locally. Let
p : U ⟶ Xbe a surjective étale morphism of schemes withXquasi-compact and quasi-separated. Then there exist a schemeYand a surjective integral morphismf : Y ⟶ Xsuch that every point ofYhas an open neighbourhoodVfor whichV ⟶ Xfactors throughp.This is the general case of the tag's existence statement: neither separatedness of
pnor any hypothesis on its fibre degrees is assumed. The source's first reduction, to an affine — hence separated — source, isStacks.MoreMorphisms.exists_of_isAffine_source; a natural-number bound for the degrees of the fibres over that affine source comes from Stacks, Tag 03JA; and the induction on that bound isStacks.MoreMorphisms.exists_isIntegralHom_factorsNear_of_boundsFiberDegrees.The tag's closing refinement, that
fmay moreover be taken finite and of finite presentation, isStacks.MoreMorphisms.exists_isFinite_finitePresentation_surjective_zariskiLocallyFactors, proved by presenting the integral refinement produced here as a limit of morphisms finite and of finite presentation.
public theorem exists_isIntegralHom_surjective_zariskiLocallyFactors (p : U ⟶ X) [Etale p]
[Surjective p] [CompactSpace X] [QuasiSeparatedSpace X] :
∃ (Y : Scheme.{u}) (f : Y ⟶ X), IsIntegralHom f ∧ Surjective f ∧
ZariskiLocallyFactors f p
Stacks.MoreMorphisms.exists_isFinite_finitePresentation_surjective_zariskiLocallyFactors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/IntegralRefinementFinite.lean, line 140. The attribute's comment: “the whole statement: the surjective refinement factoring through the covering Zariski-locally, and the closing sentence that it may be taken finite and of finite presentation”.
Stacks, Tag 09Z0: the refinement may be taken finite and of finite presentation. Let
p : U ⟶ Xbe a surjective étale morphism of schemes withXquasi-compact and quasi-separated. Then there exist a schemeYand a surjective morphismf : Y ⟶ Xwhich is finite and of finite presentation — hence in particular integral — such that every point ofYhas an open neighbourhoodVfor whichV ⟶ Xfactors throughp.This is the whole of the tag: the first assertion asks only that
fbe integral, which finiteness gives, and the closing sentence asks for exactly the finiteness and the finite presentation. No hypothesis beyond the source's is used; in particularpis not assumed separated and nothing is assumed about the degrees of its fibres.The integral refinement is
Stacks.MoreMorphisms.exists_isIntegralHom_surjective_zariskiLocallyFactors; it is presented as a limit of morphisms finite and of finite presentation byStacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation, which is Stacks, Tag 09YZ over a quasi-compact and quasi-separated base; and one stage of that limit already carries the covering and the factorisations, byAlgebraicGeometry.exists_finite_surjective_refinement_of_isLimit.
public theorem exists_isFinite_finitePresentation_surjective_zariskiLocallyFactors (p : U ⟶ X)
[Etale p] [Surjective p] [CompactSpace X] [QuasiSeparatedSpace X] :
∃ (Y : Scheme.{u}) (f : Y ⟶ X), IsIntegralHom f ∧ Surjective f ∧ IsFinite f ∧
LocallyOfFinitePresentation f ∧ QuasiCompact f ∧ QuasiSeparated f ∧
ZariskiLocallyFactors f p
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.