67.49 Normalization to 67.53 Universal homeomorphisms

Section67.49 Normalization #

Section 67.49 of the Stacks Project, Tag 07U3. 9 tags here are carried by 32 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BB1, a lemma

Tag 0BB1 in the Stacks Project.

AlgebraicGeometry.Space.exists_surjective_etale_chart_iff_hasLocallyFiniteIrreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 213. The attribute's comment: “conditions (1) and (2)”.

An algebraic space has a surjective étale scheme chart with finitely many irreducible components over each of its quasi-compact opens if and only if every étale scheme chart has that property.

theorem exists_surjective_etale_chart_iff_hasLocallyFiniteIrreducibleComponents
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F) :
    (∃ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F),
        IsSurjective B S hS f ∧ IsEtale B S hS f ∧
          ∀ V : ((BigFppfOver.toScheme B S hS).obj U).Opens,
            IsCompact (V : Set ((BigFppfOver.toScheme B S hS).obj U)) →
              (irreducibleComponents V).Finite) ↔
      HasLocallyFiniteIrreducibleComponents B S hS F

AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_finite_codimensionZeroPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 240. The attribute's comment: “conditions (2) and (3)”.

Every étale scheme chart of F has finitely many irreducible components over each of its quasi-compact opens exactly when every quasi-compact algebraic space étale over F has finitely many points of codimension zero.

theorem hasLocallyFiniteIrreducibleComponents_iff_finite_codimensionZeroPoints
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} :
    HasLocallyFiniteIrreducibleComponents B S hS F ↔
      ∀ (G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS G →
        IsQuasiCompactSpace B S hS G → ∀ g : G ⟶ F, IsEtale B S hS g →
          {x : points B S hS G | localRingDimension B S hS x = 0}.Finite

AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_finite_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 282. The attribute's comment: “conditions (2) and (4)”.

Every étale scheme chart of F has finitely many irreducible components over each of its quasi-compact opens exactly when the space of points of every quasi-compact algebraic space étale over F has finitely many irreducible components.

theorem hasLocallyFiniteIrreducibleComponents_iff_finite_irreducibleComponents
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} :
    HasLocallyFiniteIrreducibleComponents B S hS F ↔
      ∀ (G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS G →
        IsQuasiCompactSpace B S hS G → ∀ g : G ⟶ F, IsEtale B S hS g →
          (irreducibleComponents (points B S hS G)).Finite

AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 310. The attribute's comment: “representable case”.

For an algebraic space represented by a scheme of the site, HasLocallyFiniteIrreducibleComponents is finiteness of the irreducible components of the quasi-compact opens of that scheme.

theorem hasLocallyFiniteIrreducibleComponents_iff_of_isRepresentable
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} [F.IsRepresentable]
    (hF : IsAlgebraicSpace B S hS F) :
    HasLocallyFiniteIrreducibleComponents B S hS F ↔
      ∀ V : ((BigFppfOver.toScheme B S hS).obj F.reprX).Opens,
        IsCompact (V : Set ((BigFppfOver.toScheme B S hS).obj F.reprX)) →
          (irreducibleComponents V).Finite

Tag 0GMB, a lemma

Tag 0GMB in the Stacks Project.

AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationFiniteness.lean, line 88.

A locally Noetherian algebraic space over S has finitely many irreducible components over every quasi-compact open of every étale scheme chart.

theorem hasLocallyFiniteIrreducibleComponents_of_isLocallyNoetherian
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hN : HasEtaleLocalProperty B S hS F (fun T : Scheme.{u} ↦ IsLocallyNoetherian T)) :
    HasLocallyFiniteIrreducibleComponents B S hS F

Tag 0GMC, a lemma

Tag 0GMC in the Stacks Project.

AlgebraicGeometry.mem_genericPoints_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/FlatCodimensionZero.lean, line 183. The attribute's comment: “representable case”.

Stacks Project, Tag 0GMC, representable case. A flat morphism of schemes carries a generic point of an irreducible component of its source to a generic point of an irreducible component of its target. Equivalently, it carries codimension-zero points to codimension-zero points, which is the second conclusion of Tag 0GMD.

public theorem mem_genericPoints_of_flat {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f]
    {x : X} (hx : x ∈ genericPoints X) : f x ∈ genericPoints Y

AlgebraicGeometry.Space.localRingDimension_eq_zero_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 460.

A flat morphism of algebraic spaces takes points of codimension zero to points of codimension zero.

theorem localRingDimension_eq_zero_of_isFlat
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsFlat B S hS f)
    (x : points B S hS X) (hx : localRingDimension B S hS x = 0) :
    localRingDimension B S hS (pointsMap B S hS X f x) = 0

Tag 0GMD, a lemma

Tag 0GMD in the Stacks Project.

AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_and_codimensionZero_of_isFlat_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/NormalizationFlatFiniteType.lean, line 56.

Stacks 0GMD. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat and locally of finite type, and assume Y satisfies the equivalent conditions of Stacks 0BB1. Then X satisfies those conditions too, and for every point x of X of codimension zero the image f x has codimension zero in Y.

theorem hasLocallyFiniteIrreducibleComponents_and_codimensionZero_of_isFlat_of_isLocallyOfFiniteType
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsFlat B S hS f)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hYfinite : HasLocallyFiniteIrreducibleComponents B S hS Y) :
    HasLocallyFiniteIrreducibleComponents B S hS X ∧
      ∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        localRingDimension B S hS (pointsMap B S hS X f x) = 0

Tag 07U4, a lemma

Tag 07U4 in the Stacks Project.

AlgebraicGeometry.Space.NormalizationData.existsUnique_normalizationLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/NormalizationFunctoriality.lean, line 68. The attribute's comment: “part (3), for arbitrary normalization data of the two spaces: the unique lift of a morphism preserving codimension-zero points”.

Stacks 07U4, part (3). Let f : F ⟶ G be a morphism of algebraic spaces over S carrying every point of codimension zero to a point of codimension zero, and let ν : F^ν ⟶ F and μ : G^ν ⟶ G be normalizations. Then there is a unique morphism f^ν : F^ν ⟶ G^ν with μ ∘ f^ν = f ∘ ν.

This is the universal property of the normalization of G, part (4) of Stacks 0BB4, applied to the composite F^ν ⟶ F ⟶ G. Its two hypotheses on that composite are normality of F^ν, which is part (1) of Stacks 0BB4, and preservation of codimension-zero points, which holds for ν by part (3) of Stacks 0BB4 and for f by assumption.

theorem existsUnique_normalizationLift {G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (D : NormalizationData B S hS F) (D' : NormalizationData B S hS G)
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G)
    (hgeneric : ∀ x : points B S hS F, localRingDimension B S hS x = 0 →
      localRingDimension B S hS (pointsMap B S hS F f x) = 0) :
    ∃! g : D.space ⟶ D'.space, g ≫ D'.hom = D.hom ≫ f

AlgebraicGeometry.Space.NormalizationData.isIso_pullbackLift_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/NormalizationFunctoriality.lean, line 173. The attribute's comment: “part (4), for a smooth morphism and arbitrary normalization data of the two spaces”. References: SGA 3 X (8.9), “partial”.

Stacks 07U4, part (4). Let f : F ⟶ G be a smooth — in particular an étale — morphism of algebraic spaces over S with G satisfying the equivalent conditions of Stacks 0BB1, and let ν : F^ν ⟶ F and μ : G^ν ⟶ G be normalizations. Then F satisfies the equivalent conditions of Stacks 0BB1 and f carries points of codimension zero to points of codimension zero — these are the hypotheses of part (3) — and the morphism f^ν of part (3) induces an isomorphism F^ν ⟶ F ×_G G^ν.

The two hypotheses of part (3) are Stacks 0GMD and Stacks 0GMC for the flat, locally finite-type morphism f.

For the isomorphism, F ×_G G^ν is terminal among normal algebraic spaces over F preserving codimension zero in the same way F^ν is, and the comparison morphisms are therefore mutually inverse. That F ×_G G^ν is such an object is read off one chart: AlgebraicGeometry.Space.NormalizationData.exists_chart_pullback_snd_of_isSmooth exhibits a surjective étale scheme chart of F over which pullback.snd μ f is the normalization of the chart, which makes F ×_G G^ν normal — the chart of it so produced has a normal scheme — and makes pullback.snd μ f preserve codimension zero, codimension zero being tested on that chart. The universal property of F^ν, part (4) of Stacks 0BB4, then supplies the morphism F ×_G G^ν ⟶ F^ν over F; its two composites with the canonical F^ν ⟶ F ×_G G^ν are identities by the uniqueness halves of that property for F and for G.

theorem isIso_pullbackLift_of_isSmooth {G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (D : NormalizationData B S hS F) (D' : NormalizationData B S hS G)
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    {f : F ⟶ G} (hf : IsSmooth B S hS f)
    (hGfin : HasLocallyFiniteIrreducibleComponents B S hS G) :
    HasLocallyFiniteIrreducibleComponents B S hS F ∧
      (∀ x : points B S hS F, localRingDimension B S hS x = 0 →
        localRingDimension B S hS (pointsMap B S hS F f x) = 0) ∧
      ∀ (g : D.space ⟶ D'.space) (hg : g ≫ D'.hom = D.hom ≫ f),
        IsIso (pullback.lift g D.hom hg)

AlgebraicGeometry.Space.NormalizationData.exists_iso_yoneda_normalizationScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationComparison.lean, line 96. The attribute's comment: “part (2): the normalization of a scheme as an algebraic space”.

Let X be an object of the big fppf site of S every quasi-compact open of whose underlying scheme has finitely many irreducible components, and let D be normalization data for the algebraic space it represents. Then D.space is represented by an object Xν of the site whose underlying scheme is the normalization scheme of the underlying scheme of X, and under that identification D.hom is the normalization morphism.

theorem exists_iso_yoneda_normalizationScheme {X : BigFppfOver B S hS}
    (D : NormalizationData B S hS (yoneda.obj X))
    (hX : ∀ V : ((BigFppfOver.toScheme B S hS).obj X).Opens,
      IsCompact (V : Set ((BigFppfOver.toScheme B S hS).obj X)) →
        (irreducibleComponents V).Finite) :
    ∃ (Xν : BigFppfOver B S hS) (p : Xν ⟶ X)
      (e : ((BigFppfOver.toScheme B S hS).obj Xν) ≅
        Scheme.normalizationScheme ((BigFppfOver.toScheme B S hS).obj X) hX)
      (φ : D.space ≅ yoneda.obj Xν),
      (BigFppfOver.toScheme B S hS).map p =
          e.hom ≫ Scheme.normalization ((BigFppfOver.toScheme B S hS).obj X) hX ∧
        φ.hom ≫ yoneda.map p = D.hom

AlgebraicGeometry.Space.NormalizationData.isNormal_and_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationIntegral.lean, line 114. The attribute's comment: “part (1)”.

Stacks 07U4, part (1). Let F be an algebraic space over S equipped with normalization data. Then the normalization of F is a normal algebraic space over S and the normalization morphism is integral.

The two halves are AlgebraicGeometry.Space.NormalizationData.isNormal and AlgebraicGeometry.Space.NormalizationData.isIntegralHom. The hypotheses of Stacks 0BB1 are carried by the chart field of AlgebraicGeometry.Space.NormalizationData, which produces for every surjective étale scheme chart the finiteness of the sets of irreducible components of its quasi-compact opens.

theorem isNormal_and_isIntegralHom {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (D : NormalizationData B S hS F) (hF : IsAlgebraicSpace B S hS F) :
    Space.IsNormal B S hS D.space ∧ Space.IsIntegralHom B S hS D.hom

AlgebraicGeometry.Space.isNormal_and_isIntegralHom_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationProperties.lean, line 83. The attribute's comment: “part (1)”.

Stacks 07U4, part (1). Let F be an algebraic space over S satisfying the equivalent conditions of Tag 0BB1. Then its normalization F^ν is a normal algebraic space and the normalization morphism ν_F : F^ν ⟶ F is integral.

theorem isNormal_and_isIntegralHom_normalization {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS F) :
    Space.IsNormal B S hS (normalizationPresheaf B S hS hF hfin) ∧
      Space.IsIntegralHom B S hS (normalization B S hS hF hfin)

AlgebraicGeometry.Space.exists_iso_yoneda_normalizationScheme_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationProperties.lean, line 97. The attribute's comment: “part (2)”.

Stacks 07U4, part (2). Let X be an object of the big fppf site of S every quasi-compact open of whose underlying scheme has finitely many irreducible components, so that the algebraic space X represents satisfies the conditions of Tag 0BB1. Then the normalization X^ν of that algebraic space is represented by an object Xν of the site whose underlying scheme is the normalization scheme of the underlying scheme of X, and under that identification ν_X is the normalization morphism of Tag 035E.

theorem exists_iso_yoneda_normalizationScheme_normalization (X : BigFppfOver B S hS)
    (hX : ∀ V : ((BigFppfOver.toScheme B S hS).obj X).Opens,
      IsCompact (V : Set ((BigFppfOver.toScheme B S hS).obj X)) →
        (irreducibleComponents V).Finite) :
    ∃ (Xν : BigFppfOver B S hS) (p : Xν ⟶ X)
      (e : ((BigFppfOver.toScheme B S hS).obj Xν) ≅
        Scheme.normalizationScheme ((BigFppfOver.toScheme B S hS).obj X) hX)
      (φ : normalizationPresheaf B S hS (isAlgebraicSpace_yoneda B S hS X)
        (hasLocallyFiniteIrreducibleComponents_yoneda B S hS X hX) ≅ yoneda.obj Xν),
      (BigFppfOver.toScheme B S hS).map p =
          e.hom ≫ Scheme.normalization ((BigFppfOver.toScheme B S hS).obj X) hX ∧
        φ.hom ≫ yoneda.map p = normalization B S hS (isAlgebraicSpace_yoneda B S hS X)
          (hasLocallyFiniteIrreducibleComponents_yoneda B S hS X hX)

AlgebraicGeometry.Space.existsUnique_comp_normalization_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationProperties.lean, line 119. The attribute's comment: “part (3)”.

Stacks 07U4, part (3). Let f : F ⟶ G be a morphism of algebraic spaces over S both satisfying the equivalent conditions of Tag 0BB1, such that every point of codimension zero of F maps to a point of codimension zero of G. Then there is a unique morphism f^ν : F^ν ⟶ G^ν with ν_G ∘ f^ν = f ∘ ν_F.

theorem existsUnique_comp_normalization_eq {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hFfin : HasLocallyFiniteIrreducibleComponents B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (hGfin : HasLocallyFiniteIrreducibleComponents B S hS G)
    (f : F ⟶ G)
    (hgeneric : ∀ x : points B S hS F, localRingDimension B S hS x = 0 →
      localRingDimension B S hS (pointsMap B S hS F f x) = 0) :
    ∃! g : normalizationPresheaf B S hS hF hFfin ⟶ normalizationPresheaf B S hS hG hGfin,
      g ≫ normalization B S hS hG hGfin = normalization B S hS hF hFfin ≫ f

AlgebraicGeometry.Space.isIso_pullbackLift_normalization_of_isEtale_or_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationProperties.lean, line 144. The attribute's comment: “part (4)”.

Stacks 07U4, part (4). Let f : F ⟶ G be an étale or a smooth morphism of algebraic spaces over S with G satisfying the equivalent conditions of Tag 0BB1. Then the hypotheses of part (3) hold — F satisfies the conditions of Tag 0BB1 too, and f carries points of codimension zero to points of codimension zero — and the morphism f^ν : F^ν ⟶ G^ν of part (3) induces an isomorphism F^ν ⟶ F ×_G G^ν.

The third conjunct is the existence and uniqueness of f^ν, part (3) at the hypotheses just established, and the fourth is the isomorphism (f^ν, ν_F) : F^ν ⟶ F ×_G G^ν.

The condition of Tag 0BB1 on F is stated as an existential because the normalization F^ν is only defined given it; by proof irrelevance the witness does not matter. The isomorphism is asserted for every g with ν_G ∘ g = f ∘ ν_F, and by the third conjunct there is exactly one such g, namely f^ν.

theorem isIso_pullbackLift_normalization_of_isEtale_or_isSmooth
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hGfin : HasLocallyFiniteIrreducibleComponents B S hS G) {f : F ⟶ G}
    (hf : IsEtale B S hS f ∨ IsSmooth B S hS f) :
    ∃ hFfin : HasLocallyFiniteIrreducibleComponents B S hS F,
      (∀ x : points B S hS F, localRingDimension B S hS x = 0 →
        localRingDimension B S hS (pointsMap B S hS F f x) = 0) ∧
      (∃! g : normalizationPresheaf B S hS hF hFfin ⟶ normalizationPresheaf B S hS hG hGfin,
        g ≫ normalization B S hS hG hGfin = normalization B S hS hF hFfin ≫ f) ∧
      ∀ (g : normalizationPresheaf B S hS hF hFfin ⟶ normalizationPresheaf B S hS hG hGfin)
        (hg : g ≫ normalization B S hS hG hGfin = normalization B S hS hF hFfin ≫ f),
        IsIso (pullback.lift g (normalization B S hS hF hFfin) hg)

AlgebraicGeometry.Space.exists_normalizationData_isNormal_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSiteChart.lean, line 106. The attribute's comment: “the construction and part (1) at the hypotheses of the tag: an algebraic space satisfying condition (2) of Tag 0BB1 has normalization data, its normalization is normal, and its normalization morphism is integral”.

Stacks 07U4, the construction together with part (1), at the hypotheses of the tag. Let F be an algebraic space over S satisfying condition (2) of Tag 0BB1: every quasi-compact open of every étale scheme chart of F has finitely many irreducible components. Then there is normalization data for F — an algebraic space F^ν over S together with a morphism ν_F : F^ν ⟶ F whose base change along every surjective étale scheme chart of F is the normalization of that chart — with F^ν normal and ν_F integral.

Nothing is assumed beyond the two hypotheses the tag itself carries: no normalization data is given, F is not assumed representable, and no bound on sizes is imposed. The datum is AlgebraicGeometry.Space.nonempty_normalizationData, which forms F^ν as the quotient of a normalized étale presentation, and the two properties are AlgebraicGeometry.Space.NormalizationData.isNormal_and_isIntegralHom.

The other three parts of the tag are stated for an arbitrary AlgebraicGeometry.Space.NormalizationData and so are unconditional as they stand; what this statement adds to them is that their hypothesis is always satisfiable. Part (2), the identification of the normalization of a representable algebraic space with the normalization scheme of the representing scheme, is AlgebraicGeometry.Space.NormalizationData.exists_iso_yoneda_normalizationScheme. Part (3), the unique lift of a morphism carrying points of codimension zero to points of codimension zero, is AlgebraicGeometry.Space.NormalizationData.existsUnique_normalizationLift. Part (4), the identification of the normalization of the source of a smooth — in particular an étale — morphism with the base change of the normalization of the target, is AlgebraicGeometry.Space.NormalizationData.isIso_pullbackLift_of_isSmooth.

theorem exists_normalizationData_isNormal_isIntegralHom (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS F) :
    ∃ D : NormalizationData B S hS F,
      Space.IsNormal B S hS D.space ∧ Space.IsIntegralHom B S hS D.hom

AlgebraicGeometry.Space.NormalizationData.isPullback_hom_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSmoothBaseChange07U4.lean, line 172. The attribute's comment: “part (4) for a smooth morphism of algebraic spaces, with given normalizations”.

Stacks 07U4, part (4), for a smooth morphism of algebraic spaces: the normalization square is cartesian. Let φ : F ⟶ G be a smooth morphism of algebraic spaces over S, let D be normalization data for G and D' normalization data for F. Then there is a morphism F^ν ⟶ G^ν over φ exhibiting F^ν as the fibre product F ×_G G^ν.

The morphism F^ν ⟶ G^ν and its inverse comparison F ×_G G^ν ⟶ F^ν both come from the universal property of the normalization, Stacks 0BB4 part (4): F^ν is normal, and so is F ×_G G^ν, being smooth over the normal space G^ν; the relevant morphisms carry codimension zero to codimension zero because flat morphisms do (Stacks 0GMC), because the normalization morphisms do (Stacks 0BB4 part (3)), and because the projection F ×_G G^ν ⟶ F does (AlgebraicGeometry.Space.NormalizationData.localRingDimension_pullback_snd_eq_zero). The two composites are identities by the uniqueness half of the same universal property.

theorem isPullback_hom_of_isSmooth (D : NormalizationData B S hS G)
    (D' : NormalizationData B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hF : IsAlgebraicSpace B S hS F) (φ : F ⟶ G) (hφ : IsSmooth B S hS φ) :
    ∃ m : D'.space ⟶ D.space, IsPullback m D'.hom D.hom φ

AlgebraicGeometry.Space.NormalizationData.exists_isPullback_hom_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSmoothBaseChange07U4.lean, line 229. The attribute's comment: “part (4) for a smooth morphism of algebraic spaces”.

Stacks 07U4, part (4), for a smooth morphism, with the normalization of the source produced. Only normalization data for the target is given: the source satisfies the condition of Stacks 0BB1 because the target does and the morphism is flat and locally of finite type (Stacks 0GMD), so it has normalization data by Stacks 07U4, and AlgebraicGeometry.Space.NormalizationData.isPullback_hom_of_isSmooth applies to it.

theorem exists_isPullback_hom_of_isSmooth (D : NormalizationData B S hS G)
    (hG : IsAlgebraicSpace B S hS G) (hF : IsAlgebraicSpace B S hS F) (φ : F ⟶ G)
    (hφ : IsSmooth B S hS φ) (hGfin : HasLocallyFiniteIrreducibleComponents B S hS G) :
    ∃ (D' : NormalizationData B S hS F) (m : D'.space ⟶ D.space),
      IsPullback m D'.hom D.hom φ

AlgebraicGeometry.Space.nonempty_normalizationData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSpaceConstruction.lean, line 202. The attribute's comment: “the existence of the normalization”.

Tag 07U4, the existence of the normalization. An algebraic space over S every quasi-compact open of every étale scheme chart of which has finitely many irreducible components — condition (2) of Tag 0BB1 — has normalization data: an algebraic space F^ν over S with a morphism F^ν ⟶ F whose base change along every surjective étale scheme chart of F is the normalization of that chart.

The datum is glued along a surjective étale chart w : h_U ⟶ F: the normalizations of the charts along R = U ×_F U form an étale equivalence relation, the quotient sheaf is an algebraic space by Tag 02WW, and the chart condition is checked at w by a computation with the kernel pair of the quotient map and at every other chart by descent along the refinement. No representability and no bound on sizes is assumed.

The four numbered parts of Tag 07U4 are not proved here; they are the subject of StacksFrontier.AlgebraicGeometry.Spaces.Normal, StacksFrontier.AlgebraicGeometry.Spaces.NormalizationIntegral and StacksFrontier.AlgebraicGeometry.Spaces.NormalizationEtaleChart, which assume the datum this theorem produces.

theorem nonempty_normalizationData {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS F) :
    Nonempty (NormalizationData B S hS F)

Tag 0BB2, a definition

Tag 0BB2 in the Stacks Project.

AlgebraicGeometry.Space.normalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSiteChart.lean, line 188. The attribute's comment: “the normalization ν_F : F^ν ⟶ F of an algebraic space satisfying the conditions of Tag 0BB1, defined as the construction of Tag 07U4 (the quotient of the normalized étale presentation); unique up to unique isomorphism over F by existsUnique_iso_normalization”.

Stacks 0BB2, the normalization of an algebraic space. Let F be an algebraic space over S satisfying the equivalent conditions of Tag 0BB1. The normalization of F is the morphism

ν_F : F^ν ⟶ F

constructed in Tag 07U4. Concretely it is the morphism of the normalization datum AlgebraicGeometry.Space.normalizationData, which is the construction of Tag 07U4, AlgebraicGeometry.Space.NormSpaceGluing.normalizationDataOfPresentation, run on a chosen surjective étale scheme chart w : h_U ⟶ F and its kernel pair R = U ×_F U: the normalizations of the charts R^ν ⇉ U^ν form an étale equivalence relation, F^ν = U^ν / R^ν (AlgebraicGeometry.Space.normalizationPresheaf) is its quotient, an algebraic space by Tag 02WW, and ν_F is the morphism F^ν ⟶ F through which the normalization U^ν ⟶ U ⟶ F of the chart descends. No normalization datum or other structure is an input: the definition depends on F and on the two hypotheses of the tag only.

Defining properties. ν_F is characterised, up to unique isomorphism over F, by its chart condition: along every surjective étale scheme chart U ⟶ F its base change is the normalization U^ν ⟶ U of the chart (AlgebraicGeometry.Space.normalization_chart). Any morphism with this property — any AlgebraicGeometry.Space.NormalizationData for F — is identified with ν_F by a unique isomorphism over F (AlgebraicGeometry.Space.existsUnique_iso_normalization), so the choice of the chart made by the construction affects nothing up to unique isomorphism, as in the source. ν_F is moreover the universal morphism to F from a normal algebraic space which carries points of codimension zero to points of codimension zero (AlgebraicGeometry.Space.existsUnique_lift_normalization).

The theorems of Tag 07U4 about it. Part (1): F^ν is an algebraic space (AlgebraicGeometry.Space.isAlgebraicSpace_normalizationPresheaf), normal (AlgebraicGeometry.Space.isNormal_normalizationPresheaf), and ν_F is integral (AlgebraicGeometry.Space.isIntegralHom_normalization); at the hypotheses of the tag this is also AlgebraicGeometry.Space.exists_normalizationData_isNormal_isIntegralHom. Parts (2) to (4) — the comparison with the normalization of a scheme, the unique lift f^ν of a morphism preserving codimension-zero points, and X^ν ≅ X ×_Y Y^ν along a smooth morphism — are AlgebraicGeometry.Space.NormalizationData.exists_iso_yoneda_normalizationScheme, AlgebraicGeometry.Space.NormalizationData.existsUnique_normalizationLift and AlgebraicGeometry.Space.NormalizationData.isIso_pullbackLift_of_isSmooth, which hold for every normalization datum and so in particular for AlgebraicGeometry.Space.normalizationData, whose morphism this is. Surjectivity and the bijection on codimension-zero points (Tag 0BB4) are AlgebraicGeometry.Space.isSurjective_normalization and AlgebraicGeometry.Space.bijOn_codimensionZeroPoints_normalization.

The hypothesis carried is condition (2) of Tag 0BB1, AlgebraicGeometry.Space.HasLocallyFiniteIrreducibleComponents, which the comparisons of that tag — AlgebraicGeometry.Space.exists_surjective_etale_chart_iff_hasLocallyFiniteIrreducibleComponents, AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_finite_codimensionZeroPoints, AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_finite_irreducibleComponents and AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_of_isRepresentable — identify with each of the other conditions, so it is the hypothesis Tag 0BB2 itself carries. Nothing further is assumed: F is not assumed representable and no bound on sizes is imposed.

def normalization (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS F) :
    normalizationPresheaf B S hS hF hfin ⟶ F

Declarations registered for the tag:

AlgebraicGeometry.Space.NormalizationData.hom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 1144 (StacksFrontier).

Tag 0BB3, a lemma

Tag 0BB3 in the Stacks Project.

AlgebraicGeometry.Space.NormalizationData.existsUnique_lift_hom_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 1078. The attribute's comment: “the factorization through the reduction”.

The normalization morphism of an algebraic space factors uniquely through any closed subspace whose points are all the points of the space, in particular through the reduction.

theorem existsUnique_lift_hom_reduction (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) (R : Subfunctor F) (hR : IsClosedSubspace B S hS R)
    (hfull : Set.range (pointsMap B S hS R.toFunctor R.ι) = Set.univ) :
    ∃! g : D.space ⟶ R.toFunctor, g ≫ R.ι = D.hom

AlgebraicGeometry.Space.NormalizationData.existsUnique_iso_of_hom_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 1097. The attribute's comment: “the normalization of the reduction”.

The factorization of the normalization morphism through the reduction exhibits the normalization of an algebraic space as the normalization of its reduction: it is carried to any normalization morphism of the reduction by a unique isomorphism.

theorem existsUnique_iso_of_hom_reduction (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) (R : Subfunctor F) (hR : IsClosedSubspace B S hS R)
    (hfull : Set.range (pointsMap B S hS R.toFunctor R.ι) = Set.univ)
    (D' : NormalizationData B S hS R.toFunctor) (g : D.space ⟶ R.toFunctor)
    (hg : g ≫ R.ι = D.hom) :
    ∃! e : D.space ≅ D'.space, e.hom ≫ D'.hom = g

AlgebraicGeometry.Space.NormalizationData.onReduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/NormalizationReductionData.lean, line 414. The attribute's comment: “the normalization of the reduction: the factorization is normalization data”.

Stacks 0BB3, the normalization of the reduction. The normalization of an algebraic space is the normalization of its reduction: the factorization of the normalization morphism through any closed subspace whose points are all the points of the space — in particular through the reduced one — is itself normalization data for that subspace, on the same algebraic space.

The morphism is the unique factorization of AlgebraicGeometry.Space.NormalizationData.existsUnique_lift_hom_reduction, and the chart condition is AlgebraicGeometry.Space.NormalizationData.chart_of_hom_reduction. Nothing is assumed about the subspace beyond being closed and carrying every point: no normalization of it is given, it is constructed.

noncomputable def onReduction (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) (R : Subfunctor F) (hR : IsClosedSubspace B S hS R)
    (hfull : Set.range (pointsMap B S hS R.toFunctor R.ι) = Set.univ) :
    NormalizationData B S hS R.toFunctor

AlgebraicGeometry.Space.existsUnique_comp_ι_reduction_eq_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationReduction.lean, line 101. The attribute's comment: “the normalization morphism ν_X of Tag 0BB2 factors uniquely through the reduction X_red ⟶ X”.

Stacks 0BB3, the factorization. Let X be an algebraic space over S satisfying the equivalent conditions of Tag 0BB1. The normalization morphism ν_X : X^ν ⟶ X of Tag 0BB2 factors through the reduction X_red ⟶ X of Tag 047X, and the factorization is unique.

This is AlgebraicGeometry.Space.NormalizationData.existsUnique_lift_hom_reduction at the normalization datum Tag 0BB2 constructs and at the reduction.

theorem existsUnique_comp_ι_reduction_eq_normalization
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X) :
    ∃! g : normalizationPresheaf B S hS hX hfin ⟶ (reduction B S hS X hX).toFunctor,
      g ≫ (reduction B S hS X hX).ι = normalization B S hS hX hfin

AlgebraicGeometry.Space.existsUnique_iso_normalization_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationReduction.lean, line 147. The attribute's comment: “the factorization X^ν ⟶ X_red is the normalization ν_{X_red} of Tag 0BB2: they are isomorphic over X_red by a unique isomorphism”.

Stacks 0BB3, the factorization is the normalization of the reduction. Let X be an algebraic space over S satisfying the equivalent conditions of Tag 0BB1, so that its reduction X_red satisfies them too (AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_reduction). Then the factorization X^ν ⟶ X_red of the normalization morphism through the reduction is the normalization ν_{X_red} : X_red^ν ⟶ X_red of Tag 0BB2: there is a unique isomorphism X^ν ≅ X_red^ν over X_red.

Nothing is assumed about the normalization of X_red: it is the one Tag 0BB2 constructs. The statement is AlgebraicGeometry.Space.NormalizationData.existsUnique_iso_of_hom_reduction at the two normalization data Tag 0BB2 constructs, for X and for X_red.

theorem existsUnique_iso_normalization_reduction {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hfin : HasLocallyFiniteIrreducibleComponents B S hS X) :
    ∃! e : normalizationPresheaf B S hS hX hfin ≅
        normalizationPresheaf B S hS (isAlgebraicSpace_reduction B S hS hX)
          (hasLocallyFiniteIrreducibleComponents_reduction B S hS hX hfin),
      e.hom ≫ normalization B S hS (isAlgebraicSpace_reduction B S hS hX)
          (hasLocallyFiniteIrreducibleComponents_reduction B S hS hX hfin) =
        normalizationToReduction B S hS hX hfin

Tag 0BB4, a lemma

Tag 0BB4 in the Stacks Project.

AlgebraicGeometry.Space.NormalizationData.hasEtaleLocalProperty_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 566. The attribute's comment: “part (1): the normalization is normal”.

The normalization of an algebraic space is normal.

theorem hasEtaleLocalProperty_isNormal (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) :
    HasEtaleLocalProperty B S hS D.space (fun X : Scheme.{u} => IsNormal X)

AlgebraicGeometry.Space.NormalizationData.isSurjective_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 589. The attribute's comment: “part (2): the normalization morphism is surjective”.

The normalization morphism of an algebraic space is surjective.

theorem isSurjective_hom (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) : IsSurjective B S hS D.hom

AlgebraicGeometry.Space.NormalizationData.isIntegralHom_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 618. The attribute's comment: “part (2): the normalization morphism is integral”.

The normalization morphism of an algebraic space is an integral morphism of algebraic spaces.

theorem isIntegralHom_hom (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) : IsIntegralHom B S hS D.hom

AlgebraicGeometry.Space.NormalizationData.bijOn_codimensionZeroPoints_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 629. The attribute's comment: “part (3): bijection on codimension-zero points”.

The normalization morphism induces a bijection between the codimension-zero points of the normalization and those of the algebraic space.

theorem bijOn_codimensionZeroPoints_hom (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) :
    Set.BijOn (pointsMap B S hS D.space D.hom)
      {x : points B S hS D.space | localRingDimension B S hS x = 0}
      {x : points B S hS F | localRingDimension B S hS x = 0}

AlgebraicGeometry.Space.NormalizationData.existsUnique_lift_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 703. The attribute's comment: “part (4): the universal property”. References: SGA 3 X (8.9), “partial”.

A morphism to F from a normal algebraic space which carries points of codimension zero to points of codimension zero factors uniquely through the normalization of F.

theorem existsUnique_lift_hom (D : NormalizationData B S hS F)
    (hF : IsAlgebraicSpace B S hS F) {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hZ : IsAlgebraicSpace B S hS Z)
    (hZnormal : HasEtaleLocalProperty B S hS Z fun Y : Scheme.{u} => IsNormal Y) (f : Z ⟶ F)
    (hgeneric : ∀ z : points B S hS Z, localRingDimension B S hS z = 0 →
      localRingDimension B S hS (pointsMap B S hS Z f z) = 0) :
    ∃! g : Z ⟶ D.space, g ≫ D.hom = f

Tag 0BB5, a lemma

Tag 0BB5 in the Stacks Project.

AlgebraicGeometry.Space.NormalizationData.isFinite_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 955.

The normalization morphism of a Nagata algebraic space over S is a finite morphism of algebraic spaces.

theorem isFinite_hom
    (D : NormalizationData B S hS F) (hF : IsAlgebraicSpace B S hS F)
    (hNagata : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsNagataScheme X)) :
    IsFinite B S hS D.hom

Sources

LeanAlgebraicGeometry.Space.exists_surjective_etale_chart_iff_hasLocallyFiniteIrreducibleComponents · AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_finite_codimensionZeroPoints · AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_finite_irreducibleComponents · AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_iff_of_isRepresentable · AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_of_isLocallyNoetherian · AlgebraicGeometry.mem_genericPoints_of_flat · AlgebraicGeometry.Space.localRingDimension_eq_zero_of_isFlat · AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_and_codimensionZero_of_isFlat_of_isLocallyOfFiniteType

Section67.50 Separated, locally quasi-finite morphisms #

Section 67.50 of the Stacks Project, Tag 0417. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03XW, a lemma

Tag 03XW in the Stacks Project.

AlgebraicGeometry.Space.isOpenSubspace_isQuasiCompactSpace_isRepresentable_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImageRepresentableInduction.lean, line 898.

Stacks 03XW. Let t : T' ⟶ T be an étale morphism of affine objects of the big fppf category over S, let f : X ⟶ yoneda.obj T be a separated and locally quasi-finite morphism of algebraic spaces over S, and let V' be an open subspace of T' ×_T X which is quasi-affine over T'. Then the image of V' in X is a quasi-compact open subspace of X which is representable.

The image is the subspace cut out by the image of the point set of V', whose own point set is that image by Tag 03BZ. Openness and quasi-compactness are AlgebraicGeometry.Space.isOpenSubspace_isQuasiCompactSpace_image_of_isQuasiAffineHom and representability is AlgebraicGeometry.Space.isRepresentable_image_of_isQuasiAffineHom.

theorem isOpenSubspace_isQuasiCompactSpace_isRepresentable_image
    {T' T : BigFppfOver B S hS}
    (hT : IsAffine ((BigFppfOver.toScheme B S hS).obj T))
    (hT' : IsAffine ((BigFppfOver.toScheme B S hS).obj T'))
    {t : T' ⟶ T} (ht : Etale ((BigFppfOver.toScheme B S hS).map t))
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    {f : X ⟶ yoneda.obj T} (hsep : IsSeparated B S hS f)
    (hlqf : IsLocallyQuasiFinite B S hS f)
    (V : Subfunctor (pullback (yoneda.map t) f)) (hV : IsOpenSubspace B S hS V)
    (hVqa : IsQuasiAffineHom B S hS (V.ι ≫ pullback.fst (yoneda.map t) f)) :
    IsOpenSubspace B S hS (openSubspaceOfPoints B S hS X
        (Set.range (pointsMap B S hS V.toFunctor
          (V.ι ≫ pullback.snd (yoneda.map t) f)))) ∧
      IsQuasiCompactSpace B S hS (openSubspaceOfPoints B S hS X
        (Set.range (pointsMap B S hS V.toFunctor
          (V.ι ≫ pullback.snd (yoneda.map t) f)))).toFunctor ∧
      (openSubspaceOfPoints B S hS X
        (Set.range (pointsMap B S hS V.toFunctor
          (V.ι ≫ pullback.snd (yoneda.map t) f)))).toFunctor.IsRepresentable

Tag 03XX, a proposition

Tag 03XX in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_locallyQuasiFinite_separated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteSeparatedRepresentable.lean, line 413.

Stacks 03XX. A separated, locally quasi-finite algebraic space over a representable algebraic space over S is representable.

theorem isRepresentable_of_locallyQuasiFinite_separated
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hT : IsAlgebraicSpace B S hS T)
    (f : X ⟶ T)
    (hTrep : T.IsRepresentable)
    (hlqf : IsLocallyQuasiFinite B S hS f)
    (hsep : IsSeparated B S hS f) :
    X.IsRepresentable

Sources

LeanAlgebraicGeometry.Space.isOpenSubspace_isQuasiCompactSpace_isRepresentable_image · AlgebraicGeometry.Space.isRepresentable_of_locallyQuasiFinite_separated

Section67.51 Applications #

Section 67.51 of the Stacks Project, Tag 05W4. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0418, a lemma

Tag 0418 in the Stacks Project.

AlgebraicGeometry.Space.relativelyRepresentable_of_isLocallyQuasiFinite_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteSeparatedRepresentable.lean, line 465.

Stacks 0418. A separated, locally quasi-finite morphism of algebraic spaces over S is relatively representable along the Yoneda embedding of the big fppf site.

theorem relativelyRepresentable_of_isLocallyQuasiFinite_isSeparated
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyQuasiFinite B S hS f)
    (hs : IsSeparated B S hS f) :
    yoneda.relativelyRepresentable f

Tag 05W5, a lemma

Tag 05W5 in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_isEtale_of_universallyInjective_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/Isomorphism.lean, line 92.

Stacks 05W5. A morphism of algebraic spaces over S which is étale, universally injective and surjective is an isomorphism.

An étale morphism is unramified, so its relative diagonal is an open immersion; together with universal injectivity this makes the morphism a monomorphism. An étale surjection is flat and locally of finite presentation, hence a one-member fppf covering of its target and so surjective as a map of fppf sheaves.

theorem isIso_of_isEtale_of_universallyInjective_of_isSurjective
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (he : IsEtale B S hS f) (hui : UniversallyInjective B S hS f)
    (hsurj : IsSurjective B S hS f) : IsIso f

AlgebraicGeometry.Space.isOpenImmersion_of_isEtale_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleUniversallyInjectiveOpenImmersion.lean, line 47. The attribute's comment: “the open immersion clause”.

An étale universally injective morphism of algebraic spaces over S is an open immersion.

theorem isOpenImmersion_of_isEtale_of_universallyInjective (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (he : IsEtale B S hS f)
    (hui : UniversallyInjective B S hS f) :
    IsOpenImmersion B S hS f

Sources

LeanAlgebraicGeometry.Space.relativelyRepresentable_of_isLocallyQuasiFinite_isSeparated · AlgebraicGeometry.Space.isIso_of_isEtale_of_universallyInjective_of_isSurjective · AlgebraicGeometry.Space.isOpenImmersion_of_isEtale_of_universallyInjective

Section67.52 Zariski's Main Theorem (representable case)#

Section 67.52 of the Stacks Project, Tag 0ABQ. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ABR, a lemma

Tag 0ABR in the Stacks Project.

AlgebraicGeometry.Space.NormalizationInData.isOpenSubspace_quasiFiniteImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationQuasiFiniteLocus.lean, line 481. The attribute's comment: “the open subspace”.

Stacks 0ABR, the open subspace. For a representable morphism of algebraic spaces over S which is of finite type and separated, the image in the normalization of Y in X of the quasi-finite locus of f is an open subspace of that normalization.

Over a surjective étale scheme chart W ⟶ Y the quasi-finite locus base changes to the quasi-finite locus of the induced morphism of schemes (part (2) of Tag 0ABM), and Zariski's main theorem for schemes — Tag 03GW, Mathlib's AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization — says that locus maps by an open immersion into the relative normalization of the chart, which by the chart description of the normalization datum is the base change of ν. So the restriction of f' to the quasi-finite locus is an open immersion after base change along one surjective étale chart of Y', hence an open immersion, by Tag 03M4 for open immersions; its image is therefore an open subspace.

theorem isOpenSubspace_quasiFiniteImage (N : NormalizationInData B S hS f)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hrep : yoneda.relativelyRepresentable f)
    (hft : IsLocallyOfFiniteType B S hS f) (hqc : IsQuasiCompact B S hS f)
    (hsep : IsSeparated B S hS f) :
    IsOpenSubspace B S hS N.quasiFiniteImage

AlgebraicGeometry.Space.NormalizationInData.isIso_fromPreimage_quasiFiniteImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationQuasiFiniteLocus.lean, line 492. The attribute's comment: “part (1): the inverse image of the open subspace maps isomorphically onto it”.

Stacks 0ABR, part (1). The inverse image of the open subspace under f' maps isomorphically onto it.

theorem isIso_fromPreimage_quasiFiniteImage (N : NormalizationInData B S hS f)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hrep : yoneda.relativelyRepresentable f)
    (hft : IsLocallyOfFiniteType B S hS f) (hqc : IsQuasiCompact B S hS f)
    (hsep : IsSeparated B S hS f) :
    IsIso (N.quasiFiniteImage.fromPreimage N.toNorm)

AlgebraicGeometry.Space.NormalizationInData.preimage_quasiFiniteImage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationQuasiFiniteLocus.lean, line 503. The attribute's comment: “part (2): the inverse image is the quasi-finite locus, as a subspace”.

Stacks 0ABR, part (2). The inverse image of the open subspace under f' is the quasi-finite locus of f, as a subspace of X.

theorem preimage_quasiFiniteImage_eq (N : NormalizationInData B S hS f)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hrep : yoneda.relativelyRepresentable f)
    (hft : IsLocallyOfFiniteType B S hS f) (hqc : IsQuasiCompact B S hS f)
    (hsep : IsSeparated B S hS f) :
    N.quasiFiniteImage.preimage N.toNorm = quasiFiniteLocusSubspace B S hS f

AlgebraicGeometry.Space.NormalizationInData.range_pointsMap_preimage_quasiFiniteImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationQuasiFiniteLocus.lean, line 515. The attribute's comment: “part (2): the inverse image is the set of points of quasi-finiteness”.

Stacks 0ABR, part (2), on points. The point set of the inverse image of the open subspace under f' is the set of points of X at which f is quasi-finite. This is the form in which the source states part (2).

theorem range_pointsMap_preimage_quasiFiniteImage (N : NormalizationInData B S hS f)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hrep : yoneda.relativelyRepresentable f)
    (hft : IsLocallyOfFiniteType B S hS f) (hqc : IsQuasiCompact B S hS f)
    (hsep : IsSeparated B S hS f) :
    Set.range (pointsMap B S hS (N.quasiFiniteImage.preimage N.toNorm).toFunctor
        (N.quasiFiniteImage.preimage N.toNorm).ι) =
      {x : points B S hS X | IsQuasiFiniteAt B S hS f x}

AlgebraicGeometry.Space.exists_isOpenSubspace_isIso_fromPreimage_and_range_pointsMap_preimage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationQuasiFiniteLocus.lean, line 536. The attribute's comment: “the existence statement”.

Stacks 0ABR. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is representable, of finite type and separated, and let X ⟶ Y' ⟶ Y be the normalization of Y in X. Then there is an open subspace U' ⊆ Y' such that (f')⁻¹(U') ⟶ U' is an isomorphism and (f')⁻¹(U') ⊆ X is the set of points at which f is quasi-finite.

The open subspace is AlgebraicGeometry.Space.NormalizationInData.quasiFiniteImage, the image of the quasi-finite locus.

theorem exists_isOpenSubspace_isIso_fromPreimage_and_range_pointsMap_preimage_eq
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y} (N : NormalizationInData B S hS f)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hrep : yoneda.relativelyRepresentable f)
    (hft : IsLocallyOfFiniteType B S hS f) (hqc : IsQuasiCompact B S hS f)
    (hsep : IsSeparated B S hS f) :
    ∃ U' : Subfunctor N.space, IsOpenSubspace B S hS U' ∧
      IsIso (U'.fromPreimage N.toNorm) ∧
      Set.range (pointsMap B S hS (U'.preimage N.toNorm).toFunctor
          (U'.preimage N.toNorm).ι) =
        {x : points B S hS X | IsQuasiFiniteAt B S hS f x}

Tag 0ABS, a lemma

Tag 0ABS in the Stacks Project.

AlgebraicGeometry.Space.zariskiMainTheorem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremGeneral.lean, line 211. References: EGA III (4.4.12), “more general”.

Zariski's main theorem for algebraic spaces. Let f : X ⟶ Y be a quasi-finite separated morphism of algebraic spaces over a scheme S. Then f is quasi-affine, and the normalization of Y in X exists: there is a factorization X --f'--> Y' --ν--> Y of f whose base change along every étale scheme chart of Y is the relative normalization of that chart, in which f' is a quasi-compact open immersion and ν is integral.

Neither side is required to be representable and no bound on sizes is assumed: the datum is glued along a surjective étale chart of the target in AlgebraicGeometry.Space.NormalizationGluing.nonempty_normalizationInData, and the four assertions about it are the theorems of StacksFrontier.AlgebraicGeometry.Spaces.ZariskiMainTheoremQuasiFinite.

theorem zariskiMainTheorem (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f) :
    IsQuasiAffineHom B S hS f ∧
      ∃ N : NormalizationInData B S hS f,
        N.toNorm ≫ N.fromNorm = f ∧
        IsOpenImmersion B S hS N.toNorm ∧
        IsQuasiCompact B S hS N.toNorm ∧
        IsIntegralHom B S hS N.fromNorm

Sources

LeanAlgebraicGeometry.Space.NormalizationInData.isOpenSubspace_quasiFiniteImage · AlgebraicGeometry.Space.NormalizationInData.isIso_fromPreimage_quasiFiniteImage · AlgebraicGeometry.Space.NormalizationInData.preimage_quasiFiniteImage_eq · AlgebraicGeometry.Space.NormalizationInData.range_pointsMap_preimage_quasiFiniteImage · AlgebraicGeometry.Space.exists_isOpenSubspace_isIso_fromPreimage_and_range_pointsMap_preimage_eq · AlgebraicGeometry.Space.zariskiMainTheorem

Section67.53 Universal homeomorphisms #

Section 67.53 of the Stacks Project, Tag 05Z3. 7 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05Z4, a lemma

Tag 05Z4 in the Stacks Project.

AlgebraicGeometry.Space.presheaf_universalHomeomorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalHomeomorphismRepresentable.lean, line 320.

A representable morphism of algebraic spaces over S has universal homeomorphy of every one of its represented base changes, which is what being a universal homeomorphism means for a representable morphism, exactly when it is a universal homeomorphism in the sense of Stacks 05Z5: every base change of it by an algebraic space over S induces a homeomorphism on the spaces of points.

theorem presheaf_universalHomeomorphism_iff
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.UniversalHomeomorphism.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f ↔ UniversalHomeomorphism B S hS f

Tag 05Z5, a definition

Tag 05Z5 in the Stacks Project.

AlgebraicGeometry.Space.UniversalHomeomorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 180.

Stacks 05Z5. A morphism of algebraic spaces over S is a universal homeomorphism when its base change along every morphism to its target from an algebraic space over S induces a homeomorphism on the spaces of points.

abbrev UniversalHomeomorphism (f : F ⟶ G) : Prop

Tag 05Z6, an example

Tag 05Z6 in the Stacks Project.

AlgebraicGeometry.AffineLineInvolution.nonSeparatedUniversalHomeomorphism_squaringMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLineInvolutionExample.lean, line 139.

Stacks 05Z6. Let k be a field in which 2 is invertible, let B be a big fppf site containing Spec k, and let X = 𝐀¹_k/\{x ∼ -x ∣ x ≠ 0\} be the quotient of the affine line by the punctured graph of negation. Then X is an algebraic space over k, and of the two morphisms 𝐀¹_k ⟶ X ⟶ 𝐀¹_k, the projection onto the quotient and the morphism descended from squaring the coordinate:

the first is surjective and étale;

the second is universally injective;

their composition is the map x ↦ x²;

hence that composition is universally closed;

therefore the second morphism is a universal homeomorphism;

but the second morphism is not separated.

The projection is surjective and étale because the relation is an étale equivalence relation whose morphism into the self-product of the affine line is affine, which makes the presentation of Stacks 0265 unconditional here. Squaring is injective on field-valued points up to the relation and integral on the affine line, which gives (2) and (4); a universally injective, universally closed and surjective morphism of algebraic spaces is a universal homeomorphism, which gives (5). For (6) the relation is a represented base change of the relative diagonal of the squaring map and is not a closed immersion, its restriction to the punctured summand factoring through the split section of the fibre square with components the identity and negation.

theorem nonSeparatedUniversalHomeomorphism_squaringMap (hchar : (2 : k) ≠ 0) :
    IsAlgebraicSpace B (Spec (.of k)) hk (involutionQuotient k B hk).obj ∧
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B (Spec (.of k)) hk)).presheaf
          (Stacks.Groupoids.toQuotientSheaf (BigFppfOver.topology B (Spec (.of k)) hk)
            (Over.post (X := B.obj hk) B.inclusion) (involutionRelation k)) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B (Spec (.of k)) hk)).presheaf
          (Stacks.Groupoids.toQuotientSheaf (BigFppfOver.topology B (Spec (.of k)) hk)
            (Over.post (X := B.obj hk) B.inclusion) (involutionRelation k)) ∧
      Space.UniversallyInjective B (Spec (.of k)) hk (squaringMap k B hk) ∧
      Stacks.Groupoids.toQuotientSheaf (BigFppfOver.topology B (Spec (.of k)) hk)
            (Over.post (X := B.obj hk) B.inclusion) (involutionRelation k) ≫
          squaringMap k B hk =
        (Over.post (X := B.obj hk) B.inclusion).op.whiskerLeft
          (yoneda.map (affineLineSquare k)) ∧
      Space.UniversallyClosed B (Spec (.of k)) hk
          (Stacks.Groupoids.toQuotientSheaf (BigFppfOver.topology B (Spec (.of k)) hk)
              (Over.post (X := B.obj hk) B.inclusion) (involutionRelation k) ≫
            squaringMap k B hk) ∧
      Space.UniversalHomeomorphism B (Spec (.of k)) hk (squaringMap k B hk) ∧
      ¬ Space.IsSeparated B (Spec (.of k)) hk (squaringMap k B hk)

AlgebraicGeometry.Space.universallyClosed_toQuotientSheaf_comp_squaringMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 671. The attribute's comment: “closed_squaring”.

Stacks 05Z6. The composite of the projection onto the quotient of the affine line by the punctured involution relation with the descended squaring map of Stacks 05VS is universally closed.

The composite is, through AlgebraicGeometry.Space.toQuotientSheaf_comp_squaringMap_eq_conj, the morphism of represented presheaves induced by squaring of the coordinate. Squaring is an integral morphism of schemes, hence a universally closed one, so the induced morphism of presheaves is universally closed after every represented base change, and Stacks 03XD turns that into universal closedness in the sense of Stacks 03HI. No assumption on the characteristic is needed.

theorem universallyClosed_toQuotientSheaf_comp_squaringMap (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    UniversallyClosed B (Spec (.of k)) hk
      (Stacks.Groupoids.toQuotientSheaf (BigFppfOver.topology B (Spec (.of k)) hk)
          (Over.post (X := B.obj hk) B.inclusion) (involutionRelation k) ≫
        squaringMap k B hk)

AlgebraicGeometry.Space.universalHomeomorphism_squaringMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 772. The attribute's comment: “universal_homeomorphism: the map X ⟶ 𝐀¹_k is a universal homeomorphism”.

Stacks 05ZI, the last sentence: there is a universal homeomorphism X ⟶ 𝐀¹_k, exhibited directly by t ↦ t ^ 2 on affine space.

Here X is the quotient of the affine line by the relation identifying t with -t away from the origin, the algebraic space of Stacks 05Z6, and the morphism is the one Stacks 05VS descends from squaring the coordinate. It is universally closed by AlgebraicGeometry.Space.universallyClosed_squaringMap, universally injective by Stacks 05VS part (4), and surjective after every base change by AlgebraicGeometry.Space.isSurjective_pullback_fst_squaringMap; the criterion is AlgebraicGeometry.Space.universalHomeomorphism_of_universallyClosed_of_universallyInjective.

Stacks 05Z6 and Stacks 05ZI state this over an algebraically closed field of characteristic zero. Only 2 ≠ 0 in k is used, and only for universal injectivity.

theorem universalHomeomorphism_squaringMap (hchar : (2 : k) ≠ 0)
    (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    UniversalHomeomorphism B (Spec (.of k)) hk (squaringMap k B hk)

Tag 0CFT, a lemma

Tag 0CFT in the Stacks Project.

AlgebraicGeometry.Space.universalHomeomorphism_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 238.

Stacks 0CFT. A base change of a universal homeomorphism of algebraic spaces over S is a universal homeomorphism.

Nothing is needed beyond unwinding the definition: a base change of Z ×_Y X ⟶ Z along k : W ⟶ Z is a base change of X ⟶ Y along k ≫ g.

theorem universalHomeomorphism_pullback (f : X ⟶ Y) (g : Z ⟶ Y)
    (hf : UniversalHomeomorphism B S hS f) :
    UniversalHomeomorphism B S hS (pullback.fst g f)

AlgebraicGeometry.Space.universalHomeomorphism_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 294.

Stacks 0CFT for an arbitrary cartesian square: if IsPullback a b g f and f is a universal homeomorphism, then so is a.

This is AlgebraicGeometry.Space.universalHomeomorphism_pullback composed with the identification of the given square with the canonical fibre product.

theorem universalHomeomorphism_of_isPullback (hC : IsAlgebraicSpace B S hS C)
    (hZ : IsAlgebraicSpace B S hS Z) (hT : IsAlgebraicSpace B S hS T) (f : C ⟶ T) (g : Z ⟶ T)
    (hf : UniversalHomeomorphism B S hS f) {a : A ⟶ Z} {b : A ⟶ C}
    (hpb : IsPullback a b g f) : UniversalHomeomorphism B S hS a

Tag 0CFU, a lemma

Tag 0CFU in the Stacks Project.

AlgebraicGeometry.Space.universalHomeomorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 268.

Stacks 0CFU. A composition of universal homeomorphisms of algebraic spaces over S is a universal homeomorphism.

The base change W ×_Z X ⟶ W of the composite along k : W ⟶ Z is identified by the pasting isomorphism W ×_Z X ≅ (W ×_Z Y) ×_Y X with the composition of a base change of X ⟶ Y and a base change of Y ⟶ Z.

theorem universalHomeomorphism_comp (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : UniversalHomeomorphism B S hS f) (hg : UniversalHomeomorphism B S hS g) :
    UniversalHomeomorphism B S hS (f ≫ g)

Tag 08AK, a lemma

Tag 08AK in the Stacks Project.

AlgebraicGeometry.Space.universalHomeomorphism_ι_reducedClosedSubspace_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Reduction.lean, line 264. References: EGA IV (2.4.8), “(ii) univ. homeo”.

Stacks 08AK. The canonical morphism from the reduction of an algebraic space over S — the reduced closed subspace supported on all of its points — to the space itself is a universal homeomorphism.

The four clauses are independent of one another: continuity is clause (2) of Stacks 03BX, injectivity is Stacks 06RV applied to the base change of a subfunctor inclusion, surjectivity is Stacks 03H4 together with the computation of the point set of the reduction, and openness is AlgebraicGeometry.Space.universallyOpen_ι_reducedClosedSubspace_univ. None of them needs the inclusion to be representable, so no effective descent hypothesis appears.

theorem universalHomeomorphism_ι_reducedClosedSubspace_univ (hX : IsAlgebraicSpace B S hS X) :
    UniversalHomeomorphism B S hS
      (reducedClosedSubspace B S hS X hX Set.univ isClosed_univ).ι

Tag 0AEH, a lemma

Tag 0AEH in the Stacks Project.

AlgebraicGeometry.Space.supportOfSheaf_subset_of_essImage_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralPushforwardSupport.lean, line 172. The attribute's comment: “part (2), the inclusion only: a sheaf in the essential image of f_{small,*} is supported on f(|Y|), for an integral morphism and with no universal injectivity needed. The converse inclusion, and with it the full iff of part (2), is AlgebraicGeometry.Space.smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective; part (1) is ...smallEtalePushforward_essImage_iff_of_integral_universallyInjective. Both are proved at the source's own hypotheses”.

Stacks 0AEH, part (2), one inclusion of the essential image. An abelian sheaf on the small étale site of X isomorphic to a small étale direct image along an integral morphism f : Y ⟶ X of algebraic spaces over S is supported on the image of the point set of Y.

An isomorphism of abelian sheaves is locally surjective, so by part (5) of Stacks 04KB it does not enlarge the support, and the support of the direct image is bounded by AlgebraicGeometry.Space.supportOfSheaf_smallEtaleAbelianPushforward_subset_of_isIntegralHom.

Universal injectivity of f, which Stacks 0AEH also assumes, is not used: this inclusion holds for every integral morphism. It is one inclusion of the clause and carries no tag; the clause itself is AlgebraicGeometry.Space.smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective.

theorem supportOfSheaf_subset_of_essImage_of_isIntegralHom (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (F : abelianSheaves.{w} B S hS X)
    (hF : (smallEtaleAbelianPushforward B S hS f
      ((isIntegralHom_iff_representable B S hS f.hom Y.property X.property).mp hf).1).essImage
        F) :
    supportOfSheaf B S hS X.1 F ⊆ Set.range (pointsMap B S hS Y.1 f.hom)

AlgebraicGeometry.Space.smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveEssentialImage.lean, line 354. The attribute's comment: “part (2): the essential image, for an integral and universally injective morphism of algebraic spaces”.

Stacks 0AEH, part (2), the essential image. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S, an abelian sheaf on the small étale site of X lies in the essential image of the direct image along f exactly when its support is contained in the image of the point set of Y.

The forward inclusion is AlgebraicGeometry.Space.supportOfSheaf_subset_of_essImage_of_isIntegralHom, resting on Étale Cohomology 04FX for algebraic spaces, and the converse is AlgebraicGeometry.Space.isIso_unit_app_of_supportOfSheaf_subset_of_isIntegralHom together with the characterization of the essential image of a fully faithful right adjoint by invertibility of the unit.

theorem smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom)
    (F : Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1}) :
    (smallEtaleAbelianPushforward.{u + 1} B S hS f
        (relativelyRepresentable_of_isIntegralHom B S hS f hf)).essImage F ↔
      supportOfSheaf B S hS X.1 F ⊆ Set.range (pointsMap B S hS Y.1 f.hom)

AlgebraicGeometry.Space.smallEtalePushforward_essImage_iff_of_integral_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSetEssentialImage.lean, line 362. The attribute's comment: “part (1): the essential image, for an integral and universally injective morphism of algebraic spaces”.

Stacks 0AEH, part (1), the essential image. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S, a sheaf of sets on the small étale site of X lies in the essential image of the direct image along f exactly when its restriction to the open complement of the image of the point set of Y is the singleton sheaf.

One direction is Étale Cohomology 04FX for sheaves of sets, AlgebraicGeometry.Space.isTerminal_inverseImage_pushforward_integralComplement. For the other, the direct image is fully faithful, so membership of the essential image is invertibility of the unit F ⟶ f_*f^{-1}F; the unit becomes invertible under f^{-1} by the triangle identity and under restriction to the complement because both sides are then the singleton sheaf, and a map of sheaves of sets invertible on both is invertible, every geometric point of X lying either on the image of f or on its complement.

theorem smallEtalePushforward_essImage_iff_of_integral_universallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom)
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1))) :
    (smallToposMorphism B S hS f).pushforward.essImage F ↔
      Nonempty (IsTerminal ((smallToposMorphism B S hS
        (integralComplementHom B S hS f hf)).inverseImage.obj F))

AlgebraicGeometry.Space.fullyFaithfulSmallEtaleSetPushforwardOfIntegralUniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 130. The attribute's comment: “part (1): full faithfulness of the direct image on sheaves of sets”.

Stacks 0AEH, part (1), full faithfulness. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S, the direct image of sheaves of sets along f — restriction along the chart base-change morphism of small étale sites of Stacks 03G2, part (4) — is fully faithful, at any coefficient universe.

def fullyFaithfulSmallEtaleSetPushforwardOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).toIsContinuous
    ((smallBaseChange B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafPushforwardContinuous
        (Type w) (SmallEtale.topology B S hS X.1)
        (SmallEtale.topology B S hS Y.1)).FullyFaithful

AlgebraicGeometry.Space.fullyFaithfulSmallEtalePushforwardOfIntegralUniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 148. The attribute's comment: “part (1): the direct image of the morphism of small étale topoi is fully faithful”.

Stacks 0AEH, part (1), full faithfulness, through the morphism of small étale topoi. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S, the direct image of sheaves of sets along the morphism of small étale topoi of Stacks 03G2, part (3) is fully faithful.

By Stacks 03G8 that direct image is restriction along chart base change, so this is the previous statement read through an identification and not a new proof.

def fullyFaithfulSmallEtalePushforwardOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom) :
    (smallToposMorphismTypeU B S hS f).pushforward.FullyFaithful

AlgebraicGeometry.Space.smallEtaleAdjunctionCounitIsIsoOfIntegralUniversallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 166. The attribute's comment: “trailing clause for sheaves of sets: the inverse image is a left inverse”.

Stacks 0AEH, the trailing clause, for sheaves of sets. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S the counit f^{-1}f_*\mathcal{G} ⟶ \mathcal{G} of the inverse-image/direct-image adjunction on sheaves of sets is an isomorphism: the inverse image is a left inverse of the direct image.

The counit of an adjunction is an isomorphism exactly when the right adjoint is fully faithful.

theorem smallEtaleAdjunctionCounitIsIsoOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom)
    (G : Sheaf (SmallEtale.topology B S hS Y.1) (Type (max (u + 1) v))) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).toIsContinuous
    IsIso (((smallBaseChange B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafAdjunctionContinuous
        (Type (max (u + 1) v)) (SmallEtale.topology B S hS X.1)
        (SmallEtale.topology B S hS Y.1)).counit.app G)

AlgebraicGeometry.Space.smallEtalePullbackPushforwardCounitIsoOfIntegralUniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 185. The attribute's comment: “trailing clause for sheaves of sets, as a natural isomorphism f_* f^{-1} ≅ 1”.

Stacks 0AEH, the trailing clause, for sheaves of sets, as a natural isomorphism. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S the counit of the adjunction of the morphism of small étale topoi of Stacks 03G2, part (3) is a natural isomorphism f_* ⋙ f^{-1} ≅ 𝟭.

def smallEtalePullbackPushforwardCounitIsoOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom) :
    (smallToposMorphismTypeU B S hS f).pushforward ⋙
        (smallToposMorphismTypeU B S hS f).inverseImage ≅
      𝟭 (Sheaf (SmallEtale.topology B S hS Y.1) (Type u))

AlgebraicGeometry.Space.fullyFaithfulSmallEtaleAbelianPushforwardOfIntegralUniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 207. The attribute's comment: “part (2): full faithfulness of the direct image on abelian sheaves”.

Stacks 0AEH, part (2), full faithfulness. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S, the direct image of sheaves of abelian groups along f is fully faithful.

Full faithfulness of restriction along a cover-dense, locally full, continuous functor does not depend on the category of coefficients, so this is AlgebraicGeometry.Space.fullyFaithfulSmallEtaleRestrictionOfIntegralUniversallyInjective at the category of abelian groups.

def fullyFaithfulSmallEtaleAbelianPushforwardOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).toIsContinuous
    ((smallBaseChange B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafPushforwardContinuous
        AddCommGrpCat.{w} (SmallEtale.topology B S hS X.1)
        (SmallEtale.topology B S hS Y.1)).FullyFaithful

AlgebraicGeometry.Space.smallEtalePushforwardAbIsRightAdjointOfIntegralUniversallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 224. The attribute's comment: “part (2): the direct image of abelian sheaves has the inverse image as left adjoint”.

Stacks 0AEH, part (2), existence of the inverse image. For an integral morphism f : Y ⟶ X of algebraic spaces over a scheme S, the direct image of abelian sheaves along f is a right adjoint, so that the inverse image of part (2) exists.

Universal injectivity is not used: representability is all this needs.

theorem smallEtalePushforwardAbIsRightAdjointOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).toIsContinuous
    Nonempty (((smallBaseChange B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafPushforwardContinuous
        AddCommGrpCat.{max (u + 1) v} (SmallEtale.topology B S hS X.1)
        (SmallEtale.topology B S hS Y.1)).IsRightAdjoint)

AlgebraicGeometry.Space.smallEtaleAdjunctionCounitIsIsoAbelianOfIntegralUniversallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 244. The attribute's comment: “trailing clause for abelian sheaves: the inverse image is a left inverse”.

Stacks 0AEH, the trailing clause, for abelian sheaves. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S the counit of the inverse-image/direct-image adjunction on abelian sheaves is an isomorphism: the inverse image is a left inverse of the direct image.

The adjunction is the one whose existence is AlgebraicGeometry.Space.smallEtalePushforwardAbIsRightAdjointOfIntegralUniversallyInjective, as in the source, where part (2) presupposes it.

theorem smallEtaleAdjunctionCounitIsIsoAbelianOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom)
    (G : Sheaf (SmallEtale.topology B S hS Y.1) AddCommGrpCat.{max (u + 1) v}) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).toIsContinuous
    letI := Classical.choice (smallEtalePushforwardAb_isRightAdjoint.{v} B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf))
    IsIso (((smallBaseChange B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafAdjunctionContinuous
        AddCommGrpCat.{max (u + 1) v} (SmallEtale.topology B S hS X.1)
        (SmallEtale.topology B S hS Y.1)).counit.app G)

AlgebraicGeometry.Space.smallEtaleAbelianPullbackPushforwardCounitIsoOfIntegralUniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyInjectiveSmallEtale.lean, line 265. The attribute's comment: “trailing clause for abelian sheaves, as a natural isomorphism f_* f^{-1} ≅ 1”.

Stacks 0AEH, the trailing clause, for abelian sheaves, as a natural isomorphism. For an integral and universally injective morphism f : Y ⟶ X of algebraic spaces over a scheme S the counit of the adjunction of CategoryTheory.Functor.sheafAdjunctionContinuous for chart base change is a natural isomorphism f_* ⋙ f^{-1} ≅ 𝟭.

def smallEtaleAbelianPullbackPushforwardCounitIsoOfIntegralUniversallyInjective (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf)).toIsContinuous
    letI := Classical.choice (smallEtalePushforwardAb_isRightAdjoint.{v} B S hS f
      (relativelyRepresentable_of_isIntegralHom B S hS f hf))
    (smallBaseChange B S hS f
        (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafPushforwardContinuous
          AddCommGrpCat.{max (u + 1) v} (SmallEtale.topology B S hS X.1)
          (SmallEtale.topology B S hS Y.1) ⋙
      (smallBaseChange B S hS f
        (relativelyRepresentable_of_isIntegralHom B S hS f hf)).sheafPullback
          AddCommGrpCat.{max (u + 1) v} (SmallEtale.topology B S hS X.1)
          (SmallEtale.topology B S hS Y.1) ≅
      𝟭 (Sheaf (SmallEtale.topology B S hS Y.1) AddCommGrpCat.{max (u + 1) v})

Sources

LeanAlgebraicGeometry.Space.presheaf_universalHomeomorphism_iff · AlgebraicGeometry.Space.UniversalHomeomorphism · AlgebraicGeometry.AffineLineInvolution.nonSeparatedUniversalHomeomorphism_squaringMap · AlgebraicGeometry.Space.universallyClosed_toQuotientSheaf_comp_squaringMap · AlgebraicGeometry.Space.universalHomeomorphism_squaringMap · AlgebraicGeometry.Space.universalHomeomorphism_pullback · AlgebraicGeometry.Space.universalHomeomorphism_of_isPullback · AlgebraicGeometry.Space.universalHomeomorphism_comp

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

67.49 Normalization to 67.53 Universal homeomorphisms

Section67.49 Normalization#

Tag 0BB1, a lemma

Tag 0GMB, a lemma

Tag 0GMC, a lemma

Tag 0GMD, a lemma

Tag 07U4, a lemma

Tag 0BB2, a definition

Tag 0BB3, a lemma

Tag 0BB4, a lemma

Tag 0BB5, a lemma

Sources

Section67.50 Separated, locally quasi-finite morphisms#

Tag 03XW, a lemma

Tag 03XX, a proposition

Sources

Section67.51 Applications#

Tag 0418, a lemma

Tag 05W5, a lemma

Sources

Section67.52 Zariski's Main Theorem (representable case)#

Tag 0ABR, a lemma

Tag 0ABS, a lemma

Sources

Section67.53 Universal homeomorphisms#

Tag 05Z4, a lemma

Tag 05Z5, a definition

Tag 05Z6, an example

Tag 0CFT, a lemma

Tag 0CFU, a lemma

Tag 08AK, a lemma

Tag 0AEH, a lemma

Sources

Section67.49 Normalization #

Section67.50 Separated, locally quasi-finite morphisms #

Section67.51 Applications #

Section67.53 Universal homeomorphisms #