38.19 How purity is used to 38.33 Nagata compactification

Section38.19 How purity is used#

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

Tag 05L8, a lemma

Tag 05L8 in the Stacks Project.

AlgebraicGeometry.forall_injective_stalkLinearMap_associatedPoints_iff_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/InjectivityOnClosedFibre.lean, line 155. The attribute's comment: “the equivalence, both directions; S local with closed point s is rendered by the hypothesis that every point of S specializes to s, which is what a local base supplies”.

Stacks Project, Tag 05L8. Let f : X ⟶ S be a morphism of finite type, let ℱ be a quasi-coherent 𝒪_X-module of finite type, and let s be a point of S to which every point of S specializes — for instance the closed point of a local base. Assume ℱ is pure along the fibre X_s and flat over S. Then a map φ : ℱ ⟶ 𝒢 of quasi-coherent 𝒪_X-modules is injective if and only if the stalk map φ_x is injective at every point x of X_s associated to the restriction ℱ_s.

One direction is immediate: the stalk maps of a monomorphism are injective at every point. For the other, the kernel of φ has no weakly associated point — such a point would lie in Ass_{X/S}(ℱ) by flatness, would specialize into X_s by purity, and the hypothesis at the associated point of ℱ_s it specializes to by Tag 05L3 would put that point outside the support of the kernel, which is stable under specialization.

theorem forall_injective_stalkLinearMap_associatedPoints_iff_mono
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    (F G : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] [G.IsQuasicoherent]
    (s : S) (hclosed : ∀ t : S, t ⤳ s)
    (hpure : IsPureAlong ({ S := S, X := X, f := f, F := F, s := s } : PrePureSituation.{u}))
    (hflat : IsFlatOver f.toLRSHom.toShHom F) (φ : F ⟶ G) :
    (∀ x : f.fiber s,
        x ∈ Stacks.Divisors.associatedPoints ((Scheme.Modules.pullback (f.fiberι s)).obj F) →
          Function.Injective (stalkLinearMap F G φ (f.fiberι s x))) ↔ Mono φ

Tag 05MD, a proposition

Tag 05MD in the Stacks Project.

AlgebraicGeometry.isLocallyProjective_pushforward_iff_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/ProjectivePushforwardConverse.lean, line 156. The attribute's comment: “the scheme criterion, as a biconditional”. References: SGA 3 VIB (6.9), “more general”.

Stacks Project, Tag 05MD, the scheme form. For an affine morphism of finite presentation and a quasi-coherent module of finite presentation which is flat over the base, the direct image is locally projective exactly when the module is pure relative to the base.

The implication from local projectivity to purity is AlgebraicGeometry.isPureRelative_of_isLocallyProjective_pushforward, which needs neither flatness nor finite presentation; the converse is AlgebraicGeometry.isLocallyProjective_pushforward_of_isPureRelative.

theorem isLocallyProjective_pushforward_iff_isPureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [IsAffineHom f] [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation]
    (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    letI : F.IsFiniteType := SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F
    Scheme.Modules.IsLocallyProjective ((Scheme.Modules.pushforward f).obj F) ↔
      IsPureRelative f F

AlgebraicGeometry.projective_iff_isPureRelative_tilde, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/ProjectivePushforwardConverse.lean, line 177. The attribute's comment: “the affine ring specialization, as a biconditional”.

Stacks Project, Tag 05MD, the ring form. Let A → B be of finite presentation and let N be a finitely presented B-module which is flat over A. Then N is projective over A exactly when the sheaf Ñ on Spec B is pure relative to Spec A.

Both directions come from the scheme form applied to Spec B ⟶ Spec A: the direct image of Ñ is the sheaf associated to N viewed as an A-module (Tag 01I9, AlgebraicGeometry.pushforwardTildeIso), so local projectivity of the direct image is projectivity of that A-module by Tag 05JQ (AlgebraicGeometry.isLocallyProjective_tilde_iff_projective).

theorem projective_iff_isPureRelative_tilde (A B N : Type u) [CommRing A] [CommRing B]
    [Algebra A B] [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Algebra.FinitePresentation A B] [Module.FinitePresentation B N] [Module.Flat A N] :
    Module.Projective A N ↔
      IsPureRelative (Spec.map (CommRingCat.ofHom (algebraMap A B)))
        (tilde (ModuleCat.of (CommRingCat.of B) N))

AlgebraicGeometry.isPureRelative_of_isLocallyProjective_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/ProjectivePushforwardCriterion.lean, line 63. The attribute's comment: “the implication from local projectivity of the direct image to relative purity, in the scheme form”. References: SGA 3 VIB (6.9), “6.9 a)”.

Stacks Project, Tag 05MD, the implication from (1) to (2). For an affine morphism of finite type, a finite type quasi-coherent module whose direct image is locally projective on the base is pure relative to the base.

This implication of Tag 05MD assumes neither flatness over the base nor finite presentation, which the statement of that tag assumes for the converse: it is Tag 05K6, whose conclusion is universal purity relative to the base, followed by the fact that universal purity along a fibre is purity along it with the étale and elementary hypotheses on the base change dropped.

theorem isPureRelative_of_isLocallyProjective_pushforward
    {X S : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f] [LocallyOfFiniteType f] [QuasiCompact f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (hF : Scheme.Modules.IsLocallyProjective ((Scheme.Modules.pushforward f).obj F)) :
    IsPureRelative f F

AlgebraicGeometry.isPureRelative_tilde_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/ProjectivePushforwardCriterion.lean, line 90. The attribute's comment: “the implication from projectivity to relative purity, in the ring form of the final assertion”.

Stacks Project, Tag 05MD, the ring specialization of the implication from (1) to (2). Let A → B be a ring map of finite presentation and let N be a finitely presented B-module. If N is projective as an A-module, then the sheaf Ñ on Spec B is pure relative to Spec A.

As in the scheme form, flatness of N over A — which the statement of Tag 05MD assumes for the converse — is not needed for this implication. The direct image of Ñ along Spec B ⟶ Spec A is the sheaf associated to N viewed as an A-module, by Tag 01I9, so local projectivity of the direct image is projectivity of that A-module by Tag 05JQ.

theorem isPureRelative_tilde_of_projective
    (A B N : Type u) [CommRing A] [CommRing B] [Algebra A B]
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Algebra.FinitePresentation A B] [Module.FinitePresentation B N]
    (hproj : Module.Projective A N) :
    IsPureRelative (Spec.map (CommRingCat.ofHom (algebraMap A B)))
      (tilde (ModuleCat.of (CommRingCat.of B) N))

Tag 05ME, a lemma

Tag 05ME in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_projective_sections_of_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/ProjectiveSectionsAffineOpen05ME.lean, line 864.

Stacks Project, Tag 05ME. Let f : X ⟶ S be locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation, and let x ∈ X lie over s ∈ S with F flat over S at x. Then there are an affine elementary étale neighbourhood (S', s') ⟶ (S, s) and an affine open U' ⊆ X ×_S S' containing x' = (x, s') such that Γ(U', F|_{U'}) is a projective Γ(S', 𝒪_{S'})-module.

The chart whose name this declaration carries is the one of Tag 05KW, built inside AlgebraicGeometry.exists_openImmersion_projective_sections_of_affine after X has been shrunk twice: by openness of the flat locus, Tag 0399 (AlgebraicGeometry.isOpen_setOf_flatOverAt), and by finiteness of the associated points of the fibre, Tag 05AF (AlgebraicGeometry.associatedPoints_inter_finite), which removes the ones not generalizing x. The affine open produced over the shrunken X is transported to X ×_S S' along the resulting open immersion.

theorem exists_affineOpen_projective_sections_of_chart
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation]
    (s : S) (x : X) (hxs : f x = s) (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (N : EtaleNeighborhood S s) (_ : N.IsElementary) (_ : IsAffine N.scheme)
      (x' : (pullback f N.toBase : Scheme.{u}))
      (_ : pullback.fst f N.toBase x' = x)
      (_ : pullback.snd f N.toBase x' = N.point)
      (U' : (pullback f N.toBase : Scheme.{u}).Opens)
      (_ : IsAffineOpen U') (_ : x' ∈ U'),
      let G := (Scheme.Modules.pullback (pullback.fst f N.toBase)).obj F
      letI : Module Γ(N.scheme, ⊤) Γ(G, U') :=
        Module.compHom Γ(G, U') ((pullback.snd f N.toBase).appLE ⊤ U' (by simp)).hom
      Module.Projective Γ(N.scheme, ⊤) Γ(G, U')

Tag 05MF, a lemma

Tag 05MF in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSections05MF.lean, line 153. The attribute's comment: “RESTRICTED: carries hproj, this same existential with Module.Projective in place of Module.Free and the clause on the image of x' in Spec 𝒪_{S', s'} dropped, which is the 05ME half of the source's proof (Lemma 05ME composed with Proposition 05I5)”.

Stacks Project, Tag 05MF. A finite-type quasi-coherent module which is flat over the base at a point has free sections on an affine neighbourhood of the lifted point after base change to the local scheme of an affine elementary étale neighbourhood.

The obligation hproj is Lemma 05ME composed with Proposition 05I5: the same existential with Module.Projective in place of Module.Free, and with nothing asserted about the image of x' in Spec 𝒪_{S', s'}. Projectivity becomes freeness by Kaplansky's theorem (Tag 0593), and the image of x' is the distinguished point automatically, by AlgebraicGeometry.EtaleNeighborhood.fromSpecStalk_snd_eq_point.

theorem exists_elementaryEtaleNeighborhood_free_sections
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (x : X)
    (hflat : IsFlatOverAt f.toLRSHom.toShHom F x)
    (hproj : IsFlatOverAt f.toLRSHom.toShHom F x →
      ∃ (N : EtaleNeighborhood S (f x)),
        N.IsElementary ∧ IsAffine N.scheme ∧
          let g := N.scheme.fromSpecStalk N.point ≫ N.toBase
          let P := pullback f g
          ∃ (x' : P) (W : P.Opens),
            pullback.fst f g x' = x ∧
              IsAffineOpen W ∧ x' ∈ W ∧
                let F' := (Scheme.Modules.pullback (pullback.fst f g)).obj F
                letI : Module (N.scheme.presheaf.stalk N.point) Γ(F', W) :=
                  Module.compHom Γ(F', W)
                    (((Scheme.ΓSpecIso (.of (N.scheme.presheaf.stalk N.point))).inv ≫
                      (pullback.snd f g).appLE ⊤ W (by simp)).hom)
                Module.Projective (N.scheme.presheaf.stalk N.point) Γ(F', W)) :
    ∃ (N : EtaleNeighborhood S (f x)),
      N.IsElementary ∧ IsAffine N.scheme ∧
        let g := N.scheme.fromSpecStalk N.point ≫ N.toBase
        let P := pullback f g
        ∃ (x' : P) (W : P.Opens),
          pullback.fst f g x' = x ∧
            N.scheme.fromSpecStalk N.point (pullback.snd f g x') = N.point ∧
            IsAffineOpen W ∧ x' ∈ W ∧
              let F' := (Scheme.Modules.pullback (pullback.fst f g)).obj F
              letI : Module (N.scheme.presheaf.stalk N.point) Γ(F', W) :=
                Module.compHom Γ(F', W)
                  (((Scheme.ΓSpecIso (.of (N.scheme.presheaf.stalk N.point))).inv ≫
                    (pullback.snd f g).appLE ⊤ W (by simp)).hom)
              Module.Free (N.scheme.presheaf.stalk N.point) Γ(F', W)

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSections05MF.lean, line 243. The attribute's comment: “for f locally of finite presentation and F of finite presentation”.

Stacks Project, Tag 05MF for a morphism locally of finite presentation and a module of finite presentation, with no hypothesis beyond flatness at the point.

Under those hypotheses the obligation hproj of AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections is Lemma 05ME base changed to the local scheme of the neighbourhood it produces, which is AlgebraicGeometry.exists_affineOpen_projective_sections_stalk. The source states Tag 05MF for f locally of finite type and F of finite type, and reaches the hypotheses used here by a closed immersion into affine space and by Proposition 05I5; those two reductions are what the general statement still waits on.

theorem exists_elementaryEtaleNeighborhood_free_sections_of_finitePresentation
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation] (x : X)
    (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (N : EtaleNeighborhood S (f x)),
      N.IsElementary ∧ IsAffine N.scheme ∧
        let g := N.scheme.fromSpecStalk N.point ≫ N.toBase
        let P := pullback f g
        ∃ (x' : P) (W : P.Opens),
          pullback.fst f g x' = x ∧
            N.scheme.fromSpecStalk N.point (pullback.snd f g x') = N.point ∧
            IsAffineOpen W ∧ x' ∈ W ∧
              let F' := (Scheme.Modules.pullback (pullback.fst f g)).obj F
              letI : Module (N.scheme.presheaf.stalk N.point) Γ(F', W) :=
                Module.compHom Γ(F', W)
                  (((Scheme.ΓSpecIso (.of (N.scheme.presheaf.stalk N.point))).inv ≫
                    (pullback.snd f g).appLE ⊤ W (by simp)).hom)
              Module.Free (N.scheme.presheaf.stalk N.point) Γ(F', W)

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSectionsFiniteType05MF.lean, line 890.

Stacks Project, Tag 05MF. A finite-type quasi-coherent module which is flat over the base at a point has free sections on an affine neighbourhood of the lifted point after base change to the local scheme of an affine elementary étale neighbourhood.

public theorem exists_elementaryEtaleNeighborhood_free_sections_of_finiteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (x : X)
    (hflat : AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (N : AlgebraicGeometry.EtaleNeighborhood S (f x)),
      N.IsElementary ∧ IsAffine N.scheme ∧
        let g := N.scheme.fromSpecStalk N.point ≫ N.toBase
        let P := pullback f g
        ∃ (x' : P) (W : P.Opens),
          pullback.fst f g x' = x ∧
            N.scheme.fromSpecStalk N.point (pullback.snd f g x') = N.point ∧
            IsAffineOpen W ∧ x' ∈ W ∧
              let F' := (Scheme.Modules.pullback (pullback.fst f g)).obj F
              letI : Module (N.scheme.presheaf.stalk N.point) Γ(F', W) :=
                Module.compHom Γ(F', W)
                  (((Scheme.ΓSpecIso (.of (N.scheme.presheaf.stalk N.point))).inv ≫
                    (pullback.snd f g).appLE ⊤ W (by simp)).hom)
              Module.Free (N.scheme.presheaf.stalk N.point) Γ(F', W)

Tag 05U7, a lemma

Tag 05U7 in the Stacks Project.

exists_filteredColimit_free_with_injective_reduction_and_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianEssFiniteTypeColimit.lean, line 165.

Stacks Project, Tag 05U7. Let A → B be a local homomorphism of local rings which is essentially of finite type, and let N be a finite B-module which is flat as an A-module. If A is henselian, then N is a filtered colimit N = colim_i F_i of free A-modules F_i such that every transition map F_i → F_{i'} of the system induces an injective map F_i/𝔪_A F_i → F_{i'}/𝔪_A F_{i'}. Also, N is a Mittag-Leffler A-module.

The colimit is computed in ModuleCat A, in the joint universe of A and N, so its vertex is compared with the universe lift of N; F_i/𝔪_A F_i is F_i ⧸ 𝔪_A • ⊤ and the induced map is Submodule.mapQ. The Mittag-Leffler condition is that of Stacks 059F, with the finitely presented source and the test module in arbitrary universes.

theorem exists_filteredColimit_free_with_injective_reduction_and_isMittagLeffler
    {A : Type u} {B : Type v} {N : Type uM} [CommRing A] [CommRing B]
    [IsLocalRing B] [HenselianLocalRing A]
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    (hB : Algebra.EssFiniteType A B)
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Module.Finite B N] [Module.Flat A N] :
    (∃ (I : Type (max u uM)) (_ : SmallCategory I) (_ : IsFiltered I)
      (F : I ⥤ ModuleCat.{max u uM} A) (c : Cocone F),
      (∀ i, Module.Free A (F.obj i)) ∧
      (∀ {i j : I} (f : i ⟶ j), Function.Injective
        (Submodule.mapQ
          (maximalIdeal A • (⊤ : Submodule A (F.obj i)))
          (maximalIdeal A • (⊤ : Submodule A (F.obj j)))
          (F.map f).hom
          (Submodule.smul_top_le_comap_smul_top (maximalIdeal A)
            (F.map f).hom))) ∧
      Nonempty (IsColimit c) ∧
      Nonempty (c.pt ≅ ModuleCat.of A (ULift.{u} N))) ∧
    IsMittagLeffler.{u, uP, uM, max u uQ, uN} A N

isMittagLeffler_of_flat_finite_essFiniteType_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/MittagLefflerEssFiniteType.lean, line 330. The attribute's comment: “the Mittag-Leffler conclusion”.

Let A → B be an essentially finite type local homomorphism of local rings with A henselian, and let N be a finite B-module which is flat over A. Then N is a Mittag-Leffler A-module.

theorem isMittagLeffler_of_flat_finite_essFiniteType_local
    {A : Type u} {B : Type v} {N : Type uM} [CommRing A] [CommRing B]
    [IsLocalRing B] [HenselianLocalRing A]
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    (hB : Algebra.EssFiniteType A B)
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Module.Finite B N] [Module.Flat A N] :
    IsMittagLeffler.{u, uP, uM, max u uQ, uN} A N

exists_filteredColimit_free_with_injective_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/MittagLefflerFilteredColimitPresentation/FreePresentation.lean, line 580. The attribute's comment: “filtered-colimit presentation”.

Let A be a henselian local ring, A → B a local homomorphism of local rings with B essentially of finite type over A, and N a finite B-module which is flat over A. Then N is a filtered colimit of free A-modules F i such that every transition map F i → F j induces an injective map F i / 𝔪_A F i → F j / 𝔪_A F j.

public theorem exists_filteredColimit_free_with_injective_reduction
    {A : Type u} {B : Type v} {N : Type uM} [CommRing A] [CommRing B]
    [IsLocalRing B] [HenselianLocalRing A]
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    (hB : Algebra.EssFiniteType A B)
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Module.Finite B N] [Module.Flat A N] :
    ∃ (I : Type (max u uM)) (_ : SmallCategory I) (_ : IsFiltered I)
      (F : I ⥤ ModuleCat.{max u uM} A) (c : Cocone F),
      (∀ i, Module.Free A (F.obj i)) ∧
      (∀ {i j : I} (f : i ⟶ j), Function.Injective
        (Submodule.mapQ
          (maximalIdeal A • (⊤ : Submodule A (F.obj i)))
          (maximalIdeal A • (⊤ : Submodule A (F.obj j)))
          (F.map f).hom
          (Submodule.smul_top_le_comap_smul_top (maximalIdeal A)
            (F.map f).hom))) ∧
      Nonempty (IsColimit c) ∧
      Nonempty (c.pt ≅ ModuleCat.of A (ULift.{u} N))

Tag 0ASX, a lemma

Tag 0ASX in the Stacks Project.

IsContentIdeal.isPrincipal_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/ContentIdeal.lean, line 52. The attribute's comment: “the principality assertion, unconditionally and in strengthened form: no hypothesis beyond ValuationRing A is used, since a content ideal is finitely generated (0ASB) and a valuation ring is Bézout (090Q).”.

Stacks Tag 0ASX, the principality assertion. A content ideal of an element of a module over a valuation ring is a principal ideal.

The source states this for a finite module over an essentially finite type local algebra which is flat over the valuation ring, but, as its proof shows, none of that is used: a content ideal is finitely generated by Stacks 0ASB, and in a valuation ring every finitely generated ideal is principal by Stacks 090Q. Flatness of the module is not needed either, for the same reason it is not needed in Stacks 0ASB. Dropping the hypotheses only strengthens the statement.

theorem IsContentIdeal.isPrincipal_of_valuationRing
    {A : Type u} [CommRing A] [IsDomain A] [ValuationRing A]
    {N : Type w} [AddCommGroup N] [Module A N]
    {x : N} {I : Ideal A} (hI : IsContentIdeal x I) : I.IsPrincipal

exists_isContentIdeal_isPrincipal_of_valuationRing_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/ContentIdealExistence.lean, line 512.

Stacks Tag 0ASX. Let A → B be a local ring map of local rings which is essentially of finite type, and let N be a finite B-module which is flat as an A-module. If A is a valuation ring, then every element x of N has a content ideal I ⊆ A in the sense of Stacks 0ASA, and that ideal is principal.

Existence is exists_isContentIdeal_of_valuationRing and principality is IsContentIdeal.isPrincipal_of_valuationRing.

theorem exists_isContentIdeal_isPrincipal_of_valuationRing_of_flat
    {A : Type u} {B : Type v} {N : Type w}
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)]
    [Algebra.EssFiniteType A B]
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Module.Finite B N] [Module.Flat A N]
    (x : N) :
    ∃ I : Ideal A, IsContentIdeal x I ∧ I.IsPrincipal

Tag 0H2T, a lemma

Tag 0H2T in the Stacks Project.

isReduced_and_isReduced_fiber_of_isProper_over_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ReducedOverValuationRing.lean, line 437.

Let f : X ⟶ Spec R be a proper flat morphism where R is a valuation ring. If the special fibre is reduced, then X and every fibre of X ⟶ Spec R are reduced.

public theorem isReduced_and_isReduced_fiber_of_isProper_over_valuationRing
    {R : Type u} [CommRing R] [IsDomain R] [ValuationRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsProper f] [Flat f]
    (hspecial : IsReduced (f.fiber (IsLocalRing.closedPoint R))) :
    IsReduced X ∧ ∀ s : Spec (.of R), IsReduced (f.fiber s)

Sources

• Section 38.19, Tag 05L7
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.forall_injective_stalkLinearMap_associatedPoints_iff_mono · AlgebraicGeometry.isLocallyProjective_pushforward_iff_isPureRelative · AlgebraicGeometry.projective_iff_isPureRelative_tilde · AlgebraicGeometry.isPureRelative_of_isLocallyProjective_pushforward · AlgebraicGeometry.isPureRelative_tilde_of_projective · AlgebraicGeometry.exists_affineOpen_projective_sections_of_chart · AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections · AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections_of_finitePresentation

Section38.20 Flattening functors#

Section 38.20 of the Stacks Project, Tag 05MG. 15 tags here are carried by 68 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05MH, a situation

Tag 05MH in the Stacks Project.

Stacks.Flatness.ModuleMapBaseChangeSituation.IsInjectiveAfterBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 69. The attribute's comment: “the injectivity condition”.

The condition that the base-changed homomorphism is injective.

abbrev IsInjectiveAfterBaseChange (D : ModuleMapBaseChangeSituation.{u}) (T : Over D.S) : Prop

Stacks.Flatness.ModuleMapBaseChangeSituation.FlatOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 87. The attribute's comment: “the category with flat morphisms”.

The category of schemes over S whose morphisms are only the flat ones.

abbrev FlatOver (S : Scheme.{u})

Stacks.Flatness.ModuleMapBaseChangeSituation.isInjectiveAfterBaseChange_of_flat_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 94. The attribute's comment: “functoriality of the injectivity condition”.

Being injective after base change is preserved by every flat further base change: the transition morphism of base changes is then flat, so pulling back along it preserves monomorphisms, and the comparison isomorphism carries the base-changed homomorphism over T to the one over T'.

theorem isInjectiveAfterBaseChange_of_flat_hom (D : ModuleMapBaseChangeSituation.{u})
    {T T' : Over D.S} (g : T' ⟶ T) (hg : Flat g.left)
    (h : D.IsInjectiveAfterBaseChange T) : D.IsInjectiveAfterBaseChange T'

Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 111. The attribute's comment: “the injectivity functor”.

The subterminal functor on schemes over the base with flat transition morphisms recording where the base-changed homomorphism is injective.

noncomputable def injectivityFunctor (D : ModuleMapBaseChangeSituation.{u}) :
    (FlatOver D.S)ᵒᵖ ⥤ Type

Stacks.Flatness.ModuleMapBaseChangeSituation.isInjectiveAfterBaseChange_of_hom_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 123. The attribute's comment: “unrestricted functoriality of injectivity for a surjection”.

If the homomorphism is surjective then its base change is both injective and surjective whenever it is injective, hence an isomorphism, and being an isomorphism after base change is stable under an arbitrary further base change.

theorem isInjectiveAfterBaseChange_of_hom_of_epi (D : ModuleMapBaseChangeSituation.{u})
    [Epi D.hom] {T T' : Over D.S} (g : T' ⟶ T) (h : D.IsInjectiveAfterBaseChange T) :
    D.IsInjectiveAfterBaseChange T'

Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctorOfEpi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 140. The attribute's comment: “the unrestricted injectivity functor for a surjection”.

For a surjective homomorphism, injectivity after base change defines a subterminal functor on all schemes over the base.

noncomputable def injectivityFunctorOfEpi (D : ModuleMapBaseChangeSituation.{u}) [Epi D.hom] :
    (Over D.S)ᵒᵖ ⥤ Type

Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctorOfEpiRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 150. The attribute's comment: “restriction of the unrestricted injectivity functor”.

The unrestricted injectivity functor of a surjection restricts along the inclusion of the category with flat morphisms to the injectivity functor.

noncomputable def injectivityFunctorOfEpiRestrictionIso (D : ModuleMapBaseChangeSituation.{u})
    [Epi D.hom] :
    (wideSubcategoryInclusion (FlatMorphismOver D.S)).op ⋙ D.injectivityFunctorOfEpi ≅
      D.injectivityFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctorOfEpiIsoIsomorphismFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/Injectivity.lean, line 160. The attribute's comment: “injectivity equals isomorphism for a surjection”.

For a surjective homomorphism the unrestricted injectivity functor is the isomorphism functor: a surjection that is injective after base change is an isomorphism after base change, and conversely.

noncomputable def injectivityFunctorOfEpiIsoIsomorphismFunctor
    (D : ModuleMapBaseChangeSituation.{u}) [Epi D.hom] :
    D.injectivityFunctorOfEpi ≅ D.isomorphismFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 90. The attribute's comment: “the situation”.

The standing data for testing a homomorphism of quasi-coherent modules after an arbitrary base change: a morphism of schemes f : X ⟶ S, two quasi-coherent modules on X, and a homomorphism between them.

structure ModuleMapBaseChangeSituation

Stacks.Flatness.ModuleMapBaseChangeSituation.baseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 112. The attribute's comment: “the base-changed scheme”.

The base change X ×_S T of the source along a scheme T over the base.

noncomputable abbrev baseChange (D : ModuleMapBaseChangeSituation.{u}) (T : Over D.S) :
    Scheme.{u}

Stacks.Flatness.ModuleMapBaseChangeSituation.baseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 118. The attribute's comment: “the base-changed homomorphism”.

The pullback of the module homomorphism to X ×_S T.

noncomputable def baseChangeMap (D : ModuleMapBaseChangeSituation.{u}) (T : Over D.S) :
    (Scheme.Modules.pullback (pullback.fst D.f T.hom)).obj D.F ⟶
      (Scheme.Modules.pullback (pullback.fst D.f T.hom)).obj D.G

Stacks.Flatness.ModuleMapBaseChangeSituation.IsIsomorphismAfterBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 125. The attribute's comment: “the isomorphism condition”.

The condition that the base-changed homomorphism is an isomorphism.

abbrev IsIsomorphismAfterBaseChange (D : ModuleMapBaseChangeSituation.{u}) (T : Over D.S) :
    Prop

Stacks.Flatness.ModuleMapBaseChangeSituation.IsSurjectiveAfterBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 131. The attribute's comment: “the surjectivity condition”.

The condition that the base-changed homomorphism is surjective.

abbrev IsSurjectiveAfterBaseChange (D : ModuleMapBaseChangeSituation.{u}) (T : Over D.S) :
    Prop

Stacks.Flatness.ModuleMapBaseChangeSituation.IsZeroAfterBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 137. The attribute's comment: “the zero condition”.

The condition that the base-changed homomorphism is zero.

abbrev IsZeroAfterBaseChange (D : ModuleMapBaseChangeSituation.{u}) (T : Over D.S) : Prop

Stacks.Flatness.ModuleMapBaseChangeSituation.isIsomorphismAfterBaseChange_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 189. The attribute's comment: “functoriality of the isomorphism condition”.

Being an isomorphism after base change is preserved by every further base change.

theorem isIsomorphismAfterBaseChange_of_hom (D : ModuleMapBaseChangeSituation.{u})
    {T T' : Over D.S} (g : T' ⟶ T) (h : D.IsIsomorphismAfterBaseChange T) :
    D.IsIsomorphismAfterBaseChange T'

Stacks.Flatness.ModuleMapBaseChangeSituation.isSurjectiveAfterBaseChange_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 199. The attribute's comment: “functoriality of the surjectivity condition”.

Being surjective after base change is preserved by every further base change.

theorem isSurjectiveAfterBaseChange_of_hom (D : ModuleMapBaseChangeSituation.{u})
    {T T' : Over D.S} (g : T' ⟶ T) (h : D.IsSurjectiveAfterBaseChange T) :
    D.IsSurjectiveAfterBaseChange T'

Stacks.Flatness.ModuleMapBaseChangeSituation.isZeroAfterBaseChange_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 209. The attribute's comment: “functoriality of the zero condition”.

Being zero after base change is preserved by every further base change.

theorem isZeroAfterBaseChange_of_hom (D : ModuleMapBaseChangeSituation.{u}) {T T' : Over D.S}
    (g : T' ⟶ T) (h : D.IsZeroAfterBaseChange T) : D.IsZeroAfterBaseChange T'

Stacks.Flatness.ModuleMapBaseChangeSituation.isomorphismFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 218. The attribute's comment: “the isomorphism functor”.

The subterminal functor on schemes over the base recording where the base-changed homomorphism is an isomorphism.

noncomputable def isomorphismFunctor (D : ModuleMapBaseChangeSituation.{u}) :
    (Over D.S)ᵒᵖ ⥤ Type

Stacks.Flatness.ModuleMapBaseChangeSituation.surjectivityFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 228. The attribute's comment: “the surjectivity functor”.

The subterminal functor on schemes over the base recording where the base-changed homomorphism is surjective.

noncomputable def surjectivityFunctor (D : ModuleMapBaseChangeSituation.{u}) :
    (Over D.S)ᵒᵖ ⥤ Type

Stacks.Flatness.ModuleMapBaseChangeSituation.zeroFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ModuleMapBaseChange.lean, line 238. The attribute's comment: “the zero functor”.

The subterminal functor on schemes over the base recording where the base-changed homomorphism is zero.

noncomputable def zeroFunctor (D : ModuleMapBaseChangeSituation.{u}) :
    (Over D.S)ᵒᵖ ⥤ Type

Tag 05MJ, a lemma

Tag 05MJ in the Stacks Project.

Stacks.Flatness.ModuleMapBaseChangeSituation.isomorphismFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/FpqcSheaf.lean, line 76. The attribute's comment: “iso_fpqc”.

The isomorphism functor of a homomorphism of quasi-coherent modules satisfies the sheaf condition for the fpqc topology on schemes over the base.

theorem isomorphismFunctor_isSheaf_fpqc (D : ModuleMapBaseChangeSituation.{u}) :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over D.S) D.isomorphismFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.surjectivityFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/FpqcSheaf.lean, line 85. The attribute's comment: “surj_fpqc”.

The surjectivity functor of a homomorphism of quasi-coherent modules satisfies the sheaf condition for the fpqc topology on schemes over the base.

theorem surjectivityFunctor_isSheaf_fpqc (D : ModuleMapBaseChangeSituation.{u}) :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over D.S) D.surjectivityFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.zeroFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/FpqcSheaf.lean, line 94. The attribute's comment: “zero_fpqc”.

The zero functor of a homomorphism of quasi-coherent modules satisfies the sheaf condition for the fpqc topology on schemes over the base.

theorem zeroFunctor_isSheaf_fpqc (D : ModuleMapBaseChangeSituation.{u}) :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over D.S) D.zeroFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/FpqcSheaf.lean, line 103. The attribute's comment: “inj_fpqc”.

The injectivity functor of a homomorphism of quasi-coherent modules satisfies the sheaf condition for the fpqc topology on the category of schemes over the base with flat morphisms.

theorem injectivityFunctor_isSheaf_fpqc (D : ModuleMapBaseChangeSituation.{u}) :
    Presheaf.IsSheaf
      (Scheme.fpqcPrecoverage.comap
        (wideSubcategoryInclusion (FlatMorphismOver D.S) ⋙ Over.forget D.S)).toGrothendieck
      D.injectivityFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.isomorphismFunctor_preservesColimit_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/IsomorphismLimit.lean, line 249. The attribute's comment: “iso_limit”.

Stacks Project, Tag 05MJ. The isomorphism functor of a homomorphism of quasi-coherent modules with source of finite type and target of finite presentation, along a quasi-compact morphism, preserves the filtered colimit attached to a cofiltered inverse system of affine schemes over the base.

theorem isomorphismFunctor_preservesColimit_of_isAffine (D : ModuleMapBaseChangeSituation.{u})
    [QuasiCompact D.f] [D.F.IsFiniteType] [D.G.IsFinitePresentation] (I : Type u)
    [Category.{u} I] [IsCofiltered I] (T : I ⥤ Over D.S) (hT : ∀ i, IsAffine (T.obj i).left) :
    PreservesColimit T.op D.isomorphismFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.surjectivityFunctor_preservesColimit_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/SurjectivityLimit.lean, line 101. The attribute's comment: “surj_limit”.

Stacks Project, Tag 05MJ. The surjectivity functor of a homomorphism of quasi-coherent modules with target of finite type, along a quasi-compact morphism, preserves the filtered colimit attached to a cofiltered inverse system of affine schemes over the base.

theorem surjectivityFunctor_preservesColimit_of_isAffine (D : ModuleMapBaseChangeSituation.{u})
    [QuasiCompact D.f] [D.G.IsFiniteType] (I : Type u) [Category.{u} I] [IsCofiltered I]
    (T : I ⥤ Over D.S) (hT : ∀ i, IsAffine (T.obj i).left) :
    PreservesColimit T.op D.surjectivityFunctor

Stacks.Flatness.ModuleMapBaseChangeSituation.zeroFunctor_preservesColimit_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctors/ZeroLimit.lean, line 340. The attribute's comment: “zero_limit”.

Stacks Project, Tag 05MJ. The zero functor of a homomorphism of quasi-coherent modules with source of finite type, along a quasi-compact morphism, preserves the filtered colimit attached to a cofiltered inverse system of affine schemes over the base.

theorem zeroFunctor_preservesColimit_of_isAffine (D : ModuleMapBaseChangeSituation.{u})
    [QuasiCompact D.f] [D.F.IsFiniteType] (I : Type u) [Category.{u} I] [IsCofiltered I]
    (T : I ⥤ Over D.S) (hT : ∀ i, IsAffine (T.obj i).left) :
    PreservesColimit T.op D.zeroFunctor

Tag 05MK, a situation

Tag 05MK in the Stacks Project.

LocalAlgCat, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 103. The attribute's comment: “objects”.

Stacks Project, Tag 05MK. An object of the category C: a local A-algebra whose structure homomorphism is a local homomorphism of local rings.

structure LocalAlgCat (A : Type u) [CommRing A] [IsLocalRing A]

LocalAlgCat.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 129. The attribute's comment: “morphisms”.

Stacks Project, Tag 05MK. A morphism of the category C: a local homomorphism of A-algebras.

structure Hom (R S : LocalAlgCat.{u, v} A)

An instance with no name in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 138. The attribute's comment: “the category”.

Stacks Project, Tag 05MK. Local A-algebras and local A-algebra homomorphisms form a category.

instance : Category (LocalAlgCat.{u, v} A)

Module.FlatAtPointSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 171. The attribute's comment: “the situation”.

Stacks Project, Tag 05MK. The standing data of the local flattening problem: a local homomorphism A → B of local rings and a B-module M.

structure FlatAtPointSituation

Module.FlatAtPointSituation.ConditionOn.of_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 235. The attribute's comment: “base-change stability”.

Stacks Project, Tag 05MK. The flatness condition is preserved by a local homomorphism of local A-algebras. The source and the target may live in different universes.

theorem ConditionOn.of_isLocalHom {S : FlatAtPointSituation.{u, v, w}} (R : Type x) (T : Type y)
    [CommRing R] [IsLocalRing R] [Algebra S.A R] [CommRing T] [IsLocalRing T] [Algebra S.A T]
    [Algebra R T] [IsScalarTower S.A R T] [IsLocalHom (algebraMap R T)] (h : S.ConditionOn R) :
    S.ConditionOn T

Module.FlatAtPointSituation.condition_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 244. The attribute's comment: “base-change stability”.

Stacks Project, Tag 05MK. The flatness condition is preserved by a morphism of the category C of local A-algebras; this is what makes F_lf a functor.

theorem condition_of_hom (S : FlatAtPointSituation.{u, v, w}) {R T : LocalAlgCat.{u, x} S.A}
    (f : R ⟶ T) (h : S.Condition R) : S.Condition T

Module.FlatAtPointSituation.flatAtPointFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 312. The attribute's comment: “the functor”.

Stacks Project, Tag 05MK. The functor F_lf on the category C of local A-algebras: it takes the value a singleton where the flatness condition holds, and the empty set elsewhere. Functoriality is condition_of_hom.

def flatAtPointFunctor (S : FlatAtPointSituation.{u, v, w}) :
    LocalAlgCat.{u, x} S.A ⥤ Type

Tag 05ML, an equation

Tag 05ML in the Stacks Project.

Module.FlatAtPointSituation.ConditionOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 213.

Stacks Project, Tag 05ML. The flatness condition on a local A-algebra R: the base change of M is flat over R at every prime of B ⊗[A] R containing the extensions of the maximal ideals of R and of B. This is the condition of Stacks Tag 05LQ for the ideals I' = m_R and J = m_B.

def ConditionOn (S : FlatAtPointSituation.{u, v, w}) (R : Type x) [CommRing R] [IsLocalRing R]
    [Algebra S.A R] : Prop

Module.FlatAtPointSituation.Condition, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlattening.lean, line 221.

Stacks Project, Tag 05ML. The flatness condition read on an object of the category C of Stacks Tag 05MK.

abbrev Condition (S : FlatAtPointSituation.{u, v, w}) (R : LocalAlgCat.{u, x} S.A) : Prop

Tag 05MN, a lemma

Tag 05MN in the Stacks Project.

Module.FlatAtPointSituation.condition_iff_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatteningFlatDescent.lean, line 110. The attribute's comment: “flat_base_change”.

Stacks Project, Tag 05MN part (1), read on a morphism of the category C of local A-algebras of Stacks Tag 05MK: if f : R ⟶ T is flat then F_lf(R) = F_lf(T), both being determined by the flatness condition of Stacks Tag 05ML.

theorem condition_iff_of_flat (S : FlatAtPointSituation.{u, v, w}) {R T : LocalAlgCat.{u, x} S.A}
    (f : R ⟶ T) (hf : f.hom.toRingHom.Flat) :
    S.Condition R ↔ S.Condition T

Module.FlatAtPointSituation.flatAtPointFunctor_obj_eq_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatteningFlatDescent.lean, line 125. The attribute's comment: “flat_base_change”.

Stacks Project, Tag 05MN part (1), in the shape the source states it: the functor F_lf of Stacks Tag 05MM takes the same value at the two ends of a flat morphism of the category C.

The values are PLift of the flatness condition of Stacks Tag 05ML, so this is Module.FlatAtPointSituation.condition_iff_of_flat read through propext.

theorem flatAtPointFunctor_obj_eq_of_flat (S : FlatAtPointSituation.{u, v, w})
    {R T : LocalAlgCat.{u, x} S.A} (f : R ⟶ T) (hf : f.hom.toRingHom.Flat) :
    S.flatAtPointFunctor.obj R = S.flatAtPointFunctor.obj T

Module.FlatAtPointSituation.condition_colimit_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatteningLimitPreserving.lean, line 324. The attribute's comment: “limit_preserving”.

Stacks Project, Tag 05MN part (2), as an equivalence: the flatness condition of Stacks Tag 05ML holds over the apex of a filtered colimit of local A-algebras exactly when it holds at one of the stages. The easy direction is base-change stability, Module.FlatAtPointSituation.condition_of_hom.

Beyond the hypotheses of the source nothing is assumed about the colimit: that it is computed on the underlying sets, which is what Stacks Tag 05LT needs, is proved in Stacks.CommAlgCat.forget_preservesFilteredColimitsOfSize. The two UnivLE hypotheses are the size condition that result carries, namely that the index category be no larger than the algebras; a directed system in the sense of the source is indexed by a set and satisfies it.

theorem condition_colimit_iff
    (hS : (algebraMap S.A S.B).EssentiallyOfFinitePresentation)
    [Module.FinitePresentation S.B S.M]
    (hτ : IsColimit (toCommAlgCat.mapCocone τ)) :
    S.Condition τ.pt ↔ ∃ lam, S.Condition (F.obj lam)

Module.FlatAtPointSituation.isColimitMapCoconeFlatAtPointFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatteningLimitPreserving.lean, line 349. The attribute's comment: “limit_preserving”.

Stacks Project, Tag 05MN part (2). If A → B is essentially of finite presentation and M is a B-module of finite presentation, then the functor F_lf of Stacks Tag 05MM is limit preserving: for a directed system {A_i} of objects of the category C of Stacks Tag 05MK, F_lf(colim A_i) = colim F_lf(A_i).

The colimit of the system is read off the underlying system of A-algebras; it does lie in C, by LocalAlgCat.isLocalRing_pt_of_isColimit and LocalAlgCat.isLocalHom_ι_of_isColimit. The statement is that the induced cocone of sets is a colimit, which by CategoryTheory.Limits.Types.FilteredColimit.isColimitOf amounts to the descent statement Module.FlatAtPointSituation.exists_condition_of_isColimit, every value of F_lf having at most one element.

That the colimit of A-algebras is computed on the underlying sets is not assumed but proved, in Stacks.CommAlgCat.forget_preservesFilteredColimitsOfSize; the two UnivLE hypotheses are the size condition it carries, that the index category of the directed system be no larger than the algebras.

noncomputable def isColimitMapCoconeFlatAtPointFunctor
    (hS : (algebraMap S.A S.B).EssentiallyOfFinitePresentation)
    [Module.FinitePresentation S.B S.M]
    (hτ : IsColimit (toCommAlgCat.mapCocone τ)) :
    IsColimit (S.flatAtPointFunctor.mapCocone τ)

Tag 05P4, a lemma

Tag 05P4 in the Stacks Project.

Module.FlatAtPointSituation.flatAtPointFunctor_eq_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatAtPointFinite.lean, line 258.

Stacks Project, Tag 05P4. Replacing the local algebra of a flat-at-a-point situation by a finite local extension, and its module by an isomorphic module over that extension, does not change the flat-at-a-point functor.

public theorem flatAtPointFunctor_eq_of_finite (S : FlatAtPointSituation.{u, v, w})
    {C : Type x} [CommRing C] [IsLocalRing C] [Algebra S.A C] [IsLocalHom (algebraMap S.A C)]
    {N : Type y} [AddCommGroup N] [Module C N] (f : S.B →ₐ[S.A] C)
    (hf : IsLocalHom f.toRingHom) (hfinite : f.toRingHom.Finite)
    (e : letI : Module S.B N := Module.compHom N f.toRingHom
      S.M ≃ₗ[S.B] N) :
    flatAtPointFunctor.{u, v, w, z} S =
      flatAtPointFunctor.{u, x, y, z} ({ A := S.A, B := C, M := N } :
        FlatAtPointSituation.{u, x, y})

Tag 05P5, a lemma

Tag 05P5 in the Stacks Project.

Module.FlatAtPointSituation.flatAtPointFunctor_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatAtPointFlatBaseChange.lean, line 438.

Stacks Project, Tag 05P5. A flat local extension of the local algebra, with the module extended along it, does not change the flat-at-a-point functor.

public theorem flatAtPointFunctor_baseChange (S : FlatAtPointSituation.{u, v, w}) (C : Type z)
    [CommRing C] [IsLocalRing C] [Algebra S.B C] [IsLocalHom (algebraMap S.B C)]
    [Module.Flat S.B C] :
    (S.flatAtPointFunctor : LocalAlgCat.{u, x} S.A ⥤ Type) =
      (baseChange S C).flatAtPointFunctor

Tag 05MP, a situation

Tag 05MP in the Stacks Project.

AlgebraicGeometry.FreeAtGenericPointsSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPoints.lean, line 76. The attribute's comment: “the situation”.

The standing situation of a smooth morphism with geometrically irreducible fibres and a finite type quasi-coherent module on its source.

structure FreeAtGenericPointsSituation

AlgebraicGeometry.FreeAtGenericPointsSituation.Condition, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPoints.lean, line 113. The attribute's comment: “the fibrewise condition”.

The module pulled back to X ×_S T is free of rank p near the generic point of every fibre over T.

abbrev Condition (D : FreeAtGenericPointsSituation.{u}) (p : ℕ)
    (T : Over D.S) : Prop

AlgebraicGeometry.FreeAtGenericPointsSituation.condition_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPoints.lean, line 195. The attribute's comment: “base-change stability”.

The fibrewise generic-point condition is preserved by a further base change.

theorem condition_of_hom (D : FreeAtGenericPointsSituation.{u}) (p : ℕ)
    {T T' : Over D.S} (g : T' ⟶ T) (h : D.Condition p T) :
    D.Condition p T'

AlgebraicGeometry.FreeAtGenericPointsSituation.freeAtGenericPointsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPoints.lean, line 259. The attribute's comment: “the functor”.

The subterminal set-valued functor recording whether the pulled-back module is free of rank p near the generic point of every fibre.

noncomputable def freeAtGenericPointsFunctor
    (D : FreeAtGenericPointsSituation.{u}) (p : ℕ) :
    (Over D.S)ᵒᵖ ⥤ Type u

Tag 05MS, a lemma

Tag 05MS in the Stacks Project.

AlgebraicGeometry.FreeAtGenericPointsSituation.freeAtGenericPointsFunctor_limitPreserving_small, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPointsDescent.lean, line 248. The attribute's comment: “part (2), the generic-rank functor is limit preserving”.

Stacks Project, Tag 05MS, part (2). The generic-rank functor of a module of finite presentation is limit preserving: over a cofiltered limit of affine schemes over the base the functor has a section as soon as one stage of the system has one.

The approximation statement which freeAtGenericPointsFunctor_limitPreserving_small_iff identifies with this clause is AlgebraicGeometry.FreeAtGenericPointsSituation.exists_condition_of_isLimit, so nothing is assumed here.

theorem freeAtGenericPointsFunctor_limitPreserving_small [D.F.IsFinitePresentation] :
    LimitPreserving.{u, u, u, u, u + 1, u} (Over.forget D.S)
      (D.freeAtGenericPointsFunctor p)

AlgebraicGeometry.FreeAtGenericPointsSituation.freeAtGenericPointsFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPointsFpqcSheaf.lean, line 314. The attribute's comment: “part (1), the generic-rank functor is an fpqc sheaf”.

Stacks Project, Tag 05MS, part (1). The generic-rank functor satisfies the sheaf property for the fpqc topology.

By freeAtGenericPointsFunctor_isSheaf_fpqc_of_fpqcCover this is fpqc-locality of the generic-point condition, and the source proves that locality in two steps: descent along the covering gives a free stalk of rank p at the generic point of every fibre over the base (stalkFreeOfRank_of_fpqcCover), and AlgebraicGeometry.freeAtPointOfRank_of_forall_stalkFreeOfRank spreads those free stalks out to neighbourhoods.

theorem freeAtGenericPointsFunctor_isSheaf_fpqc (D : FreeAtGenericPointsSituation.{u}) (p : ℕ) :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over D.S) (D.freeAtGenericPointsFunctor p)

Tag 0CWF, a lemma

Tag 0CWF in the Stacks Project.

AlgebraicGeometry.topologicalKrullDim_not_isFlatOverAt_fiber_lt_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/NonFlatLocusFibreDimension.lean, line 288. The attribute's comment: “the dimension criterion”.

Stacks Project, Tag 0CWF. Let f : X ⟶ S be locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type and let n be a natural number. The closed subset of each fibre where F is not flat over S has dimension less than n if and only if trdeg_{κ(f x)} κ(x) < n at every point x where F is not flat over S.

theorem topologicalKrullDim_not_isFlatOverAt_fiber_lt_iff {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (n : ℕ) :
    (∀ s : S, topologicalKrullDim
        ↥{y : f.fiber s | ¬ IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s y)} <
          (n : WithBot ℕ∞)) ↔
      ∀ x : X, ¬ IsFlatOverAt f.toLRSHom.toShHom F x →
        letI : Algebra (S.residueField (f x)) (X.residueField x) :=
          (f.residueFieldMap x).hom.toAlgebra
        (Cardinal.toENat (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) :
          WithBot ℕ∞) < (n : WithBot ℕ∞)

AlgebraicGeometry.topologicalKrullDim_not_isFlatOverAt_fiber_lt_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/NonFlatLocusFibreDimension.lean, line 307. The attribute's comment: “stability under base change”.

Stacks Project, Tag 0CWF. The dimension criterion is stable under base change: if the non-flat locus has dimension less than n in every fibre of f, then the same holds for the pullback of F along any base change of f.

theorem topologicalKrullDim_not_isFlatOverAt_fiber_lt_of_isPullback {X S S' X' : Scheme.{u}}
    {f : X ⟶ S} {g : S' ⟶ S} {g' : X' ⟶ X} {f' : X' ⟶ S'} (hsq : IsPullback g' f' f g)
    [LocallyOfFiniteType f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (n : ℕ)
    (hF : ∀ s : S, topologicalKrullDim
        ↥{y : f.fiber s | ¬ IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s y)} <
          (n : WithBot ℕ∞)) (s' : S') :
    topologicalKrullDim
        ↥{y : f'.fiber s' | ¬ IsFlatOverAt f'.toLRSHom.toShHom
            ((Scheme.Modules.pullback g').obj F) (f'.fiberι s' y)} < (n : WithBot ℕ∞)

Tag 0CWG, a definition

Tag 0CWG in the Stacks Project.

AlgebraicGeometry.IsFlatOverInDimensionsGE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatInDimensionsGE.lean, line 83.

Stacks Project, Tag 0CWG. Let f : X ⟶ S be locally of finite type and let F be a quasi-coherent 𝒪_X-module of finite type. Then F is flat over S in dimensions ≥ n if for every point s of S the closed subset of the fibre X_s of points at which F is not flat over S has dimension less than n.

This is the first of the two equivalent conditions of Stacks 0CWF; the second one is AlgebraicGeometry.isFlatOverInDimensionsGE_iff_forall_toENat_trdeg_lt.

def IsFlatOverInDimensionsGE {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (n : ℕ) : Prop

Tag 05MT, a situation

Tag 05MT in the Stacks Project.

AlgebraicGeometry.FlatDimensionSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 83. The attribute's comment: “the situation”.

A morphism of schemes f : X ⟶ S locally of finite type together with a quasi-coherent module F of finite type on X and a bound n on fibre dimensions.

public structure FlatDimensionSituation

AlgebraicGeometry.FlatDimensionSituation.baseChangeMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 107. The attribute's comment: “the base-changed morphism”.

The base-changed morphism X_T = X ×_S T ⟶ T.

public noncomputable abbrev baseChangeMap (D : FlatDimensionSituation.{u}) (T : Over D.S) :
    pullback D.f T.hom ⟶ T.left

AlgebraicGeometry.FlatDimensionSituation.baseChangeModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 114. The attribute's comment: “the base-changed module”.

The base change F_T of the module, i.e. its pullback along the projection X_T = X ×_S T ⟶ X.

public noncomputable abbrev baseChangeModule (D : FlatDimensionSituation.{u}) (T : Over D.S) :
    (pullback D.f T.hom).Modules

AlgebraicGeometry.FlatDimensionSituation.baseChangeMap_locallyOfFiniteType, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 120. The attribute's comment: “X_T → T is of finite type”.

The base-changed morphism X_T ⟶ T is again locally of finite type.

public instance baseChangeMap_locallyOfFiniteType (D : FlatDimensionSituation.{u})
    (T : Over D.S) : LocallyOfFiniteType (D.baseChangeMap T)

AlgebraicGeometry.FlatDimensionSituation.baseChangeModule_isFiniteType, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 127. The attribute's comment: “F_T is of finite type”.

The base-changed module F_T is again of finite type.

public noncomputable instance baseChangeModule_isFiniteType (D : FlatDimensionSituation.{u})
    (T : Over D.S) : (D.baseChangeModule T).IsFiniteType

AlgebraicGeometry.FlatDimensionSituation.IsFlatInDimensionsGEAfterBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 139. The attribute's comment: “the condition tested by the functor”.

The base-changed module F_T is flat over T in dimensions ≥ n.

public noncomputable abbrev IsFlatInDimensionsGEAfterBaseChange
    (D : FlatDimensionSituation.{u}) (T : Over D.S) : Prop

AlgebraicGeometry.FlatDimensionSituation.isFlatInDimensionsGEAfterBaseChange_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 156. The attribute's comment: “base-change stability of the condition”.

Flatness of the base-changed module in dimensions ≥ n is inherited along a morphism T' ⟶ T of schemes over S.

public theorem isFlatInDimensionsGEAfterBaseChange_of_hom (D : FlatDimensionSituation.{u})
    {T T' : Over D.S} (g : T' ⟶ T) (h : D.IsFlatInDimensionsGEAfterBaseChange T) :
    D.IsFlatInDimensionsGEAfterBaseChange T'

AlgebraicGeometry.FlatDimensionSituation.flatDimensionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionFunctor.lean, line 166. The attribute's comment: “the functor F_n”.

The functor F_n : (Sch/S)ᵒᵖ ⥤ Sets sending a scheme T over S to a singleton if F_T is flat over T in dimensions ≥ n, and to the empty set otherwise.

public noncomputable def flatDimensionFunctor (D : FlatDimensionSituation.{u}) :
    (Over D.S)ᵒᵖ ⥤ Type

Tag 05MV, a lemma

Tag 05MV in the Stacks Project.

AlgebraicGeometry.FlatDimensionSituation.flatDimensionFunctor_isSheaf_fpqc_and_limitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionSheafAndLimitPreserving.lean, line 63. The attribute's comment: “parts (1) and (2)”.

Stacks Project, Tag 05MV. In Situation 05MT:

1. the functor F_n satisfies the sheaf property for the fpqc topology; and
2. if f is quasi-compact and locally of finite presentation and F is of finite presentation, then the functor F_n is limit preserving, i.e. it carries a cofiltered inverse limit of affine schemes over S to a filtered colimit of sets.

The three finiteness assumptions of (2) are hypotheses of (2) only: (1) holds in the ambient situation alone.

public theorem flatDimensionFunctor_isSheaf_fpqc_and_limitPreserving
    (D : FlatDimensionSituation.{max u v w}) :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over D.S) D.flatDimensionFunctor ∧
      (QuasiCompact D.f → LocallyOfFinitePresentation D.f → D.F.IsFinitePresentation →
        LimitPreserving.{max u v w, 0, v, w, max u v w + 1, max u v w}
          (Over.forget D.S) D.flatDimensionFunctor)

Tag 05MW, a situation

Tag 05MW in the Stacks Project.

AlgebraicGeometry.FlatnessSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/Basic.lean, line 61. The attribute's comment: “the situation”.

A morphism of schemes together with a quasi-coherent module on its source.

public structure FlatnessSituation

AlgebraicGeometry.FlatnessSituation.baseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/Basic.lean, line 78. The attribute's comment: “the base-changed scheme”.

The fibre product X ×_S T.

public noncomputable abbrev baseChange (D : FlatnessSituation.{u})
    (T : Over D.S) : Scheme.{u}

AlgebraicGeometry.FlatnessSituation.baseChangeModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/Basic.lean, line 84. The attribute's comment: “the base-changed module”.

The pullback of the module to X ×_S T.

public noncomputable abbrev baseChangeModule (D : FlatnessSituation.{u})
    (T : Over D.S) :
    SheafOfModules.{u} (structureSheafRing (D.baseChange T).toRingedSpace)

AlgebraicGeometry.FlatnessSituation.IsFlatAfterBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/Basic.lean, line 91. The attribute's comment: “the flatness condition”.

The base-changed module is flat over T.

public abbrev IsFlatAfterBaseChange (D : FlatnessSituation.{u})
    (T : Over D.S) : Prop

AlgebraicGeometry.FlatnessSituation.isFlatAfterBaseChange_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/Basic.lean, line 130. The attribute's comment: “base-change stability”.

Flatness of the pulled-back module persists under further base change.

public theorem isFlatAfterBaseChange_of_hom (D : FlatnessSituation.{u})
    {T T' : Over D.S} (g : T' ⟶ T) (h : D.IsFlatAfterBaseChange T) :
    D.IsFlatAfterBaseChange T'

AlgebraicGeometry.FlatnessSituation.flatFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/Basic.lean, line 137. The attribute's comment: “the functor”.

The subterminal functor recording flatness of the base-changed module.

public noncomputable def flatFunctor (D : FlatnessSituation.{u}) :
    (Over D.S)ᵒᵖ ⥤ Type

Tag 05MY, a lemma

Tag 05MY in the Stacks Project.

AlgebraicGeometry.FlatnessSituation.flatFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FpqcSheaf.lean, line 118. The attribute's comment: “flat_functor_fpqc_sheaf”.

Stacks Project, Tag 05MY. Part (1): the flatness functor of a quasi-coherent module satisfies the sheaf condition for the fpqc topology on schemes over the base.

public theorem flatFunctor_isSheaf_fpqc :
    Presheaf.IsSheaf (Scheme.fpqcTopology.over D.S) D.flatFunctor

AlgebraicGeometry.FlatnessSituation.flatFunctor_limitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/LimitPreserving.lean, line 288. The attribute's comment: “flat_functor_limit_preserving”.

Stacks Project, Tag 05MY. Part (2): for a quasi-compact morphism which is locally of finite presentation and a quasi-coherent module of finite presentation, the flatness functor is limit preserving: it carries a cofiltered inverse limit of affine schemes over the base to a filtered colimit of sets.

public theorem flatFunctor_limitPreserving (D : FlatnessSituation.{max u v w})
    [QuasiCompact D.f] [LocallyOfFinitePresentation D.f] [D.F.IsFinitePresentation] :
    LimitPreserving.{max u v w, 0, v, w, max u v w + 1, max u v w}
      (Over.forget D.S) D.flatFunctor

Sources

• Section 38.20, Tag 05MG
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Flatness.ModuleMapBaseChangeSituation.IsInjectiveAfterBaseChange · Stacks.Flatness.ModuleMapBaseChangeSituation.FlatOver · Stacks.Flatness.ModuleMapBaseChangeSituation.isInjectiveAfterBaseChange_of_flat_hom · Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctor · Stacks.Flatness.ModuleMapBaseChangeSituation.isInjectiveAfterBaseChange_of_hom_of_epi · Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctorOfEpi · Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctorOfEpiRestrictionIso · Stacks.Flatness.ModuleMapBaseChangeSituation.injectivityFunctorOfEpiIsoIsomorphismFunctor

Section38.21 Flattening stratifications#

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

Tag 05P6, a definition

Tag 05P6 in the Stacks Project.

AlgebraicGeometry.FlatnessSituation.HasUniversalFlattening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/Basic.lean, line 48. The attribute's comment: “the universal flattening of a module”.

A quasi-coherent module admits a universal flattening when its flatness functor is represented by a scheme over the base.

public noncomputable abbrev FlatnessSituation.HasUniversalFlattening
    (D : FlatnessSituation.{u}) : Prop

AlgebraicGeometry.HasUniversalFlattening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/Basic.lean, line 63. The attribute's comment: “the universal flattening of a scheme”.

A scheme over S admits a universal flattening when its structure sheaf does.

public noncomputable abbrev HasUniversalFlattening {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Tag 0FJ1, an example

Tag 0FJ1 in the Stacks Project.

AlgebraicGeometry.PlaneFlatteningExample.flatFunctor_unique_isEmpty_not_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/PlaneExampleNotRepresentable.lean, line 254.

Stacks 0FJ1. Let k be a field, X = S = Spec k[x, y] and 𝓕 the quasi-coherent module associated to k[x, x⁻¹, y]/(y), with flatness functor F_flat, and write F_flat(A) = F_flat(Spec A) for a k[x, y]-algebra A. Then F_flat(k[x, y]/(x, y)^n) is a singleton for every n, while F_flat(k[[x, y]]) is empty. Hence F_flat is not representable even by an algebraic space (on any big fppf site containing Spec k[[x, y]], the restriction of F_flat is isomorphic to no algebraic space over S), and in particular it is not representable by a scheme over S: the universal flattening of 𝓕 does not exist.

public theorem flatFunctor_unique_isEmpty_not_representable (E : PlaneFlatteningExample.{u}) :
    (∀ n : ℕ, Nonempty (Unique (E.flatValue (E.R ⧸ Ideal.span ({E.x, E.y} : Set E.R) ^ n)))) ∧
    IsEmpty (E.flatValue E.formalPlane) ∧
    (∀ (B : BigFppfSite.{u}) (hS : B.Contains E.X), B.Contains (Spec (.of E.formalPlane)) →
      ¬ ∃ X : (BigFppfOver B E.X hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B E.X hS X ∧
        Nonempty (X ≅ (Over.post B.inclusion).op ⋙
          E.flatnessSituation.flatFunctor ⋙ uliftFunctor)) ∧
    ¬ E.flatnessSituation.flatFunctor.IsRepresentable

Tag 05P7, a definition

Tag 05P7 in the Stacks Project.

AlgebraicGeometry.FlatnessSituation.HasFlatteningStratification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/Basic.lean, line 74. The attribute's comment: “the module”.

A quasi-coherent module has a flattening stratification if its flatness functor is represented by the monomorphism associated to a locally finite scheme-theoretic stratification of the base: closed subschemes J i, indexed by a partial order, whose supports cover S and form a locally finite family, with J i ⊔ J j the infimum of the J k for k ≤ i and k ≤ j, together with opens U i of the subschemes J i whose images are the supports of J i minus those of the J j with j < i, such that the representing object is isomorphic over S to the coproduct of the U i and its structure morphism is a monomorphism.

public def FlatnessSituation.HasFlatteningStratification (D : FlatnessSituation.{u}) : Prop

AlgebraicGeometry.HasFlatteningStratification, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/Basic.lean, line 91. The attribute's comment: “the scheme”.

A scheme over S has a flattening stratification when its structure sheaf does.

public abbrev HasFlatteningStratification {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Sources

• Section 38.21, Tag 052F
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FlatnessSituation.HasUniversalFlattening · AlgebraicGeometry.HasUniversalFlattening · AlgebraicGeometry.PlaneFlatteningExample.flatFunctor_unique_isEmpty_not_representable · AlgebraicGeometry.FlatnessSituation.HasFlatteningStratification · AlgebraicGeometry.HasFlatteningStratification

Section38.22 Flattening stratification over an Artinian ring#

Section 38.22 of the Stacks Project, Tag 05PA. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05PB, a lemma

Tag 05PB in the Stacks Project.

AlgebraicGeometry.FlatnessSituation.exists_closedUniversalFlattening_of_isArtinianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/Artinian.lean, line 236. The attribute's comment: “the closed universal flattening”. References: SGA 6 XII (4.5), “special case”.

Stacks Project, Tag 05PB. A quasi-coherent module on a scheme over the spectrum of an Artinian ring admits a universal flattening, and the representing morphism is a closed immersion.

public theorem exists_closedUniversalFlattening_of_isArtinianRing {R : Type u} [CommRing R]
    [IsArtinianRing R] (D : FlatnessSituation.{u}) (hS : D.S = Spec (.of R)) :
    ∃ W : Over D.S, IsClosedImmersion W.hom ∧ Nonempty (D.flatFunctor.RepresentableBy W)

AlgebraicGeometry.FlatnessSituation.hasFlatteningStratification_of_isArtinianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/Artinian.lean, line 270. The attribute's comment: “the flattening stratification”. References: SGA 6 XII (4.5), “special case”.

Stacks Project, Tag 05PB. A quasi-coherent module on a scheme over the spectrum of an Artinian ring has a flattening stratification.

public theorem hasFlatteningStratification_of_isArtinianRing {R : Type u} [CommRing R]
    [IsArtinianRing R] (D : FlatnessSituation.{u}) (hS : D.S = Spec (.of R)) :
    D.HasFlatteningStratification

Sources

• Section 38.22, Tag 05PA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FlatnessSituation.exists_closedUniversalFlattening_of_isArtinianRing · AlgebraicGeometry.FlatnessSituation.hasFlatteningStratification_of_isArtinianRing

Section38.23 Flattening a map#

Section 38.23 of the Stacks Project, Tag 05PC. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05PD, a lemma

Tag 05PD in the Stacks Project.

AlgebraicGeometry.mono_pullbackPushforwardUnit_of_relativeAssassin_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningInjective.lean, line 88. The attribute's comment: “injectivity”.

Stacks Project, Tag 05PD. Let S be a scheme, let g : X' ⟶ X be a flat morphism of schemes over S with X locally of finite type over S, and let F be a finite type quasi-coherent 𝒪_X-module which is flat over S. If Ass_{X/S}(F) ⊆ g(X'), then the canonical map F ⟶ g_* g^* F is injective.

theorem mono_pullbackPushforwardUnit_of_relativeAssassin_subset_range
    {X' X S : Scheme.{u}} (f : X ⟶ S) (g : X' ⟶ X)
    [LocallyOfFiniteType f] [Flat g]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hF : IsFlatOver f.toLRSHom.toShHom F)
    (hAss : Stacks.Divisors.relativeAssassin f F ⊆ Set.range g.base) :
    Mono ((Scheme.Modules.pullbackPushforwardAdjunction g).unit.app F)

AlgebraicGeometry.mono_baseChange_pullbackPushforwardUnit_of_relativeAssassin_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningInjective.lean, line 102. The attribute's comment: “after arbitrary base change”.

Stacks Project, Tag 05PD. The canonical map of the preceding statement remains injective after an arbitrary base change h : T ⟶ S: the map F_T ⟶ (g_T)_* (g_T)^* F_T on X ×_S T is injective as well.

theorem mono_baseChange_pullbackPushforwardUnit_of_relativeAssassin_subset_range
    {X' X S : Scheme.{u}} (f : X ⟶ S) (g : X' ⟶ X)
    [LocallyOfFiniteType f] [Flat g]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hF : IsFlatOver f.toLRSHom.toShHom F)
    (hAss : Stacks.Divisors.relativeAssassin f F ⊆ Set.range g.base) :
    ∀ (T : Scheme.{u}) (h : T ⟶ S),
      Mono ((Scheme.Modules.pullbackPushforwardAdjunction (compBaseChangeMap f g h)).unit.app
        ((Scheme.Modules.pullback (pullback.fst f h)).obj F))

Tag 05PE, a lemma

Tag 05PE in the Stacks Project.

Module.exists_ideal_bijective_rTensor_iff_map_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/VanishingAfterBaseChange.lean, line 91.

Stacks Project, Tag 05PE. A surjection from a projective module has a flattening ideal: after every base change, the map is an isomorphism exactly when the image of this ideal vanishes.

theorem exists_ideal_bijective_rTensor_iff_map_eq_bot
    (u : M →ₗ[A] N) (hu : Function.Surjective u) [Module.Projective A M] :
    ∃ I : Ideal A, ∀ (B : Type*) [CommRing B] [Algebra A B],
      Function.Bijective (u.rTensor B) ↔ Ideal.map (algebraMap A B) I = ⊥

Tag 05PF, a theorem

Tag 05PF in the Stacks Project.

Stacks.Flatness.exists_closedImmersion_representableBy_isomorphismFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/EtaleLocalRepresentability.lean, line 638. The attribute's comment: “representability by a closed immersion”.

Stacks Project, Tag 05PF, first assertion. Let f : X ⟶ S be of finite presentation and let u : F ⟶ G be a surjection of quasi-coherent modules on X with F of finite presentation, flat over S and pure relative to S. Then the locus where u becomes an isomorphism after base change is represented by a closed immersion into S.

The source's devissage: purity reduces the question, étale locally on S, to an affine situation whose module of sections is projective, where the locus is cut out by the flattening ideal of Tag 05PE; the étale base changes cover S in the fpqc topology and the functor is an fpqc sheaf, so the local closed subschemes glue.

theorem exists_closedImmersion_representableBy_isomorphismFunctor
    (D : ModuleMapBaseChangeSituation.{u})
    [LocallyOfFinitePresentation D.f] [QuasiCompact D.f] [QuasiSeparated D.f]
    [D.F.IsFinitePresentation] [D.F.IsFiniteType] [Epi D.hom]
    (hflat : IsFlatOver D.f.toLRSHom.toShHom D.F)
    (hpure : AlgebraicGeometry.IsPureRelative D.f D.F) :
    ∃ W : Over D.S, IsClosedImmersion W.hom ∧
      Nonempty (D.isomorphismFunctor.RepresentableBy W)

Stacks.Flatness.isomorphismFunctor_representableBy_closedImmersion_of_affineTests, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/IsoLocusAffineTests.lean, line 121. The attribute's comment: “representability by a closed immersion”.

Stacks Project, Tag 05PF. The isomorphism-after-base-change functor of a surjection from a finitely presented, flat and pure module is represented by a closed immersion into the base.

The representing closed subscheme is cut out by an ideal sheaf which it suffices to exhibit on affine schemes over the base, by Stacks.Flatness.ModuleMapBaseChangeSituation.isFlatteningIdeal_of_isFlatteningIdealOnAffines; étale localization on the base reduces the construction to an affine situation whose module of sections is projective, where the ideal sheaf is the flattening ideal of Tag 05PE. That devissage is Stacks.Flatness.exists_closedImmersion_representableBy_isomorphismFunctor.

theorem isomorphismFunctor_representableBy_closedImmersion_of_affineTests
    (D : ModuleMapBaseChangeSituation.{u})
    [LocallyOfFinitePresentation D.f] [QuasiCompact D.f] [QuasiSeparated D.f]
    [D.F.IsFinitePresentation] [D.F.IsFiniteType] [Epi D.hom]
    (hflat : IsFlatOver D.f.toLRSHom.toShHom D.F)
    (hpure : IsPureRelative D.f D.F) :
    ∃ W : Over D.S, IsClosedImmersion W.hom ∧
      Nonempty (D.isomorphismFunctor.RepresentableBy W)

Stacks.Flatness.finitePresentation_hom_of_representableBy_isomorphismFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/IsoLocusAffineTests.lean, line 147. The attribute's comment: “finite presentation of the representing closed immersion”.

Stacks Project, Tag 05PF. A closed immersion Z ⟶ S representing the isomorphism-after-base-change functor is of finite presentation as soon as the target module G is of finite presentation.

Local finite presentation is Tag 01ZC: by Tag 05MJ(4) the isomorphism functor turns a cofiltered inverse limit of affine schemes over the base into a filtered colimit, so the functor of points of Z is limit preserving in the sense of Tag 05LX. Quasi-compactness holds because a closed immersion is an affine morphism, and quasi-separatedness because the functor is subterminal, so that Z ⟶ S is a monomorphism.

The hypotheses are about the morphism i at hand, and they are satisfiable: a closed immersion representing the functor exists under the source's own hypotheses, by Stacks.Flatness.isomorphismFunctor_representableBy_closedImmersion_of_affineTests. Stating the assertion for an arbitrary representative rather than for that one is no weaker, since any two representatives of a functor are isomorphic over the base.

theorem finitePresentation_hom_of_representableBy_isomorphismFunctor
    (D : ModuleMapBaseChangeSituation.{u}) [QuasiCompact D.f]
    [D.F.IsFiniteType] [D.G.IsFinitePresentation]
    {Z : Scheme.{u}} (i : Z ⟶ D.S) [IsClosedImmersion i]
    (e : D.isomorphismFunctor.RepresentableBy (Over.mk i)) :
    FinitePresentation i

Stacks.Flatness.isomorphismFunctor_representableBy_closedImmersion_of_projective_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/IsoLocusProjectiveSections.lean, line 419. The attribute's comment: “representability by a closed immersion, for an affine situation whose source module has projective global sections: this is the terminal case of the source's devissage, Step 4 of its proof together with Tag 05PE. The étale localization of Steps 1-3, which reduces the general case to this one, is Stacks.Flatness.exists_closedImmersion_representableBy_isomorphismFunctor”. References: SGA 3 VIB (6.2.3), “(i), special case”; SGA 3 VIII (6.4), “special case”.

Stacks Project, Tag 05PF. The isomorphism-after-base-change functor of a surjection u : F ⟶ G of quasi-coherent modules on an affine scheme X over an affine base S, whose source has projective module of global sections over Γ(S, 𝒪_S), is represented by a closed immersion Z ⟶ S.

This is the situation in which the devissage of the source's proof terminates: the representing closed subscheme is cut out by the ideal of Γ(S, 𝒪_S) supplied by Tag 05PE, which after every base change vanishes exactly when u becomes an isomorphism. The hypotheses of the source — that f and F be of finite presentation and that F be flat and pure relative to S — are what the source's étale localization uses to reduce the general case to this one; they are not needed once the situation is affine with projective sections, and are therefore absent here.

theorem isomorphismFunctor_representableBy_closedImmersion_of_projective_sections
    (D : ModuleMapBaseChangeSituation.{u}) [IsAffine D.X] [IsAffine D.S] [Epi D.hom]
    (hproj : letI : Module Γ(D.S, ⊤) Γ(D.F, ⊤) := Module.compHom Γ(D.F, ⊤) D.f.appTop.hom
      Module.Projective Γ(D.S, ⊤) Γ(D.F, ⊤)) :
    ∃ W : Over D.S, IsClosedImmersion W.hom ∧
      Nonempty (D.isomorphismFunctor.RepresentableBy W)

Tag 07AI, a lemma

Tag 07AI in the Stacks Project.

Stacks.Flatness.weilRestriction_representableBy_closedImmersion_of_affineTests, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/WeilRestriction.lean, line 434. The attribute's comment: “representability by a closed immersion”.

Stacks Project, Tag 07AI. The Weil restriction f_* Y of a closed subscheme Y of X along a morphism f : X ⟶ S which is of finite presentation, flat and pure is represented by a closed immersion Z ⟶ S.

By the equivalence Stacks.Flatness.WeilRestriction.isIsomorphismAfterBaseChange_iff_isIso_closedSubschemeBaseChange the functor is the isomorphism functor of the surjection u : 𝒪_X ⟶ 𝒪_X/I cutting out Y, whose hypotheses in Tag 05PF are exactly the ones assumed here: 𝒪_X is of finite type and of finite presentation over itself, it is flat over S because f is flat, and it is pure relative to S because X is.

theorem weilRestriction_representableBy_closedImmersion_of_affineTests
    (i : Y ⟶ X) (f : X ⟶ S) [IsClosedImmersion i]
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f] [Flat f]
    (hpure : AlgebraicGeometry.IsSchemePureRelative f) :
    ∃ W : Over S, IsClosedImmersion W.hom ∧
      Nonempty ((weilRestrictionFunctor i f).RepresentableBy W)

Stacks.Flatness.finitePresentation_hom_of_representableBy_weilRestrictionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/WeilRestriction.lean, line 469. The attribute's comment: “finite presentation of the representing closed immersion”. References: SGA 3 VIB (6.2.3), “(ii)”; SGA 3 VIB (6.5.2), “special case”; SGA 3 XI (6.8), “special case”.

Stacks Project, Tag 07AI. If the closed subscheme Y is of finite presentation over S, every closed immersion representing the Weil restriction f_* Y is of finite presentation.

The quotient 𝒪_X/I is then of finite presentation, by Tag 01TV and Stacks.Flatness.WeilRestriction.isFinitePresentation_pushforwardUnit, which is the hypothesis Tag 05PF's second assertion needs; the assertion itself is Stacks.Flatness.finitePresentation_hom_of_representableBy_isomorphismFunctor, and needs no flattening ideal. Unlike the first assertion this one constructs no representative: it applies to any representing closed immersion, and such a one exists by the first assertion.

theorem finitePresentation_hom_of_representableBy_weilRestrictionFunctor
    (i : Y ⟶ X) (f : X ⟶ S) [IsClosedImmersion i]
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (hY : AlgebraicGeometry.FinitePresentation (i ≫ f))
    {Z : Scheme.{u}} (p : Z ⟶ S) [AlgebraicGeometry.IsClosedImmersion p]
    (e : (weilRestrictionFunctor i f).RepresentableBy (Over.mk p)) :
    AlgebraicGeometry.FinitePresentation p

Sources

• Section 38.23, Tag 05PC
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.mono_pullbackPushforwardUnit_of_relativeAssassin_subset_range · AlgebraicGeometry.mono_baseChange_pullbackPushforwardUnit_of_relativeAssassin_subset_range · Module.exists_ideal_bijective_rTensor_iff_map_eq_bot · Stacks.Flatness.exists_closedImmersion_representableBy_isomorphismFunctor · Stacks.Flatness.isomorphismFunctor_representableBy_closedImmersion_of_affineTests · Stacks.Flatness.finitePresentation_hom_of_representableBy_isomorphismFunctor · Stacks.Flatness.isomorphismFunctor_representableBy_closedImmersion_of_projective_sections · Stacks.Flatness.weilRestriction_representableBy_closedImmersion_of_affineTests

Section38.24 Flattening in the local case#

Section 38.24 of the Stacks Project, Tag 05MZ. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05PG, a theorem

Tag 05PG in the Stacks Project.

Module.FlatAtPointSituation.exists_ideal_condition_iff_map_eq_bot_of_henselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/HenselianFlatteningTheorem.lean, line 88.

Stacks Project, Tag 05PG. Let A → B be a local homomorphism of local rings with A henselian and B essentially of finite type over A, and let M be a finite B-module. There is an ideal I ⊆ A such that A ⧸ I corepresents the functor F_lf of Stacks Tag 05MK: for every local A-algebra A' with local structure map, the base change of M is flat over A' at every prime of B ⊗_A A' containing the extensions of the maximal ideals of A' and of B exactly when I dies in A'. If B is essentially of finite presentation over A and M is of finite presentation over B, then I is finitely generated.

theorem exists_ideal_condition_iff_map_eq_bot_of_henselian
    (S : FlatAtPointSituation.{u, v, w}) [HenselianLocalRing S.A]
    [Algebra.EssFiniteType S.A S.B] [Module.Finite S.B S.M] :
    ∃ I : Ideal S.A,
      (∀ R : LocalAlgCat.{u, x} S.A, S.Condition R ↔ Ideal.map (algebraMap S.A R) I = ⊥) ∧
      ((algebraMap S.A S.B).EssentiallyOfFinitePresentation →
        Module.FinitePresentation S.B S.M → I.FG)

Tag 05PH, a remark

Tag 05PH in the Stacks Project.

AlgebraicGeometry.exists_closedSubscheme_flatOverAt_iff_factorStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/LocalFlatteningSubscheme.lean, line 232. The attribute's comment: “the local flattening subscheme”.

Stacks Project, Tag 05PH. A closed subscheme detects flatness of the pulled-back module at every point of the distinguished fibre lying above x.

theorem exists_closedSubscheme_flatOverAt_iff_factorStalk
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (x : X) (s : S) (hxs : f x = s)
    [HenselianLocalRing (S.presheaf.stalk s)]
    [IsIso (S.fromSpecStalk s)] :
    ∃ I : S.IdealSheafData,
      ∀ {T : Scheme.{u}} (g : T ⟶ S) (t : T) (_ht : g t = s),
        (∀ y : pullback (C := Scheme.{u}) f g,
            (pullback.snd f g y = t) →
            (pullback.fst f g y = x) →
              AlgebraicGeometry.IsFlatOverAt
                (pullback.snd f g).toLRSHom.toShHom
                ((Scheme.Modules.pullback (pullback.fst f g)).obj F) y) ↔
          ∃ h : Spec (T.presheaf.stalk t) ⟶ I.subscheme,
            h ≫ I.subschemeι = T.fromSpecStalk t ≫ g

AlgebraicGeometry.exists_finitePresentation_closedSubscheme_flatOverAt_iff_factorStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/LocalFlatteningSubscheme.lean, line 351. The attribute's comment: “finite-presentation refinement”.

Stacks Project, Tag 05PH. Under pointwise finite-presentation hypotheses, the local flattening subscheme can be finitely presented.

theorem exists_finitePresentation_closedSubscheme_flatOverAt_iff_factorStalk
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (x : X) (s : S) (hxs : f x = s)
    [HenselianLocalRing (S.presheaf.stalk s)]
    [IsIso (S.fromSpecStalk s)]
    (hfp : FinitePresentationAt f x)
    (hFfp :
      letI : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) F.val x
      Module.FinitePresentation (X.presheaf.stalk x)
        (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x)) :
    ∃ I : S.IdealSheafData,
      FinitePresentation I.subschemeι ∧
      ∀ {T : Scheme.{u}} (g : T ⟶ S) (t : T) (_ht : g t = s),
        (∀ y : pullback (C := Scheme.{u}) f g,
            (pullback.snd f g y = t) →
            (pullback.fst f g y = x) →
              AlgebraicGeometry.IsFlatOverAt
                (pullback.snd f g).toLRSHom.toShHom
                ((Scheme.Modules.pullback (pullback.fst f g)).obj F) y) ↔
          ∃ h : Spec (T.presheaf.stalk t) ⟶ I.subscheme,
            h ≫ I.subschemeι = T.fromSpecStalk t ≫ g

Tag 05PI, a lemma

Tag 05PI in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_closedSubscheme_flatOverAt_iff_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ClosedFibreFlatteningFinitePresentation.lean, line 154. The attribute's comment: “finite-presentation refinement”.

Stacks Project, Tag 05PI. When the morphism and the module are in addition locally of finite presentation and the chosen subset of the closed fibre is closed and quasi-compact, the closed subscheme of the henselian local base detecting flatness along that subset can be chosen of finite presentation.

theorem exists_finitePresentation_closedSubscheme_flatOverAt_iff_factors
    (A : Type u) [CommRing A] [HenselianLocalRing A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f]
    [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    [F.IsFinitePresentation]
    (E : Set (f.fiber (IsLocalRing.closedPoint A)))
    (_ : IsClosed E) (hEcompact : IsCompact E) :
    ∃ I : (Spec (.of A)).IdealSheafData,
      FinitePresentation I.subschemeι ∧
      ∀ (T : Scheme.{u}) (g : T ⟶ Spec (.of A)) (t : T)
        (_ : g t = IsLocalRing.closedPoint A),
        (∀ y : (pullback f g : Scheme.{u}),
          (pullback.snd f g) y = t →
          (pullback.fst f g) y ∈
            (f.fiberι (IsLocalRing.closedPoint A)) '' E →
          AlgebraicGeometry.IsFlatOverAt (pullback.snd f g).toLRSHom.toShHom
            ((Scheme.Modules.pullback (pullback.fst f g)).obj F) y) ↔
        ∃ h : Spec (T.presheaf.stalk t) ⟶ I.subscheme,
          h ≫ I.subschemeι = T.fromSpecStalk t ≫ g

AlgebraicGeometry.exists_closedSubscheme_flatOverAt_iff_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ClosedFibreFlatteningSubscheme.lean, line 70. The attribute's comment: “closed flattening subscheme”.

Stacks Project, Tag 05PI. Flatness of a finite type quasi-coherent module along an arbitrary subset E of the closed fibre, after an arbitrary pointed base change of a henselian local base, is detected by a closed subscheme of that base: the flatness condition for a pointed scheme (T, t) over (Spec A, closed point) holds exactly when Spec O_{T,t} ⟶ Spec A factors through the closed subscheme.

theorem exists_closedSubscheme_flatOverAt_iff_factors
    (A : Type u) [CommRing A] [HenselianLocalRing A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (E : Set (f.fiber (IsLocalRing.closedPoint A))) :
    ∃ I : (Spec (.of A)).IdealSheafData,
      ∀ (T : Scheme.{u}) (g : T ⟶ Spec (.of A)) (t : T)
        (_ : g t = IsLocalRing.closedPoint A),
        (∀ y : (pullback f g : Scheme.{u}),
          (pullback.snd f g) y = t →
          (pullback.fst f g) y ∈
            (f.fiberι (IsLocalRing.closedPoint A)) '' E →
          AlgebraicGeometry.IsFlatOverAt (pullback.snd f g).toLRSHom.toShHom
            ((Scheme.Modules.pullback (pullback.fst f g)).obj F) y) ↔
        ∃ h : Spec (T.presheaf.stalk t) ⟶ I.subscheme,
          h ≫ I.subschemeι = T.fromSpecStalk t ≫ g

Tag 052G, a remark

Tag 052G in the Stacks Project.

AlgebraicGeometry.exists_idealSheafData_forall_isFlatOverAt_iff_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/CompleteLocalFlattening.lean, line 311. The attribute's comment: “the closed subscheme of Lemma 05PI for E = X_s over a Noetherian complete local base, constructed from finite affine charts and Lemma 0528”.

Stacks Project, Tag 052G. Let S = Spec A be the spectrum of a Noetherian complete local ring with closed point s, let f : X ⟶ S be of finite type and let F be a quasi-coherent 𝒪_X-module of finite type. Then the closed subscheme Z ⊆ S of Lemma 05PI for E = X_s exists: for every morphism of pointed schemes (T, t) ⟶ (S, s), the pulled back module F_T is flat over T at every point of the fibre X_t if and only if Spec(𝒪_{T,t}) ⟶ S factors through Z. As the remark explains, the proof is elementary: a finite affine open cover reduces to X affine, where Z is cut out by the least flattening ideal of More on Algebra, Lemma 0526, whose universal property is Lemma 0528.

theorem exists_idealSheafData_forall_isFlatOverAt_iff_of_isAdicComplete
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f] [QuasiCompact f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] :
    ∃ Z : (Spec (.of A)).IdealSheafData,
      ∀ (T : Scheme.{u}) (g : T ⟶ Spec (.of A)) (t : T),
        g t = IsLocalRing.closedPoint A →
        ((∀ y : (pullback f g : Scheme.{u}), pullback.snd f g y = t →
            IsFlatOverAt (pullback.snd f g).toLRSHom.toShHom
              ((Scheme.Modules.pullback (pullback.fst f g)).obj F) y) ↔
          ∃ h : Spec (T.presheaf.stalk t) ⟶ Z.subscheme,
            h ≫ Z.subschemeι = T.fromSpecStalk t ≫ g)

Sources

• Section 38.24, Tag 05MZ
• AxiomMath/Stacks at 5ed82d14

LeanModule.FlatAtPointSituation.exists_ideal_condition_iff_map_eq_bot_of_henselian · AlgebraicGeometry.exists_closedSubscheme_flatOverAt_iff_factorStalk · AlgebraicGeometry.exists_finitePresentation_closedSubscheme_flatOverAt_iff_factorStalk · AlgebraicGeometry.exists_finitePresentation_closedSubscheme_flatOverAt_iff_factors · AlgebraicGeometry.exists_closedSubscheme_flatOverAt_iff_factors · AlgebraicGeometry.exists_idealSheafData_forall_isFlatOverAt_iff_of_isAdicComplete

Section38.25 Variants of a lemma#

Section 38.25 of the Stacks Project, Tag 0ASZ. 14 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AT0, a situation

Tag 0AT0 in the Stacks Project.

AlgebraicGeometry.InjectiveModuloMaximalIdealSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/MaximalIdealInjectivity.lean, line 60.

The standing data and hypotheses of Stacks Project, Tag 0AT0: a local homomorphism A → B of local rings which is essentially of finite type, a flat A-module M, a finite B-module N, and an A-linear map N → M which is injective modulo the maximal ideal of A.

structure InjectiveModuloMaximalIdealSituation

Tag 0AT1, a lemma

Tag 0AT1 in the Stacks Project.

AlgebraicGeometry.universallyInjective_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/MaximalIdealInjectivity.lean, line 152. The attribute's comment: “universal injectivity”.

Stacks Project, Tag 0AT1. In Situation 0AT0 over a Noetherian base, the given map is universally injective over the base ring.

theorem universallyInjective_of_isNoetherianRing
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    [IsNoetherianRing S.A] : UniversallyInjectivePoly S.u

AlgebraicGeometry.flat_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/MaximalIdealInjectivity.lean, line 161. The attribute's comment: “flatness”.

Stacks Project, Tag 0AT1. In Situation 0AT0 over a Noetherian base, the source module is flat over the base ring.

theorem flat_of_isNoetherianRing
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    [IsNoetherianRing S.A] : Module.Flat S.A S.N

Declarations registered for the tag:

• Module.finitePresentation_of_finite registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/MaximalIdealInjectivity.lean, line 124 (StacksFrontier): “finite presentation”. References: EGA 0 (1.0.5), “more general”; EGA 0 (1.3.5), “more general”.

Tag 0AT2, a lemma

Tag 0AT2 in the Stacks Project.

AlgebraicGeometry.universallyInjective_of_localizedPolynomial_cases, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/PolynomialLocalizationReduction.lean, line 546. The attribute's comment: “universal injectivity”.

Universal injectivity in Situation 0AT0 reduces to the case of a localization of a finite polynomial algebra with finitely presented source module.

theorem universallyInjective_of_localizedPolynomial_cases
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    (h : ∀ (T : InjectiveModuloMaximalIdealSituation.{u₁, max u₁ u₂, u₃, max u₁ u₂ u₄}),
      SameBaseLocalRing S T → PolynomialLocalizationPresentation T.A T.B →
        Module.FinitePresentation T.B T.N →
          InjectiveModuloMaximalIdealConclusion.{max u₁ u₅} T) :
    UniversallyInjectivePoly.{_, u₅} S.u

AlgebraicGeometry.finitePresentation_of_localizedPolynomial_cases, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/PolynomialLocalizationReduction.lean, line 558. The attribute's comment: “finite presentation”.

Finite presentation in Situation 0AT0 reduces to the case of a localization of a finite polynomial algebra with finitely presented source module.

theorem finitePresentation_of_localizedPolynomial_cases
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    (h : ∀ (T : InjectiveModuloMaximalIdealSituation.{u₁, max u₁ u₂, u₃, max u₁ u₂ u₄}),
      SameBaseLocalRing S T → PolynomialLocalizationPresentation T.A T.B →
        Module.FinitePresentation T.B T.N →
          InjectiveModuloMaximalIdealConclusion.{max u₁ u₅} T) :
    Module.FinitePresentation S.B S.N

AlgebraicGeometry.flat_of_localizedPolynomial_cases, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/PolynomialLocalizationReduction.lean, line 570. The attribute's comment: “flatness”.

Flatness in Situation 0AT0 reduces to the case of a localization of a finite polynomial algebra with finitely presented source module.

theorem flat_of_localizedPolynomial_cases
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    (h : ∀ (T : InjectiveModuloMaximalIdealSituation.{u₁, max u₁ u₂, u₃, max u₁ u₂ u₄}),
      SameBaseLocalRing S T → PolynomialLocalizationPresentation T.A T.B →
        Module.FinitePresentation T.B T.N →
          InjectiveModuloMaximalIdealConclusion.{max u₁ u₅} T) :
    Module.Flat S.A S.N

Tag 0AT3, a lemma

Tag 0AT3 in the Stacks Project.

AlgebraicGeometry.injectiveModuloMaximalIdealConclusion_of_henselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/HenselianBase.lean, line 273.

Stacks Project, Tag 0AT3. In Situation 0AT0 with A henselian the lemma holds: if A → B is a local homomorphism of local rings essentially of finite type, M is a flat A-module, N is a finite B-module and u : N → M is an A-linear map whose reduction N/𝔪_A N → M/𝔪_A M is injective, then u is A-universally injective, N is of finite presentation over B, and N is flat over A.

theorem injectiveModuloMaximalIdealConclusion_of_henselianLocalRing
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄}) [HenselianLocalRing S.A] :
    InjectiveModuloMaximalIdealConclusion.{u₅} S

Tag 0AT4, a lemma

Tag 0AT4 in the Stacks Project.

AlgebraicGeometry.universallyInjective_and_finitePresentation_and_flat_of_linearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/HenselizationReduction.lean, line 322. The attribute's comment: “N/𝔪_A N → M/𝔪_A M is the Submodule.mapQ of u for 𝔪_A • ⊤, and A-universal injectivity is UniversallyInjectivePoly of u with scalars restricted to A.”.

Stacks Project, Tag 0AT4. Let A → B be a local homomorphism of local rings which is essentially of finite type and let u : N → M be a B-linear map. If N is a finite B-module, M is flat over A, and the induced map N/𝔪_A N → M/𝔪_A M is injective, then u is universally injective over A, N is finitely presented over B, and N is flat over A.

This is HenselizationReduction.conclusions_of_henselian_cases applied to the henselian case Stacks 0AT3, injectiveModuloMaximalIdealConclusion_of_henselianLocalRing.

theorem universallyInjective_and_finitePresentation_and_flat_of_linearMap
    {A : Type u₁} {B : Type u₂} {M : Type u₃} {N : Type u₄}
    [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B] [Algebra A B]
    [IsLocalHom (algebraMap A B)] [Algebra.EssFiniteType A B]
    [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Flat A M]
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N] [Module.Finite B N]
    (u : N →ₗ[B] M)
    (hu : Function.Injective (Submodule.mapQ (maximalIdeal A • (⊤ : Submodule A N))
      (maximalIdeal A • (⊤ : Submodule A M)) (u.restrictScalars A)
      (Submodule.smul_top_le_comap_smul_top (maximalIdeal A) (u.restrictScalars A)))) :
    UniversallyInjectivePoly.{_, w} (u.restrictScalars A) ∧ Module.FinitePresentation B N ∧
      Module.Flat A N

Tag 0AT5, a lemma

Tag 0AT5 in the Stacks Project.

AlgebraicGeometry.flat_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ValuationRingBase.lean, line 241. The attribute's comment: “the flatness assertion of the lemma' for Situation 0AT0: in Situation 0AT0 withAa valuation ring,Nis flat overA. Proved from 0AT0's own hypotheses together withValuationRing A`.”.

Stacks Project, Tag 0AT5 (flatness). In Situation 0AT0 with the base ring A a valuation ring, the finite B-module N is flat over A.

theorem flat_of_valuationRing
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    [IsDomain S.A] [ValuationRing S.A] : Module.Flat S.A S.N

AlgebraicGeometry.finitePresentation_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ValuationRingBase.lean, line 252. The attribute's comment: “the finite-presentation assertion of the lemma' for Situation 0AT0: in Situation 0AT0 withAa valuation ring,Nis of finite presentation overB. Proved from 0AT0's own hypotheses together withValuationRing A`.”.

Stacks Project, Tag 0AT5 (finite presentation). In Situation 0AT0 with the base ring A a valuation ring, the finite B-module N is of finite presentation over B.

theorem finitePresentation_of_valuationRing
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄})
    [IsDomain S.A] [ValuationRing S.A] : Module.FinitePresentation S.B S.N

Tag 0AT6, an equation

Tag 0AT6 in the Stacks Project.

AlgebraicGeometry.FinitelyPresentedLocalizedModuleSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/LocalizedModuleSpreadout.lean, line 60.

Stacks Project, Tag 0AT6. The standing situation of a finitely presented algebra B over A, a multiplicative subset S ⊆ B, and a finitely presented module over a localization of B at S.

structure FinitelyPresentedLocalizedModuleSituation

Tag 0AT7, a lemma

Tag 0AT7 in the Stacks Project.

AlgebraicGeometry.exists_isContentIdeal_of_pureSpreadout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ContentIdeals.lean, line 125. The attribute's comment: “content_ideals”.

Stacks Project, Tag 0AT7. If a pure spreadout exists, every element of the localized module has a content ideal over the base ring.

theorem exists_isContentIdeal_of_pureSpreadout
    (X : FinitelyPresentedLocalizedModuleSituation.{u₁, u₂, u₃, u₄})
    (hspread : Nonempty (PureSpreadout.{u₁, u₂, u₃, u₄, u₁} X)) (x : X.N) :
    ∃ I : Ideal X.A, IsContentIdeal x I

AlgebraicGeometry.universallyInjective_of_injective_mod_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/UniversalInjectivity.lean, line 312. The attribute's comment: “universal_injectivity”.

Stacks Project, Tag 0AT7 (universal injectivity). A map into a flat module which is injective modulo each maximal ideal is universally injective, provided the distinguished localized module admits a pure spreadout.

theorem universallyInjective_of_injective_mod_maximalIdeal
    (X : FinitelyPresentedLocalizedModuleSituation.{u₁, u₂, u₃, u₄})
    (hspread : Nonempty (PureSpreadout.{u₁, u₂, u₃, u₄, u₄} X))
    {M : Type u₄} [AddCommGroup M] [Module X.A M] [Module.Flat X.A M]
    (u : X.N →ₗ[X.A] M)
    (hu : ∀ (m : Ideal X.A) [m.IsMaximal],
      Function.Injective
        (Submodule.mapQ (m • (⊤ : Submodule X.A X.N))
          (m • (⊤ : Submodule X.A M)) u
          (Submodule.smul_top_le_comap_smul_top m u))) :
    UniversallyInjective u

Tag 0AT8, a lemma

Tag 0AT8 in the Stacks Project.

AlgebraicGeometry.FinitelyPresentedLocalizedModuleSituation.exists_fg_ideal_localQuotientBaseChange_pureSpreadout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/PureSpreadoutQuotient.lean, line 495.

Stacks Project, Tag 0AT8. In the standing situation of Stacks 0AT6, for every prime 𝔭 of the base ring there is a finitely generated ideal I of the local ring A_𝔭, contained in the extension of 𝔭, such that the base change of the situation to A_𝔭 ⧸ I carries a pure spreadout.

The test-module universe of the universal injectivity packaged in the pure spreadout is left free, so the statement instantiates at any test universe.

theorem exists_fg_ideal_localQuotientBaseChange_pureSpreadout (p : Ideal X.A) [p.IsPrime] :
    ∃ I : Ideal (Localization.AtPrime p), I.FG ∧
      I ≤ p.map (algebraMap X.A (Localization.AtPrime p)) ∧
      ∃ Y : FinitelyPresentedLocalizedModuleSituation.{u₁, max u₁ u₂, max u₁ u₃,
          max u₁ (max u₃ u₄)},
        Nonempty (LocalQuotientBaseChange X Y p I) ∧
          Nonempty (PureSpreadout.{u₁, max u₁ u₂, max u₁ u₃, max u₁ (max u₃ u₄), u₅} Y)

Tag 0AT9, a lemma

Tag 0AT9 in the Stacks Project.

AlgebraicGeometry.universallyInjective_of_rTensor_residueField_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/PureSpreadoutQuotient.lean, line 531.

Stacks Project, Tag 0AT9, unconditionally. In the finitely presented localized-module situation, a linear map between flat modules which is injective on every residue-field fibre is universally injective.

This is AlgebraicGeometry.universallyInjective_of_rTensor_residueField_injective_of_pureSpreadout with its hAT8 hypothesis discharged by Stacks 0AT8, instantiated at the test-module universe that binder pins.

theorem universallyInjective_of_rTensor_residueField_injective
    (X : FinitelyPresentedLocalizedModuleSituation.{u₁, u₂, u₃, u₄})
    {M : Type u₄} [AddCommGroup M] [Module X.A M]
    [Module.Flat X.A X.N] [Module.Flat X.A M]
    (u : X.N →ₗ[X.A] M)
    (hu : ∀ (p : Ideal X.A) [p.IsPrime],
      Function.Injective (u.rTensor p.ResidueField)) :
    UniversallyInjective u

Tag 0ATA, a lemma

Tag 0ATA in the Stacks Project.

PrimeSpectrum.sInf_eq_bot_of_iUnion_zeroLocus_eq_compl_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ZeroLocusOnLocalSpectrum.lean, line 61.

Stacks Project, Tag 0ATA. A multiplicatively closed collection of finitely generated ideals whose zero loci cover every non-generic point of the spectrum of a local domain has zero intersection.

theorem sInf_eq_bot_of_iUnion_zeroLocus_eq_compl_genericPoint
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    (hA : ¬ IsField A) (S : Set (Ideal A))
    (hSfg : ∀ I ∈ S, I.FG)
    (hSmul : ∀ I ∈ S, ∀ J ∈ S, I * J ∈ S)
    (hcover : (⋃ I ∈ S, PrimeSpectrum.zeroLocus (I : Set A)) =
      {p : PrimeSpectrum A | p.asIdeal ≠ ⊥}) :
    sInf S = ⊥

Tag 0ATB, a lemma

Tag 0ATB in the Stacks Project.

PrimeSpectrum.closedPoints_compl_zeroLocus_subset_zeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ZeroLocusOnLocalSpectrum.lean, line 155.

Stacks Project, Tag 0ATB. If J is a proper finitely generated ideal of a local ring and I is contained in every positive power of J, then V(I) contains every closed point of Spec(A) \ V(J).

theorem closedPoints_compl_zeroLocus_subset_zeroLocus
    {A : Type u} [CommRing A] [IsLocalRing A] (I J : Ideal A)
    (hJ : J ≠ ⊤) (hJfg : J.FG)
    (hIJ : ∀ n : ℕ, 0 < n → I ≤ J ^ n) :
    Subtype.val '' closedPoints
        ((PrimeSpectrum.zeroLocus (J : Set A))ᶜ : Set (PrimeSpectrum A)) ⊆
      PrimeSpectrum.zeroLocus (I : Set A)

Tag 0ATC, a lemma

Tag 0ATC in the Stacks Project.

AlgebraicGeometry.smallerFlatnessIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/FlatnessIdeal.lean, line 67. The attribute's comment: “the ideal I₂”.

The ideal I₂ = Ker (I → Γ(U, (I/I²)~)) of A, for an ideal I of A and an open U ⊆ Spec A: the image in A of the kernel of the composite of I → I/I² with the map taking a global conormal class to its sections over U.

def smallerFlatnessIdeal {A : Type u} [CommRing A]
    (I : Ideal A) (U : (Spec (.of A)).Opens) : Ideal A

AlgebraicGeometry.flat_quotient_smallerFlatnessIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/FlatnessIdeal.lean, line 330. The attribute's comment: “flatness modulo I₂”.

Stacks Project, Tag 0ATC. Let I be an ideal of a commutative ring A and let U ⊆ Spec A be a quasi-compact open. If M/IM is flat over A/I and M~ is flat on U, then M/I₂M is flat over A/I₂, where I₂ = Ker (I → Γ(U, (I/I²)~)).

The source assumes A local; locality is not used.

theorem flat_quotient_smallerFlatnessIdeal
    {A : Type u} [CommRing A]
    {M : Type u} [AddCommGroup M] [Module A M]
    (I : Ideal A) (U : (Spec (.of A)).Opens)
    (hU : IsCompact U.1)
    (hquot : Module.Flat (A ⧸ I) (M ⧸ I • (⊤ : Submodule A M)))
    (hflat : SheafOfModules.IsFlat.{u, u, u, u} (O := (U : Scheme).sheaf)
      (show (U : Scheme).Modules from
        (tilde (ModuleCat.of A M)).restrict U.ι)) :
    Module.Flat (A ⧸ smallerFlatnessIdeal I U)
      (M ⧸ smallerFlatnessIdeal I U • (⊤ : Submodule A M))

Stacks.flat_quotient_sectionsKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatteningSectionsKernel.lean, line 132.

Let I ⊆ A be an ideal, M an A-module and U = ⋃ i, D(f i) a quasi-compact open of Spec A. If M/IM is flat over A/I and M is flat over U, that is M_{f i} is flat over A_{f i} for each i, then M/I₂M is flat over A/I₂, where I₂ = Ker (I → Γ(U, I/I²)) is sectionsKernel I f.

theorem flat_quotient_sectionsKernel (I : Ideal A) {ι : Type w} [Finite ι] (f : ι → A)
    (hI : Module.Flat (A ⧸ I) (M ⧸ I • (⊤ : Submodule A M)))
    (hU : ∀ i, Module.Flat (Localization.Away (f i)) (Localization.Away (f i) ⊗[A] M)) :
    Module.Flat (A ⧸ sectionsKernel I f)
      (M ⧸ sectionsKernel I f • (⊤ : Submodule A M))

Tag 05U9, a proposition

Tag 05U9 in the Stacks Project.

AlgebraicGeometry.conclusion_of_injectiveModuloMaximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/NilpotentFlatteningClaimOneIndex.lean, line 283. The attribute's comment: “universal injectivity, finite presentation and flatness”.

Stacks Project, Tag 05U9. Let A → B be a local homomorphism of local rings which is essentially of finite type, let M be a flat A-module, let N be a finite B-module and let u : N → M be an A-linear map whose reduction ū : N ⧸ 𝔪_AN → M ⧸ 𝔪_AM is injective. Then

1. u is A-universally injective,
2. N is of finite presentation over B, and
3. N is flat over A.

The hypotheses are the data of Situation 0AT0 (AlgebraicGeometry.InjectiveModuloMaximalIdealSituation) and the three conclusions are AlgebraicGeometry.InjectiveModuloMaximalIdealConclusion.

Stacks 0AT2 reduces all three to the case where B is a localization at a prime of a polynomial algebra over A in finitely many variables and N is of finite presentation over B, and AlgebraicGeometry.conclusion_of_presentation settles that case through Claim 1 of the source's proof.

theorem conclusion_of_injectiveModuloMaximalIdeal
    (S : InjectiveModuloMaximalIdealSituation.{u₁, u₂, u₃, u₄}) :
    InjectiveModuloMaximalIdealConclusion.{u₅} S

Sources

• Section 38.25, Tag 0ASZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.InjectiveModuloMaximalIdealSituation · AlgebraicGeometry.universallyInjective_of_isNoetherianRing · AlgebraicGeometry.flat_of_isNoetherianRing · Module.finitePresentation_of_finite · AlgebraicGeometry.universallyInjective_of_localizedPolynomial_cases · AlgebraicGeometry.finitePresentation_of_localizedPolynomial_cases · AlgebraicGeometry.flat_of_localizedPolynomial_cases · AlgebraicGeometry.injectiveModuloMaximalIdealConclusion_of_henselianLocalRing

Section38.26 Flat finite type modules, Part III#

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

Tag 05UA, a theorem

Tag 05UA in the Stacks Project.

AlgebraicGeometry.isFlatOverAt_iff_forall_isAssociatedPoint_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatAtAssociatedPoints.lean, line 260. The attribute's comment: “Ass_{X_s}(F_s) is Stacks.Divisors.associatedPoints of the pullback of F to the scheme-theoretic fibre f.fiber (f x), and flatness at a point is IsFlatOverAt.”.

Stacks 05UA. Let f : X ⟶ S be locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type and let x ∈ X. Then F is flat over S at x if and only if F is flat over S at every associated point of the restriction of F to the fibre over f x which specializes to x.

theorem isFlatOverAt_iff_forall_isAssociatedPoint_specializes {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (x : X) :
    IsFlatOverAt f.toLRSHom.toShHom F x ↔
      ∀ x' : f.fiber (f x),
        x' ∈ Stacks.Divisors.associatedPoints
            ((Scheme.Modules.pullback (f.fiberι (f x))).obj F) →
          f.fiberι (f x) x' ⤳ x → IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι (f x) x')

Tag 05UB, a lemma

Tag 05UB in the Stacks Project.

AlgebraicGeometry.isFlatOver_of_isFlatOverAt_closedFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ClosedFibreFlatnessCheck.lean, line 92. The attribute's comment: “Ass_{X/S}(F) is Stacks.Divisors.relativeAssassin, the closed fibre X_s is f.fiber s placed in X by f.fiberι s, and flatness over the base at a point is IsFlatOverAt. A local scheme is an affine scheme whose ring of global sections is local.”.

Stacks Project, Tag 05UB. Let S be a local scheme with closed point s, let f : X ⟶ S be locally of finite type and let F be a finite type quasi-coherent 𝒪_X-module. If every point of Ass_{X/S}(F) specializes to a point of the closed fibre X_s, and F is flat over S at every point of X_s, then F is flat over S.

The criterion of Stacks 05UA is isFlatOverAt_iff_forall_isAssociatedPoint_specializes, read at every point of the source. Everything else is isFlatOverAt_of_mem_relativeAssassin: the two hypotheses on F give flatness at every point of the relative assassin, which is what that criterion tests.

theorem isFlatOver_of_isFlatOverAt_closedFiber
    {X S : Scheme.{u}} [IsAffine S] [IsLocalRing Γ(S, ⊤)]
    (s : S) (_hs : s ∈ closedPoints S)
    (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hass : ∀ x ∈ Stacks.Divisors.relativeAssassin f F,
      ∃ y : f.fiber s, Specializes x (f.fiberι s y))
    (hflat : ∀ y : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s y)) :
    IsFlatOver f.toLRSHom.toShHom F

Sources

• Section 38.26, Tag 05U8
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isFlatOverAt_iff_forall_isAssociatedPoint_specializes · AlgebraicGeometry.isFlatOver_of_isFlatOverAt_closedFiber

Section38.27 Universal flattening#

Section 38.27 of the Stacks Project, Tag 05PS. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05UC, a lemma

Tag 05UC in the Stacks Project.

AlgebraicGeometry.FreeAtGenericPointsSituation.isImmersion_representableBy_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPointsImmersion.lean, line 95. The attribute's comment: “representability of H_p by a locally closed immersion”.

Stacks Project, Tag 05UC. In Situation 05MP, for each p ≥ 0 the functor H_p of 05MR is representable by a locally closed immersion S_p ⟶ S.

theorem isImmersion_representableBy_fittingRankStratum :
    ∃ W : Over D.S, IsImmersion W.hom ∧
      Nonempty ((D.freeAtGenericPointsFunctor p).RepresentableBy W)

AlgebraicGeometry.FreeAtGenericPointsSituation.finitePresentation_hom_of_representableBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FreeAtGenericPointsImmersion.lean, line 113. The attribute's comment: “finite presentation of S_p ⟶ S when the module is of finite presentation”.

Stacks Project, Tag 05UC. In Situation 05MP, if ℱ is of finite presentation then S_p ⟶ S is of finite presentation.

The assertion is proved for an arbitrary morphism representing the generic-rank functor, which is legitimate because any two representatives are isomorphic over the base.

theorem finitePresentation_hom_of_representableBy [D.F.IsFinitePresentation]
    {W : Over D.S} (e : (D.freeAtGenericPointsFunctor p).RepresentableBy W) :
    FinitePresentation W.hom

Tag 05UD, a lemma

Tag 05UD in the Stacks Project.

AlgebraicGeometry.FlatDimensionSituation.isFlat_etaleChart_and_iff_of_relativeAssassin_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/FlatDimensionEtaleComparison.lean, line 373.

Stacks Project, Tag 05UD. In Situation 05MT, let h : X' ⟶ X be étale and let F'_n be the functor of Stacks 05MU for (f ∘ h, h^* F). Then F_n is a subfunctor of F'_n, and if h(X') contains Ass_{X/S}(F) then F_n = F'_n.

Both functors are subterminal, so the first assertion is the implication between the two conditions after every base change T ⟶ S, and the second is their equivalence.

theorem isFlat_etaleChart_and_iff_of_relativeAssassin_subset {X' : Scheme.{u}} (h : X' ⟶ D.X)
    [Etale h] :
    (∀ T : Over D.S, D.IsFlatInDimensionsGEAfterBaseChange T →
      (D.etaleChart h).IsFlatInDimensionsGEAfterBaseChange T) ∧
    (Stacks.Divisors.relativeAssassin D.f D.F ⊆ Set.range h → ∀ T : Over D.S,
      D.IsFlatInDimensionsGEAfterBaseChange T ↔
        (D.etaleChart h).IsFlatInDimensionsGEAfterBaseChange T)

Tag 05UE, a lemma

Tag 05UE in the Stacks Project.

AlgebraicGeometry.FreeAtGenericPointsSituation.flatDimensionFunctor_iso_coproduct_freeAtGenericPointsFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/GenericRankCoproduct.lean, line 291.

Let f : X ⟶ S be a smooth morphism of affine schemes with geometrically irreducible fibres of dimension d and let F be a quasi-coherent 𝒪_X-module of finite presentation. Then there is a c ≥ 0 with

F_d = ∐_{p = 0, …, c} H_p

where F_d is the functor of flatness in dimensions ≥ d of Stacks 05MT and H_p is the functor of Stacks 05MP, the coproduct being taken in Zariski sheaves over S.

The comparison map out of the pointwise disjoint union is locally bijective, hence becomes an isomorphism after sheafification, and sheafification preserves coproducts.

Sheafifying the left-hand side too is not a weakening: F_d is an fpqc sheaf by Stacks 05MV, a fortiori a Zariski sheaf, so it is isomorphic to its own sheafification. It is written sheafified here only so that the statement takes no input from that tag.

theorem flatDimensionFunctor_iso_coproduct_freeAtGenericPointsFunctor [IsAffine D.X]
    [IsAffine D.S] [D.F.IsFinitePresentation] {d : ℕ} (hd : RelativeDimension D.f d) :
    ∃ c : ℕ, Nonempty
      ((presheafToSheaf (Scheme.zariskiTopology.over D.S) (Type (u + 1))).obj
          ((D.toFlatDimensionSituation d).flatDimensionFunctor ⋙ uliftFunctor.{u + 1}) ≅
        ∐ fun p : Fin (c + 1) ↦
          (presheafToSheaf (Scheme.zariskiTopology.over D.S) (Type (u + 1))).obj
            (D.freeAtGenericPointsFunctor p.val ⋙ uliftFunctor.{u + 1}))

AlgebraicGeometry.isFlatOverInDimensionsGE_iff_forall_exists_freeAtPointOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/GenericRankDecomposition.lean, line 248. The attribute's comment: “F_d is the union of the H_p”.

Stacks Project, Tag 05UE. Let f : X ⟶ S be a smooth morphism of affine schemes with geometrically irreducible fibres of dimension d and let F be a quasi-coherent 𝒪_X-module of finite presentation. Then F is flat over S in dimensions ≥ d if and only if F is free of some finite rank on a neighbourhood of the generic point of every fibre.

This is the decomposition F_d = ∐_p H_p of the source read on sections: H_p of Stacks 05MP is freeness of the fixed rank p near every fibre's generic point, and the right hand side is the union of the H_p. Since every hypothesis is stable under base change, the equivalence over S carries the same equivalence over every scheme T over S.

theorem isFlatOverInDimensionsGE_iff_forall_exists_freeAtPointOfRank [IsAffine X] [IsAffine S]
    [Smooth f] (hirr : ∀ s : S, GeometricallyIrreducible (f.fiberToSpecResidueField s)) {d : ℕ}
    (hd : RelativeDimension f d) (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    [F.IsFinitePresentation] :
    IsFlatOverInDimensionsGE f F d ↔
      ∀ (s : S) (ξ : f.fiber s), IsGenericPoint ξ (Set.univ : Set (f.fiber s)) →
        ∃ r : ℕ, FreeAtPointOfRank F (f.fiberι s ξ) r

Tag 05UF, a lemma

Tag 05UF in the Stacks Project.

AlgebraicGeometry.FlatDimensionSituation.exists_mono_finitePresentation_representableBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FlatDimensionFunctorRepresentability.lean, line 344.

Stacks Project, Tag 05UF. In Situation 05MT, let s be a point of S and let d = n be the bound of the situation. Assume that

1. there exists a complete dévissage of F/X/S over s,
2. X is of finite presentation over S,
3. F is an 𝒪_X-module of finite presentation, and
4. F is flat over S in dimensions ≥ d + 1.

Then, after replacing S by an open neighbourhood U of s, the functor F_d of Stacks 05MU is representable by a monomorphism Z_d ⟶ U of finite presentation.

Hypothesis (1) is the source's own: the existence of a complete dévissage is assumed by Tag 05UF, and is produced étale locally (Tag 05HU) only in the proof of Tag 05UG.

theorem exists_mono_finitePresentation_representableBy (s : D.S)
    (hdev : Nonempty (CompleteDevissage D.f D.F s)) (hf : FinitePresentation D.f)
    [D.F.IsFinitePresentation] (h : IsFlatOverInDimensionsGE D.f D.F (D.n + 1)) :
    ∃ U : D.S.Opens, s ∈ U ∧ ∃ Z : Over U.toScheme,
      Mono Z.hom ∧ FinitePresentation Z.hom ∧
        Nonempty ((D.openFlatDimensionFunctor U).RepresentableBy Z)

Tag 05UG, a theorem

Tag 05UG in the Stacks Project.

AlgebraicGeometry.FlatDimensionSituation.exists_mono_finitePresentation_representableBy_of_isPure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FlatDimensionFunctorPure.lean, line 432.

Stacks Project, Tag 05UG. In Situation 05MT, assume moreover that f is of finite presentation, that F is an 𝒪_X-module of finite presentation, and that F is pure relative to S. Then F_n is representable by a monomorphism Z_n ⟶ S of finite presentation.

f of finite presentation is spelled out as locally of finite presentation, quasi-compact and quasi-separated.

theorem exists_mono_finitePresentation_representableBy_of_isPure [LocallyOfFinitePresentation D.f]
    [QuasiCompact D.f] [QuasiSeparated D.f] [D.F.IsFinitePresentation]
    (hpure : IsPureRelative D.f D.F) :
    ∃ Z : Over D.S, Mono Z.hom ∧ FinitePresentation Z.hom ∧
      Nonempty (D.flatDimensionFunctor.RepresentableBy Z)

Tag 05UH, a lemma

Tag 05UH in the Stacks Project.

AlgebraicGeometry.exists_mono_finitePresentation_representableBy_of_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/UniversalFlatteningOfPure.lean, line 79. The attribute's comment: “part (1)”.

Stacks Project, Tag 05UH, part (1). Let f : X ⟶ S be of finite presentation and let F be an 𝒪_X-module of finite presentation which is pure relative to S. Then the universal flattening Z ⟶ S of F exists and is a monomorphism of finite presentation.

theorem exists_mono_finitePresentation_representableBy_of_isPureRelative
    {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] [F.IsFinitePresentation]
    (hpure : IsPureRelative f F) :
    ∃ Z : Over S, Mono Z.hom ∧ FinitePresentation Z.hom ∧
      Nonempty (Functor.RepresentableBy
        ({ S := S, X := X, f := f, F := F, isQuasicoherent := ‹F.IsQuasicoherent› } :
          FlatnessSituation.{u}).flatFunctor Z)

AlgebraicGeometry.exists_mono_finitePresentation_representableBy_of_isSchemePureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/UniversalFlatteningOfPure.lean, line 100. The attribute's comment: “part (2)”.

Stacks Project, Tag 05UH, part (2). Let f : X ⟶ S be of finite presentation and let X be pure relative to S. Then the universal flattening Z ⟶ S of X exists and is a monomorphism of finite presentation.

theorem exists_mono_finitePresentation_representableBy_of_isSchemePureRelative
    {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (hpure : IsSchemePureRelative f) :
    ∃ Z : Over S, Mono Z.hom ∧ FinitePresentation Z.hom ∧
      Nonempty ((structureSheafFlatnessSituation f).flatFunctor.RepresentableBy Z)

AlgebraicGeometry.exists_mono_finitePresentation_representableBy_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/UniversalFlatteningOfPure.lean, line 115. The attribute's comment: “part (3)”.

Stacks Project, Tag 05UH, part (3). Let f : X ⟶ S be proper and of finite presentation and let F be an 𝒪_X-module of finite presentation. Then the universal flattening Z ⟶ S of F exists and is a monomorphism of finite presentation.

theorem exists_mono_finitePresentation_representableBy_of_isProper
    {X S : Scheme.{u}}
    (f : X ⟶ S) [IsProper f] [LocallyOfFinitePresentation f] (F : X.Modules)
    [F.IsQuasicoherent] [F.IsFinitePresentation] :
    ∃ Z : Over S, Mono Z.hom ∧ FinitePresentation Z.hom ∧
      Nonempty (Functor.RepresentableBy
        ({ S := S, X := X, f := f, F := F, isQuasicoherent := ‹F.IsQuasicoherent› } :
          FlatnessSituation.{u}).flatFunctor Z)

AlgebraicGeometry.exists_mono_finitePresentation_representableBy_structureSheaf_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/UniversalFlatteningOfPure.lean, line 131. The attribute's comment: “part (4)”.

Stacks Project, Tag 05UH, part (4). Let f : X ⟶ S be proper and of finite presentation. Then the universal flattening Z ⟶ S of X exists, and it is a monomorphism of finite presentation.

theorem exists_mono_finitePresentation_representableBy_structureSheaf_of_isProper
    {X S : Scheme.{u}}
    (f : X ⟶ S) [IsProper f] [LocallyOfFinitePresentation f] :
    ∃ Z : Over S, Mono Z.hom ∧ FinitePresentation Z.hom ∧
      Nonempty ((structureSheafFlatnessSituation f).flatFunctor.RepresentableBy Z)

Sources

• Section 38.27, Tag 05PS
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FreeAtGenericPointsSituation.isImmersion_representableBy_fittingRankStratum · AlgebraicGeometry.FreeAtGenericPointsSituation.finitePresentation_hom_of_representableBy · AlgebraicGeometry.FlatDimensionSituation.isFlat_etaleChart_and_iff_of_relativeAssassin_subset · AlgebraicGeometry.FreeAtGenericPointsSituation.flatDimensionFunctor_iso_coproduct_freeAtGenericPointsFunctor · AlgebraicGeometry.isFlatOverInDimensionsGE_iff_forall_exists_freeAtPointOfRank · AlgebraicGeometry.FlatDimensionSituation.exists_mono_finitePresentation_representableBy · AlgebraicGeometry.FlatDimensionSituation.exists_mono_finitePresentation_representableBy_of_isPure · AlgebraicGeometry.exists_mono_finitePresentation_representableBy_of_isPureRelative

Section38.28 Grothendieck's Existence Theorem, IV#

Section 38.28 of the Stacks Project, Tag 0CTB. 9 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CTC, a situation

Tag 0CTC in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceSituation.lean, line 60.

The standing data of Grothendieck's existence theorem for modules: an inverse system of rings with surjective, locally nilpotent transitions, a separated scheme of finite presentation over the inverse-limit ring, and a compatible system of finitely presented sheaves on its base changes which are flat over, and have proper support over, the affine base at their level.

structure ExistenceSituation

Tag 0CTD, a lemma

Tag 0CTD in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.nonempty_derivedLimitQCoh_and_isDerivedLimit_isGE_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceCoheratorLimit.lean, line 462.

Stacks Project, Tag 0CTD. In Situation [Stacks, Tag 0CTC] consider K = R lim_{D_QCoh(𝒪_X)}(Fₙ) = DQ_X(R lim_{D(𝒪_X)} Fₙ). Then K is in D^b_QCoh(𝒪_X) and in fact K has nonzero cohomology sheaves only in degrees ≥ 0.

Here, at any model of D(𝒪_X), the data d of AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh are a derived limit L = R lim_{D(𝒪_X)} Fₙ and K = DQ_X(L), characterized by its universal property; such data exist (first conjunct). For any of them, K is also a derived limit R lim_{D_QCoh(𝒪_X)}(Fₙ) of the system read in D_QCoh(𝒪_X), which is the displayed equality, and its cohomology sheaves vanish outside [0, c] for some c.

theorem nonempty_derivedLimitQCoh_and_isDerivedLimit_isGE_isLE :
    Nonempty S.DerivedLimitQCoh ∧ ∀ d : S.DerivedLimitQCoh,
      (∃ _hp : HasProduct fun n : ℕ => S.quasiCoherentPushforwardSystem.obj ⟨n⟩,
        IsDerivedLimit S.quasiCoherentPushforwardSystem ⟨d.K, d.quasicoherent⟩) ∧
      d.K.IsGE 0 ∧ ∃ c : ℤ, d.K.IsLE c

AlgebraicGeometry.GrothendieckExistence.isDerivedLimit_coherator_obj_pushforwardSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceDerivedLimit.lean, line 259. The attribute's comment: “the displayed equality only; the coherator of Stacks 0CR0 is an argument, as in Stacks 0CSA and 0CR2”.

[Stacks, Tag 0CTD], the displayed equality. In Situation [Stacks, Tag 0CTC], if K is a derived limit in D(𝒪_X) of the system (iₙ,* Fₙ) of AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.derivedPushforwardSystem, then DQ_X(K) is a derived limit of the system (DQ_X(iₙ,* Fₙ)) in D_QCoh(𝒪_X). This is the equality R lim_{D_QCoh(𝒪_X)}(Fₙ) = DQ_X(R lim_{D(𝒪_X)} Fₙ) of the statement of the tag; the existence of the product of the images is part of the conclusion.

The reason is the source's: DQ_X is a right adjoint, so it commutes with the countable product occurring in a derived-limit triangle, and it is exact because the adjunction ι ⊣ DQ_X is triangulated.

theorem isDerivedLimit_coherator_obj_pushforwardSystem (adj : quasiCoherentι S.X.left ⊣ DQ)
    [DQ.CommShift ℤ] [adj.IsTriangulated]
    [HasProduct fun n : ℕ => S.derivedPushforwardSystem.obj ⟨n⟩]
    (K : DerivedCategory S.X.left.Modules)
    (hK : IsDerivedLimit S.derivedPushforwardSystem K) :
    ∃ h : HasProduct fun n : ℕ => DQ.obj (S.derivedPushforwardSystem.obj ⟨n⟩),
      @IsDerivedLimit (quasiCoherentDerivedCategory S.X.left) _ _ _ _ _ _
        (S.derivedPushforwardSystem ⋙ DQ) h (DQ.obj K)

Tag 0CTE, a lemma

Tag 0CTE in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.isPerfect_and_isIso_sheafHomBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistencePerfectSheafHom.lean, line 204. The attribute's comment: “(2)”.

Stacks Project, Tag 0CTE, part (2). In Situation [Stacks, Tag 0CTC] let K be as in [Stacks, Tag 0CTD] and let E be a perfect object of D(𝒪_X). Then N = RHom_X(E, K) = RΓ_A(X, R𝓗om(E, K)) is a perfect object of D(A), and there is a canonical isomorphism N ⊗^𝐋_A Aₙ ≅ RHom_{Xₙ}(E|_{Xₙ}, ℱₙ) in D(Aₙ) for every n, with E|_{Xₙ} the derived pullback: the derived base change of AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.sheafHomLevelMap, built from a cone p exhibiting L = R lim ℱₙ, is invertible.

As in the source, part (2) and part (1) are translated into each other by [Stacks, Tag 08DQ]; here part (2) is read off part (1) at E^∨. Stated at HasDerivedCategory.standard (scoped to this declaration).

theorem DerivedLimitQCoh.isPerfect_and_isIso_sheafHomBaseChange (d : S.DerivedLimitQCoh)
    (E : DerivedCategory S.X.left.Modules)
    (hE : RingedSpace.IsPerfect (X := S.X.left.toRingedSpace) E) :
    StacksDraft.Perfect.IsPerfect ((derivedGlobalSectionsOver S.X.hom).obj
        (((derivedSheafHom S.X.left.sheaf).obj (op E)).obj d.K)) ∧
      ∀ (p : d.L ⟶ ∏ᶜ fun n : ℕ => S.derivedPushforwardSystemOfModel.obj ⟨n⟩),
        S.IsDerivedLimitCone p → ∀ n : ℕ,
          IsIso (derivedBaseChangeComparison (S.limitProjection n)
            (DerivedLimitQCoh.sheafHomLevelMap S d E hE p n))

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.isPerfect_and_isIso_tensorBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistencePerfectTensor.lean, line 377. The attribute's comment: “(1)”.

Stacks Project, Tag 0CTE, part (1). In Situation [Stacks, Tag 0CTC] let K be as in [Stacks, Tag 0CTD] and let E be a perfect object of D(𝒪_X). Then M = RΓ(X, K ⊗^𝐋 E) is a perfect object of D(A), and the canonical map M ⊗^𝐋_A Aₙ ⟶ RΓ(Xₙ, ℱₙ ⊗^𝐋 E|_{Xₙ}) is an isomorphism in D(Aₙ) for every n, with E|_{Xₙ} the derived pullback.

Here K is given by the data d of AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh, the canonical map is (DerivedLimitQCoh.tensorBaseChange S d p n).app E, built from a cone p exhibiting L = R lim ℱₙ, and the index n stands for the level n + 1 of the source. Stated at HasDerivedCategory.standard (scoped to this declaration).

theorem DerivedLimitQCoh.isPerfect_and_isIso_tensorBaseChange (d : S.DerivedLimitQCoh)
    (E : DerivedCategory S.X.left.Modules)
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := S.X.left.toRingedSpace) E) :
    StacksDraft.Perfect.IsPerfect ((derivedGlobalSectionsOver S.X.hom).obj
        (((derivedTensorProductFunctor S.X.left.toRingedSpace.sheaf).obj d.K).obj E)) ∧
      ∀ (p : d.L ⟶ ∏ᶜ fun n : ℕ => S.derivedPushforwardSystemOfModel.obj ⟨n⟩),
        S.IsDerivedLimitCone p → ∀ n : ℕ,
          IsIso ((DerivedLimitQCoh.tensorBaseChange S d p n).app E)

Tag 0CTF, a lemma

Tag 0CTF in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistencePseudoCoherent.lean, line 64.

[Stacks, Tag 0CTF]. In Situation [Stacks, Tag 0CTC], let K be as in [Stacks, Tag 0CTD], i.e. K = DQ_X(R lim_{D(𝒪_X)} iₙ,* ℱₙ). Then K is pseudo-coherent relative to A = lim Aₙ: relatively pseudo-coherent ([Stacks, Tag 09UI]) for the structure morphism X ⟶ Spec A. Stated at the standard model.

theorem DerivedLimitQCoh.isPseudoCoherent (d : S.DerivedLimitQCoh) :
    S.X.hom.IsPseudoCoherent d.K

Tag 0CTG, a lemma

Tag 0CTG in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.isIso_sectionsOverComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceTheorem.lean, line 54.

[Stacks, Tag 0CTG]. In Situation [Stacks, Tag 0CTC], let K be as in [Stacks, Tag 0CTD], with a derived-limit cone p of R lim (iₙ,* ℱₙ). For every quasi-compact open U ⊆ X, the canonical map RΓ(U, K) ⊗_A^𝐋 Aₙ ⟶ RΓ(Uₙ, ℱₙ) of D(Aₙ), Uₙ = U ∩ Xₙ, is an isomorphism. Stated at the standard model.

theorem isIso_sectionsOverComparison (d : S.DerivedLimitQCoh)
    (p : d.L ⟶ ∏ᶜ fun n : ℕ => S.derivedPushforwardSystemOfModel.obj ⟨n⟩)
    (hp : S.IsDerivedLimitCone p) (U : S.X.left.Opens) (hU : IsCompact (U : Set S.X.left))
    (n : ℕ) : IsIso (S.sectionsOverComparison d p U n)

Tag 0CTH, a lemma

Tag 0CTH in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.exists_open_isZero_homology_isFinitePresentation_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceTheorem.lean, line 69.

[Stacks, Tag 0CTH]. In Situation [Stacks, Tag 0CTC], let K be as in [Stacks, Tag 0CTD], with a derived-limit cone p. There is an open W ⊆ X containing X₀ such that Hⁱ(K)|_W = 0 for i ≠ 0, ℱ = H⁰(K)|_W is of finite presentation, and ℱₙ = ℱ ⊗_{𝒪_X} 𝒪_{Xₙ}: the canonical maps iₙ^* H⁰(K) ⟶ ℱₙ, adjoint to the maps H⁰(K) ⟶ iₙ,* ℱₙ induced by K ⟶ iₙ,* ℱₙ, are isomorphisms. Stated at the standard model.

theorem exists_open_isZero_homology_isFinitePresentation_isIso (d : S.DerivedLimitQCoh)
    (p : d.L ⟶ ∏ᶜ fun n : ℕ => S.derivedPushforwardSystemOfModel.obj ⟨n⟩)
    (hp : S.IsDerivedLimitCone p) :
    ∃ W : S.X.left.Opens, Set.range (S.closedImmersion 0) ⊆ W ∧
      (∀ j : ℤ, j ≠ 0 →
        IsZero (((DerivedCategory.homologyFunctor S.X.left.Modules j).obj d.K).restrict W.ι)) ∧
      (((DerivedCategory.homologyFunctor S.X.left.Modules 0).obj d.K).restrict
        W.ι).IsFinitePresentation ∧
      ∀ n : ℕ, IsIso
        (((Scheme.Modules.pullbackPushforwardAdjunction (S.closedImmersion n)).homEquiv _ _).symm
          (S.zerothLevelMap d p n))

Tag 0CTI, a lemma

Tag 0CTI in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.exists_open_isProperOver_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceTheorem.lean, line 90.

[Stacks, Tag 0CTI]. In Situation [Stacks, Tag 0CTC], with K as in [Stacks, Tag 0CTD] and W as in [Stacks, Tag 0CTH]: after shrinking W, the support of ℱ = H⁰(K)|_W is proper over A. The open produced keeps the three properties of [Stacks, Tag 0CTH]. Stated at the standard model.

theorem exists_open_isProperOver_supp (d : S.DerivedLimitQCoh)
    (p : d.L ⟶ ∏ᶜ fun n : ℕ => S.derivedPushforwardSystemOfModel.obj ⟨n⟩)
    (hp : S.IsDerivedLimitCone p) :
    ∃ W : S.X.left.Opens, Set.range (S.closedImmersion 0) ⊆ W ∧
      (∀ j : ℤ, j ≠ 0 →
        IsZero (((DerivedCategory.homologyFunctor S.X.left.Modules j).obj d.K).restrict W.ι)) ∧
      (((DerivedCategory.homologyFunctor S.X.left.Modules 0).obj d.K).restrict
        W.ι).IsFinitePresentation ∧
      (∀ n : ℕ, IsIso
        (((Scheme.Modules.pullbackPushforwardAdjunction (S.closedImmersion n)).homEquiv _ _).symm
          (S.zerothLevelMap d p n))) ∧
      ∃ Z : Closeds W.toScheme, (Z : Set W.toScheme) = SheafOfModules.supp
          (((DerivedCategory.homologyFunctor S.X.left.Modules 0).obj d.K).restrict W.ι) ∧
        IsProperOver (W.ι ≫ S.X.hom) Z

Tag 0CTJ, a lemma

Tag 0CTJ in the Stacks Project.

AlgebraicGeometry.isIso_of_forall_spec_factors_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Monomorphism.lean, line 101.

Let A be the limit of a sequence of rings whose transition maps are surjective with locally nilpotent kernels. A monomorphism f : T ⟶ Spec A locally of finite type through which every Spec Aₙ ⟶ Spec A factors is an isomorphism.

theorem isIso_of_forall_spec_factors_of_isLimit (hc : IsLimit c)
    (hF : ∀ n : ℕ, Function.Surjective (F.map (homOfLE (Nat.le_succ n)).op).hom ∧
      RingHom.ker (F.map (homOfLE (Nat.le_succ n)).op).hom ≤ nilradical (F.obj (.op (n + 1))))
    {T : Scheme.{u}} (f : T ⟶ Spec c.pt) [Mono f] [LocallyOfFiniteType f]
    (hfac : ∀ n : ℕ, ∃ g : Spec (F.obj (.op n)) ⟶ T, g ≫ f = Spec.map (c.π.app (.op n))) :
    IsIso f

Tag 0CTK, a theorem

Tag 0CTK in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.exists_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowingUp/GrothendieckExistenceTheorem.lean, line 113.

[Stacks, Tag 0CTK], Grothendieck's existence theorem for flat modules. In Situation [Stacks, Tag 0CTC] there is a finitely presented 𝒪_X-module ℱ, flat over A, with support proper over A, such that ℱₙ = ℱ ⊗_{𝒪_X} 𝒪_{Xₙ} for all n compatibly with the maps φₙ. The derived categories in the proof are the standard ones; none appears in the statement.

theorem exists_algebraization :
    ∃ (F : S.X.left.Modules) (_ : F.IsFinitePresentation),
      IsFlatOver S.X.hom.toLRSHom.toShHom F ∧
      (∃ Z : Closeds S.X.left, (Z : Set S.X.left) = SheafOfModules.supp F ∧
        IsProperOver S.X.hom Z) ∧
      ∃ e : ∀ n : ℕ, (Scheme.Modules.pullback (S.closedImmersion n)).obj F ≅ S.F n,
        ∀ n : ℕ,
          (Scheme.Modules.pullbackComp (S.transitionScheme n) (S.closedImmersion (n + 1))).app F ≪≫
            (Scheme.Modules.pullbackCongr (S.transition_fst n)).app F ≪≫ e n =
          (Scheme.Modules.pullback (S.transitionScheme n)).mapIso (e (n + 1)) ≪≫ S.φ n

Sources

• Section 38.28, Tag 0CTB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GrothendieckExistence.ExistenceSituation · AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.nonempty_derivedLimitQCoh_and_isDerivedLimit_isGE_isLE · AlgebraicGeometry.GrothendieckExistence.isDerivedLimit_coherator_obj_pushforwardSystem · AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.isPerfect_and_isIso_sheafHomBaseChange · AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.isPerfect_and_isIso_tensorBaseChange · AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.DerivedLimitQCoh.isPseudoCoherent · AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.isIso_sectionsOverComparison · AlgebraicGeometry.GrothendieckExistence.ExistenceSituation.exists_open_isZero_homology_isFinitePresentation_isIso

Section38.29 Grothendieck's Existence Theorem, V#

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

Tag 0DIB, a situation

Tag 0DIB in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/Basic.lean, line 99.

Stacks Project, Tag 0DIB. The standing data of Grothendieck's existence theorem in its derived form: an inverse system of rings with surjective, locally nilpotent transitions, a proper flat scheme of finite presentation over the inverse-limit ring, and a compatible system of pseudo-coherent objects on its base changes.

public structure DerivedExistenceSituation

Tag 0DIC, a lemma

Tag 0DIC in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.isDerivedLimit_coherator_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/DerivedLimitBounded.lean, line 164. The attribute's comment: “the displayed equality only; the coherator of Stacks 0CR0 is an argument, as in Stacks 0CSA and 0CR2, and the tower is an arbitrary inverse system in D(O_X) rather than the system Ri_n,* K_n of Situation 0DIB, which this library cannot yet form at the locally small model the coherator lives at”.

The displayed equality of [Stacks, Tag 0DIC]: Rlim_{D_QCoh(𝒪_X)}(Kₙ) and DQ_X(Rlim_{D(𝒪_X)} Kₙ) agree. Precisely, if K is a derived limit of an inverse system (Kₙ) in D(𝒪_X) then DQ_X(K) is a derived limit of the system (DQ_X(Kₙ)) in D_QCoh(𝒪_X); the existence of the product of the images is part of the conclusion.

This is the source's reason for the equality: DQ_X is a right adjoint, so it commutes with products, and it is exact because the adjunction ι ⊣ DQ_X is triangulated, so it carries the derived-limit triangle of (Kₙ) to the derived-limit triangle of (DQ_X(Kₙ)).

theorem isDerivedLimit_coherator_obj (adj : quasiCoherentι X ⊣ DQ) [DQ.CommShift ℤ]
    [adj.IsTriangulated] (L : ℕᵒᵖ ⥤ DerivedCategory X.Modules)
    [HasProduct fun n : ℕ => L.obj ⟨n⟩] (K : DerivedCategory X.Modules)
    (hK : IsDerivedLimit L K) :
    ∃ h : HasProduct fun n : ℕ => DQ.obj (L.obj ⟨n⟩),
      @IsDerivedLimit (quasiCoherentDerivedCategory X) _ _ _ _ _ _ (L ⋙ DQ) h (DQ.obj K)

AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.limitObject_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/DerivedLimitBoundedAbove.lean, line 183.

Stacks Project, Tag 0DIC. In Situation [Stacks, Tag 0DIB] consider K = R lim_{D_QCoh(𝒪_X)}(Kₙ) = DQ_X(R lim_{D(𝒪_X)} Kₙ). Then K is in D^-_QCoh(𝒪_X).

Here R lim_{D(𝒪_X)} Kₙ is a chosen derived limit (AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.derivedLimit) of the system (R(iₙ)_* Kₙ) whose transition maps are the adjoints of the φₙ, and DQ_X is the coherator of [Stacks, Tag 0CR0]. The three conjuncts are:

• the displayed equality: DQ_X(R lim_{D(𝒪_X)} Kₙ) is a derived limit R lim_{D_QCoh(𝒪_X)}(Kₙ) of the system in D_QCoh(𝒪_X);
• K, read at the model of the situation (AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.limitObject), has quasi-coherent cohomology sheaves;
• K is bounded above.

The proof is the source's, see the module documentation and that of StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/DerivedLimitObject.lean.

theorem limitObject_spec :
    (∃ _ : HasProduct fun n : ℕ => S.qcohTower.obj (op n),
      IsDerivedLimit S.qcohTower S.coheratorLimit) ∧
    letI := HasDerivedCategory.standard
      (StrictlyPerfect.OXMod.{u, u, u} S.X.left.toRingedSpace)
    (∀ j : ℤ, ((DerivedCategory.homologyFunctor _ j).obj S.limitObject).IsQuasicoherent) ∧
      ∃ c : ℤ, S.limitObject.IsLE c

Tag 0DID, a lemma

Tag 0DID in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.isPseudoCoherent_cohomology_and_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/CohomologyAgainstPerfect.lean, line 617.

[Stacks, Tag 0DID]. In Situation [Stacks, Tag 0DIB] let K be as in [Stacks, Tag 0DIC]. For any perfect object E of D(𝒪_X) the cohomology M = RΓ(X, K ⊗^L E) is a pseudo-coherent object of D(A) and there is a canonical isomorphism RΓ(X_n, K_n ⊗^L E|_{X_n}) = M ⊗^L_A A_n in D(A_n), where E|_{X_n} is the derived pullback of E to X_n.

Here K is AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.limitObject, M is AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.cohomology, and the canonical isomorphism is the base change map M ⊗^L_A A_n ⟶ RΓ(X_n, K_n ⊗^L E|_{X_n}) adjoint to the canonical map M ⟶ RΓ(X_n, K_n ⊗^L E|_{X_n}) (AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.cohomologyMap): pull back along X_n ⟶ X, identify (K ⊗^L E)|_{X_n} = K|_{X_n} ⊗^L E|_{X_n}, and apply the canonical map K|_{X_n} ⟶ K_n.

The proof is the source's. RΓ(X, - ⊗^L E) carries the derived-limit triangle of K = DQ_X(R lim K_n) to a triangle presenting M as R lim M_n for M_n = RΓ(X_n, K_n ⊗^L E_n) (AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.exists_distTriang_cohomology); the M_n are pseudo-coherent ([Stacks, Tag 0CSD]) with M_{n+1} ⊗^L A_n = M_n by flat base change; and [Stacks, Tag 0CQF] concludes.

theorem isPseudoCoherent_cohomology_and_isIso
    (hE : RingedSpace.IsPerfect (X := S.X.left.toRingedSpace) E) :
    StacksDraft.PseudoCoherence.IsPseudoCoherent (S.cohomology E) ∧
      ∀ n : ℕ, IsIso (StacksDraft.DerivedInverseLimit.derivedBaseChangeComparison.{u, u, u}
        (limit.π S.system (op n)).hom (S.cohomologyMap E n))

Tag 0DIE, a lemma

Tag 0DIE in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.isPseudoCoherent_limitObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/LimitObjectPseudoCoherent.lean, line 77.

Stacks Project, Tag 0DIE. In Situation [Stacks, Tag 0DIB] let K be as in [Stacks, Tag 0DIC]. Then K is pseudo-coherent on X.

Here K = DQ_X(R lim Kₙ) is AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.limitObject, an object of D(𝒪_X) at the model at which the Kₙ are given. By [Stacks, Tag 0DID] (its first assertion, DerivedExistenceSituation.isPseudoCoherent_cohomology_and_isIso) RΓ(X, K ⊗^𝐋 E) is pseudo-coherent for every perfect E; [Stacks, Tag 0GES] (which is [Stacks, Tags 0CSH and 0CSL] together, X being separated and of finite presentation over A and K lying in D_QCoh(𝒪_X) by [Stacks, Tag 0DIC]) makes K pseudo-coherent relative to A, and [Stacks, Tag 09UU] (for schemes, [Stacks, Tag 0DII]) turns that into pseudo-coherence on X, X being flat and of finite presentation over A.

theorem isPseudoCoherent_limitObject (S : DerivedExistenceSituation.{u}) :
    letI := HasDerivedCategory.standard (StrictlyPerfect.OXMod.{u, u, u} S.X.left.toRingedSpace)
    RingedSpace.IsPseudoCoherent (X := S.X.left.toRingedSpace) S.limitObject

Tag 0DIF, a lemma

Tag 0DIF in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.isIso_derivedBaseChangeComparison_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/DerivedSectionsBaseChange.lean, line 155.

In Situation [Stacks, Tag 0DIB] let K be as in [Stacks, Tag 0DIC]. For any quasi-compact open U ⊆ X we have RΓ(U, K) ⊗^𝐋_A Aₙ = RΓ(Uₙ, Kₙ) in D(Aₙ), where Uₙ = U ∩ Xₙ.

Here K is AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.limitObject, RΓ(U, K) is the A-linear derived global sections of K|_U, RΓ(Uₙ, Kₙ) the Aₙ-linear derived global sections of Kₙ|_{Uₙ}, and the identification is the canonical map RΓ(U, K) ⊗^𝐋_A Aₙ ⟶ RΓ(Uₙ, Kₙ): the adjoint of AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.openRestrictionMap, which pulls derived sections back along Uₙ ⟶ U and applies the canonical map K|_{Xₙ} ⟶ Kₙ adjoint to the projection K ⟶ R(iₙ)_* Kₙ.

theorem isIso_derivedBaseChangeComparison_derivedSections (hU : IsCompact (U : Set S.X.left)) :
    IsIso (derivedBaseChangeComparison (limit.π S.system (op n)).hom
      (S.openRestrictionMap U n S.limitObject (S.restrictionMap n)))

Tag 0DIG, a theorem

Tag 0DIG in the Stacks Project.

AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.exists_isPseudoCoherent_derivedPullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/DerivedExistenceTheorem.lean, line 66.

[Stacks, Tag 0DIG], Grothendieck's existence theorem in its derived form. In Situation [Stacks, Tag 0DIB] there is a pseudo-coherent K ∈ D(𝒪_X) together with isomorphisms βₙ : K ⊗ᴸ_{𝒪_X} 𝒪_{Xₙ} = L(iₙ)^* K ≅ Kₙ compatible with the maps φₙ: the composite L(jₙ)^* L(iₙ₊₁)^* K ≅ L(iₙ)^* K ⟶ Kₙ of the composition isomorphism with βₙ is L(jₙ)^* βₙ₊₁ followed by φₙ.

theorem exists_isPseudoCoherent_derivedPullback_iso :
    ∃ K : DerivedCategory (StrictlyPerfect.OXMod.{u, u, u} S.X.left.toRingedSpace),
      RingedSpace.IsPseudoCoherent (X := S.X.left.toRingedSpace) K ∧
        ∃ β : ∀ n : ℕ, (derivedPullback (S.levelInclusion n)).obj K ≅ S.K n,
          ∀ n : ℕ,
            (Stacks.DerivedPullback.Composition.derivedPullbackCompIsoCanonical
                (S.levelTransition n) (S.levelInclusion (n + 1))).hom.app K ≫
              eqToHom (congrArg (fun t : (schemeAt S.system S.X n).toRingedSpace ⟶
                  S.X.left.toRingedSpace => (derivedPullback t).obj K)
                (S.levelTransition_comp_levelInclusion n)) ≫ (β n).hom =
            (derivedPullback (S.levelTransition n)).map (β (n + 1)).hom ≫ S.φ n

Sources

• Section 38.29, Tag 0DIA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation · AlgebraicGeometry.GrothendieckExistence.isDerivedLimit_coherator_obj · AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.limitObject_spec · AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.isPseudoCoherent_cohomology_and_isIso · AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.isPseudoCoherent_limitObject · AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.isIso_derivedBaseChangeComparison_derivedSections · AlgebraicGeometry.GrothendieckExistence.DerivedExistenceSituation.exists_isPseudoCoherent_derivedPullback_iso

Section38.30 Blowing up and flatness#

Section 38.30 of the Stacks Project, Tag 080X. 7 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 080Y, a remark

Tag 080Y in the Stacks Project.

AlgebraicGeometry.exists_admissibleBlowup_forall_restrict_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleLocalOnBase.lean, line 91. The attribute's comment: “locality on S: finitely many admissible blowups of quasi-compact opens of S are all refined by the restrictions of a single U-admissible blowup of S, each refinement itself an admissible blowup of the local solution”.

Stacks Project, Tag 080Y, the locality on S of Remark 38.30.1, for a finite family of quasi-compact opens. Let S be quasi-compact and quasi-separated, U ⊆ S a quasi-compact open, and let W j ⊆ S be finitely many quasi-compact opens carrying W j ∩ U-admissible blowups c j : V j ⟶ W j. There is one U-admissible blowup p : S' ⟶ S whose restriction to each W j factors through c j.

Each c j extends to a U-admissible blowup q j : T j ⟶ S with IsPullback (c j) \_ (W j).ι (q j) by [Stacks, Tag 080M], and [Stacks, Tag 080N] produces a U-admissible p : S' ⟶ S factoring through every q j by a q j ⁻¹ᵁ U-admissible blowup k j. The restriction p ∣_ W j and the composite (p ⁻¹ᵁ W j).ι ≫ k j agree over S, so the cartesian square of [Stacks, Tag 080M] lifts them to the required map r to V j; and r is the base change of k j along the flat g j, hence admissible.

public theorem exists_admissibleBlowup_forall_restrict_factors
    [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens) (hU : IsCompact (U : Set S))
    {ι : Type*} [Finite ι] (W : ι → S.Opens) (hW : ∀ j, IsCompact ((W j : S.Opens) : Set S))
    (V : ι → Scheme.{u}) (c : ∀ j, V j ⟶ (W j).toScheme)
    (hc : ∀ j, Stacks.Blowup.IsAdmissibleBlowup ((W j).ι ⁻¹ᵁ U) (c j)) :
    ∃ (S' : Scheme.{u}) (p : S' ⟶ S), Stacks.Blowup.IsAdmissibleBlowup U p ∧
      ∀ j, ∃ r : (p ⁻¹ᵁ W j).toScheme ⟶ V j, r ≫ c j = p ∣_ (W j) ∧
        Stacks.Blowup.IsAdmissibleBlowup (c j ⁻¹ᵁ ((W j).ι ⁻¹ᵁ U)) r

AlgebraicGeometry.exists_admissibleBlowup_finite_cover_restrict_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AdmissibleLocalOnBase.lean, line 134. The attribute's comment: “locality on S: a solution on a quasi-compact open neighbourhood of every point of S is refined, over a finite subcover, by the restrictions of a single U-admissible blowup of S, each refinement itself an admissible blowup of the local solution”.

Stacks Project, Tag 080Y, the locality on S of Remark 38.30.1 in the paragraph's own formulation. Let S be quasi-compact and quasi-separated and U ⊆ S a quasi-compact open. Suppose that every point s of S has a quasi-compact open neighbourhood W s carrying a W s ∩ U-admissible blowup c s : V s ⟶ W s. Then there is a finite set of points whose neighbourhoods already cover S, and one U-admissible blowup p : S' ⟶ S whose restriction to each of those neighbourhoods factors through the blowup given there.

The finite set comes from quasi-compactness of S, the blowup from AlgebraicGeometry.exists_admissibleBlowup_forall_restrict_factors applied to the finite subfamily.

public theorem exists_admissibleBlowup_finite_cover_restrict_factors
    [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens) (hU : IsCompact (U : Set S))
    (W : S → S.Opens) (hWmem : ∀ s : S, s ∈ W s)
    (hW : ∀ s : S, IsCompact ((W s : S.Opens) : Set S))
    (V : S → Scheme.{u}) (c : ∀ s : S, V s ⟶ (W s).toScheme)
    (hc : ∀ s : S, Stacks.Blowup.IsAdmissibleBlowup ((W s).ι ⁻¹ᵁ U) (c s)) :
    ∃ (F : Finset S) (S' : Scheme.{u}) (p : S' ⟶ S),
      (∀ x : S, ∃ s ∈ F, x ∈ W s) ∧ Stacks.Blowup.IsAdmissibleBlowup U p ∧
        ∀ s ∈ F, ∃ r : (p ⁻¹ᵁ W s).toScheme ⟶ V s, r ≫ c s = p ∣_ (W s) ∧
          Stacks.Blowup.IsAdmissibleBlowup (c s ⁻¹ᵁ ((W s).ι ⁻¹ᵁ U)) r

AlgebraicGeometry.cartierBoundaryDivisorReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/CartierBoundaryDivisorReduction.lean, line 80. The attribute's comment: “the reduction to a divisor: after one U-admissible blowup the boundary is an effective Cartier divisor whose complement is the inverse image of U, and that inverse image is scheme theoretically dense”.

Stacks Project, Tag 080Y, the reduction to a divisor of Remark 38.30.1 in full. On a quasi-compact and quasi-separated scheme S a quasi-compact open U becomes, after a single U-admissible blowup, the complement of an effective Cartier divisor D supported on the boundary; and then U is scheme theoretically dense.

The centre is the one of AlgebraicGeometry.cartierBoundaryReduction, and D is the exceptional divisor of its blowup: an effective Cartier divisor by [Stacks, Tag 02OS] part (2) (Stacks.Blowup.isEffectiveCartierDivisor_exceptionalIdeal), whose support is the boundary by that theorem. The density is then [Stacks, Tag 07ZU] (Stacks.Divisors.isSchemeTheoreticallyDense_compl_of_isEffectiveCartierDivisor): the complement of an effective Cartier divisor is scheme theoretically dense.

public theorem cartierBoundaryDivisorReduction [CompactSpace S] [QuasiSeparatedSpace S]
    (U : S.Opens) (hU : IsCompact (U : Set S)) : CartierBoundaryDivisorReduction S U

AlgebraicGeometry.cartierBoundaryReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/DominatedByBlowup.lean, line 178.

Stacks Project, Tag 080Y. On a quasi-compact and quasi-separated scheme S, a quasi-compact open U becomes the complement of an effective Cartier divisor after a single U-admissible blowup: a finite type quasi-coherent ideal sheaf I cutting out S ∖ U is finitely presented as a closed subscheme, is disjoint from U, and the exceptional divisor of the blowup of S in I is exactly the complement of the inverse image of U.

public theorem cartierBoundaryReduction [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens)
    (hU : IsCompact (U : Set S)) : CartierBoundaryReduction S U

AlgebraicGeometry.StrictTransformProblem.isSolvable_of_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransformProblem/LocalGlobal.lean, line 268. The attribute's comment: “the local-global reduction, the remark's third paragraph; the locality of P on the base is the hypothesis the remark states it under”.

[Stacks, Tag 080Y], the local-global reduction. Suppose the property P is local on the base: for every strict-transform problem with that property, if the base is covered by finitely many quasi-compact opens over each of which the restricted triple has P, then the triple itself has P. Then the strict-transform problem is local on the base too: if every point of S has a quasi-compact open neighbourhood over which the problem is solvable, the problem is solvable.

public theorem isSolvable_of_local (D : StrictTransformProblem.{u})
    (hP : ∀ E : StrictTransformProblem.{u}, @E.P = @D.P →
      ∀ {ι : Type} [Finite ι] (W : ι → E.S.Opens) (hW : ∀ i, IsCompact (W i : Set E.S)),
        (⋃ i, (W i : Set E.S)) = Set.univ →
        (∀ i, (E.restrict (W i) (hW i)).P (E.restrict (W i) (hW i)).f
          (E.restrict (W i) (hW i)).F) →
        E.P E.f E.F)
    (hlocal : ∀ s : D.S, ∃ (W : D.S.Opens) (hW : IsCompact (W : Set D.S)),
      s ∈ (W : Set D.S) ∧ (D.restrict W hW).IsSolvable) :
    D.IsSolvable

AlgebraicGeometry.StrictTransformProblem.isSolvable_of_isSolvableIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransformProblem/Successive.lean, line 135. The attribute's comment: “the successive reduction, the paragraph beginning `The general strategy will be to use that a composition of U-admissible blowups is a U-admissible blowup': it suffices to find a sequence of U-admissible blowups S = S_0 <- S_1 <- ... <- S_n such that, setting F_0 = F and X_0 = X and F_i/X_i the strict transform of F_{i-1}/X_{i-1}, the triple F_n/X_n/S_n has P. The sequence is IsSolvableIn n and the single blowup it is replaced by is IsSolvable”.

[Stacks, Tag 080Y], the successive reduction. To solve the strict-transform problem it suffices to find a sequence of U-admissible blowups S = S₀ ← S₁ ← … ← Sₙ whose iterated strict transform has the property P: such a sequence is replaced by a single U-admissible blowup with the same effect.

The sequence is contracted one stage at a time: the amalgamation of [Stacks, Tag 080B], fed by the second-centre factorization of [Stacks, Tag 0803], replaces the last two centres by a single admissible centre on the previous base, and [Stacks, Tag 080I] identifies the iterated strict transform with the strict transform in it.

public theorem isSolvable_of_isSolvableIn (n : ℕ) (D : StrictTransformProblem.{u})
    (h : D.IsSolvableIn n) : D.IsSolvable

Tag 0810, a lemma

Tag 0810 in the Stacks Project.

AlgebraicGeometry.exists_idealSheafData_forall_blowUp_exists_free_of_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/BlowupIntegralFibresGeometric.lean, line 316. The attribute's comment: “the scheme-level form”.

Stacks Project, Tag 0810. Let S be an affine scheme, s : Γ(S, ⊤), r ≥ 0 an integer, f : X ⟶ S an affine morphism and F a quasi-coherent 𝒪_X-module. Assume

1. f is of finite presentation and flat with geometrically integral fibres;
2. F is of finite type;
3. F restricted to f⁻¹(D(s)) is of finite presentation;
4. for every point x of X which is generic in its fibre and whose image lies in D(s), the stalk F_x is free of rank r over 𝒪_{X,x}.

Then there is a quasi-coherent sheaf of ideals ℐ on S whose ideal of global sections is finitely generated and whose support is V(s), such that over every point z of the blowup Bl_ℐ(S) there is a point of X ×_S Bl_ℐ(S) above z with an open neighbourhood on which the strict transform of F is free of rank r.

This is the geometric reading of the ring-level AlgebraicGeometry.exists_fg_ideal_forall_blowup_chart_exists_away_basis: hypotheses (1)–(4) are converted into its hypotheses on Γ(S, ⊤) → Γ(X, ⊤) and Γ(F, ⊤), and its conclusion — the a-power-torsion quotient of the base change becomes free of rank r after inverting one element per prime of each affine blowup chart — is carried onto the sheaf-level strict transform by AlgebraicGeometry.exists_free_open_of_chart_at.

public theorem exists_idealSheafData_forall_blowUp_exists_free_of_rank
    {S X : Scheme.{u}} [IsAffine S] (f : X ⟶ S) [IsAffineHom f] [Flat f]
    [GeometricallyIntegral f] (hf : AlgebraicGeometry.FinitePresentation f)
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (s : Γ(S, ⊤)) (r : ℕ)
    (hFU : (F.restrict (f ⁻¹ᵁ S.basicOpen s).ι).IsFinitePresentation)
    (hrank : ∀ x : X, f.base x ∈ S.basicOpen s → f.base ⁻¹' {f.base x} ⊆ closure {x} →
      letI := Stacks.ModuleStalkSpecialization.stalkModule F x
      Nonempty (Module.Basis (Fin r) (X.presheaf.stalk x) (F.presheaf.stalk x))) :
    ∃ ℐ : S.IdealSheafData,
      (ℐ.ideal ⟨⊤, isAffineOpen_top S⟩).FG ∧
      (ℐ.support : Set S) = (↑(S.basicOpen s))ᶜ ∧
      ∀ z : Stacks.Blowup.blowUp ℐ,
        ∃ (W : (Limits.pullback f (Stacks.Blowup.blowUpToBase ℐ)).Opens)
          (x : ↥(Limits.pullback f (Stacks.Blowup.blowUpToBase ℐ))),
          x ∈ W ∧ (pullback.snd f (Stacks.Blowup.blowUpToBase ℐ)).base x = z ∧
          Nonempty ((Stacks.StrictTransform.sheaf f (Stacks.Blowup.blowUpToBase ℐ)
            (Stacks.Blowup.exceptionalIdeal ℐ) F).restrict W.ι ≅
              SheafOfModules.free.{u} (ULift.{u} (Fin r)))

Stacks.StrictTransform.exists_fg_ideal_forall_chartFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/AffineChartSections.lean, line 302. The attribute's comment: “the conclusion read on the strict transform of [Stacks, Tag 080D]: on every affine chart of a base change on which the inverse image of the centre is the zero locus of the image of the chart's denominator, the strict transform of the module is free of rank r on a basic open through every extended prime of the chart base. The hypotheses are the source's own, read on the global sections of the two affine schemes; the existence of such charts is not claimed”.

Stacks Project, Tag 0810, read on the strict transform. Let S be an affine scheme, X an affine scheme over it with Γ(S, ⊤) ⟶ Γ(X, ⊤) flat and of finite presentation with geometrically integral fibres, let F be a quasi-coherent module on X presented as M^~ with M finite over Γ(X, ⊤), let t : Γ(S, ⊤) and r : ℕ, and assume M is finitely presented after inverting t and free of rank r at every extended prime qΓ(X, ⊤) with t ∉ q. Then there is a finitely generated ideal I ⊆ Γ(S, ⊤) with V(t) = V(I) such that for every a ∈ I and every prime q' of the affine blowup algebra Γ(S, ⊤)[I/a], the chart Spec (Γ(X, ⊤) ⊗_{Γ(S,⊤)} Γ(S, ⊤)[I/a]) of a base change satisfies Stacks.StrictTransform.ChartFreeOfRank for the image of a and the extension of q': on every such chart on which the inverse image of the centre is the zero locus of the image of a, the strict transform of F of [Stacks, Tag 080D] is free of rank r on a basic open D(g) with g outside q'·(Γ(X, ⊤) ⊗ Γ(S, ⊤)[I/a]).

This is the scheme-level form of the ring-level exists_fg_ideal_forall_blowup_chart_exists_away_basis: the ideal, the chart algebras and the element g are the ring-level ones, and the module the ring-level statement produces a basis for is identified with the strict transform by Stacks.StrictTransform.affineChartSheafIso, through Stacks.StrictTransform.nonempty_restrict_basicOpen_free_of_basis. It is the form the proof of [Stacks, Tag 0811] consumes, which is about the strict transform and not about the chart-level torsion quotient: freeness of the strict transform near the generic point of a fibre of X ×_S Bl_I(S) ⟶ Bl_I(S) is the flatness conjunct of AlgebraicGeometry.GenericFibreFlatteningBlowup.

The charts are universally quantified inside Stacks.StrictTransform.ChartFreeOfRank: nothing is claimed here about their existence, which is the content of [Stacks, Tag 0804] for the blowup of S in I together with the base change of that covering along f.

public theorem exists_fg_ideal_forall_chartFreeOfRank [IsAffine X] [IsAffine S] (f : X ⟶ S)
    (F : X.Modules) [F.IsQuasicoherent] (M : ModuleCat.{u} Γ(X, ⊤))
    (e : F ≅ (Scheme.Modules.pullback X.isoSpec.hom).obj (tilde M))
    [Algebra Γ(S, ⊤) Γ(X, ⊤)]
    (halg : (algebraMap Γ(S, ⊤) Γ(X, ⊤) : Γ(S, ⊤) →+* Γ(X, ⊤)) = f.appTop.hom)
    [Algebra.FinitePresentation Γ(S, ⊤) Γ(X, ⊤)] [Module.Flat Γ(S, ⊤) Γ(X, ⊤)]
    [Module.Finite Γ(X, ⊤) M] (t : Γ(S, ⊤)) (r : ℕ)
    (hfibre : ∀ (q : Ideal Γ(S, ⊤)) (hq : q.IsPrime),
      letI := hq
      Algebra.IsGeometricallyIntegral q.ResidueField (q.Fiber Γ(X, ⊤)))
    (hfp : Module.FinitePresentation (Localization.Away (algebraMap Γ(S, ⊤) Γ(X, ⊤) t))
      (LocalizedModule (Submonoid.powers (algebraMap Γ(S, ⊤) Γ(X, ⊤) t)) M))
    (hrank : ∀ (q : Ideal Γ(S, ⊤)) (hq : q.IsPrime), t ∉ q →
      letI := hq
      let 𝔮 := Ideal.map (algebraMap Γ(S, ⊤) Γ(X, ⊤)) q
      ∀ h𝔮 : 𝔮.IsPrime,
        letI := h𝔮
        Nonempty (LocalizedModule 𝔮.primeCompl M ≃ₗ[Localization 𝔮.primeCompl]
          (Fin r → Localization 𝔮.primeCompl))) :
    ∃ I : Ideal Γ(S, ⊤), I.FG ∧
      (∀ q : Ideal Γ(S, ⊤), q.IsPrime → (t ∈ q ↔ I ≤ q)) ∧
      ∀ (a : Γ(S, ⊤)) (ha : a ∈ I),
        letI : Fact (a ∈ I) := ⟨ha⟩
        ∀ q' : Ideal (Blowup I a), q'.IsPrime →
          ChartFreeOfRank f F M (CommRingCat.of (Γ(X, ⊤) ⊗[Γ(S, ⊤)] Blowup I a))
            (CommRingCat.ofHom (algebraMap Γ(X, ⊤) (Γ(X, ⊤) ⊗[Γ(S, ⊤)] Blowup I a)))
            (algebraMap Γ(X, ⊤) (Γ(X, ⊤) ⊗[Γ(S, ⊤)] Blowup I a) (f.appTop.hom a)) r
            (Ideal.map Algebra.TensorProduct.includeRight q')

exists_fg_ideal_forall_blowup_chart_exists_away_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BlowupFlattening.lean, line 57.

Stacks Project, Tag 0810. Let R → S be flat and of finite presentation with geometrically integral fibres, let f : R, and let M be a finite S-module which is finitely presented after inverting f and free of rank r at every extended prime pS with f ∉ p. Then there is a finitely generated ideal I ⊆ R with V(f) = V(I) such that for every a ∈ I, writing R' = R[I/a] and S' = S ⊗[R] R', the quotient M' of S' ⊗[S] M by its a-power torsion is free of rank r after inverting some g : S' outside p'S', for every prime p' of R'.

This is exists_fg_ideal_forall_blowup_chart_exists_away_basis_of_projective with its hypothesis Module.Projective R S supplied by Stacks 05FT, Algebra.projective_of_geometricallyIntegral_fibres.

public theorem exists_fg_ideal_forall_blowup_chart_exists_away_basis
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [Module.Flat R S]
    (M : Type v) [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M]
    [Module.Finite S M] (f : R) (r : ℕ)
    (hfibre : ∀ (p : Ideal R) (hp : p.IsPrime),
      letI := hp
      Algebra.IsGeometricallyIntegral p.ResidueField (p.Fiber S))
    (hfp : Module.FinitePresentation (Localization.Away (algebraMap R S f))
      (LocalizedModule (Submonoid.powers (algebraMap R S f)) M))
    (hrank : ∀ (p : Ideal R) (hp : p.IsPrime), f ∉ p →
      letI := hp
      let q := Ideal.map (algebraMap R S) p
      ∀ hq : q.IsPrime,
        letI := hq
        Nonempty
          (LocalizedModule q.primeCompl M ≃ₗ[Localization q.primeCompl]
            (Fin r → Localization q.primeCompl))) :
    ∃ I : Ideal R, I.FG ∧
      (∀ (p : Ideal R), p.IsPrime → (f ∈ p ↔ I ≤ p)) ∧
      ∀ (a : R) (ha : a ∈ I),
        letI : Fact (a ∈ I) := ⟨ha⟩
        let R' := Blowup I a
        let S' := S ⊗[R] R'
        let N := S' ⊗[S] M
        let M' := N ⧸ Submodule.torsion' S' N
          (Submonoid.powers (algebraMap S S' (algebraMap R S a)))
        ∀ (p' : Ideal R') (_hp' : p'.IsPrime), ∃ g : S',
          g ∉ Ideal.map Algebra.TensorProduct.includeRight p' ∧
          Nonempty
            (LocalizedModule (Submonoid.powers g) M' ≃ₗ[Localization.Away g]
              (Fin r → Localization.Away g))

Tag 0811, a lemma

Tag 0811 in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_opens_finitelyLocallyFree_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/BlowupIntegralFibres0811.lean, line 147. The attribute's comment: “the full statement under hypotheses (1)-(4) of the source: a U-admissible blowup and an open of the base change on which the strict transform is finitely locally free and which surjects onto the blowup”.

Stacks Project, Tag 0811. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be a morphism, let F be a quasi-coherent 𝒪_X-module and let U ⊆ S be a quasi-compact open. Assume

1. f is affine, of finite presentation, flat, with geometrically integral fibres;
2. F is of finite type;
3. F restricted to X_U is of finite presentation;
4. F is flat over S at every generic point of a fibre over a point of U.

Then there is a U-admissible blowup of S — given by a centre I of finite presentation whose support avoids U — and an open subscheme V of X ×_S Bl_I(S) such that

• (a) the strict transform of F along the blowup is free of finite rank on an open neighbourhood, inside V, of every point of V, that is, finitely locally free on V, and
• (b) V surjects onto Bl_I(S).

The rank at the generic point of a fibre over U is made constant by iterating [Stacks, Tag 080P]; the complement of U is made an effective Cartier divisor and then, locally on the base, principal on an affine open, by the observations of [Stacks, Tag 080Y]; and that case is [Stacks, Tag 0810].

theorem exists_isAdmissibleBlowup_opens_finitelyLocallyFree_surjective
    {S X : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S] (f : X ⟶ S)
    [IsAffineHom f] [Flat f] [GeometricallyIntegral f]
    (hf : AlgebraicGeometry.FinitePresentation f)
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (U : S.Opens)
    (hU : IsCompact (U : Set S))
    (hFU : (F.restrict (f ⁻¹ᵁ U).ι).IsFinitePresentation)
    (hflat : ∀ x : X, f.base x ∈ U → f.base ⁻¹' {f.base x} ⊆ closure {x} →
      IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ I : S.IdealSheafData,
      FinitePresentation I.subschemeι ∧
      Disjoint (U : Set S) (I.support : Set S) ∧
      Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
      ∃ V : (Stacks.StrictTransform.baseChange f (blowUpToBase I)).Opens,
        (∀ z : Stacks.StrictTransform.baseChange f (blowUpToBase I), z ∈ V →
          ∃ (W : (Stacks.StrictTransform.baseChange f (blowUpToBase I)).Opens) (n : ℕ),
            z ∈ W ∧ W ≤ V ∧
            Nonempty ((Stacks.StrictTransform.sheaf f (blowUpToBase I)
              (exceptionalIdeal I) F).restrict W.ι ≅
                SheafOfModules.free.{u} (ULift.{u} (Fin n)))) ∧
        Function.Surjective (V.ι ≫ pullback.snd f (blowUpToBase I)).base

Tag 0812, a lemma

Tag 0812 in the Stacks Project.

fittingIdealZero_quotient_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FittingIdealEtale.lean, line 83. The attribute's comment: “finite generation of the Fitting ideal”.

Stacks Project, Tag 0812. The zeroth Fitting ideal of a quotient of a finite projective algebra by a finitely generated ideal is finitely generated.

theorem fittingIdealZero_quotient_fg
    (A : Type u) (C : Type v) [CommRing A] [CommRing C] [Algebra A C]
    [Module.Finite A C] [Module.Projective A C] (J : Ideal C) (hJ : J.FG) :
    (fittingIdeal (R := A) (M := C ⧸ J) 0).FG

map_fittingIdealZero_quotient_eq_mul_of_etale_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FittingIdealEtale.lean, line 263. The attribute's comment: “factorization after localization”.

Stacks Project, Tag 0812. Let C be a finite locally free A-algebra and let J be an ideal of C. If C becomes étale over A after inverting h, then the extension of the zeroth Fitting ideal of C ⧸ J is the product of the extension of J with another ideal. This other ideal can be chosen finitely generated whenever J is finitely generated.

theorem map_fittingIdealZero_quotient_eq_mul_of_etale_away
    (A : Type u) (C : Type v) [CommRing A] [CommRing C] [Algebra A C]
    [Module.Finite A C] [Module.Projective A C] (h : C)
    (het : Algebra.Etale A (Localization.Away h)) (J : Ideal C) :
    ∃ J' : Ideal (Localization.Away h),
      (fittingIdeal (R := A) (M := C ⧸ J) 0).map (algebraMap A (Localization.Away h)) =
          J.map (algebraMap C (Localization.Away h)) * J' ∧
        (J.FG → J'.FG)

Tag 0813, a lemma

Tag 0813 in the Stacks Project.

exists_ideal_map_eq_mul_after_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/FittingIdealEtale.lean, line 403.

Stacks Project, Tag 0813. Let A → B be étale, let a ∈ A, and let J be a finitely generated ideal of B with V(J) ⊆ V(aB). At every prime q of B, after localizing at some g ∉ q, the extension of a finitely generated ideal I of A, with V(I) ⊆ V(a), is the product of the extension of J and a finitely generated ideal.

theorem exists_ideal_map_eq_mul_after_localization
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [Algebra.Etale A B] (a : A) (J : Ideal B) (hJ : J.FG)
    (hV : algebraMap A B a ∈ J.radical) (q : Ideal B) [q.IsPrime] :
    ∃ I : Ideal A, I.FG ∧ a ∈ I.radical ∧
      ∃ g : B, g ∉ q ∧
        ∃ J' : Ideal (Localization.Away g), J'.FG ∧
          Ideal.map ((algebraMap B (Localization.Away g)).comp (algebraMap A B)) I =
            Ideal.map (algebraMap B (Localization.Away g)) J * J'

Tag 0814, a lemma

Tag 0814 in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_isFlatOver_strictTransformSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/EtaleLocalFlatteningDescent.lean, line 106. The attribute's comment: “the surjectivity half of condition (1) is not assumed; it is unused”.

Stacks Project, Tag 0814. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be a morphism of schemes, let F be a quasi-coherent 𝒪_X-module and let U ⊆ S be a quasi-compact open. Assume given finitely many commutative squares jᵢ ≫ f = fᵢ ≫ eᵢ with

1. eᵢ : Sᵢ ⟶ S quasi-compact and étale,
2. jᵢ : Xᵢ ⟶ X étale and jointly surjective,
3. a centre Iᵢ on Sᵢ which is finitely presented as a closed subscheme and supported away from eᵢ⁻¹(U) — so the blowup of Sᵢ in Iᵢ is an eᵢ⁻¹(U)-admissible blowup — such that the strict transform of jᵢ^* F along it is flat over it.

Then there is a centre I on S, finitely presented and supported away from U, exhibiting the blowup of S in I as a U-admissible blowup, such that the strict transform of F along that blowup is flat over it.

theorem exists_isAdmissibleBlowup_isFlatOver_strictTransformSheaf {S X : Scheme.{u}}
    [CompactSpace S] [QuasiSeparatedSpace S] (f : X ⟶ S) (F : X.Modules) [F.IsQuasicoherent]
    (U : S.Opens) (hU : IsCompact (U : Set S)) {ι : Type*} [Finite ι]
    (Sᵢ Xᵢ : ι → Scheme.{u}) (e : ∀ i, Sᵢ i ⟶ S) (j : ∀ i, Xᵢ i ⟶ X)
    (fᵢ : ∀ i, Xᵢ i ⟶ Sᵢ i) (Iᵢ : ∀ i, (Sᵢ i).IdealSheafData)
    (he : ∀ i, Etale (e i) ∧ QuasiCompact (e i)) (hj : ∀ i, Etale (j i))
    (hcoverX : ∀ x : X, ∃ i : ι, ∃ y : Xᵢ i, (j i).base y = x)
    (hcomm : ∀ i, j i ≫ f = fᵢ i ≫ e i)
    (hadm : ∀ i, FinitePresentation (Iᵢ i).subschemeι ∧
      Disjoint (e i ⁻¹ᵁ U : Set (Sᵢ i)) ((Iᵢ i).support : Set (Sᵢ i)))
    (hflat : ∀ i, IsFlatOver
      (pullback.snd (fᵢ i) (blowUpToBase (Iᵢ i))).toLRSHom.toShHom
      (Stacks.StrictTransform.sheaf (fᵢ i) (blowUpToBase (Iᵢ i)) (exceptionalIdeal (Iᵢ i))
        ((Scheme.Modules.pullback (j i)).obj F))) :
    ∃ I : S.IdealSheafData,
      FinitePresentation I.subschemeι ∧
      Disjoint (U : Set S) (I.support : Set S) ∧
      Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
      IsFlatOver (pullback.snd f (blowUpToBase I)).toLRSHom.toShHom
        (Stacks.StrictTransform.sheaf f (blowUpToBase I) (exceptionalIdeal I) F)

Tag 0815, a theorem

Tag 0815 in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_isFlatOver_strictTransformSheaf_of_affineCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/ModuleFlatteningBlowup.lean, line 129.

Stacks Project, Tag 0815. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be locally of finite presentation with X quasi-compact, let F be a quasi-coherent 𝒪_X-module of finite type and let U ⊆ S be a quasi-compact open such that the restriction of F to f⁻¹(U) is of finite presentation and flat over U. Then there is a centre I on S, finitely presented and supported away from U, exhibiting the blowup of S in I as a U-admissible blowup, such that the strict transform of F along that blowup is an 𝒪_{X ×_S S'}-module of finite presentation and flat over the blowup.

The centre is the one of AlgebraicGeometry.exists_flatteningCentre_supportSet_eq_compl, whose support is S ∖ U; so the inverse image of U in the blowup is the complement of the exceptional divisor, hence retrocompact and scheme-theoretically dense, and [Stacks, Tag 081N] gives finite presentation of the flat strict transform from its finite presentation over that open.

theorem exists_isAdmissibleBlowup_isFlatOver_strictTransformSheaf_of_affineCharts
    [CompactSpace S] [QuasiSeparatedSpace S] [CompactSpace X] (f : X ⟶ S)
    [LocallyOfFinitePresentation f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (U : S.Opens) (hU : IsCompact (U : Set S))
    (hFfp : ((Scheme.Modules.pullback (f ⁻¹ᵁ U).ι).obj F).IsFinitePresentation)
    (hFflat : IsFlatOver (f ∣_ U).toLRSHom.toShHom
      ((Scheme.Modules.pullback (f ⁻¹ᵁ U).ι).obj F)) :
    ∃ I : S.IdealSheafData,
      FinitePresentation I.subschemeι ∧
      Disjoint (U : Set S) (I.support : Set S) ∧
      Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
      (Stacks.StrictTransform.sheaf f (blowUpToBase I)
        (exceptionalIdeal I) F).IsFinitePresentation ∧
      IsFlatOver (pullback.snd f (blowUpToBase I)).toLRSHom.toShHom
        (Stacks.StrictTransform.sheaf f (blowUpToBase I) (exceptionalIdeal I) F)

Sources

• Section 38.30, Tag 080X
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_admissibleBlowup_forall_restrict_factors · AlgebraicGeometry.exists_admissibleBlowup_finite_cover_restrict_factors · AlgebraicGeometry.cartierBoundaryDivisorReduction · AlgebraicGeometry.cartierBoundaryReduction · AlgebraicGeometry.StrictTransformProblem.isSolvable_of_local · AlgebraicGeometry.StrictTransformProblem.isSolvable_of_isSolvableIn · AlgebraicGeometry.exists_idealSheafData_forall_blowUp_exists_free_of_rank · Stacks.StrictTransform.exists_fg_ideal_forall_chartFreeOfRank

Section38.31 Applications#

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

Tag 081R, a lemma

Tag 081R in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_flat_finitePresentation_strictTransform_of_affineCase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/StrictTransformFinitePresentationFromFlat.lean, line 407. The attribute's comment: “the conclusion in full -- the strict transform flat AND of finite presentation -- under exactly the source's hypotheses (1) and (2): the affine case of the flatness assertion of [Stacks, Tag 0815] that the proof consumes is AlgebraicGeometry.AffineChartFlatteningCentreUnderSourceHypotheses.of_compactSpace, itself proved from [Stacks, Tag 0811]”.

Stacks Project, Tag 081R. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be of finite type and quasi-separated and let U ⊆ S be a quasi-compact open such that X_U ⟶ U is flat and locally of finite presentation. Then there is a U-admissible blowup of S along which the strict transform of X is flat and of finite presentation.

Both hypotheses of the source are present: (1) f of finite type and quasi-separated, and (2) X_U ⟶ U flat and locally of finite presentation. Hypothesis (2) is what exists_isAdmissibleBlowup_flat_finitePresentation_strictTransform_of_affineCharts and AlgebraicGeometry.exists_isAdmissibleBlowup_flat_strictTransform omit the flatness half of, on the ground that it enters only through the affine case they take as an input. It does enter only through it, but the hypothesis-free AlgebraicGeometry.AffineChartFlatteningCentre that those forms take is false in general, so no proof of the affine case can supply it. With hypothesis (2) present the chain closes: AlgebraicGeometry.AffineChartFlatteningCentre.of_affineCase produces the chart predicate precisely from hypothesis (2), by the source's own route through the immersion into affine space of [Stacks, Tag 04II], and the affine case it calls on is AffineChartFlatteningCentreUnderSourceHypotheses.of_compactSpace, itself proved from [Stacks, Tag 0811].

theorem exists_isAdmissibleBlowup_flat_finitePresentation_strictTransform_of_affineCase
    [CompactSpace S] [QuasiSeparatedSpace S] [LocallyOfFiniteType f] [QuasiCompact f]
    [QuasiSeparated f] (U : S.Opens) (hU : IsCompact (U : Set S)) (hflat : Flat (f ∣_ U))
    (hfp : LocallyOfFinitePresentation (f ∣_ U)) :
    ∃ ℐ : S.IdealSheafData,
      FinitePresentation ℐ.subschemeι ∧
        Disjoint (U : Set S) (ℐ.support : Set S) ∧
          Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase ℐ) ∧
            Flat (strictTransformToBlowUp f ℐ) ∧
              FinitePresentation (strictTransformToBlowUp f ℐ)

AlgebraicGeometry.exists_isAdmissibleBlowup_flat_strictTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/StrictTransformSchemeFlattening.lean, line 195. The attribute's comment: “the flatness assertion of the conclusion; the affine case is carried as the hypothesis AlgebraicGeometry.AffineChartFlatteningCentre, inherited from the flatness half of [Stacks, Tag 0815], and hypothesis (2) of the source — X_U ⟶ U flat and locally of finite presentation — is not assumed separately because it enters only through that hypothesis; finite presentation of the strict transform is not claimed”.

Stacks Project, Tag 081R, flatness assertion. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be of finite type and quasi-separated and let U ⊆ S be a quasi-compact open. Granted the affine case AlgebraicGeometry.AffineChartFlatteningCentre for the structure sheaf of X, there is a centre I on S, finitely presented and supported away from U, exhibiting the blowup of S in I as a U-admissible blowup, such that the strict transform of X along that blowup is flat over it.

The flatness assertion of [Stacks, Tag 0815] for 𝒪_X gives the centre and the flatness of the strict transform of 𝒪_X, and AlgebraicGeometry.flat_strictTransformToBlowUp_iff reads that as flatness of the strict transform of X.

theorem exists_isAdmissibleBlowup_flat_strictTransform [CompactSpace S] [QuasiSeparatedSpace S]
    [LocallyOfFiniteType f] [QuasiCompact f] [QuasiSeparated f] (U : S.Opens)
    (hU : IsCompact (U : Set S)) (H : AffineChartFlatteningCentre f X.unitModule U) :
    ∃ I : S.IdealSheafData,
      FinitePresentation I.subschemeι ∧
        Disjoint (U : Set S) (I.support : Set S) ∧
          Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
            Flat (strictTransformToBlowUp f I)

Tag 0B49, a lemma

Tag 0B49 in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_isFiniteLocallyFree_strictTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Applications/FiniteLocallyFreeStrictTransform.lean, line 155. The attribute's comment: “the conclusion of Tag 081R -- a U-admissible centre whose strict transform is flat and locally of finite presentation -- is carried as the hypothesis h081R. The library proves its first three clauses in AlgebraicGeometry.exists_isAdmissibleBlowup_flat_strictTransform, itself carrying the affine case AffineChartFlatteningCentre of Tag 0815, and does not claim the fourth, local finite presentation of the strict transform, at all. Everything else is proved here: the composite centre and its finite presentation, its support being exactly the complement of U, its admissibility, the two-step-blowup identification, vanishing of the second strict-transform ideal by flatness, density of the inverse image of U, and the passage to finite locally free”.

Stacks Project, Tag 0B49. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be proper and let U ⊆ S be a quasi-compact open over which X is finite locally free. Granted the conclusion of [Stacks, Tag 081R] for f and U, there is a U-admissible blowup of S along which the strict transform of X is finite locally free.

theorem exists_isAdmissibleBlowup_isFiniteLocallyFree_strictTransform {X S : Scheme.{u}}
    [CompactSpace S] [QuasiSeparatedSpace S] (f : X ⟶ S) [IsProper f] (U : S.Opens)
    (hU : IsCompact (U : Set S))
    [Stacks.Morphisms.IsFiniteLocallyFree (pullback.snd f U.ι)]
    (h081R : ∃ I : S.IdealSheafData,
      FinitePresentation I.subschemeι ∧ Disjoint (U : Set S) (I.support : Set S) ∧
        Flat (strictTransformToBlowUp f I) ∧
          LocallyOfFinitePresentation (strictTransformToBlowUp f I)) :
    ∃ I : S.IdealSheafData,
      Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
        Stacks.Morphisms.IsFiniteLocallyFree (strictTransformToBlowUp f I)

AlgebraicGeometry.exists_isAdmissibleBlowup_isFiniteLocallyFree_strictTransform_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Applications/FiniteLocallyFreeStrictTransformOfProper.lean, line 46. The attribute's comment: “the conclusion in full, under exactly the source's hypotheses (1) and (2)”.

Stacks Project, Tag 0B49. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be proper and let U ⊆ S be a quasi-compact open over which X is finite locally free. Then there is a U-admissible blowup of S along which the strict transform of X is finite locally free.

theorem exists_isAdmissibleBlowup_isFiniteLocallyFree_strictTransform_of_isProper
    {X S : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S] (f : X ⟶ S) [IsProper f]
    (U : S.Opens) (hU : IsCompact (U : Set S))
    [Stacks.Morphisms.IsFiniteLocallyFree (pullback.snd f U.ι)] :
    ∃ I : S.IdealSheafData,
      Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
        Stacks.Morphisms.IsFiniteLocallyFree (strictTransformToBlowUp f I)

Tag 081S, a lemma

Tag 081S in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_isOpenImmersion_strictTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/StrictTransformOpenSubscheme.lean, line 55.

Let f : X ⟶ S be a separated morphism of finite type with S quasi-compact and quasi-separated, and let U ⊆ S be a quasi-compact open such that f is an isomorphism over U. Then there is a centre M on S, finitely presented and supported away from U, such that the blowup of S in M is U-admissible and the strict transform of X along it is an open subscheme of that blowup.

theorem exists_isAdmissibleBlowup_isOpenImmersion_strictTransform {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens) (hU : IsCompact (U : Set S))
    [IsIso (f ∣_ U)] :
    ∃ M : S.IdealSheafData, FinitePresentation M.subschemeι ∧
      Disjoint (U : Set S) (M.support : Set S) ∧
        Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase M) ∧
          IsOpenImmersion (strictTransformToBlowUp f M)

AlgebraicGeometry.strictTransformOpenImmersion_of_isIso_morphismRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/StrictTransformOpenSubscheme.lean, line 142.

A separated morphism of finite type which is an isomorphism over a quasi-compact open U of a quasi-compact quasi-separated base satisfies AlgebraicGeometry.StrictTransformOpenImmersion: along the blowup in some finitely presented centre avoiding U, its strict transform is an open subscheme of the blowup.

theorem strictTransformOpenImmersion_of_isIso_morphismRestrict {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens) (hU : IsCompact (U : Set S))
    [IsIso (f ∣_ U)] : StrictTransformOpenImmersion f U

Tag 081T, a lemma

Tag 081T in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_dominating, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/DominatedByBlowup.lean, line 203. The attribute's comment: “conditional on cited 080Y and 081S, carried as hypotheses; qc/qs dropped”.

Stacks Project, Tag 081T. A proper morphism f : X ⟶ S which is an isomorphism over an open U ⊆ S is dominated by a U-admissible blowup: there are a U-admissible blowup b : S' ⟶ S and a morphism g : S' ⟶ X with g ≫ f = b.

public theorem exists_isAdmissibleBlowup_dominating (f : X ⟶ S) [IsProper f] (U : S.Opens)
    [IsIso (f ∣_ U)] (h080Y : CartierBoundaryReduction S U)
    (h081S : StrictTransformOpenImmersion f U) :
    ∃ (S' : Scheme.{u}) (b : S' ⟶ S),
      Stacks.Blowup.IsAdmissibleBlowup U b ∧ ∃ g : S' ⟶ X, g ≫ f = b

AlgebraicGeometry.exists_isAdmissibleBlowup_dominating_of_affineCase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/DominatingBlowupFromFlattening.lean, line 90. The attribute's comment: “the conclusion in full, under exactly the source's hypotheses: the cited [Stacks, Tag 080Y] is supplied by AlgebraicGeometry.cartierBoundaryReduction and the cited [Stacks, Tag 081S] by AlgebraicGeometry.strictTransformOpenImmersion_of_isIso_morphismRestrict, each of which stands on its own hypotheses alone”.

Stacks Project, Tag 081T. Let f : X ⟶ S be a proper morphism with S quasi-compact and quasi-separated, and let U ⊆ S be a quasi-compact open such that f is an isomorphism over U. Then there is a U-admissible blowup b : S' ⟶ S which dominates X: a morphism g : S' ⟶ X with g ≫ f = b.

The hypotheses are exactly the source's. Both results the source cites are supplied by proved declarations: [Stacks, Tag 080Y] by AlgebraicGeometry.cartierBoundaryReduction and [Stacks, Tag 081S] by AlgebraicGeometry.strictTransformOpenImmersion_of_isIso_morphismRestrict, each of which stands on its own hypotheses alone.

theorem exists_isAdmissibleBlowup_dominating_of_affineCase (f : X ⟶ S) [IsProper f]
    [CompactSpace S] [QuasiSeparatedSpace S] (U : S.Opens) (hU : IsCompact (U : Set S))
    [IsIso (f ∣_ U)] :
    ∃ (S' : Scheme.{u}) (b : S' ⟶ S),
      Stacks.Blowup.IsAdmissibleBlowup U b ∧ ∃ g : S' ⟶ X, g ≫ f = b

Tag 0CP1, a lemma

Tag 0CP1 in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_extending_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/SectionExtension.lean, line 96. The attribute's comment: “with Stacks 080Y and 081S as hypotheses, in the shape Stacks 081T consumes them”.

Stacks Project, Tag 0CP1. Let S be a quasi-compact and quasi-separated scheme, let W ⊆ S be a quasi-compact open subscheme and let U ⊆ W be a quasi-compact open subscheme. Let f : X ⟶ W be proper and let s : U ⟶ X satisfy s ≫ f = U.ι. Then there is a U-admissible blowup b : S' ⟶ S and a morphism s' : b⁻¹(W) ⟶ X with s' ≫ f = b|_{b⁻¹(W)} extending s, the extension being witnessed by a morphism t : U ⟶ b⁻¹(W) over W.

theorem exists_isAdmissibleBlowup_extending_section [CompactSpace S] [QuasiSeparatedSpace S]
    (W : S.Opens) (U : W.toScheme.Opens) (hW : IsCompact (W : Set S))
    (hU : IsCompact (U : Set W.toScheme)) (f : X ⟶ W.toScheme) [IsProper f]
    (s : U.toScheme ⟶ X) (hs : s ≫ f = U.ι)
    (h080Y : CartierBoundaryReduction W.toScheme U)
    (h081S : StrictTransformOpenImmersion (s.imageι ≫ f) U) :
    ∃ (S' : Scheme.{u}) (b : S' ⟶ S),
      Stacks.Blowup.IsAdmissibleBlowup (W.ι ''ᵁ U) b ∧
        ∃ s' : (b ⁻¹ᵁ W).toScheme ⟶ X,
          s' ≫ f = b ∣_ W ∧
            ∃ t : U.toScheme ⟶ (b ⁻¹ᵁ W).toScheme, t ≫ b ∣_ W = U.ι ∧ t ≫ s' = s

AlgebraicGeometry.exists_isAdmissibleBlowup_extending_section_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/SectionExtensionOfQcqs.lean, line 46. The attribute's comment: “the conclusion in full, under exactly the source's hypotheses (1)-(3)”.

Stacks Project, Tag 0CP1. Let S be a quasi-compact and quasi-separated scheme, let W ⊆ S be a quasi-compact open subscheme and let U ⊆ W be a quasi-compact open subscheme. Let f : X ⟶ W be proper and let s : U ⟶ X satisfy s ≫ f = U.ι. Then there is a U-admissible blowup b : S' ⟶ S and a morphism s' : b⁻¹(W) ⟶ X with s' ≫ f = b|_{b⁻¹(W)} extending s, the extension being witnessed by a morphism t : U ⟶ b⁻¹(W) over W.

theorem exists_isAdmissibleBlowup_extending_section_of_qcqs [CompactSpace S]
    [QuasiSeparatedSpace S] (W : S.Opens) (U : W.toScheme.Opens) (hW : IsCompact (W : Set S))
    (hU : IsCompact (U : Set W.toScheme)) (f : X ⟶ W.toScheme) [IsProper f]
    (s : U.toScheme ⟶ X) (hs : s ≫ f = U.ι) :
    ∃ (S' : Scheme.{u}) (b : S' ⟶ S),
      Stacks.Blowup.IsAdmissibleBlowup (W.ι ''ᵁ U) b ∧
        ∃ s' : (b ⁻¹ᵁ W).toScheme ⟶ X,
          s' ≫ f = b ∣_ W ∧
            ∃ t : U.toScheme ⟶ (b ⁻¹ᵁ W).toScheme, t ≫ b ∣_ W = U.ι ∧ t ≫ s' = s

Sources

• Section 38.31, Tag 081Q
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_isAdmissibleBlowup_flat_finitePresentation_strictTransform_of_affineCase · AlgebraicGeometry.exists_isAdmissibleBlowup_flat_strictTransform · AlgebraicGeometry.exists_isAdmissibleBlowup_isFiniteLocallyFree_strictTransform · AlgebraicGeometry.exists_isAdmissibleBlowup_isFiniteLocallyFree_strictTransform_of_isProper · AlgebraicGeometry.exists_isAdmissibleBlowup_isOpenImmersion_strictTransform · AlgebraicGeometry.strictTransformOpenImmersion_of_isIso_morphismRestrict · AlgebraicGeometry.exists_isAdmissibleBlowup_dominating · AlgebraicGeometry.exists_isAdmissibleBlowup_dominating_of_affineCase

Section38.32 Compactifications#

Section 38.32 of the Stacks Project, Tag 0ATT. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ATU, a lemma

Tag 0ATU in the Stacks Project.

AlgebraicGeometry.CategoryOfCompactifications.isCofiltered_category, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/DenseInterior.lean, line 267. The attribute's comment: “part (a)”.

The category of compactifications of a scheme over a quasi-compact, quasi-separated base is cofiltered.

theorem isCofiltered_category : IsCofiltered D.category

AlgebraicGeometry.CategoryOfCompactifications.initial_ι_hasDenseInterior, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/DenseInterior.lean, line 283. The attribute's comment: “part (b)”.

The full subcategory of compactifications whose interior is dense and scheme-theoretically dense is initial.

theorem initial_ι_hasDenseInterior : (HasDenseInterior D.X).ι.Initial

AlgebraicGeometry.preimage_range_immersion_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/Compactifications.lean, line 140. The attribute's comment: “preimage_of_interior”.

Stacks Project, Tag 0ATU. For a morphism between compactifications whose source interior is dense, the inverse image of the target interior is exactly the source interior.

lemma preimage_range_immersion_eq
    (D : CategoryOfCompactifications.{u}) (j' j : D.category) (f : j' ⟶ j)
    (hdense : DenseRange j'.immersion.base) :
    (CompactificationOf.Hom.map f).base ⁻¹'
      Set.range j.immersion.base = Set.range j'.immersion.base

AlgebraicGeometry.CategoryOfCompactifications.isCofiltered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/CompactificationsCofiltered.lean, line 167. The attribute's comment: “cofiltered”.

Stacks Project, Tag 0ATU. The category of compactifications of a scheme over a quasi-compact and quasi-separated base is cofiltered.

instance isCofiltered : IsCofiltered D.category

AlgebraicGeometry.CategoryOfCompactifications.denseCompactification_initial, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/CompactificationsCofiltered.lean, line 195. The attribute's comment: “dense_compactifications_initial”.

Stacks Project, Tag 0ATU. The compactifications in which the image of X is dense and scheme-theoretically dense form an initial full subcategory of the category of all compactifications.

instance denseCompactification_initial :
    (ObjectProperty.ι (IsDenseCompactification D : ObjectProperty D.category)).Initial

Tag 0A9Z, a lemma

Tag 0A9Z in the Stacks Project.

AlgebraicGeometry.exists_quasiCompact_compactification_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/OverIntermediate.lean, line 47. References: SGA 4 XVII (3.2.2), “(v)”.

A compactifiable S-scheme is also compactifiable over a separated finite-type S-scheme through which its structure morphism factors.

theorem exists_quasiCompact_compactification_over
    {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S]
    [IsSeparated g] [LocallyOfFiniteType g] [QuasiCompact g]
    (hX : ∃ j : CompactificationOf (Over.mk (f ≫ g)),
      QuasiCompact j.immersion) :
    ∃ j : CompactificationOf (Over.mk f),
      QuasiCompact j.immersion

Tag 0ATV, a lemma

Tag 0ATV in the Stacks Project.

AlgebraicGeometry.interiorIsomorphisms_hasRightCalculusOfFractions, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/CompactificationFractions.lean, line 365.

Stacks Project, Tag 0ATV. Morphisms of compactifications inducing an isomorphism on the open subschemes form a right multiplicative system.

instance interiorIsomorphisms_hasRightCalculusOfFractions (S : Scheme.{u}) :
    (interiorIsomorphisms S).HasRightCalculusOfFractions

Tag 0ATW, a lemma

Tag 0ATW in the Stacks Project.

AlgebraicGeometry.localizedInteriorEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/LocalizationEquivalence.lean, line 390. The attribute's comment: “the equivalence”.

Stacks Project, Tag 0ATW. The equivalence induced by forgetting the ambient proper scheme after localizing compactifications at interior isomorphisms.

noncomputable def localizedInteriorEquivalence (S : Scheme.{u})
    [CompactSpace S] [QuasiSeparatedSpace S] :
    (interiorIsomorphisms S).Localization ≌ Compactifyable S

AlgebraicGeometry.localizedInteriorEquivalenceCompQ, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/LocalizationEquivalence.lean, line 404. The attribute's comment: “the forgetful functor”.

Stacks Project, Tag 0ATW. The equivalence extends the forgetful functor from compactifications, up to a canonical natural isomorphism.

noncomputable def localizedInteriorEquivalenceCompQ (S : Scheme.{u})
    [CompactSpace S] [QuasiSeparatedSpace S] :
    (interiorIsomorphisms S).Q ⋙
        (localizedInteriorEquivalence S).functor ≅ compactificationInterior S

Sources

• Section 38.32, Tag 0ATT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.CategoryOfCompactifications.isCofiltered_category · AlgebraicGeometry.CategoryOfCompactifications.initial_ι_hasDenseInterior · AlgebraicGeometry.preimage_range_immersion_eq · AlgebraicGeometry.CategoryOfCompactifications.isCofiltered · AlgebraicGeometry.CategoryOfCompactifications.denseCompactification_initial · AlgebraicGeometry.exists_quasiCompact_compactification_over · AlgebraicGeometry.interiorIsomorphisms_hasRightCalculusOfFractions · AlgebraicGeometry.localizedInteriorEquivalence

Section38.33 Nagata compactification#

Section 38.33 of the Stacks Project, Tag 0F3T. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0F3U, a lemma

Tag 0F3U in the Stacks Project.

AlgebraicGeometry.isSeparated_of_sup_eq_top_of_isClosedImmersion_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/SeparatedTwoOpens.lean, line 47.

Stacks Project, Tag 0F3U. Two separated open subschemes covering the source, whose overlap is closed in their fibre product over the base, give a separated morphism.

theorem isSeparated_of_sup_eq_top_of_isClosedImmersion_mapDesc
    {X S : Scheme.{u}} (f : X ⟶ S) (U V : X.Opens)
    (hcover : U ⊔ V = ⊤)
    [IsSeparated (U.ι ≫ f)] [IsSeparated (V.ι ≫ f)]
    (hUV : IsClosedImmersion (pullback.mapDesc U.ι V.ι f)) :
    IsSeparated f

Tag 0F3V, a lemma

Tag 0F3V in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_disjoint_strictTransforms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Separation.lean, line 331. The attribute's comment: “separate_strict_transforms”.

Stacks Project, Tag 0F3V, part (1). Let X be a quasi-compact and quasi-separated scheme and U ⊆ X an open. Let Z₁ = V(ℐ₁) and Z₂ = V(ℐ₂) be closed subschemes of finite presentation which do not meet inside U. Then there is a centre of finite presentation disjoint from U — so that the blowup of X in it is a U-admissible blowup — on which the strict transforms of Z₁ and Z₂ are disjoint.

Quasi-compactness of U is not needed; see the implementation notes of this file.

theorem exists_isAdmissibleBlowup_disjoint_strictTransforms [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (I₁ I₂ : X.IdealSheafData)
    (h₁ : FinitePresentation I₁.subschemeι) (h₂ : FinitePresentation I₂.subschemeι)
    (hdisj : Disjoint ((U : Set X) ∩ (I₁.support : Set X)) (I₂.support : Set X)) :
    ∃ I : X.IdealSheafData, Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase I) ∧
      Disjoint (U : Set X) (I.support : Set X) ∧
        Disjoint (Set.range (strictTransformToBlowUp I₁.subschemeι I).base)
          (Set.range (strictTransformToBlowUp I₂.subschemeι I).base)

AlgebraicGeometry.exists_isAdmissibleBlowup_disjoint_closures, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Separation.lean, line 474. The attribute's comment: “separate_constructible_closures”.

Stacks Project, Tag 0F3V, part (2). Let X be a quasi-compact and quasi-separated scheme, let U ⊆ X be a quasi-compact open and let T₁, T₂ ⊆ U be disjoint constructible closed subsets. Then there is a U-admissible blowup X' ⟶ X in which the closures of T₁ and T₂ are disjoint.

This is part (1) applied to closed subschemes of X cutting out T₁ and T₂ on U: the closure of the preimage of Tᵢ is contained in the strict transform of the i-th subscheme, which is closed because the subscheme is a closed subscheme of X.

theorem exists_isAdmissibleBlowup_disjoint_closures [CompactSpace X] [QuasiSeparatedSpace X]
    (U : X.Opens) (hU : IsCompact (U : Set X)) (T₁ T₂ : Set U.toScheme)
    (hT₁ : IsClosed T₁) (hT₂ : IsClosed T₂) (hc₁ : Topology.IsConstructible T₁)
    (hc₂ : Topology.IsConstructible T₂) (hdisj : Disjoint T₁ T₂) :
    ∃ (X' : Scheme.{u}) (f : X' ⟶ X), Stacks.Blowup.IsAdmissibleBlowup U f ∧
      Disjoint (closure (f.base ⁻¹' (U.ι.base '' T₁)))
        (closure (f.base ⁻¹' (U.ι.base '' T₂)))

Tag 0F3W, a lemma

Tag 0F3W in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_strictTransform_isIso_near_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/IsoNearClosure.lean, line 178.

Stacks Project, Tag 0F3W. A proper morphism which is an isomorphism over an open containing a subset T closed in a quasi-compact open V becomes, after a V-admissible blowup, a morphism whose strict transform is an isomorphism over an open neighbourhood of the closure of the inverse image of T.

theorem exists_isAdmissibleBlowup_strictTransform_isIso_near_closure
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
    [CompactSpace X] [QuasiSeparatedSpace X]
    [CompactSpace Y] [QuasiSeparatedSpace Y]
    (V : Y.Opens) (hV : IsCompact (V : Set Y))
    (T : Set Y) (hTV : T ⊆ (V : Set Y))
    (hT : IsClosed (V.ι.base ⁻¹' T))
    (hiso : ∃ W : Y.Opens, W ≤ V ∧ T ⊆ (W : Set Y) ∧ IsIso (f ∣_ W)) :
    ∃ I : Y.IdealSheafData,
      FinitePresentation I.subschemeι ∧
      Disjoint (V : Set Y) (I.support : Set Y) ∧
      ∃ W : (blowUp I).Opens,
        closure ((blowUpToBase I).base ⁻¹' T) ⊆ (W : Set (blowUp I)) ∧
        IsIso (strictTransformToBlowUp f I ∣_ W)

Tag 0F3X, a lemma

Tag 0F3X in the Stacks Project.

AlgebraicGeometry.exists_common_isAdmissibleBlowup_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/CommonAdmissibleBlowups.lean, line 214.

Stacks Project, Tag 0F3X. Let S be a quasi-compact and quasi-separated scheme and let u₁ : U ⟶ X₁ and u₂ : U ⟶ X₂ be open immersions of schemes over S, with U, X₁ and X₂ of finite type and separated over S. Then there is a commutative diagram of schemes over S in which Xᵢ' ⟶ Xᵢ is a U-admissible blowup, Xᵢ' ⟶ X is an open immersion, and X is separated and of finite type over S.

theorem exists_common_isAdmissibleBlowup_isOpenImmersion {S U X₁ X₂ : Scheme.{u}}
    [CompactSpace S] [QuasiSeparatedSpace S]
    (fU : U ⟶ S) (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S)
    [LocallyOfFiniteType fU] [QuasiCompact fU] [IsSeparated fU]
    [LocallyOfFiniteType f₁] [QuasiCompact f₁] [IsSeparated f₁]
    [LocallyOfFiniteType f₂] [QuasiCompact f₂] [IsSeparated f₂]
    (u₁ : U ⟶ X₁) (u₂ : U ⟶ X₂) [IsOpenImmersion u₁] [IsOpenImmersion u₂]
    (hu₁ : u₁ ≫ f₁ = fU) (hu₂ : u₂ ≫ f₂ = fU) :
    ∃ (X₁' X₂' X : Scheme.{u}) (b₁ : X₁' ⟶ X₁) (b₂ : X₂' ⟶ X₂)
      (j₁ : X₁' ⟶ X) (j₂ : X₂' ⟶ X)
      (v₁ : U ⟶ X₁') (v₂ : U ⟶ X₂') (v : U ⟶ X) (f : X ⟶ S),
      Stacks.Blowup.IsAdmissibleBlowup u₁.opensRange b₁ ∧
        Stacks.Blowup.IsAdmissibleBlowup u₂.opensRange b₂ ∧
          IsOpenImmersion j₁ ∧ IsOpenImmersion j₂ ∧
            LocallyOfFiniteType f ∧ QuasiCompact f ∧ IsSeparated f ∧
              (v₁ ≫ b₁ = u₁) ∧ (v₂ ≫ b₂ = u₂) ∧
                (v₁ ≫ j₁ = v) ∧ (v₂ ≫ j₂ = v) ∧
                  (b₁ ≫ f₁ = j₁ ≫ f) ∧ (b₂ ≫ f₂ = j₂ ≫ f) ∧ (v ≫ f = fU)

Tag 0F3Y, a lemma

Tag 0F3Y in the Stacks Project.

Stacks.Blowup.exists_iso_image_strictTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/StrictTransformImage.lean, line 242.

Stacks Project, Tag 0F3Y. For f : V ⟶ X ×_S Y quasi-compact with first projection landing in an open U ⊆ X, a U-admissible blowup b : X' ⟶ X and a lift g : V ⟶ X' ×_S Y of f, the scheme-theoretic image of g is the strict transform along b of that of f.

theorem exists_iso_image_strictTransform
    {X Y S V X' : Scheme.{u}} (p : X ⟶ S) (q : Y ⟶ S)
    (U : X.Opens) (b : X' ⟶ X)
    (f : V ⟶ pullback p q) [QuasiCompact f]
    (g : V ⟶ pullback (b ≫ p) q)
    (hfU : Set.range (f ≫ pullback.fst p q).base ⊆ (U : Set X))
    (hbgX : g ≫ pullback.fst (b ≫ p) q ≫ b = f ≫ pullback.fst p q)
    (hbgY : g ≫ pullback.snd (b ≫ p) q = f ≫ pullback.snd p q)
    (hb : IsAdmissibleBlowup U b) :
    ∃ I : X.IdealSheafData,
      ∃ e : X' ≅ blowUp I,
        e.hom ≫ blowUpToBase I = b ∧
        Disjoint (U : Set X) (I.support : Set X) ∧
        ∃ (j : strictTransform (f.imageι ≫ pullback.fst p q) I ⟶ pullback (b ≫ p) q)
          (a : g.image ≅ strictTransform (f.imageι ≫ pullback.fst p q) I),
          j ≫ pullback.fst (b ≫ p) q ≫ e.hom =
            strictTransformι (f.imageι ≫ pullback.fst p q) I ≫
              pullback.snd (f.imageι ≫ pullback.fst p q) (blowUpToBase I) ∧
          j ≫ pullback.snd (b ≫ p) q =
            strictTransformι (f.imageι ≫ pullback.fst p q) I ≫
              pullback.fst (f.imageι ≫ pullback.fst p q) (blowUpToBase I) ≫
                f.imageι ≫ pullback.snd p q ∧
          a.hom ≫ j = g.imageι

Tag 0F3Z, a lemma

Tag 0F3Z in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_properExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/ProperExtension.lean, line 62.

Stacks Project, Tag 0F3Z. After a V-admissible blowup b : Y' ⟶ Y of a compactification j of a quasi-compact open subscheme V of U, the blowup contains an open subscheme V' which maps properly to U, extending the inclusion of V, and whose copy of V is exactly the inverse image of the interior of the compactification.

theorem exists_isAdmissibleBlowup_properExtension
    {S U : Scheme.{u}} (f : U ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S]
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    (V : U.Opens) [QuasiCompact V.ι]
    (j : CompactificationOf (Over.mk (V.ι ≫ f))) :
    ∃ (Y' : Scheme.{u}) (b : Y' ⟶ j.space) (V' : Y'.Opens)
      (e : V.toScheme ⟶ V'.toScheme) (p : V'.toScheme ⟶ U),
      Stacks.Blowup.IsAdmissibleBlowup j.immersion.opensRange b ∧
        IsOpenImmersion e ∧
        Set.range (e ≫ V'.ι).base =
          (b ⁻¹ᵁ j.immersion.opensRange : Y'.Opens) ∧
        e ≫ V'.ι ≫ b = j.immersion ∧
        IsProper p ∧
        e ≫ p = V.ι ∧ p ≫ f = V'.ι ≫ b ≫ j.toBase

Tag 0F40, a lemma

Tag 0F40 in the Stacks Project.

AlgebraicGeometry.hasCompactification_of_two_opens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/TwoOpens.lean, line 162.

Stacks Project, Tag 0F40. A separated finite-type scheme over a Noetherian base has a compactification as soon as it is covered by two compactifiable open subschemes whose intersection is dense.

theorem hasCompactification_of_two_opens
    {S U : Scheme.{u}} (f : U ⟶ S)
    [IsNoetherian S] [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    (U₁ U₂ : U.Opens) (hcover : U₁ ⊔ U₂ = ⊤)
    (hdense : Dense ((U₁ ⊓ U₂ : U.Opens) : Set U))
    (h₁ : HasCompactification (U₁.ι ≫ f)) (h₂ : HasCompactification (U₂.ι ≫ f)) :
    HasCompactification f

Tag 0F41, a theorem

Tag 0F41 in the Stacks Project.

AlgebraicGeometry.exists_quasiCompact_compactificationOf_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Compactification/QuasiAffineSource.lean, line 86. The attribute's comment: “the case of a quasi-affine source”. References: SGA 4½ Arcata (4.5.3), “special case”; SGA 4½ Th finitude (2.8), “more general”; SGA 7 XIII (2.1.6), “2.1.6 c), special case”.

Nagata compactification for a quasi-affine source (Stacks Project, Tag 0F41). A separated morphism of finite type from a quasi-affine scheme to a quasi-compact and quasi-separated scheme admits a compactification: a quasi-compact open immersion into a scheme proper over the base.

The source statement has no quasi-affineness hypothesis; this is the case of its proof in which the source immerses into relative projective space directly, with no gluing along a covering.

theorem exists_quasiCompact_compactificationOf_of_isQuasiAffine
    {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S] [IsSeparated f]
    [LocallyOfFiniteType f] [QuasiCompact f] [X.IsQuasiAffine] :
    ∃ j : CompactificationOf (Over.mk f), QuasiCompact j.immersion

AlgebraicGeometry.hasCompactification_of_compactSpace_quasiSeparatedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataCompactification/Basic.lean, line 152. References: SGA 4 XVII (3.2.2), “more general”; SGA 4 XVII (3.2.3), “(iii), special case”; SGA 4½ Th finitude (2.8), “more general”; SGA 7 XIII (2.1.6), “more general”.

Nagata compactification (Stacks Project, Tag 0F41). Let S be a quasi-compact and quasi-separated scheme and let f : X ⟶ S be a separated morphism of finite type. Then X has a compactification over S: f factors as a quasi-compact open immersion of X into a scheme proper over S.

[Stacks, Tag 01ZJ] factors f through a closed immersion into a separated morphism of finite presentation, and compactifiability descends along a closed immersion.

theorem hasCompactification_of_compactSpace_quasiSeparatedSpace {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S] [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] : HasCompactification f

Sources

• Section 38.33, Tag 0F3T
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isSeparated_of_sup_eq_top_of_isClosedImmersion_mapDesc · AlgebraicGeometry.exists_isAdmissibleBlowup_disjoint_strictTransforms · AlgebraicGeometry.exists_isAdmissibleBlowup_disjoint_closures · AlgebraicGeometry.exists_isAdmissibleBlowup_strictTransform_isIso_near_closure · AlgebraicGeometry.exists_common_isAdmissibleBlowup_isOpenImmersion · Stacks.Blowup.exists_iso_image_strictTransform · AlgebraicGeometry.exists_isAdmissibleBlowup_properExtension · AlgebraicGeometry.hasCompactification_of_two_opens

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.