38.34 The h topology to 38.42 An operator introduced by…

Section38.34 The h topology #

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

Tag 0ETR, a lemma

Tag 0ETR in the Stacks Project.

AlgebraicGeometry.isPHCovering_iff_isVCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/PhVFlatteningModification.lean, line 493. The attribute's comment: “the equivalence of (1) and (2) for a family locally of finite presentation, which is the whole of the lemma”.

Stacks 0ETR. A family of morphisms of schemes which are locally of finite presentation is a ph covering if and only if it is a V covering.

The implication from a ph covering to a V covering is AlgebraicGeometry.isVCovering_of_isPHCovering and needs nothing; the converse is the six-step argument of the source, whose last input — the refinement of a standard V covering of an affine scheme by a standard ph covering, AlgebraicGeometry.StandardVCoveringHasPHRefinement — is AlgebraicGeometry.standardVCoveringHasPHRefinement above.

theorem isPHCovering_iff_isVCovering {T : Scheme.{u}} {I : Type v} (X : I → Scheme.{u})
    (f : ∀ i, X i ⟶ T) (hfp : ∀ i, LocallyOfFinitePresentation (f i)) :
    IsPHCovering X f ↔ IsVCovering X f

Tag 0ETS, a definition

Tag 0ETS in the Stacks Project.

AlgebraicGeometry.IsHCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/Coverings.lean, line 34.

A family {X i ⟶ T} of morphisms of schemes is an h covering when every member is locally of finite presentation and the family is a ph covering.

public abbrev IsHCovering {T : Scheme.{u}} {I : Type v} (X : I → Scheme.{u})
    (f : ∀ i, X i ⟶ T) : Prop

Tag 0ETT, a lemma

Tag 0ETT in the Stacks Project.

AlgebraicGeometry.isHCovering_of_universallySubmersive_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SubmersiveFlatteningRefinement.lean, line 329. The attribute's comment: “(1) implies (2)”.

Stacks 0ETT, (1) implies (2). A finite family of morphisms of finite type to a Noetherian scheme whose disjoint-union morphism is universally submersive is an h covering.

This is AlgebraicGeometry.isHCovering_of_universallySubmersive with its hypothesis supplied by AlgebraicGeometry.universallySubmersiveHasPHRefinement.

theorem isHCovering_of_universallySubmersive_of_isNoetherian {X : Scheme.{u}} [IsNoetherian X]
    {I : Type v} [Finite I] [Small.{u} I] {Y : I → Scheme.{u}} (f : ∀ i, Y i ⟶ X)
    [∀ i, LocallyOfFiniteType (f i)] [∀ i, QuasiCompact (f i)]
    (hsub : UniversallySubmersive (Sigma.desc f)) : IsHCovering Y f

AlgebraicGeometry.universallySubmersive_sigmaDesc_iff_isHCovering_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SubmersiveFlatteningRefinement.lean, line 345.

Stacks 0ETT. For a finite family {X i ⟶ X} of morphisms of finite type to a Noetherian scheme X, the morphism ∐ X i ⟶ X is universally submersive if and only if the family is an h covering.

The implication from the h covering condition is AlgebraicGeometry.universallySubmersive_sigmaDesc_of_isHCovering and needs neither finiteness nor the Noetherian hypothesis; the converse is AlgebraicGeometry.isHCovering_of_universallySubmersive_of_isNoetherian above.

theorem universallySubmersive_sigmaDesc_iff_isHCovering_of_isNoetherian {X : Scheme.{u}}
    [IsNoetherian X] {I : Type v} [Finite I] [Small.{u} I] {Y : I → Scheme.{u}} (f : ∀ i, Y i ⟶ X)
    [∀ i, LocallyOfFiniteType (f i)] [∀ i, QuasiCompact (f i)] :
    UniversallySubmersive (Sigma.desc f) ↔ IsHCovering Y f

AlgebraicGeometry.universallySubmersive_sigmaDesc_of_isHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/UniversallySubmersive.lean, line 114. The attribute's comment: “(2) implies (1)”.

Stacks 0ETT, (2) implies (1). The morphism from the disjoint union of the sources of an h covering to its target is universally submersive.

An h covering is a ph covering, hence a V covering, and the disjoint-union morphism of a V covering is universally submersive. No Noetherian or finiteness hypothesis is involved.

theorem universallySubmersive_sigmaDesc_of_isHCovering {X : Scheme.{u}} {I : Type v}
    [Small.{u} I] {Y : I → Scheme.{u}} {f : ∀ i, Y i ⟶ X} (hf : IsHCovering Y f) :
    UniversallySubmersive (Sigma.desc f)

AlgebraicGeometry.isHCovering_of_universallySubmersive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/UniversallySubmersive.lean, line 168. The attribute's comment: “(1) implies (2)”.

Stacks 0ETT, (1) implies (2), granted AlgebraicGeometry.UniversallySubmersiveHasPHRefinement: a finite family of morphisms of finite type to a Noetherian scheme whose disjoint-union morphism is universally submersive is an h covering.

The hypothesis supplies a ph covering refining the family; a family of morphisms locally of finite type refined by a ph covering is a ph covering (Stacks 0ET9), and over a locally Noetherian base the ph coverings are exactly the h coverings (Stacks 0H45).

theorem isHCovering_of_universallySubmersive (H : UniversallySubmersiveHasPHRefinement.{u, v})
    {X : Scheme.{u}} [IsNoetherian X] {I : Type v} [Finite I] [Small.{u} I]
    {Y : I → Scheme.{u}} (f : ∀ i, Y i ⟶ X) [∀ i, LocallyOfFiniteType (f i)]
    [∀ i, QuasiCompact (f i)] (hsub : UniversallySubmersive (Sigma.desc f)) :
    IsHCovering Y f

AlgebraicGeometry.universallySubmersive_sigmaDesc_iff_isHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/UniversallySubmersive.lean, line 184.

Stacks 0ETT, granted AlgebraicGeometry.UniversallySubmersiveHasPHRefinement: for a finite family {X i ⟶ X} of morphisms of finite type to a Noetherian scheme X, the morphism ∐ X i ⟶ X is universally submersive if and only if the family is an h covering.

The implication from the h covering condition is unconditional; the hypothesis is used only for the converse.

theorem universallySubmersive_sigmaDesc_iff_isHCovering
    (H : UniversallySubmersiveHasPHRefinement.{u, v}) {X : Scheme.{u}} [IsNoetherian X]
    {I : Type v} [Finite I] [Small.{u} I] {Y : I → Scheme.{u}} (f : ∀ i, Y i ⟶ X)
    [∀ i, LocallyOfFiniteType (f i)] [∀ i, QuasiCompact (f i)] :
    UniversallySubmersive (Sigma.desc f) ↔ IsHCovering Y f

Tag 0H45, a lemma

Tag 0H45 in the Stacks Project.

AlgebraicGeometry.isHCovering_iff_isPHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Coverings.lean, line 124.

Stacks 0H45. Over a locally Noetherian scheme a family of morphisms is an h covering if and only if it is a ph covering, because there local finite presentation and local finite type agree.

public theorem isHCovering_iff_isPHCovering {T : Scheme.{u}} [IsLocallyNoetherian T]
    {I : Type v} (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T) :
    IsHCovering X f ↔ IsPHCovering X f

Tag 0ETU, a lemma

Tag 0ETU in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_proper_refinement_of_isHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/ProperFinitePresentationRefinement.lean, line 157.

Stacks 0ETU. An h covering of an affine scheme T is refined by a finite family of affine opens of a single proper surjective morphism Y ⟶ T of finite presentation: the opens cover Y and each of them maps to a member of the h covering over T.

public theorem exists_finitePresentation_proper_refinement_of_isHCovering
    {T : Scheme.{u}} [IsAffine T] {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : IsHCovering X f) :
    ∃ (J : Type u) (Y : Scheme.{u}) (p : Y ⟶ T)
      (V : J → Scheme.{u}) (j : ∀ k, V k ⟶ Y),
      Finite J ∧
        IsProper p ∧
        Surjective p ∧
        FinitePresentation p ∧
        (∀ k, IsAffine (V k)) ∧
        (∀ k, IsOpenImmersion (j k)) ∧
        (⋃ k, Set.range (j k)) = Set.univ ∧
        (∀ k, ∃ i : I, ∃ h : V k ⟶ X i, h ≫ f i = j k ≫ p)

Tag 0ETV, a lemma

Tag 0ETV in the Stacks Project.

AlgebraicGeometry.IsHCovering.of_fppf_syntomic_smooth_etale_zariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/FppfHComparison.lean, line 104.

[Stacks, Tag 0ETV]. An fppf covering is an h covering. Hence syntomic, smooth, étale and Zariski coverings are h coverings as well.

Here a family {f i : X i ⟶ T} is an fppf (resp. syntomic, smooth, étale, Zariski) covering when its members are flat and locally of finite presentation (resp. syntomic, smooth, étale, open immersions) and jointly surjective, that is, when Presieve.ofArrows X f belongs to the corresponding precoverage; it is an h covering, AlgebraicGeometry.IsHCovering (Stacks 0ETS), when its members are locally of finite presentation and it is a ph covering (Stacks 0DBG).

The fppf case holds because the members of an fppf covering are locally of finite presentation and an fppf covering is a ph covering, Stacks 0DBT; the other four follow from it and Stacks 021N.

public theorem IsHCovering.of_fppf_syntomic_smooth_etale_zariski {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T) :
    (Presieve.ofArrows X f ∈ Scheme.fppfPrecoverage T → IsHCovering X f) ∧
    (Presieve.ofArrows X f ∈
      Scheme.precoverage (@Syntomic : MorphismProperty Scheme.{u}) T → IsHCovering X f) ∧
    (Presieve.ofArrows X f ∈
      Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}) T → IsHCovering X f) ∧
    (Presieve.ofArrows X f ∈ Scheme.etalePrecoverage T → IsHCovering X f) ∧
    (Presieve.ofArrows X f ∈ Scheme.zariskiPrecoverage T → IsHCovering X f)

Tag 0ETW, a lemma

Tag 0ETW in the Stacks Project.

AlgebraicGeometry.surjective_proper_isHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Coverings.lean, line 115.

Stacks 0ETW. A surjective proper morphism of schemes of finite presentation is an h covering by itself.

public theorem surjective_proper_isHCovering {X Y : Scheme.{u}} (f : Y ⟶ X)
    [Surjective f] [IsProper f] (hf : FinitePresentation f) :
    IsHCovering (fun _ : Unit ↦ Y) (fun _ ↦ f)

Tag 0ETX, a lemma

Tag 0ETX in the Stacks Project.

AlgebraicGeometry.isHCovering_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/CoveringRefinement.lean, line 49.

Stacks 0ETX. A family of morphisms of schemes which are locally of finite presentation is an h covering if and only if some h covering refines it, if and only if its disjoint-union morphism is an h covering.

public theorem isHCovering_tfae {T : Scheme.{u}} {I : Type v} [Small.{u} I]
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hlfp : ∀ i, LocallyOfFinitePresentation (f i)) :
    List.TFAE [
      IsHCovering X f,
      ∃ (K : Type v) (Y : K → Scheme.{u}) (g : ∀ k, Y k ⟶ T),
        IsHCovering Y g ∧
          Nonempty
            (({ I₀ := K, X := Y, f := g } : PreZeroHypercover T).Hom
              ({ I₀ := I, X := X, f := f } : PreZeroHypercover T)),
      IsHCovering (fun _ : Unit ↦ ∐ X) (fun _ ↦ Sigma.desc f)]

Tag 0ETY, a lemma

Tag 0ETY in the Stacks Project.

AlgebraicGeometry.isHCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Coverings.lean, line 108. The attribute's comment: “part (1)”.

Stacks 0ETY, part (1). An isomorphism of schemes, regarded as a family indexed by a type with exactly one element, is an h covering.

public theorem isHCovering_of_isIso {T' T : Scheme.{u}} {I : Type v} [Unique I] (f : T' ⟶ T)
    [IsIso f] : IsHCovering (fun _ : I ↦ T') (fun _ ↦ f)

AlgebraicGeometry.isHCovering_bind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Coverings.lean, line 185. The attribute's comment: “part (2)”.

Stacks 0ETY part (2). Composing an h covering with an h covering of each of its members gives an h covering.

Local finite presentation is closed under composition, and the ph-covering condition is AlgebraicGeometry.isPHCovering_bind, which is Stacks 0DBI part (2).

public theorem isHCovering_bind {T : Scheme.{u}}
    (E : PreZeroHypercover.{v} T) (hE : IsHCovering E.X E.f)
    (F : ∀ i, PreZeroHypercover.{w} (E.X i))
    (hF : ∀ i, IsHCovering (F i).X (F i).f) :
    IsHCovering (E.bind F).X (E.bind F).f

AlgebraicGeometry.isHCovering_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Coverings.lean, line 202. The attribute's comment: “part (3)”.

Stacks 0ETY part (3). The base change of an h covering along an arbitrary morphism of schemes is an h covering.

Local finite presentation is stable under base change, and the ph-covering condition is AlgebraicGeometry.isPHCovering_pullback, which is Stacks 0DBI part (3).

public theorem isHCovering_pullback {T T' : Scheme.{u}} {I : Type v} {X : I → Scheme.{u}}
    {f : ∀ i, X i ⟶ T} (hf : IsHCovering X f) (g : T' ⟶ T) :
    IsHCovering (fun i ↦ pullback (f i) g) (fun i ↦ pullback.snd (f i) g)

Tag 0ETZ, a definition

Tag 0ETZ in the Stacks Project.

AlgebraicGeometry.BigHSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/BigSite.lean, line 71.

Stacks 0ETZ. A big h site consists of an initial set of schemes and initial h coverings, a sufficiently large cutoff category containing them, and a bounded collection of h coverings satisfying the site axioms and representing every h covering.

public structure BigHSite

Tag 0EUY, a definition

Tag 0EUY in the Stacks Project.

AlgebraicGeometry.IsStandardHCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/StandardCoverings.lean, line 50. The attribute's comment: “part (1)”.

Stacks 0EUY, part (1). A family fᵢ : Xᵢ ⟶ T over an affine scheme T is a standard h covering when its index type is finite, every Xᵢ is affine, every fᵢ is of finite presentation, and some standard ph covering of T refines the family.

public noncomputable def IsStandardHCovering {T : Scheme.{u}} [IsAffine T] {I : Type v}
    {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ T) : Prop

Tag 0EU0, a lemma

Tag 0EU0 in the Stacks Project.

AlgebraicGeometry.BigHSite.exists_isCovering_tautologicallyEquivalent_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SiteCoveringRefinement.lean, line 92. The attribute's comment: “part (3)”.

Stacks 0EU0, part (3). A Zariski covering of an object of a big h site is tautologically equivalent to a covering belonging to that site.

public theorem BigHSite.exists_isCovering_tautologicallyEquivalent_openCover
    (B : BigHSite.{u}) (T : B.Schemes) (𝒰 : (B.inclusion.obj T).OpenCover.{v}) :
    ∃ 𝒱 : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, 𝒱⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent 𝒰.toPreZeroHypercover
          (𝒱.map B.inclusion)

AlgebraicGeometry.exists_isCovering_refinement_of_isHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SiteCoveringRefinement.lean, line 144. The attribute's comment: “part (1)”.

Stacks 0EU0, part (1). An arbitrary h covering of an object of a big h site is refined by one of the site's own covering families.

The affine opens of the target are a Zariski covering, hence by part (3) tautologically equivalent to a chosen family G. Each member of G is isomorphic over the target to an affine open, so the base change of the given family to it is an h covering of an affine scheme; Stacks 0ETU refines that base change by a standard h covering, which part (2) realizes inside the site. The site's composition axiom assembles the realized families into the required covering.

public theorem exists_isCovering_refinement_of_isHCovering
    (B : BigHSite.{u}) (T : B.Schemes) (𝒰 : PreZeroHypercover.{v} (B.inclusion.obj T))
    (h𝒰 : IsHCovering 𝒰.X 𝒰.f) :
    ∃ 𝒱 : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, 𝒱⟩ ∧ Nonempty ((𝒱.map B.inclusion).Hom 𝒰)

AlgebraicGeometry.exists_isCovering_tautologicallyEquivalent_standardHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SiteCoverings.lean, line 53. The attribute's comment: “part (2)”.

Stacks 0EU0, part (2). A standard h covering of an affine object of a big h site is tautologically equivalent to a covering belonging to that site.

Parts (1) and (3) are AlgebraicGeometry.exists_isCovering_refinement_of_isHCovering and AlgebraicGeometry.BigHSite.exists_isCovering_tautologicallyEquivalent_openCover.

public theorem exists_isCovering_tautologicallyEquivalent_standardHCovering
    (B : BigHSite.{u}) (T : B.Schemes) [IsAffine (B.inclusion.obj T)]
    (𝒰 : PreZeroHypercover.{v} (B.inclusion.obj T))
    (hstandard : IsStandardHCovering 𝒰.f) :
    ∃ 𝒱 : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, 𝒱⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent 𝒰 (𝒱.map B.inclusion)

Tag 0EU1, a definition

Tag 0EU1 in the Stacks Project.

AlgebraicGeometry.BigHOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/BigSite.lean, line 178. The attribute's comment: “part (1), category”.

Stacks 0EU1, part (1). The big h category of S is the slice of the chosen big h category over its object S.

public abbrev BigHOver

AlgebraicGeometry.BigHOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/BigSite.lean, line 193. The attribute's comment: “part (1), coverings”.

Stacks 0EU1, part (1). A family in the slice covers precisely when its underlying family covers in the chosen big h site.

public abbrev IsCovering (E : Covering (BigHOver B S hS)) : Prop

AlgebraicGeometry.BigAffineH, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/BigSite.lean, line 209. The attribute's comment: “part (2), category”.

Stacks 0EU1, part (2). The big affine h category is the full subcategory of affine objects in the big h category over S.

public abbrev BigAffineH

AlgebraicGeometry.BigAffineH.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/BigSite.lean, line 233. The attribute's comment: “part (2), coverings”.

Stacks 0EU1, part (2). An affine family covers exactly when it covers in the big h site over S and is a standard h covering.

public abbrev IsCovering (E : Covering (BigAffineH B S hS)) : Prop

Tag 0EU2, a lemma

Tag 0EU2 in the Stacks Project.

AlgebraicGeometry.BigAffineH.isSite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigAffineSite.lean, line 54.

Stacks 0EU2. The standard h covering families of the affine objects of the big h category over S satisfy the site axioms.

public lemma BigAffineH.isSite (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    IsSite (BigAffineH.IsCovering B S hS)

Tag 0EU3, a lemma

Tag 0EU3 in the Stacks Project.

AlgebraicGeometry.bigHSites_hasPullbacks_preservesPullbacks_final, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/H/Limits.lean, line 132.

Stacks 0EU3. Let B be a big h site containing the scheme S. The underlying categories of the big h site, of the big h site over S, and of the big affine h site over S have fibre products; in each case the canonical functor to the category of all schemes commutes with fibre products; and S / S is a final object of the big h site over S.

public theorem bigHSites_hasPullbacks_preservesPullbacks_final :
    (HasPullbacks B.Schemes ∧ HasPullbacks (BigHOver B S hS) ∧
        HasPullbacks (BigAffineH B S hS)) ∧
      (PreservesLimitsOfShape WalkingCospan B.inclusion ∧
        PreservesLimitsOfShape WalkingCospan (BigHOver.toScheme B S hS) ∧
        PreservesLimitsOfShape WalkingCospan (BigAffineH.toScheme B S hS)) ∧
      Nonempty (IsTerminal (Over.mk (𝟙 (B.obj S hS)) : BigHOver B S hS))

Tag 0EU4, a lemma

Tag 0EU4 in the Stacks Project.

AlgebraicGeometry.BigAffineH.isCocontinuous_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AffineSiteEquivalence.lean, line 175. The attribute's comment: “cocontinuity”.

Let B be a big h site containing a scheme S. The inclusion of the big affine h category over S into the big h category over S is cocontinuous for the two topologies of Stacks 0EU1.

public theorem isCocontinuous_inclusion :
    (inclusion B S hS).IsCocontinuous (topology B S hS) (BigHOver.topology B S hS)

AlgebraicGeometry.BigAffineH.isDenseSubsite_inclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AffineSiteEquivalence.lean, line 307. The attribute's comment: “equivalence of topoi”.

Let B be a big h site containing a scheme S. The inclusion of the big affine h category over S into the big h category over S exhibits the big affine h site as a dense subsite of the big h site over S, in the sense of CategoryTheory.Functor.IsDenseSubsite; consequently the two halves of the induced morphism of topoi are equivalences of categories and Sh((Aff/S)_h) ≃ Sh((Sch/S)_h).

public instance isDenseSubsite_inclusion :
    (inclusion B S hS).IsDenseSubsite (topology B S hS) (BigHOver.topology B S hS)

AlgebraicGeometry.BigAffineH.toposEquivInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AffineSiteEquivalence.lean, line 340. The attribute's comment: “equivalence of topoi”.

The topos of set-valued sheaves on the big affine h site over S is equivalent to the topos of set-valued sheaves on the big h site over S, the equivalence being restriction along the inclusion.

public noncomputable def toposEquivInclusion :
    Sheaf (topology B S hS) (Type (u + 1)) ≌
      Sheaf (BigHOver.topology B S hS) (Type (u + 1))

Tag 0EU5, a lemma

Tag 0EU5 in the Stacks Project.

AlgebraicGeometry.BigHOver.IsProperFinitePresentationSheaf.affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 246. The attribute's comment: “(2) implies (2′)”.

Stacks 0EU5, (2) implies (2′). Condition (2′) is the restriction of condition (2) to an affine target, so it is implied by it with no use of condition (1).

public theorem IsProperFinitePresentationSheaf.affine
    (hF : BigHOver.IsProperFinitePresentationSheaf B S hS F) :
    BigHOver.IsAffineProperFinitePresentationSheaf B S hS F

AlgebraicGeometry.BigHOver.isZariskiSheaf_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 301. The attribute's comment: “only if, condition (1)”.

Stacks 0EU5, a sheaf satisfies condition (1). A sheaf on the big h site over S satisfies the sheaf condition for Zariski coverings.

A jointly surjective family of open immersions is a Zariski covering, hence a ph covering by Stacks 0DBH; its members are locally of finite presentation, so the family is an h covering.

public theorem isZariskiSheaf_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsZariskiSheaf B S hS F

AlgebraicGeometry.BigHOver.isProperFinitePresentationSheaf_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 319. The attribute's comment: “only if, condition (2)”.

Stacks 0EU5, a sheaf satisfies condition (2). A sheaf on the big h site over S satisfies the sheaf condition for the one-element family attached to a morphism of the site which is proper, surjective and of finite presentation.

Such a morphism is an h covering all by itself, by Stacks 0ETW.

public theorem isProperFinitePresentationSheaf_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsProperFinitePresentationSheaf B S hS F

AlgebraicGeometry.BigHOver.bijective_mapToEqualizer_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 341. The attribute's comment: “only if, condition (2) in equalizer form”.

Stacks 0EU5, condition (2) for a sheaf, in equalizer form. Let f : V ⟶ U be a morphism of the big h category over S whose underlying morphism of schemes is proper, surjective and of finite presentation, and let p₁, p₂ : W ⟶ V complete f to a cartesian square, so that W = V ×_U V. Then a sheaf F on the big h site over S maps F(U) bijectively onto the equalizer of the two maps F(V) ⟶ F(W).

This is the form in which the source states condition (2). The case of an affine target U is condition (2′).

public theorem bijective_mapToEqualizer_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F)
    {V U W : BigHOver B S hS} (f : V ⟶ U) (p₁ p₂ : W ⟶ V)
    (hW : IsPullback p₁ p₂ f f)
    (hproper : IsProper ((BigHOver.toScheme B S hS).map f))
    (hsurj : Surjective ((BigHOver.toScheme B S hS).map f))
    (hfp : FinitePresentation ((BigHOver.toScheme B S hS).map f)) :
    Function.Bijective (regularTopology.mapToEqualizer F f p₁ p₂ hW.w)

AlgebraicGeometry.BigHOver.isProperFinitePresentationSheaf_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 587. The attribute's comment: “(1) and (2′) imply (2)”.

Stacks 0EU5, (1) and (2′) imply (2). Given the sheaf condition for Zariski coverings, the sheaf condition for a proper surjective morphism of finite presentation need only be checked when its target has affine underlying scheme.

The target X is covered by the affine opens of its underlying scheme, a Zariski covering of the site; the base change of f over each of them has affine target, so condition (2′) applies, and the base change over a fibre product of two of them is separated by properFP_pullback_isSeparated. The Zariski covering is strongly sheaf for F by condition (1), and CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_of_pullback assembles the local sheaf conditions into the sheaf condition for {f} itself.

public theorem isProperFinitePresentationSheaf_of_affine
    {F : (BigHOver B S hS)ᵒᵖ ⥤ Type v}
    (hZ : BigHOver.IsZariskiSheaf B S hS F)
    (hA : BigHOver.IsAffineProperFinitePresentationSheaf B S hS F) :
    BigHOver.IsProperFinitePresentationSheaf B S hS F

AlgebraicGeometry.BigHOver.isProperFinitePresentationSheaf_iff_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 627. The attribute's comment: “given (1), (2) is equivalent to (2′)”.

Stacks 0EU5, the final assertion. Given the sheaf condition for Zariski coverings, condition (2) of Stacks 0EU5 is equivalent to its restriction (2′) to morphisms whose target has affine underlying scheme.

public theorem isProperFinitePresentationSheaf_iff_affine
    {F : (BigHOver B S hS)ᵒᵖ ⥤ Type v}
    (hZ : BigHOver.IsZariskiSheaf B S hS F) :
    BigHOver.IsProperFinitePresentationSheaf B S hS F ↔
      BigHOver.IsAffineProperFinitePresentationSheaf B S hS F

AlgebraicGeometry.BigHOver.isSheaf_of_isZariskiSheaf_of_isProperFinitePresentationSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 1001. The attribute's comment: “if, (1) and (2) imply the sheaf condition”.

Stacks 0EU5, the sufficiency direction. Conditions (1) and (2) together force a presheaf of sets on the big h category over S to be a sheaf for the h topology.

public theorem isSheaf_of_isZariskiSheaf_of_isProperFinitePresentationSheaf
    {F : (BigHOver B S hS)ᵒᵖ ⥤ Type v}
    (hZ : BigHOver.IsZariskiSheaf B S hS F)
    (hP : BigHOver.IsProperFinitePresentationSheaf B S hS F) :
    Presieve.IsSheaf (BigHOver.topology B S hS) F

AlgebraicGeometry.BigHOver.isSheaf_iff_isZariskiSheaf_and_isProperFinitePresentationSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/SheafCriterion.lean, line 1032. The attribute's comment: “sheaf characterization”.

Stacks 0EU5, the characterization. A presheaf of sets on the big h category over S is a sheaf for the h topology if and only if it satisfies condition (1), the sheaf condition for Zariski coverings, and condition (2), the sheaf condition for every morphism of the site which is proper, surjective and of finite presentation.

By AlgebraicGeometry.isSheafFor_singleton_iff_bijective_mapToEqualizer condition (2) is the source's requirement that the sections over the target map bijectively onto the equalizer of the two maps to the sections over V ×_U V.

public theorem isSheaf_iff_isZariskiSheaf_and_isProperFinitePresentationSheaf
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigHOver B S hS)ᵒᵖ ⥤ Type v) :
    Presheaf.IsSheaf (BigHOver.topology B S hS) F ↔
      (BigHOver.IsZariskiSheaf B S hS F ∧
        BigHOver.IsProperFinitePresentationSheaf B S hS F)

Tag 0EU6, a lemma

Tag 0EU6 in the Stacks Project.

AlgebraicGeometry.isCocontinuous_bigHOverMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 76. The attribute's comment: “u : V/T ↦ V/S is cocontinuous”.

Stacks 0EU6. The functor u : (Sch/T)_h ⥤ (Sch/S)_h, V/T ↦ V/S, is cocontinuous.

public theorem isCocontinuous_bigHOverMap :
    (Over.map f).IsCocontinuous (B.topology.over T) (B.topology.over S)

AlgebraicGeometry.isContinuous_bigHOverMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 83. The attribute's comment: “u : V/T ↦ V/S is continuous”.

Stacks 0EU6, used in the proof. The functor u : (Sch/T)_h ⥤ (Sch/S)_h, V/T ↦ V/S, is continuous.

public theorem isContinuous_bigHOverMap :
    (Over.map f).IsContinuous (B.topology.over T) (B.topology.over S)

AlgebraicGeometry.bigHOverMapPullbackAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 90. The attribute's comment: “v : U/S ↦ U ×_S T/T is a right adjoint of u”.

Stacks 0EU6. The functor v : (Sch/S)_h ⥤ (Sch/T)_h given by base change along f is a right adjoint of u: for U/T and V/S one has Mor_S(u(U), V) = Mor_T(U, V ×_S T).

public noncomputable def bigHOverMapPullbackAdj : Over.map f ⊣ Over.pullback f

AlgebraicGeometry.isContinuous_bigHOverPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 102. The attribute's comment: “v : U/S ↦ U ×_S T/T is continuous”.

Stacks 0EU6. The functor v : (Sch/S)_h ⥤ (Sch/T)_h, U/S ↦ U ×_S T/T, is continuous.

public theorem isContinuous_bigHOverPullback :
    (Over.pullback f).IsContinuous (B.topology.over S) (B.topology.over T)

AlgebraicGeometry.bigHMorphismOfTopoi_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 110. The attribute's comment: “u and v induce the same morphism of topoi f_big, direct images”.

Stacks 0EU6. The functors u and v induce the same morphism of topoi: the direct image {}_s u attached to cocontinuity of u is the direct image v^s of AlgebraicGeometry.bigHMorphismOfTopoi.

public noncomputable def bigHMorphismOfTopoi_pushforwardIso :
    (Over.map f).sheafPushforwardCocontinuous (Type (u + 1))
        (B.topology.over T) (B.topology.over S) ≅
      (bigHMorphismOfTopoi B f).pushforward

AlgebraicGeometry.bigHMorphismOfTopoi_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 120. The attribute's comment: “u and v induce the same morphism of topoi f_big, inverse images”.

Stacks 0EU6. The inverse image (u^p -)^# attached to cocontinuity of u is the inverse image of AlgebraicGeometry.bigHMorphismOfTopoi, namely plain restriction along u: the sheafification is unnecessary.

public noncomputable def bigHMorphismOfTopoi_inverseImageIso :
    (Over.map f).sheafPullbackCocontinuous (Type (u + 1))
        (B.topology.over T) (B.topology.over S) ≅
      (bigHMorphismOfTopoi B f).inverseImage

AlgebraicGeometry.bigHMorphismOfTopoi_inverseImage_obj_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 129. The attribute's comment: “f_big⁻¹(G)(U/T) = G(U/S)”.

Stacks 0EU6, the formula f_big^{-1}(G)(U/T) = G(U/S).

public theorem bigHMorphismOfTopoi_inverseImage_obj_obj_obj
    (G : Sheaf (BigHOver.topology B S.obj S.property) (Type (u + 1))) (U : Over T) :
    ((bigHMorphismOfTopoi B f).inverseImage.obj G).obj.obj (op U) =
      G.obj.obj (op ((Over.map f).obj U))

AlgebraicGeometry.bigHMorphismOfTopoi_pushforward_obj_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 137. The attribute's comment: “f_big,*(F)(U/S) = F(U ×_S T/T)”.

Stacks 0EU6, the formula f_{big,*}(F)(U/S) = F(U ×_S T/T).

public theorem bigHMorphismOfTopoi_pushforward_obj_obj_obj
    (F : Sheaf (BigHOver.topology B T.obj T.property) (Type (u + 1))) (U : Over S) :
    ((bigHMorphismOfTopoi B f).pushforward.obj F).obj.obj (op U) =
      F.obj.obj (op ((Over.pullback f).obj U))

AlgebraicGeometry.bigHSheafPushforwardCocontinuousObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 146. The attribute's comment: “f_big,*(F)(U/S) = F(U ×_S T/T)”.

Stacks 0EU6, the formula f_{big,*}(F)(U/S) = F(U ×_S T/T) for the direct image {}_s u attached to cocontinuity of u.

public noncomputable def bigHSheafPushforwardCocontinuousObjIso
    (F : Sheaf (BigHOver.topology B T.obj T.property) (Type (u + 1))) (U : Over S) :
    (((Over.map f).sheafPushforwardCocontinuous (Type (u + 1))
        (B.topology.over T) (B.topology.over S)).obj F).obj.obj (op U) ≅
      F.obj.obj (op ((Over.pullback f).obj U))

AlgebraicGeometry.bigHLowerShriekAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 157. The attribute's comment: “f_big⁻¹ has a left adjoint f_big!”.

Stacks 0EU6. The inverse image f_big^{-1} has a left adjoint f_{big!}, namely the sheaf pullback along the continuous functor u.

public noncomputable def bigHLowerShriekAdj :
    (Over.map f).sheafPullback (Type (u + 1)) (B.topology.over T) (B.topology.over S) ⊣
      (bigHMorphismOfTopoi B f).inverseImage

AlgebraicGeometry.preservesLimitsOfShape_bigHLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 166. The attribute's comment: “f_big! commutes with fibre products and equalizers”.

Stacks 0EU6. The left adjoint f_{big!} of f_big^{-1} commutes with fibre products and equalizers, and more generally with every finite connected limit.

public theorem preservesLimitsOfShape_bigHLowerShriek
    (I : Type t) [SmallCategory I] [FinCategory I] [IsConnected I] :
    PreservesLimitsOfShape I
      ((Over.map f).sheafPullback (Type (u + 1))
        (B.topology.over T) (B.topology.over S))

AlgebraicGeometry.preservesLimitsOfShape_walkingCospan_bigHLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 183. The attribute's comment: “f_big! commutes with fibre products and equalizers”.

Stacks 0EU6. f_{big!} commutes with fibre products.

public theorem preservesLimitsOfShape_walkingCospan_bigHLowerShriek :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (B.topology.over T) (B.topology.over S))

AlgebraicGeometry.preservesLimitsOfShape_walkingParallelPair_bigHLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/BigTopoiFormulas.lean, line 191. The attribute's comment: “f_big! commutes with fibre products and equalizers”.

Stacks 0EU6. f_{big!} commutes with equalizers.

public theorem preservesLimitsOfShape_walkingParallelPair_bigHLowerShriek :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (B.topology.over T) (B.topology.over S))

Declarations registered for the tag:

StacksRelocalization.sheafPushforwardOverMapIso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/BigHTopos.lean, line 34 (StacksFrontier): “same_topos”.

Tag 0EU7, a lemma

Tag 0EU7 in the Stacks Project.

AlgebraicGeometry.bigHMorphismOfTopoi_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Composition.lean, line 53. The attribute's comment: “direct image”.

Stacks 0EU7. The direct image of the morphism of big h topoi attached to a composite is canonically isomorphic to the composite of the direct images.

public noncomputable def bigHMorphismOfTopoi_comp_pushforwardIso (B : BigHSite.{u})
    {X Y Z : B.Schemes} (f : X ⟶ Y) (g : Y ⟶ Z) :
    ((bigHMorphismOfTopoi B g).comp (bigHMorphismOfTopoi B f)).pushforward ≅
      (bigHMorphismOfTopoi B (f ≫ g)).pushforward

AlgebraicGeometry.bigHMorphismOfTopoi_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Composition.lean, line 67. The attribute's comment: “inverse image”.

Stacks 0EU7. The inverse image of the morphism of big h topoi attached to a composite is canonically isomorphic to the composite of the inverse images; the isomorphism is the adjunction mate of the comparison of direct images.

public noncomputable def bigHMorphismOfTopoi_comp_inverseImageIso (B : BigHSite.{u})
    {X Y Z : B.Schemes} (f : X ⟶ Y) (g : Y ⟶ Z) :
    ((bigHMorphismOfTopoi B g).comp (bigHMorphismOfTopoi B f)).inverseImage ≅
      (bigHMorphismOfTopoi B (f ≫ g)).inverseImage

AlgebraicGeometry.bigHMorphismOfTopoi_comp_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/Composition.lean, line 79. The attribute's comment: “compatibility with the adjunction”.

Stacks 0EU7. The comparisons of direct and inverse images for a composite respect the units of the geometric adjunctions, so together they form an isomorphism of morphisms of topoi.

public theorem bigHMorphismOfTopoi_comp_unit (B : BigHSite.{u}) {X Y Z : B.Schemes}
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (V : Sheaf (BigHOver.topology B Z.obj Z.property) (Type (u + 1))) :
    (bigHMorphismOfTopoi B (f ≫ g)).adj.unit.app V ≫
        (bigHMorphismOfTopoi B (f ≫ g)).pushforward.map
          ((bigHMorphismOfTopoi_comp_inverseImageIso B f g).inv.app V) ≫
        (bigHMorphismOfTopoi_comp_pushforwardIso B f g).inv.app
          (((bigHMorphismOfTopoi B g).comp (bigHMorphismOfTopoi B f)).inverseImage.obj V) =
      ((bigHMorphismOfTopoi B g).comp (bigHMorphismOfTopoi B f)).adj.unit.app V

Sources

LeanAlgebraicGeometry.isPHCovering_iff_isVCovering · AlgebraicGeometry.IsHCovering · AlgebraicGeometry.isHCovering_of_universallySubmersive_of_isNoetherian · AlgebraicGeometry.universallySubmersive_sigmaDesc_iff_isHCovering_of_isNoetherian · AlgebraicGeometry.universallySubmersive_sigmaDesc_of_isHCovering · AlgebraicGeometry.isHCovering_of_universallySubmersive · AlgebraicGeometry.universallySubmersive_sigmaDesc_iff_isHCovering · AlgebraicGeometry.isHCovering_iff_isPHCovering

Section38.35 More on the h topology #

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

Tag 0EV0, an example

Tag 0EV0 in the Stacks Project.

AlgebraicGeometry.not_isSheafFor_isHCovering_gamma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/StructureSheafFailure.lean, line 252.

The structure sheaf is not a sheaf for the h topology: the presheaf of global sections on schemes fails the sheaf condition for some h covering family.

public theorem not_isSheafFor_isHCovering_gamma :
    ¬ ∀ (T : Scheme.{u}) (I : Type t) (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T),
        IsHCovering X f →
          (Presieve.ofArrows X f).IsSheafFor (Scheme.Γ.{u} ⋙ forget CommRingCat.{u})

Tag 0EV1, an example

Tag 0EV1 in the Stacks Project.

AlgebraicGeometry.BigHOver.not_subcanonical_topology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/StructureSheafFailure.lean, line 529.

On a big h site over a nonempty base scheme S the h topology is not subcanonical: not every representable presheaf on (Sch/S)_h is a sheaf.

public theorem not_subcanonical_topology [Nonempty S] :
    ¬ (topology B S hS).Subcanonical

Tag 0EV2, a lemma

Tag 0EV2 in the Stacks Project.

AlgebraicGeometry.exists_isStandardHCovering_model_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/StandardCoveringsLimit.lean, line 720. The attribute's comment: “part (1)”.

Stacks 0EV2, part (1). Let an affine scheme be written as the limit of a cofiltered inverse system of affine schemes. Then every standard h covering of the limit is isomorphic to the base change of a standard h covering of one of the stages, with the same index type.

public theorem exists_isStandardHCovering_model_of_isLimit {I : Type v} [Category.{w} I]
    [IsCofiltered I] [EssentiallySmall.{u} I] (D : I ⥤ Scheme.{u}) [∀ i, IsAffine (D.obj i)]
    (c : Cone D) (hc : IsLimit c) (E : PreZeroHypercover.{v} c.pt)
    (hE : letI : IsAffine c.pt := Scheme.isAffine_of_isLimit c hc
      IsStandardHCovering E.f) :
    ∃ (i : I) (F : PreZeroHypercover.{v} (D.obj i)), IsStandardHCovering F.f ∧
      Nonempty (F.pullback₂ (c.π.app i) ≅ E)

AlgebraicGeometry.exists_hom_isStandardHCovering_model_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/StandardCoveringsLimit.lean, line 742. The attribute's comment: “part (2)”.

Stacks 0EV2, part (2). Let an affine scheme be written as the limit of a cofiltered inverse system of affine schemes, and let two standard h coverings of a stage be given. Every morphism between their base changes to the limit is the base change of a morphism between their base changes to some later stage, compared through the canonical identifications AlgebraicGeometry.pullback₂CompIso of the iterated base changes with the direct ones.

public theorem exists_hom_isStandardHCovering_model_of_isLimit {I : Type v} [Category.{w} I]
    [IsCofiltered I] [EssentiallySmall.{u} I] (D : I ⥤ Scheme.{u}) [∀ i, IsAffine (D.obj i)]
    (c : Cone D) (hc : IsLimit c) (i : I) (E F : PreZeroHypercover.{v} (D.obj i))
    (hE : IsStandardHCovering E.f) (hF : IsStandardHCovering F.f)
    (f : (E.pullback₂ (c.π.app i)).Hom (F.pullback₂ (c.π.app i))) :
    ∃ (j : I) (e : j ⟶ i) (g : (E.pullback₂ (D.map e)).Hom (F.pullback₂ (D.map e))),
      (pullback₂CompIso (D.map e) (c.π.app j) (c.π.app i) (c.w e) E).hom ≫ f =
        g.pullback₂ (c.π.app j) ≫
          (pullback₂CompIso (D.map e) (c.π.app j) (c.π.app i) (c.w e) F).hom

AlgebraicGeometry.eventually_eq_hom_isStandardHCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/StandardCoveringsLimit.lean, line 798. The attribute's comment: “part (3)”.

Stacks 0EV2, part (3). Let an affine scheme be written as the limit of a cofiltered inverse system of affine schemes. Two morphisms of standard h coverings of a stage whose base changes to the limit are equal are already equal after base change to some later stage.

public theorem eventually_eq_hom_isStandardHCovering_of_isLimit {I : Type v} [Category.{w} I]
    [IsCofiltered I] [EssentiallySmall.{u} I] (D : I ⥤ Scheme.{u}) [∀ i, IsAffine (D.obj i)]
    (c : Cone D) (hc : IsLimit c) (i : I) (E F : PreZeroHypercover.{v} (D.obj i))
    (hE : IsStandardHCovering E.f) (hF : IsStandardHCovering F.f) (f g : E.Hom F)
    (hfg : f.pullback₂ (c.π.app i) = g.pullback₂ (c.π.app i)) :
    ∃ (j : I) (e : j ⟶ i), f.pullback₂ (D.map e) = g.pullback₂ (D.map e)

Tag 0EV3, a lemma

Tag 0EV3 in the Stacks Project.

AlgebraicGeometry.ExtendingFunctors.isHSheaf_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/ExtendingFunctors.lean, line 595. The attribute's comment: “the sheaf condition for all h coverings”.

Stacks 0EV3, the sheaf condition for all h coverings. Let S be a scheme contained in a big h site, let 𝒞 = (Sch/S)_h be a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW and let F : 𝒞ᵒᵖ ⥤ Set be an h sheaf satisfying condition (b) of Stacks 0EUW. Then the extension F' = AlgebraicGeometry.ExtendingFunctors.extension of F to all schemes over S satisfies the sheaf condition for every h covering of every scheme over S.

The reduction to the standard h coverings of the affine objects lying over an affine open of S is AlgebraicGeometry.ExtendingFunctors.isHSheaf_of_isStandardAffineHSheaf, and the restricted sheaf condition is deduced from the h sheaf property of F by AlgebraicGeometry.ExtendingFunctors.isStandardAffineHSheaf_extension, through the descent of a standard h covering along a directed limit of affines, Stacks 0EV2.

theorem isHSheaf_extension (P : ObjectProperty (Over S))
    (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1))) (hP1 : HasAffineOpens P)
    (hP2 : HasFinitePresentationAffines P)
    (hF : IsHCoveringSheafOnSubcategory.{max w (u + 1), u, u} P F)
    (hbF : PreservesAffineLimitsOnSubcategory P F) :
    IsHSheaf.{max w (u + 1), u, v} (extension P F)

AlgebraicGeometry.ExtendingFunctors.isLimitPreserving_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/ExtendingFunctors.lean, line 613. The attribute's comment: “limit preserving: the extension carries a directed inverse limit of affine schemes over the base to a filtered colimit”.

Stacks 0EV3, limit preserving. For S a scheme contained in a big h site, 𝒞 = (Sch/S)_h a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW and F : 𝒞ᵒᵖ ⥤ Set an h sheaf, the extension F' = AlgebraicGeometry.ExtendingFunctors.extension of F to all schemes over S is limit preserving in the sense of Limits, Remark 05LX: it carries a directed inverse limit of affine schemes over S to a filtered colimit.

theorem isLimitPreserving_extension (P : ObjectProperty (Over S))
    (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1))) (hP1 : HasAffineOpens P)
    (hP2 : HasFinitePresentationAffines P)
    (hF : IsHCoveringSheafOnSubcategory.{max w (u + 1), u, u} P F) :
    PreservesAffineLimits (extension P F)

Sources

LeanAlgebraicGeometry.not_isSheafFor_isHCovering_gamma · AlgebraicGeometry.BigHOver.not_subcanonical_topology · AlgebraicGeometry.exists_isStandardHCovering_model_of_isLimit · AlgebraicGeometry.exists_hom_isStandardHCovering_model_of_isLimit · AlgebraicGeometry.eventually_eq_hom_isStandardHCovering_of_isLimit · AlgebraicGeometry.ExtendingFunctors.isHSheaf_extension · AlgebraicGeometry.ExtendingFunctors.isLimitPreserving_extension

Section38.36 Blow up squares and the ph topology #

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

Tag 0EV5, an equation

Tag 0EV5 in the Stacks Project.

AlgebraicGeometry.BlowUpSquare, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/Basic.lean, line 66.

The data fixed by a blowup square: a closed centre of finite presentation in its base scheme. The other corners and all the arrows are canonically determined.

public structure BlowUpSquare

AlgebraicGeometry.BlowUpSquare.isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/Basic.lean, line 124. The attribute's comment: “the blow up square”. References: SGA 6 0 (6.Lemma3), “partial”; SGA 6 VII (3.7), “more general”.

Stacks Project, Tag 0EV5. The blowup square
E ⟶ X'
↓    ↓ b
Z ⟶ X
commutes and is cartesian: the exceptional divisor E is the inverse image b⁻¹(Z) of the centre, hence the fibre product of the blowup morphism b and the inclusion of the centre. Commutativity alone is AlgebraicGeometry.BlowUpSquare.isPullback.w.

public theorem isPullback :
    IsPullback s.exceptionalInclusion s.exceptionalProjection s.blowUpMorphism
      s.centerInclusion

Declarations registered for the tag:

Scheme.IdealSheafData.comapIso registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/Basic.lean, line 61 (StacksFrontier): “cartesian square”.

Tag 0EW1, a lemma

Tag 0EW1 in the Stacks Project.

AlgebraicGeometry.BigPHOver.isPullback_map_of_blowUpSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowUpSquare/PhSheaf.lean, line 498.

Stacks Project, Tag 0EW1. Let F be a sheaf of sets on a big ph site over S. For every blow up square in that site — a closed centre Z ⊆ X of finite presentation, the blowup b : X' ⟶ X of X in Z, and the exceptional divisor E = b⁻¹(Z) — the square of restriction maps F(X) → F(Z) → F(E) and F(X) → F(X') → F(E) is cartesian in the category of sets.

public theorem isPullback_map_of_blowUpSquare
    (B : BigPHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigPHOver B S hS)ᵒᵖ ⥤ Type v)
    (hF : Presheaf.IsSheaf (BigPHOver.topology B S hS) F)
    {X X' Z E : BigPHOver B S hS}
    (b : X' ⟶ X) (z : Z ⟶ X) (p : E ⟶ X') (e : E ⟶ Z)
    (I : ((BigPHOver.toScheme B S hS).obj X).IdealSheafData)
    (hI : FinitePresentation I.subschemeι)
    (hb : Nonempty (Over.mk ((BigPHOver.toScheme B S hS).map b) ≅ Over.mk (blowUpToBase I)))
    (hZ : Nonempty (Over.mk ((BigPHOver.toScheme B S hS).map z) ≅ Over.mk I.subschemeι))
    (hSquare : IsPullback
      ((BigPHOver.toScheme B S hS).map e) ((BigPHOver.toScheme B S hS).map p)
      ((BigPHOver.toScheme B S hS).map z) ((BigPHOver.toScheme B S hS).map b)) :
    IsPullback (F.map z.op) (F.map b.op) (F.map e.op) (F.map p.op)

Tag 0EW2, a lemma

Tag 0EW2 in the Stacks Project.

AlgebraicGeometry.BigPHOver.bijective_map_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowUpSquare/PhThickening.lean, line 52.

Stacks Project, Tag 0EW2. Restriction of a ph sheaf along a thickening is a bijection of sections.

theorem BigPHOver.bijective_map_of_isThickening
    (B : BigPHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : Sheaf (BigPHOver.topology B S hS) (Type v))
    {X X' : BigPHOver B S hS} (i : X ⟶ X')
    (hi : Stacks.Thickenings.IsThickening ((BigPHOver.toScheme B S hS).map i)) :
    Function.Bijective (F.obj.map i.op)

Sources

LeanAlgebraicGeometry.BlowUpSquare · AlgebraicGeometry.BlowUpSquare.isPullback · Scheme.IdealSheafData.comapIso · AlgebraicGeometry.BigPHOver.isPullback_map_of_blowUpSquare · AlgebraicGeometry.BigPHOver.bijective_map_of_isThickening

Section38.37 Almost blow up squares and the h topology #

Section 38.37 of the Stacks Project, Tag 0EV4. 14 tags here are carried by 33 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EV6, an equation

Tag 0EV6 in the Stacks Project.

AlgebraicGeometry.isIso_restrict_compl_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AlmostBlowUp/IsomorphismAwayFromCenter.lean, line 117. The attribute's comment: “isomorphism_away_from_center”.

Stacks Project, Tag 0EV6. The modification of an almost blowup square is an isomorphism over the complement of the centre of the square.

public theorem isIso_restrict_compl_support {X X' : Scheme.{u}}
    (I : X.IdealSheafData) (b : X' ⟶ X) (hb : IsAlmostBlowUpSquare I b) :
    IsIso (b ∣_ (⟨I.supportᶜ, I.support.isClosed.isOpen_compl⟩ : X.Opens))

Declarations registered for the tag:

AlgebraicGeometry.IsAlmostBlowUpSquare, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/Basic.lean, line 60 (StacksFrontier): “almost_blow_up_square”.
AlgebraicGeometry.supportedSectionsIdeal_ideal, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AlmostBlowUp/SupportedSections.lean, line 120 (StacksFrontier): “almost_blow_up_square”.

Tag 0EV7, a lemma

Tag 0EV7 in the Stacks Project.

AlgebraicGeometry.isAlmostBlowUpSquare_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/BaseChange.lean, line 89.

An almost blowup square stays an almost blowup square after an arbitrary base change: the new centre is the inverse image of the old one and the new modification is the base change of the old one.

public theorem isAlmostBlowUpSquare_baseChange {X X' Y : Scheme.{u}} (I : X.IdealSheafData)
    (b : X' ⟶ X) (f : Y ⟶ X) (h : IsAlmostBlowUpSquare I b) :
    IsAlmostBlowUpSquare (I.comap f) (pullback.fst f b)

Tag 0EV8, a lemma

Tag 0EV8 in the Stacks Project.

AlgebraicGeometry.isIso_restrict_iff_le_supportedSectionsIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AlmostBlowUp/IsomorphismAwayFromCenter.lean, line 106. The attribute's comment: “(1) iff (2)”.

Stacks Project, Tag 0EV8. The closed subscheme cut out by an ideal sheaf is an isomorphism over the complement of a closed set exactly when the ideal sheaf is contained in the ideal of sections supported on that set.

public theorem isIso_restrict_iff_le_supportedSectionsIdeal {X : Scheme.{u}} (Z : Set X)
    (hZ : IsClosed Z) (J : X.IdealSheafData) :
    IsIso (J.subschemeι ∣_ (⟨Zᶜ, hZ.isOpen_compl⟩ : X.Opens)) ↔
      J ≤ supportedSectionsIdeal Z

AlgebraicGeometry.le_supportedSectionsIdeal_iff_isAlmostBlowUpSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/Shrinking.lean, line 117. The attribute's comment: “(2) iff (3)”.

Stacks Project, Tag 0EV8. For a finitely presented closed subscheme of the modification of an almost blowup square, containing the blowup of the centre is equivalent to the induced square, with the scheme-theoretic inverse image of the centre, being again an almost blowup square.

public theorem le_supportedSectionsIdeal_iff_isAlmostBlowUpSquare {X X' : Scheme.{u}}
    (I : X.IdealSheafData) (b : X' ⟶ X) (h : IsAlmostBlowUpSquare I b)
    (J : X'.IdealSheafData) (hJ : FinitePresentation J.subschemeι) :
    J ≤ supportedSectionsIdeal (I.comap b).support ↔
      IsAlmostBlowUpSquare I (J.subschemeι ≫ b)

Tag 0EV9, a lemma

Tag 0EV9 in the Stacks Project.

AlgebraicGeometry.isFiltered_and_exists_isLimit_blowUpCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AlmostBlowUp/BlowUpAsLimit.lean, line 138.

Consider an almost blowup square with centre I.subscheme and modification b : X' ⟶ X, with X quasi-compact and quasi-separated. The closed subschemes X'ᵢ ⊆ X' of finite presentation satisfying the equivalent conditions of Tag 0EV8 — their ideal sheaves J are finitely presented with J ≤ almostBlowUpIdeal I b, that is, the blowup X'' is scheme theoretically contained in X'ᵢ (condition (2)), equivalently X'ᵢ contains X' ∖ E scheme theoretically (condition (1), AlgebraicGeometry.le_almostBlowUpIdeal_iff) — form a directed system, and the blowup X'' of X in the centre, identified by i over X with the closed subscheme of X' cut out by almostBlowUpIdeal I b, is its limit X'' = lim X'ᵢ, both as schemes over X' and as schemes.

public theorem isFiltered_and_exists_isLimit_blowUpCone [CompactSpace X] [QuasiSeparatedSpace X]
    (h : IsAlmostBlowUpSquare I b) :
    IsFiltered (FinitePresentationSubscheme (almostBlowUpIdeal I b)) ∧
      ∃ i : blowUp I ⟶ (almostBlowUpIdeal I b).subscheme, IsIso i ∧
        i ≫ (almostBlowUpIdeal I b).subschemeι ≫ b = blowUpToBase I ∧
        Nonempty (IsLimit (blowUpCone I b i)) ∧
        Nonempty (IsLimit ((Over.forget X').mapCone (blowUpCone I b i)))

Tag 0EVA, a lemma

Tag 0EVA in the Stacks Project.

AlgebraicGeometry.exists_isAlmostBlowUpSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/Existence.lean, line 66.

Stacks Project, Tag 0EVA. Let X be a quasi-compact and quasi-separated scheme and let I be a quasi-coherent ideal sheaf of finite type on X, cutting out a closed subscheme Z. Then there is an almost blowup square with centre Z, that is, a modification b : X' ⟶ X making (I.comap b, X', Z, X) an almost blowup square.

public theorem exists_isAlmostBlowUpSquare (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] (I : X.IdealSheafData)
    (hI : Scheme.IdealSheafData.IsFiniteType I) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X), IsAlmostBlowUpSquare I b

Tag 0EVB, a lemma

Tag 0EVB in the Stacks Project.

AlgebraicGeometry.exists_isAlmostBlowUpSquare_closedImmersion_to_both, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/CommonRefinement.lean, line 46.

Let X be a quasi-compact and quasi-separated scheme, let I be a quasi-coherent ideal sheaf of finite type on X, and let b₁ : X₁ ⟶ X and b₂ : X₂ ⟶ X be the modifications of two almost blowup squares with centre I. Then there is an almost blowup square with centre I and modification b : X' ⟶ X together with closed immersions i₁ : X' ⟶ X₁ and i₂ : X' ⟶ X₂ over X for which the exceptional subscheme of b is the inverse image of the exceptional subscheme of b₁ and of b₂.

public theorem exists_isAlmostBlowUpSquare_closedImmersion_to_both
    {X X₁ X₂ : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (I : X.IdealSheafData) (hI : Scheme.IdealSheafData.IsFiniteType I)
    (b₁ : X₁ ⟶ X) (b₂ : X₂ ⟶ X)
    (h₁ : IsAlmostBlowUpSquare I b₁) (h₂ : IsAlmostBlowUpSquare I b₂) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X) (i₁ : X' ⟶ X₁) (i₂ : X' ⟶ X₂),
      IsAlmostBlowUpSquare I b ∧
        IsClosedImmersion i₁ ∧ IsClosedImmersion i₂ ∧
        i₁ ≫ b₁ = b ∧ i₂ ≫ b₂ = b ∧
        I.comap b = (I.comap b₁).comap i₁ ∧
        I.comap b = (I.comap b₂).comap i₂

Tag 0EVC, a lemma

Tag 0EVC in the Stacks Project.

AlgebraicGeometry.hasFlatAlmostBlowUpSquarePair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/Flattening.lean, line 203. The attribute's comment: “locally Noetherian base; the affine case of the flatness half of [Stacks, Tag 0815] carried as the hypothesis AlgebraicGeometry.AffineChartFlatteningCentre, inherited from the library's form of [Stacks, Tag 081R]”.

Stacks Project, Tag 0EVC. Let Y be a quasi-compact and quasi-separated scheme, let X be a scheme of finite presentation over Y, and let V ⊆ Y be a quasi-compact open. Then there is a diagram as in the tag: two almost blowup squares, over Y with a centre disjoint from V and over X with the inverse-image centre, whose lower and top squares are cartesian (AlgebraicGeometry.lowerSquareIso, AlgebraicGeometry.topSquareIso) and whose relative morphism X' ⟶ Y' is flat and of finite presentation.

The flattening centre comes from AlgebraicGeometry.exists_isAdmissibleBlowup_flat_strictTransform, the library's form of Stacks tag 081R, and two things are carried beyond the tag's own hypotheses. The base is assumed locally Noetherian: this is the case the Stacks proof calls immediate, the general case being reduced to it by absolute Noetherian approximation, which is not done here. And the affine case of the flatness half of Stacks tag 0815 is carried as AlgebraicGeometry.AffineChartFlatteningCentre f X.unitModule V, exactly as that form of tag 081R carries it. The tag's remaining hypothesis that X_V ⟶ V be flat is not assumed separately, because in the source it enters only through that affine case; so the statement below is a generalization in that respect.

public theorem hasFlatAlmostBlowUpSquarePair [IsLocallyNoetherian Y] [CompactSpace Y]
    [QuasiSeparatedSpace Y] (f : X ⟶ Y) (hf : FinitePresentation f) (V : Y.Opens)
    (hV : IsCompact (V : Set Y)) (H : AffineChartFlatteningCentre f X.unitModule V) :
    HasFlatAlmostBlowUpSquarePair f V

AlgebraicGeometry.hasFlatAlmostBlowUpSquarePair_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/FlatteningApproximation.lean, line 288.

[Stacks, Tag 0EVC]. Let Y be a quasi-compact and quasi-separated scheme, let X be a scheme of finite presentation over Y, and let V ⊆ Y be a quasi-compact open such that X_V ⟶ V is flat. Then there is a diagram as in the tag: two almost blowup squares, over Y with a centre disjoint from V and over X with the inverse-image centre, whose lower and top squares are cartesian (AlgebraicGeometry.lowerSquareIso, AlgebraicGeometry.topSquareIso) and whose relative morphism X' ⟶ Y' is flat and of finite presentation.

The general case is reduced to the locally Noetherian case AlgebraicGeometry.hasFlatAlmostBlowUpSquarePair by absolute Noetherian approximation; see the module docstring.

public theorem hasFlatAlmostBlowUpSquarePair_of_flat {X Y : Scheme.{u}}
    [CompactSpace Y] [QuasiSeparatedSpace Y] (f : X ⟶ Y) (hf : FinitePresentation f)
    (V : Y.Opens) (hV : IsCompact (V : Set Y)) (hflat : Flat (pullback.snd f V.ι)) :
    HasFlatAlmostBlowUpSquarePair f V

AlgebraicGeometry.hasFlatAlmostBlowUpSquarePair_of_affineCase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/FlatteningFlatModel.lean, line 289. The attribute's comment: “the conclusion in full, under exactly the source's hypotheses and with no Noetherian hypothesis on the base: 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 0EVC. Let Y be a quasi-compact and quasi-separated scheme, let f : X ⟶ Y be of finite presentation and let V ⊆ Y be a quasi-compact open such that X_V ⟶ V is flat. Then there is a diagram as in the tag: two almost blowup squares, over Y with a centre disjoint from V and over X with the inverse-image centre, whose lower and top squares are cartesian (AlgebraicGeometry.lowerSquareIso, AlgebraicGeometry.topSquareIso) and whose relative morphism X' ⟶ Y' is flat and of finite presentation.

Every hypothesis of the source is present, with no Noetherian hypothesis on Y: the Noetherian case is AlgebraicGeometry.hasFlatAlmostBlowUpSquarePair_of_flat, run at the Noetherian model supplied by AlgebraicGeometry.exists_isNoetherian_model_of_finitePresentation_of_flat and pulled back along Y ⟶ Y₀. The affine case of the flatness assertion of [Stacks, Tag 0815] it consumes is AlgebraicGeometry.AffineChartFlatteningCentreUnderSourceHypotheses.of_compactSpace, itself proved from [Stacks, Tag 0811], which AlgebraicGeometry.NoetherianAffineChartFlatteningCentre.of_affineCase turns into the form the Noetherian case consumes.

The tag's hypothesis that X_V ⟶ V be flat is essential and is present here, where AlgebraicGeometry.hasFlatAlmostBlowUpSquarePair omits it: without it the affine case cannot be applied at the model at all, its own hypothesis (5) being exactly that flatness.

theorem hasFlatAlmostBlowUpSquarePair_of_affineCase {X Y : Scheme.{u}} [CompactSpace Y]
    [QuasiSeparatedSpace Y] (f : X ⟶ Y) (hf : FinitePresentation f) (V : Y.Opens)
    (hV : IsCompact (V : Set Y)) (hflat : Flat (f ∣_ V)) :
    HasFlatAlmostBlowUpSquarePair f V

Tag 0EVD, a lemma

Tag 0EVD in the Stacks Project.

AlgebraicGeometry.isPullback_of_almostBlowUpSquare_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpDescent.lean, line 905. The attribute's comment: “big h site”.

Stacks 0EVD. A sheaf on the big h site over a scheme sends an almost blowup square to a cartesian square of sets.

public theorem isPullback_of_almostBlowUpSquare_bigH
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigHOver B S hS)ᵒᵖ ⥤ Type v)
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F)
    {X X' Z E : BigHOver B S hS}
    (b : X' ⟶ X) (z : Z ⟶ X) (p : E ⟶ X') (e : E ⟶ Z)
    (I : ((BigHOver.toScheme B S hS).obj X).IdealSheafData)
    (hb : IsAlmostBlowUpSquare I ((BigHOver.toScheme B S hS).map b))
    (hZ : Nonempty
      (Over.mk ((BigHOver.toScheme B S hS).map z) ≅
        Over.mk I.subschemeι))
    (hSquare : IsPullback
      ((BigHOver.toScheme B S hS).map e)
      ((BigHOver.toScheme B S hS).map p)
      ((BigHOver.toScheme B S hS).map z)
      ((BigHOver.toScheme B S hS).map b)) :
    IsPullback (F.map z.op) (F.map b.op) (F.map e.op) (F.map p.op)

AlgebraicGeometry.isPullback_of_almostBlowUpSquare_bigAffineH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpDescent.lean, line 950. The attribute's comment: “big affine h site”.

Stacks 0EVD. A sheaf on the big affine h site over a scheme sends an almost blowup square to a cartesian square of sets.

public theorem isPullback_of_almostBlowUpSquare_bigAffineH
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigAffineH B S hS)ᵒᵖ ⥤ Type v)
    (hF : Presheaf.IsSheaf (BigAffineH.topology B S hS) F)
    {X X' Z E : BigAffineH B S hS}
    (b : X' ⟶ X) (z : Z ⟶ X) (p : E ⟶ X') (e : E ⟶ Z)
    (I : ((BigAffineH.toScheme B S hS).obj X).IdealSheafData)
    (hb : IsAlmostBlowUpSquare I ((BigAffineH.toScheme B S hS).map b))
    (hZ : Nonempty
      (Over.mk ((BigAffineH.toScheme B S hS).map z) ≅
        Over.mk I.subschemeι))
    (hSquare : IsPullback
      ((BigAffineH.toScheme B S hS).map e)
      ((BigAffineH.toScheme B S hS).map p)
      ((BigAffineH.toScheme B S hS).map z)
      ((BigAffineH.toScheme B S hS).map b)) :
    IsPullback (F.map z.op) (F.map b.op) (F.map e.op) (F.map p.op)

Tag 0EVE, a lemma

Tag 0EVE in the Stacks Project.

AlgebraicGeometry.bijective_map_of_isThickening_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpDescent.lean, line 1016. The attribute's comment: “big h site”.

Stacks 0EVE. A sheaf on the big h site over a scheme restricts bijectively along a morphism of the site which is a thickening and of finite presentation.

public theorem bijective_map_of_isThickening_bigH
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigHOver B S hS)ᵒᵖ ⥤ Type v)
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F)
    {X X' : BigHOver B S hS} (i : X ⟶ X')
    (hi : IsThickening ((BigHOver.toScheme B S hS).map i))
    (hfp : FinitePresentation ((BigHOver.toScheme B S hS).map i)) :
    Function.Bijective (F.map i.op)

AlgebraicGeometry.bijective_map_of_isThickening_bigAffineH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpDescent.lean, line 1036. The attribute's comment: “big affine h site”.

Stacks 0EVE. A sheaf on the big affine h site over a scheme restricts bijectively along a morphism of the site which is a thickening and of finite presentation.

public theorem bijective_map_of_isThickening_bigAffineH
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigAffineH B S hS)ᵒᵖ ⥤ Type v)
    (hF : Presheaf.IsSheaf (BigAffineH.topology B S hS) F)
    {X X' : BigAffineH B S hS} (i : X ⟶ X')
    (hi : IsThickening ((BigAffineH.toScheme B S hS).map i))
    (hfp : FinitePresentation ((BigAffineH.toScheme B S hS).map i)) :
    Function.Bijective (F.map i.op)

Tag 0EVF, a proposition

Tag 0EVF in the Stacks Project.

AlgebraicGeometry.BigHOver.isAffineFlatProperFinitePresentationSheaf_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpSheafCriterion.lean, line 210. The attribute's comment: “only if, condition (2)”.

Stacks 0EVF, a sheaf satisfies condition (2). A sheaf on the big h site over S satisfies the sheaf condition for the one-element family attached to a morphism of the site with affine target which is flat, proper, surjective and of finite presentation.

Flatness is not used: such a morphism is an h covering all by itself, and so is every proper surjective morphism of finite presentation, which is the content of condition (2) of Stacks 0EU5.

public theorem isAffineFlatProperFinitePresentationSheaf_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F

AlgebraicGeometry.BigHOver.IsAffineFlatProperFinitePresentationSheaf.bijective_mapToEqualizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpSheafCriterion.lean, line 225. The attribute's comment: “condition (2) in equalizer form”.

Condition (2) of Stacks 0EVF in the source's equalizer form. Let f : V ⟶ U be a morphism of the big h category over S whose target has affine underlying scheme and whose underlying morphism of schemes is flat, proper, surjective and of finite presentation, and let p₁, p₂ : W ⟶ V complete f to a cartesian square, so that W = V ×_U V. Then condition (2) says exactly that F(U) maps bijectively onto the equalizer of the two maps F(V) ⟶ F(W).

This is the form in which the source states the condition; the two are identified by AlgebraicGeometry.isSheafFor_singleton_iff_bijective_mapToEqualizer.

public theorem IsAffineFlatProperFinitePresentationSheaf.bijective_mapToEqualizer
    (hF : BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F)
    {V U W : BigHOver B S hS} (f : V ⟶ U) (p₁ p₂ : W ⟶ V) (hW : IsPullback p₁ p₂ f f)
    (haffine : IsAffine ((BigHOver.toScheme B S hS).obj U))
    (hflat : Flat ((BigHOver.toScheme B S hS).map f))
    (hproper : IsProper ((BigHOver.toScheme B S hS).map f))
    (hsurj : Surjective ((BigHOver.toScheme B S hS).map f))
    (hfp : FinitePresentation ((BigHOver.toScheme B S hS).map f)) :
    Function.Bijective (regularTopology.mapToEqualizer F f p₁ p₂ hW.w)

AlgebraicGeometry.BigHOver.isAffineAlmostBlowUpSheaf_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpSheafCriterion.lean, line 243. The attribute's comment: “only if, condition (3)”.

Stacks 0EVF, a sheaf satisfies condition (3). A sheaf on the big h site over S sends an almost blowup square of the site with affine base to a cartesian square of sets.

Affineness of the base is not used: this is Stacks 0EVD for an arbitrary almost blowup square of the site.

public theorem isAffineAlmostBlowUpSheaf_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsAffineAlmostBlowUpSheaf B S hS F

AlgebraicGeometry.BigHOver.zariski_and_affineFlatProperFP_and_affineAlmostBlowUp_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpSheafCriterion.lean, line 261. The attribute's comment: “only if, all three conditions”.

Stacks 0EVF, the three conditions are necessary. A sheaf on the big h site over S satisfies condition (1), the sheaf condition for Zariski coverings, condition (2), the sheaf condition for every morphism of the site with affine target which is flat, proper, surjective and of finite presentation, and condition (3), the cartesianness of the image of every almost blowup square of the site with affine base.

The converse is AlgebraicGeometry.BigHOver.isSheaf_of_zariski_and_affineFlatProperFP_and_affineAlmostBlowUp, and the two together are AlgebraicGeometry.BigHOver.isSheaf_iff_zariski_and_affineFlatProperFP_and_affineAlmostBlowUp, both in StacksFrontier.AlgebraicGeometry.Topologies.HTopology.AlmostBlowUpSheafInduction.

public theorem zariski_and_affineFlatProperFP_and_affineAlmostBlowUp_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsZariskiSheaf B S hS F ∧
      BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F ∧
      BigHOver.IsAffineAlmostBlowUpSheaf B S hS F

AlgebraicGeometry.BigHOver.isSheaf_of_zariski_and_affineFlatProperFP_and_affineAlmostBlowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpSheafInduction.lean, line 541.

Stacks 0EVF, the three conditions are sufficient. A presheaf of sets on the big h category over S which satisfies condition (1), the sheaf condition for Zariski coverings, condition (2), the sheaf condition for every morphism of the site with affine target which is flat, proper, surjective and of finite presentation, and condition (3), the cartesianness of the image of every almost blowup square of the site with affine base, is a sheaf for the h topology.

public theorem isSheaf_of_zariski_and_affineFlatProperFP_and_affineAlmostBlowUp
    (hZ : BigHOver.IsZariskiSheaf B S hS F)
    (h2 : BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F)
    (h3 : BigHOver.IsAffineAlmostBlowUpSheaf B S hS F) :
    Presheaf.IsSheaf (BigHOver.topology B S hS) F

AlgebraicGeometry.BigHOver.isSheaf_iff_zariski_and_affineFlatProperFP_and_affineAlmostBlowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/AlmostBlowUpSheafInduction.lean, line 557.

Stacks 0EVF. A presheaf of sets on the big h category over S is a sheaf for the h topology if and only if it satisfies condition (1), the sheaf condition for Zariski coverings, condition (2), the sheaf condition for every morphism of the site with affine target which is flat, proper, surjective and of finite presentation, and condition (3), the cartesianness of the image of every almost blowup square of the site with affine base.

public theorem isSheaf_iff_zariski_and_affineFlatProperFP_and_affineAlmostBlowUp :
    Presheaf.IsSheaf (BigHOver.topology B S hS) F ↔
      (BigHOver.IsZariskiSheaf B S hS F ∧
        BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F ∧
        BigHOver.IsAffineAlmostBlowUpSheaf B S hS F)

Tag 0EVG, an example

Tag 0EVG in the Stacks Project.

AlgebraicGeometry.isAlmostBlowUpSquare_quotient_of_pow_mul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/PrincipalCenter.lean, line 321.

Stacks Project, Tag 0EVG. For a finitely generated ideal J of A annihilated by a power of f, the closed immersion Spec (A ⧸ J) ⟶ Spec A is the modification of an almost blowup square whose centre is the closed subscheme cut out by f.

public theorem isAlmostBlowUpSquare_quotient_of_pow_mul_eq_zero (A : Type u) [CommRing A]
    (f : A) (J : Ideal A) (hJ : J.FG) (h : ∃ n : ℕ, ∀ x ∈ J, f ^ n * x = 0) :
    IsAlmostBlowUpSquare
      (Scheme.IdealSheafData.ofIdealTop
        (Ideal.map (Scheme.ΓSpecIso (.of A)).inv.hom (Ideal.span {f})))
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J)))

Tag 0EVH, an example

Tag 0EVH in the Stacks Project.

Stacks.AlmostBlowUp.isAlmostBlowUpSquare_twoGeneratorSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/TwoGeneratorSupportedSections.lean, line 612.

Stacks Project, Tag 0EVH. Let A be a ring and f₁, f₂ ∈ A. The square
E = Proj ((A/(f₁,f₂))[T₀,T₁]) ⟶ Proj (A[T₀,T₁]/(f₂T₀-f₁T₁)) = X'
            ↓                                ↓
     Z = Spec (A/(f₁,f₂))      ⟶       Spec A = X
is an almost blowup square: it is cartesian, so that E = b⁻¹(Z); its lower arrow is, over Spec A, the closed subscheme cut out by (f₁,f₂); and the right-hand arrow b with that centre satisfies the conditions of an almost blowup square.

theorem isAlmostBlowUpSquare_twoGeneratorSquare :
    letI := (twoGeneratorSquare A f₁ f₂).modificationGraded
    IsPullback (exceptionalToModification A f₁ f₂) (exceptionalToCenter A f₁ f₂)
        (modificationToBase A f₁ f₂) (centerToBase A f₁ f₂) ∧
      Nonempty (Over.mk (centerToBase A f₁ f₂) ≅
        Over.mk (centerIdealSheaf A f₁ f₂).subschemeι) ∧
      AlgebraicGeometry.IsAlmostBlowUpSquare (centerIdealSheaf A f₁ f₂)
        (modificationToBase A f₁ f₂)

Tag 0EVI, a lemma

Tag 0EVI in the Stacks Project.

AlgebraicGeometry.BigHOver.isSheaf_iff_zariski_and_flatProper_and_generatorSquares, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpReduction.lean, line 786.

Stacks 0EVI. A presheaf of sets on the big h category over S is a sheaf for the h topology if and only if it satisfies condition (1), the sheaf condition for Zariski coverings, condition (2), the sheaf condition for every morphism of the site with affine target which is flat, proper, surjective and of finite presentation, condition (3), cartesianness of the image of every almost blowup square of the site with affine base and the shape of Example 0EVG, and condition (4), the same for the shape of Example 0EVH.

The sufficiency direction is the sufficiency direction of Stacks 0EVF, AlgebraicGeometry.affineAlmostBlowUpHSheafCriterion, applied after the reduction of its condition (3) to the two shapes, AlgebraicGeometry.generatorAlmostBlowUpSquaresSuffice. Condition (2) in the source's equalizer form is AlgebraicGeometry.BigHOver.IsAffineFlatProperFinitePresentationSheaf.bijective_mapToEqualizer.

theorem isSheaf_iff_zariski_and_flatProper_and_generatorSquares
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigHOver B S hS)ᵒᵖ ⥤ Type v) :
    Presheaf.IsSheaf (BigHOver.topology B S hS) F ↔
      (BigHOver.IsZariskiSheaf B S hS F ∧
        BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F ∧
        BigHOver.IsOneGeneratorAlmostBlowUpSheaf B S hS F ∧
        BigHOver.IsTwoGeneratorAlmostBlowUpSheaf B S hS F)

AlgebraicGeometry.BigHOver.isSheaf_iff_generatorAlmostBlowUpConditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpSheafCharacterization.lean, line 52.

Stacks 0EVI. A presheaf of sets on the big h category over S is a sheaf for the h topology if and only if it is a Zariski sheaf, satisfies the sheaf condition for every flat proper surjection of finite presentation of the site onto an affine object, and sends the almost blowup squares of the site of the shapes of Examples 0EVG and 0EVH to cartesian squares of sets.

public theorem isSheaf_iff_generatorAlmostBlowUpConditions :
    Presheaf.IsSheaf (BigHOver.topology B S hS) F ↔
      (IsZariskiSheaf B S hS F ∧ IsAffineFlatProperFinitePresentationSheaf B S hS F ∧
        IsOneGeneratorAlmostBlowUpSheaf B S hS F ∧ IsTwoGeneratorAlmostBlowUpSheaf B S hS F)

AlgebraicGeometry.BigHOver.isOneGeneratorAlmostBlowUpSheaf_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpSheafCriterion.lean, line 245. The attribute's comment: “only if, condition (3)”.

Stacks 0EVI, a sheaf satisfies condition (3). A sheaf on the big h site over S sends an almost blowup square of the site of the shape of Example 0EVG to a cartesian square of sets.

Neither the shape nor affineness of the base is used: this is Stacks 0EVD for an arbitrary almost blowup square of the site.

public theorem isOneGeneratorAlmostBlowUpSheaf_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsOneGeneratorAlmostBlowUpSheaf B S hS F

AlgebraicGeometry.BigHOver.isTwoGeneratorAlmostBlowUpSheaf_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpSheafCriterion.lean, line 257. The attribute's comment: “only if, condition (4)”.

Stacks 0EVI, a sheaf satisfies condition (4). A sheaf on the big h site over S sends an almost blowup square of the site of the shape of Example 0EVH to a cartesian square of sets.

Neither the shape nor affineness of the base is used: this is Stacks 0EVD for an arbitrary almost blowup square of the site.

public theorem isTwoGeneratorAlmostBlowUpSheaf_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsTwoGeneratorAlmostBlowUpSheaf B S hS F

AlgebraicGeometry.BigHOver.zariski_and_affineFlatProperFP_and_generatorSquares_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpSheafCriterion.lean, line 269. The attribute's comment: “only if, all four conditions”.

Stacks 0EVI, the necessity of all four conditions. A sheaf on the big h site over S is a sheaf for the Zariski topology, satisfies the equalizer condition for every morphism of the site with affine target which is flat, proper, surjective and of finite presentation, and sends an almost blowup square of the shape of Example 0EVG, respectively of Example 0EVH, to a cartesian square of sets.

public theorem zariski_and_affineFlatProperFP_and_generatorSquares_of_isSheaf
    (hF : Presheaf.IsSheaf (BigHOver.topology B S hS) F) :
    BigHOver.IsZariskiSheaf B S hS F ∧
      BigHOver.IsAffineFlatProperFinitePresentationSheaf B S hS F ∧
      BigHOver.IsOneGeneratorAlmostBlowUpSheaf B S hS F ∧
      BigHOver.IsTwoGeneratorAlmostBlowUpSheaf B S hS F

Tag 0EX9, a lemma

Tag 0EX9 in the Stacks Project.

AlgebraicGeometry.BigHOver.isStackInGroupoids_iff_generatorSquares, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpStackCharacterization.lean, line 69. The attribute's comment: “with condition (2) in its descent form: the source's literal condition (2) is false for h stacks, see AlgebraicGeometry.BigHOver.IsAffineFlatProperFinitePresentationDescent”.

Stacks 0EX9. A category fibred over the big h category over S is a stack in groupoids for the h topology if and only if it is a stack in groupoids for the Zariski topology, has effective descent along every surjective flat proper morphism of finite presentation onto an affine object of the site, and has 𝒮_X ⟶ 𝒮_Z ×_{𝒮_E} 𝒮_{X'} an equivalence for every almost blowup square of the site with affine base of the shape of Example 0EVG or of Example 0EVH.

Condition (2) is in its descent form: the source's literal condition (2), equivalence onto the two-fibre product, is false for h stacks, as recorded in the module documentation. Conditions (1) and (3) are the source's.

public theorem isStackInGroupoids_iff_generatorSquares :
    p.IsStackInGroupoids.{u + 1} (BigHOver.topology B S hS) ↔
      IsZariskiStackInGroupoids B S hS p ∧ IsAffineFlatProperFinitePresentationDescent B S hS p ∧
        IsOneGeneratorAlmostBlowUpStack B S hS p ∧ IsTwoGeneratorAlmostBlowUpStack B S hS p

AlgebraicGeometry.BigHOver.isZariskiStackInGroupoids_of_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpStackCriterion.lean, line 342. The attribute's comment: “only if, condition (1)”.

Stacks 0EX9, necessity of condition (1). A category fibred in groupoids over the big h category over S which is a stack in groupoids for the h topology is a stack in groupoids for the Zariski topology.

The Zariski topology on (Sch/S)_h is coarser than the h topology, AlgebraicGeometry.BigHOver.zariskiTopology_le_topology, and the conditions of Stacks 02ZI are indexed by the covering families of the topology.

public theorem isZariskiStackInGroupoids_of_isStackInGroupoids
    (hp : p.IsStackInGroupoids.{u + 1} (BigHOver.topology B S hS)) :
    BigHOver.IsZariskiStackInGroupoids B S hS p

AlgebraicGeometry.BigHOver.isAffineFlatProperFinitePresentationDescent_of_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpStackCriterion.lean, line 393. The attribute's comment: “only if, condition (2) in its descent form”.

Stacks 0EX9, necessity of condition (2) in its descent form. A category fibred in groupoids over the big h category over S which is a stack in groupoids for the h topology has effective descent, with descent of morphisms, along every surjective flat proper morphism of finite presentation onto an affine object of the site.

Flatness and affineness of the target are not used: AlgebraicGeometry.BigHOver.isEquivalence_toDescentData_singleton_of_isStackInGroupoids holds for every proper surjection of finite presentation, such a morphism being an h covering by itself.

public theorem isAffineFlatProperFinitePresentationDescent_of_isStackInGroupoids [p.IsFibered]
    (hp : p.IsStackInGroupoids.{u + 1} (BigHOver.topology B S hS)) :
    IsAffineFlatProperFinitePresentationDescent B S hS p

AlgebraicGeometry.BigHOver.isOneGeneratorAlmostBlowUpStack_of_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpStackNecessity.lean, line 152. The attribute's comment: “only if, condition (3) for the shape of Example 0EVG”.

Stacks 0EX9, necessity of condition (3) for the shape of Example 0EVG. A stack in groupoids for the h topology satisfies condition (3) for the squares of Example 0EVG; this is AlgebraicGeometry.BigHOver.isEquivalence_twoFibreProductComparison_of_isStackInGroupoids, which needs neither the affineness of the base nor the shape.

public theorem isOneGeneratorAlmostBlowUpStack_of_isStackInGroupoids [p.IsFibered]
    (hp : p.IsStackInGroupoids.{u + 1} (BigHOver.topology B S hS)) :
    IsOneGeneratorAlmostBlowUpStack B S hS p

AlgebraicGeometry.BigHOver.isTwoGeneratorAlmostBlowUpStack_of_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpStackNecessity.lean, line 163. The attribute's comment: “only if, condition (3) for the shape of Example 0EVH”.

Stacks 0EX9, necessity of condition (3) for the shape of Example 0EVH. A stack in groupoids for the h topology satisfies condition (3) for the squares of Example 0EVH; this is AlgebraicGeometry.BigHOver.isEquivalence_twoFibreProductComparison_of_isStackInGroupoids, which needs neither the affineness of the base nor the shape.

public theorem isTwoGeneratorAlmostBlowUpStack_of_isStackInGroupoids [p.IsFibered]
    (hp : p.IsStackInGroupoids.{u + 1} (BigHOver.topology B S hS)) :
    IsTwoGeneratorAlmostBlowUpStack B S hS p

AlgebraicGeometry.BigHOver.isStackInGroupoids_of_generatorSquares, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/GeneratorAlmostBlowUpStackSufficiency.lean, line 171. The attribute's comment: “if, with condition (2) in its descent form”.

Stacks 0EX9, the sufficiency direction. A category fibred in groupoids over the big h category over S which

is a stack in groupoids for the Zariski topology,

has effective descent, with descent of morphisms, along every surjective flat proper morphism of finite presentation X ⟶ Y of the site with Y affine: the functor from 𝒮_Y to the descent data relative to {X ⟶ Y} is an equivalence, and

has 𝒮_X ⟶ 𝒮_Z ×_{𝒮_E} 𝒮_{X'} an equivalence for every almost blow up square of the site of the shape of Example 0EVG or of Example 0EVH

is a stack in groupoids for the h topology.

Conditions (1) and (3) are those of the source. Condition (2) is the source's condition (2) with the two-fibre product 𝒮_X ×_{𝒮_{X ×_Y X}} 𝒮_X replaced by the category of descent data, which adds the cocycle condition over X ×_Y X ×_Y X: the literal condition fails for every h stack with a nontrivial automorphism over an affine object, by the fold-map computation in the module documentation of StacksFrontier.AlgebraicGeometry.Topologies.HTopology.GeneratorAlmostBlowUpStackCriterion, and the descent form is what the source's proof uses. The three hypotheses are those of the sheaf-level criterion of Stacks 0EVI that the proof of the source applies, read for a category fibred in groupoids: the Zariski one is the topology condition (1) of 0EVI quantifies over, and the descent along {X ⟶ Y} and the two equivalences range over the morphisms and squares conditions (2), (3) and (4) of 0EVI range over.

The proof runs Stacks 0EVI on the two auxiliary presheaves of sets on the slice (Sch/S)_h / U that the source builds out of 𝒮: the presheaf of morphisms between two objects of the fibre over U, whose sheaf property is AlgebraicGeometry.BigHOver.isMorSheaf_of_generatorSquares, and the presheaf of solutions of a descent problem, whose sheaf property is AlgebraicGeometry.BigHOver.nonempty_descentSolution_id. Both are run through AlgebraicGeometry.BigHOver.of_localOnGenerators.

public theorem isStackInGroupoids_of_generatorSquares
    (h1 : IsZariskiStackInGroupoids B S hS p)
    (h2 : IsAffineFlatProperFinitePresentationDescent B S hS p)
    (h3 : IsOneGeneratorAlmostBlowUpStack B S hS p)
    (h4 : IsTwoGeneratorAlmostBlowUpStack B S hS p) :
    p.IsStackInGroupoids.{u + 1} (BigHOver.topology B S hS)

Sources

LeanAlgebraicGeometry.isIso_restrict_compl_support · AlgebraicGeometry.IsAlmostBlowUpSquare · AlgebraicGeometry.supportedSectionsIdeal_ideal · AlgebraicGeometry.isAlmostBlowUpSquare_baseChange · AlgebraicGeometry.isIso_restrict_iff_le_supportedSectionsIdeal · AlgebraicGeometry.le_supportedSectionsIdeal_iff_isAlmostBlowUpSquare · AlgebraicGeometry.isFiltered_and_exists_isLimit_blowUpCone · AlgebraicGeometry.exists_isAlmostBlowUpSquare

Section38.38 Absolute weak normalization and h coverings #

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

Tag 0EVJ, a lemma

Tag 0EVJ in the Stacks Project.

Stacks.AlmostBlowUp.surjective_Γ_modificationToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/TwoGeneratorCohomology.lean, line 222. The attribute's comment: “surjectivity”.

Stacks Project, Tag 0EVJ. For the two-generator almost blowup square the ring map Γ(X, 𝒪_X) ⟶ Γ(X', 𝒪_{X'}) is surjective.

A global function on X' has a value on each of the two standard charts; the two agree on the overlap, so Stacks.AlmostBlowUp.exists_chartAwayMap_eq produces an element of A with those two values, and a global function is determined by its chart values.

theorem surjective_Γ_modificationToBase :
    letI := (twoGeneratorSquare A f₁ f₂).modificationGraded
    Function.Surjective (Scheme.Γ.map (modificationToBase A f₁ f₂).op).hom

Stacks.AlmostBlowUp.isZero_hgroup_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/TwoGeneratorCohomology.lean, line 364. The attribute's comment: “higher cohomology vanishing”.

Stacks Project, Tag 0EVJ. Hᵖ(X', 𝒪_{X'}) = 0 for p > 0.

The modification of the two-generator almost blowup square is covered by the two standard affine opens D₊(T₀) and D₊(T₁), whose intersection D₊(T₀T₁) is affine too. Mayer--Vietoris therefore reduces positive-degree cohomology over the whole space to positive-degree cohomology over those three affines, which vanishes by Serre, plus — in degree one — the surjectivity of Stacks.AlmostBlowUp.exists_restrict_add_restrict_eq.

theorem isZero_hgroup_structureSheaf (p : ℕ) (hp : 0 < p) :
    letI := (twoGeneratorSquare A f₁ f₂).modificationGraded
    IsZero (Hgroup (AlgebraicGeometry.Proj (modificationGrading A f₁ f₂)).ringCatSheaf ⊤ p
      (SheafOfModules.unit
        (AlgebraicGeometry.Proj (modificationGrading A f₁ f₂)).ringCatSheaf))

Stacks.AlmostBlowUp.modificationToBase_ker_sq_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/TwoGeneratorKernel.lean, line 221. The attribute's comment: “kernel_square_zero”.

Stacks Project, Tag 0EVJ. The global functions on Spec A killed by the modification of the two-generator almost blowup square form an ideal of square zero.

theorem modificationToBase_ker_sq_eq_bot (A : Type u) [CommRing A] (f₁ f₂ : A) :
    letI := (twoGeneratorSquare A f₁ f₂).modificationGraded
    RingHom.ker (Scheme.Γ.map (modificationToBase A f₁ f₂).op).hom ^ 2 = ⊥

Tag 0EVK, a lemma

Tag 0EVK in the Stacks Project.

AlgebraicGeometry.BigHOver.existsUnique_iso_frobeniusColimitSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/FrobeniusColimitHSheaf.lean, line 957.

Stacks 0EVK. Let p be a prime number, let S be a scheme over 𝔽_p (that is, p vanishes in Γ(S, 𝒪_S)), and let (Sch/S)_h be a big h site over S as in Stacks 0EU1. There is a unique sheaf ℱ on (Sch/S)_h such that ℱ(X) = colim_F Γ(X, 𝒪_X) for every quasi-compact quasi-separated object X.

The identification is a morphism of presheaves colim_F Γ(-, 𝒪) ⟶ ℱ that is bijective on quasi-compact quasi-separated objects, so naturality in X expresses compatibility with restriction. The first conjunct is existence and the second is uniqueness: two such sheaves are isomorphic, by a unique isomorphism compatible with the identifications.

The sheaf constructed is X ↦ Γ(Xᵃʷⁿ, 𝒪), global functions on the absolute weak normalization. The proof does not use the criterion of Stacks 0EVI, whose sufficiency direction this development lacks; it uses the absolute weak normalization instead. The sheaf property comes from the descent statements behind Stacks 0EVT and the h-sheaf criterion Stacks 0EU5. The comparison colim_F Γ(X, 𝒪_X) ⟶ Γ(Xᵃʷⁿ, 𝒪) is bijective on quasi-compact quasi-separated X. On an affine open this is Stacks 0EVW, and the affine pieces glue over a finite affine covering because the overlaps are quasi-compact.

public theorem existsUnique_iso_frobeniusColimitSections (p : ℕ) (hp : p.Prime)
    (hSp : Stacks.Frobenius.IsInCharacteristic S p) :
    (∃ (F : (BigHOver B S hS)ᵒᵖ ⥤ Type u) (φ : frobeniusColimitSections B S hS p ⟶ F),
      Presheaf.IsSheaf (BigHOver.topology B S hS) F ∧
        ∀ X : BigHOver B S hS, CompactSpace ((BigHOver.toScheme B S hS).obj X) →
          QuasiSeparatedSpace ((BigHOver.toScheme B S hS).obj X) →
            Function.Bijective (φ.app (op X))) ∧
    ∀ {F G : (BigHOver B S hS)ᵒᵖ ⥤ Type u}
      (φ : frobeniusColimitSections B S hS p ⟶ F) (ψ : frobeniusColimitSections B S hS p ⟶ G),
      Presheaf.IsSheaf (BigHOver.topology B S hS) F →
      Presheaf.IsSheaf (BigHOver.topology B S hS) G →
      (∀ X : BigHOver B S hS, CompactSpace ((BigHOver.toScheme B S hS).obj X) →
        QuasiSeparatedSpace ((BigHOver.toScheme B S hS).obj X) →
          Function.Bijective (φ.app (op X))) →
      (∀ X : BigHOver B S hS, CompactSpace ((BigHOver.toScheme B S hS).obj X) →
        QuasiSeparatedSpace ((BigHOver.toScheme B S hS).obj X) →
          Function.Bijective (ψ.app (op X))) →
      ∃! e : F ≅ G, φ ≫ e.hom = ψ

Tag 0EVL, a lemma

Tag 0EVL in the Stacks Project.

AlgebraicGeometry.BigHOver.isSheaf_frobeniusLimitSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/FrobeniusLimitHSheafCriterion.lean, line 69.

Stacks 0EVL. Let p be a prime number and let S be a scheme over 𝔽_p, contained in a big h site B. Then X ↦ lim_F Γ(X, 𝒪_X), the limit of the p-power map on global functions, is a sheaf on the big h site (Sch/S)_h.

The four conditions of the h sheaf criterion Stacks 0EVI hold for this presheaf; the sufficiency direction of that criterion is AlgebraicGeometry.affineAlmostBlowUpHSheafCriterion together with AlgebraicGeometry.generatorAlmostBlowUpSquaresSuffice.

public theorem isSheaf_frobeniusLimitSections
    (p : ℕ) (hp : p.Prime) (hChar : Stacks.Frobenius.IsInCharacteristic S p) :
    Presheaf.IsSheaf (BigHOver.topology B S hS) (frobeniusLimitSections B S hS p)

Tag 0EVT, a lemma

Tag 0EVT in the Stacks Project.

AlgebraicGeometry.isSheaf_absoluteWeakNormalizationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/PhSheafOfSections.lean, line 866.

On a big ph site, global functions on absolute weak normalizations form a sheaf.

Together with AlgebraicGeometry.existsUnique_hom_absoluteWeakNormalizationSections, this shows that the canonical map from the structure sheaf exhibits this sheaf as its ph sheafification.

theorem isSheaf_absoluteWeakNormalizationSections (B : BigPHSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    Presheaf.IsSheaf (BigPHOver.topology B S hS) (absoluteWeakNormalizationSections B S hS)

Tag 0EVU, a lemma

Tag 0EVU in the Stacks Project.

AlgebraicGeometry.isSheaf_absoluteWeakNormalizationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/PhSheafOfSections.lean, line 866. The attribute's comment: “ph topology, the sheaf property”.

On a big ph site, global functions on absolute weak normalizations form a sheaf.

Together with AlgebraicGeometry.existsUnique_hom_absoluteWeakNormalizationSections, this shows that the canonical map from the structure sheaf exhibits this sheaf as its ph sheafification.

theorem isSheaf_absoluteWeakNormalizationSections (B : BigPHSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    Presheaf.IsSheaf (BigPHOver.topology B S hS) (absoluteWeakNormalizationSections B S hS)

AlgebraicGeometry.existsUnique_hom_absoluteWeakNormalizationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/StructureSheafSheafification.lean, line 661. The attribute's comment: “ph topology”.

Stacks Project, Tag 0EVU, the ph case. On a big ph site over S, global functions on absolute weak normalizations are the sheafification of the structure sheaf: every map from the structure sheaf to a sheaf of rings factors uniquely through the canonical map. The other half of the statement, that the target is a sheaf, is Stacks 0EVT.

theorem existsUnique_hom_absoluteWeakNormalizationSections
    (G : (BigPHOver B S hS)ᵒᵖ ⥤ CommRingCat.{u})
    (hG : Presheaf.IsSheaf (BigPHOver.topology B S hS) G)
    (α : (BigPHOver.toScheme B S hS).op ⋙ Scheme.Γ ⟶ G) :
    ∃! χ : absoluteWeakNormalizationSections B S hS ⟶ G,
      absoluteWeakNormalizationSectionsMap (BigPHOver.toScheme B S hS) ≫ χ = α

AlgebraicGeometry.BigHOver.isSheaf_absoluteWeakNormalizationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/StructureSheafSheafification.lean, line 722. The attribute's comment: “h topology, the sheaf property”.

Stacks Project, Tag 0EVU, the sheaf property in the h case. On a big h site over S, global functions on absolute weak normalizations form a sheaf for the h topology.

This is the h analogue of Stacks 0EVT, and is proved from the same two descent statements — Zariski descent and descent along a proper surjection onto an affine — through the h sheaf criterion of Stacks 0EU5, whose second condition carries the extra hypothesis that the proper surjection is of finite presentation.

theorem isSheaf_absoluteWeakNormalizationSections :
    Presheaf.IsSheaf (BigHOver.topology B S hS)
      (absoluteWeakNormalizationSectionsOver (BigHOver.toScheme B S hS))

AlgebraicGeometry.BigHOver.existsUnique_hom_absoluteWeakNormalizationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/StructureSheafSheafification.lean, line 758. The attribute's comment: “h topology, the universal property of the sheafification”.

Stacks Project, Tag 0EVU, the h case. On a big h site over S, global functions on absolute weak normalizations are the sheafification of the structure sheaf: every map from the structure sheaf to a sheaf of rings factors uniquely through the canonical map. Together with AlgebraicGeometry.BigHOver.isSheaf_absoluteWeakNormalizationSections, which is the other half of the statement, this says that the rule X ↦ Γ(Xᵃʷⁿ, 𝒪) is the sheafification of the structure sheaf on the big h site.

theorem existsUnique_hom_absoluteWeakNormalizationSections
    (G : (BigHOver B S hS)ᵒᵖ ⥤ CommRingCat.{u})
    (hG : Presheaf.IsSheaf (BigHOver.topology B S hS) G)
    (α : (BigHOver.toScheme B S hS).op ⋙ Scheme.Γ ⟶ G) :
    ∃! χ : absoluteWeakNormalizationSectionsOver (BigHOver.toScheme B S hS) ⟶ G,
      absoluteWeakNormalizationSectionsMap (BigHOver.toScheme B S hS) ≫ χ = α

Tag 0EVV, a lemma

Tag 0EVV in the Stacks Project.

isAbsolutelyWeaklyNormalRing_iff_perfectRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/AbsolutelyWeaklyNormalPerfect.lean, line 56.

An algebra over 𝐅_p, for p prime, is absolutely weakly normal if and only if its Frobenius endomorphism is bijective.

lemma isAbsolutelyWeaklyNormalRing_iff_perfectRing
    (p : ℕ) (hp : p.Prime) (A : Type*) [CommRing A] [Algebra (ZMod p) A] :
    IsAbsolutelyWeaklyNormalRing A ↔ PerfectRing A p

Tag 0EVW, a lemma

Tag 0EVW in the Stacks Project.

Algebra.existsUnique_frobeniusColimit_iso_absoluteWeakNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/FrobeniusColimit.lean, line 229. The attribute's comment: “frobenius_colimit”.

For p prime and A an algebra over ZMod p, the colimit of the Frobenius sequence of A is the absolute weak normalization of A, by a unique isomorphism compatible with the canonical maps out of A.

theorem existsUnique_frobeniusColimit_iso_absoluteWeakNormalization
    (p : ℕ) (hp : p.Prime) (A : Type u) [CommRing A] [Algebra (ZMod p) A] :
    letI : Fact p.Prime := ⟨hp⟩
    ∃! e : colimit (frobeniusDiagram p A) ≅
        CommRingCat.of (AbsoluteWeakNormalization A),
      colimit.ι (frobeniusDiagram p A) 0 ≫ e.hom =
        CommRingCat.ofHom (algebraMap A (AbsoluteWeakNormalization A))

AlgebraicGeometry.BigHOver.exists_bijective_hom_frobeniusColimitSections_of_isSheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/FrobeniusColimitSheafification.lean, line 86. The attribute's comment: “the h sheafification of the structure sheaf on qcqs objects”.

Part (2) of Stacks Project, Tag 0EVW. Let p be a prime number and let S be a scheme over 𝔽_p, that is, a scheme in which p vanishes on global functions. Let (Sch/S)_h be a big h site over S as in Stacks 0EU1. Let G be the h sheafification of the structure sheaf 𝒪: a sheaf of rings together with a map α : 𝒪 ⟶ G initial among the maps from 𝒪 to sheaves of rings. Then the sections of G over a quasi-compact quasi-separated object X are colim_F Γ(X, 𝒪_X).

The identification is given by a map of presheaves colim_F Γ(-, 𝒪) ⟶ G which agrees with α on the stage 0 of the Frobenius tower and is bijective over every quasi-compact quasi-separated object; naturality is compatibility with restriction.

public theorem exists_bijective_hom_frobeniusColimitSections_of_isSheafification (p : ℕ)
    (hp : p.Prime) (hSp : Stacks.Frobenius.IsInCharacteristic S p)
    (G : (BigHOver B S hS)ᵒᵖ ⥤ CommRingCat.{u})
    (hG : Presheaf.IsSheaf (BigHOver.topology B S hS) G)
    (α : (BigHOver.toScheme B S hS).op ⋙ Scheme.Γ.{u} ⟶ G)
    (hα : ∀ H : (BigHOver B S hS)ᵒᵖ ⥤ CommRingCat.{u},
      Presheaf.IsSheaf (BigHOver.topology B S hS) H →
      ∀ β : (BigHOver.toScheme B S hS).op ⋙ Scheme.Γ.{u} ⟶ H, ∃! χ : G ⟶ H, α ≫ χ = β) :
    ∃ φ : frobeniusColimitSections B S hS p ⟶ G ⋙ CategoryTheory.forget CommRingCat.{u},
      (∀ (X : BigHOver B S hS) (a : Γ((BigHOver.toScheme B S hS).obj X, ⊤)),
        φ.app (op X) (colimitStage B S hS p 0 X a) = α.app (op X) a) ∧
      ∀ X : BigHOver B S hS, CompactSpace ((BigHOver.toScheme B S hS).obj X) →
        QuasiSeparatedSpace ((BigHOver.toScheme B S hS).obj X) →
          Function.Bijective (φ.app (op X))

AlgebraicGeometry.frobeniusColimit_absoluteWeakNormalization_and_hSheafificationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/FrobeniusColimitSheafification.lean, line 176.

Stacks Project, Tag 0EVW. Let p be a prime number.

(1) If A is an algebra over 𝔽_p, then colim_F A = A^{awn}: the colimit of the Frobenius tower of A is the absolute weak normalization of A, by a unique isomorphism compatible with the canonical maps out of A.

(2) If S is a scheme over 𝔽_p and (Sch/S)_h is a big h site over S as in Stacks 0EU1, then the h sheafification of the structure sheaf 𝒪 — a sheaf of rings G with a map α : 𝒪 ⟶ G initial among the maps from 𝒪 to sheaves of rings — sends a quasi-compact quasi-separated object X to colim_F Γ(X, 𝒪_X), by an identification agreeing with α on the stage 0 of the Frobenius tower.

public theorem frobeniusColimit_absoluteWeakNormalization_and_hSheafificationSections (p : ℕ)
    (hp : p.Prime) :
    letI : Fact p.Prime := ⟨hp⟩
    (∀ (A : Type u) [CommRing A] [Algebra (ZMod p) A],
      ∃! e : colimit (Algebra.frobeniusDiagram p A) ≅
          CommRingCat.of (Algebra.AbsoluteWeakNormalization A),
        colimit.ι (Algebra.frobeniusDiagram p A) 0 ≫ e.hom =
          CommRingCat.ofHom (algebraMap A (Algebra.AbsoluteWeakNormalization A))) ∧
    (∀ (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S),
      Stacks.Frobenius.IsInCharacteristic S p →
      ∀ (G : (BigHOver B S hS)ᵒᵖ ⥤ CommRingCat.{u}),
        Presheaf.IsSheaf (BigHOver.topology B S hS) G →
      ∀ α : (BigHOver.toScheme B S hS).op ⋙ Scheme.Γ.{u} ⟶ G,
        (∀ H : (BigHOver B S hS)ᵒᵖ ⥤ CommRingCat.{u},
          Presheaf.IsSheaf (BigHOver.topology B S hS) H →
          ∀ β : (BigHOver.toScheme B S hS).op ⋙ Scheme.Γ.{u} ⟶ H, ∃! χ : G ⟶ H, α ≫ χ = β) →
        ∃ φ : BigHOver.frobeniusColimitSections B S hS p ⟶
            G ⋙ CategoryTheory.forget CommRingCat.{u},
          (∀ (X : BigHOver B S hS) (a : Γ((BigHOver.toScheme B S hS).obj X, ⊤)),
            φ.app (op X) (BigHOver.colimitStage B S hS p 0 X a) = α.app (op X) a) ∧
          ∀ X : BigHOver B S hS, CompactSpace ((BigHOver.toScheme B S hS).obj X) →
            QuasiSeparatedSpace ((BigHOver.toScheme B S hS).obj X) →
              Function.Bijective (φ.app (op X)))

Sources

LeanStacks.AlmostBlowUp.surjective_Γ_modificationToBase · Stacks.AlmostBlowUp.isZero_hgroup_structureSheaf · Stacks.AlmostBlowUp.modificationToBase_ker_sq_eq_bot · AlgebraicGeometry.BigHOver.existsUnique_iso_frobeniusColimitSections · AlgebraicGeometry.BigHOver.isSheaf_frobeniusLimitSections · AlgebraicGeometry.isSheaf_absoluteWeakNormalizationSections · AlgebraicGeometry.existsUnique_hom_absoluteWeakNormalizationSections · AlgebraicGeometry.BigHOver.isSheaf_absoluteWeakNormalizationSections

Section38.39 Descent vector bundles in positive characteristic #

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

Tag 0EXA, the section

Tag 0EXA in the Stacks Project.

AlgebraicGeometry.frobeniusColimitVectModelEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectExplicit.lean, line 78. The attribute's comment: “colim_F Vect(S) is the category of pairs (E, n) described in the tag”.

Stacks Tag 0EXA: the explicit category is the colimit. The category frobeniusColimitVectModel, whose objects are the pairs (ℰ, n) and whose Hom-sets are the colimits colim_N Hom_S(F^{N - n, *}ℰ, F^{N - m, *}𝒢), is equivalent to the colimit colim_F Vect(S) of Vect(S) →F* Vect(S) →F* ⋯ in Cat.

noncomputable def frobeniusColimitVectModelEquivalence :
    frobeniusColimitVectModel X p hX ≌ frobeniusColimitVect X p hX

AlgebraicGeometry.exists_frobeniusColimitVect_obj_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectExplicit.lean, line 101. The attribute's comment: “an object of colim_F Vect(S) is a pair (E, n)”.

Stacks Tag 0EXA: the objects of colim_F Vect(S) are the pairs (ℰ, n). Every object of the colimit in Cat is the image of a finite locally free 𝒪_S-module ℰ under the stage-n coprojection, for some n.

theorem exists_frobeniusColimitVect_obj_eq (Y : frobeniusColimitVect X p hX) :
    ∃ (n : ℕ) (E : X.Vect),
      (EndoColim.catStage.{u + 1} (frobeniusPullback X p hX) n).obj E = Y

AlgebraicGeometry.frobeniusColimitVectModelHomIsColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectExplicit.lean, line 133. The attribute's comment: “Hom((E, n), (G, m)) = colim_N Hom_S(F^{N - n, }E, F^{N - m, }G)”.

Stacks Tag 0EXA: the Hom-sets of colim_F Vect(S). In the explicit category, Hom((ℰ, n), (𝒢, m)) is the colimit colim_N Hom_S(F^{N - n, *}ℰ, F^{N - m, *}𝒢) over the N ≥ n, m along F^*, the colimit maps taking a morphism of Vect(S) to the morphism it presents.

noncomputable def frobeniusColimitVectModelHomIsColimit (E G : X.Vect) (n m : ℕ) :
    IsColimit (EndoColim.homCocone (⟨E, n⟩ : frobeniusColimitVectModel X p hX) ⟨G, m⟩)

AlgebraicGeometry.frobeniusColimitVectHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectExplicit.lean, line 142. The attribute's comment: “Hom((E, n), (G, m)) = colim_N Hom_S(F^{N - n, }E, F^{N - m, }G), for the colimit in Cat”.

Stacks Tag 0EXA: the Hom-sets of colim_F Vect(S), in the colimit in Cat. The morphisms between the images of ℰ and 𝒢 under the stage-n and stage-m coprojections are in bijection with colim_N Hom_S(F^{N - n, *}ℰ, F^{N - m, *}𝒢).

noncomputable def frobeniusColimitVectHomEquiv (E G : X.Vect) (n m : ℕ) :
    ((EndoColim.catStage.{u + 1} (frobeniusPullback X p hX) n).obj E ⟶
        (EndoColim.catStage.{u + 1} (frobeniusPullback X p hX) m).obj G) ≃
      colimit (EndoColim.homDiagram (⟨E, n⟩ : frobeniusColimitVectModel X p hX) ⟨G, m⟩)

AlgebraicGeometry.frobeniusColimitVectModelShiftIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectExplicit.lean, line 170. The attribute's comment: “the object (E, n) is isomorphic to the object (F^* E, n + 1)”.

Stacks Tag 0EXA: (ℰ, n) ≅ (F^*ℰ, n + 1) in colim_F Vect(S).

noncomputable def frobeniusColimitVectModelShiftIso (E : X.Vect) (n : ℕ) :
    (⟨E, n⟩ : frobeniusColimitVectModel X p hX) ≅ ⟨(frobeniusPullback X p hX).obj E, n + 1⟩

AlgebraicGeometry.frobeniusColimitVect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectorBundles.lean, line 274.

The category colim_F Vect(X) of Stacks Tag 0EXA. It is the colimit of the sequential diagram of categories of finite locally free 𝒪_X-modules whose transition functors are all pullback along the absolute Frobenius.

noncomputable def frobeniusColimitVect : Cat.{u + 1, u + 1}

Tag 0EXB, a lemma

Tag 0EXB in the Stacks Project.

AlgebraicGeometry.frobeniusColimitVectEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectEssSurj.lean, line 186. The attribute's comment: “the category colim_F Vect(X) of Tag 0EXA is equivalent to the category of finite locally free modules over the sheaf of rings colim_F O_X”.

Stacks Project, Tag 0EXB. The category colim_F Vect(X) of Stacks Tag 0EXA is equivalent to the category of finite locally free modules over the sheaf of rings colim_F 𝒪_X, the equivalence being the comparison functor of the tag.

noncomputable def frobeniusColimitVectEquivalence [CompactSpace X] [QuasiSeparatedSpace X] :
    frobeniusColimitVectModel X p hX ≌ frobeniusColimitVectorBundles X p hX

Tag 0EXC, a lemma

Tag 0EXC in the Stacks Project.

AlgebraicGeometry.colimVectComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BlowUpSquares/OneGeneratorColimVectCornerCompat.lean, line 268.

Let p be a prime, let A be a ring with p = 0, let f ∈ A and let J ⊆ A be an ideal annihilated by f ^ n, so that
A ⧸ (J + fA) <--- A ⧸ J
      ^             ^
      |             |
   A ⧸ fA   <---    A
is the almost blowup square of More on Flatness, Example 0EVG. Then the comparison functor

colim\_F Vect(Spec A) ⟶ colim\_F Vect(Spec (A ⧸ fA)) ×\_\{colim\_F Vect(Spec (A ⧸ (J + fA)))} colim\_F Vect(Spec (A ⧸ J))

of Frobenius-colimit categories of vector bundles is an equivalence.

theorem colimVectComparison_isEquivalence (A : Type u) [CommRing A] (f : A) (J : Ideal A)
    (n : ℕ) (hann : ∀ x ∈ J, f ^ n * x = 0) (p : ℕ) [Fact p.Prime] (hp : (p : A) = 0) :
    (colimVectComparison A f J p hp).IsEquivalence

Tag 0EXD, a lemma

Tag 0EXD in the Stacks Project.

AlgebraicGeometry.isEquivalence_twoGeneratorColimVectComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitTwoGeneratorColimVect.lean, line 136. The attribute's comment: “for the categories colim_F Vect of Tag 0EXA”.

[Stacks, Tag 0EXD], for the categories colim_F Vect of [Stacks, Tag 0EXA]. Let p be a prime, A a ring in which p vanishes and f₁, f₂ ∈ A. For the almost blowup square X = Spec A, Z = Spec (A/(f₁,f₂)), X' = Proj (A[T₀,T₁]/(f₂T₀ - f₁T₁)), E = 𝐏¹_Z of [Stacks, Example 0EVH], the functor colim_F Vect(X) ⟶ colim_F Vect(Z) ×_{colim_F Vect(E)} colim_F Vect(X') built from the transition functors of the models colim_F Vect(-) is an equivalence.

It is AlgebraicGeometry.isEquivalence_twoGeneratorFrobeniusColimitComparison carried back along the comparison functors of [Stacks, Tag 0EXB] (AlgebraicGeometry.isEquivalence_colimVectSquare_of_frobeniusColimitVectorBundlesComparison): the base is affine, the modification and the exceptional line are Proj of finitely generated graded rings, so all four corners are quasi-compact and quasi-separated.

theorem isEquivalence_twoGeneratorColimVectComparison :
    letI := (twoGeneratorSquare A f₁ f₂).modificationGraded
    ((CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback _ _ _).obj
      (colimVectSquareCatCommSqOver p (modificationToBase A f₁ f₂) (centerToBase A f₁ f₂)
        (exceptionalToModification A f₁ f₂) (exceptionalToCenter A f₁ f₂)
        (isInCharacteristic_spec A p hpA)
        (isInCharacteristic_twoGeneratorModification A f₁ f₂ p hpA)
        (isInCharacteristic_twoGeneratorCenter A f₁ f₂ p hpA)
        (isInCharacteristic_twoGeneratorExceptional A f₁ f₂ p hpA)
        (twoGenerator_isPullback A f₁ f₂).w)).IsEquivalence

AlgebraicGeometry.isEquivalence_twoGeneratorFrobeniusColimitComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitTwoGeneratorEquivalence.lean, line 128.

[Stacks, Tag 0EXD]. Let p be a prime and consider the almost blowup square X, X', Z, E of [Stacks, Example 0EVH] in characteristic p, i.e. over a ring A in which p vanishes, with arbitrary f₁, f₂ ∈ A. Then the functor G : colim_F Vect(X) ⟶ colim_F Vect(Z) ×_{colim_F Vect(E)} colim_F Vect(X') is an equivalence.

theorem isEquivalence_twoGeneratorFrobeniusColimitComparison :
    letI := (twoGeneratorSquare A f₁ f₂).modificationGraded
    (twoGeneratorFrobeniusColimitComparison A f₁ f₂ p hpA).IsEquivalence

Tag 0EXE, a proposition

Tag 0EXE in the Stacks Project.

AlgebraicGeometry.frobeniusVectorBundleGroupoidFiberEquivCoreColimitVect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectorBundleGroupoidColimitVect.lean, line 98. The attribute's comment: “moreover: if U is quasi-compact and quasi-separated, then the fibre S_U of the category fibred in groupoids S over (Sch/S)_h is colim_F Vect(U), as its maximal subgroupoid”.

Stacks Tag 0EXE, the "moreover" clause. Let S be a scheme in characteristic p and let U be an object of (Sch/S)_h whose underlying scheme is quasi-compact and quasi-separated. Then the fibre 𝒮_U over U of the category fibred in groupoids 𝒮 ⟶ (Sch/S)_h of finite locally free colim_F 𝒪-modules is colim_F Vect(U), read as a groupoid: it is equivalent to the maximal subgroupoid of the colimit colim_F Vect(U) in Cat of Stacks Tag 0EXA.

The fibre is the groupoid of finite locally free modules over colim_F 𝒪_U (AlgebraicGeometry.frobeniusVectorBundleGroupoidFiberEquiv), which is the core of the category of such modules (CategoryTheory.ObjectProperty.coreFullSubcategoryEquiv); Stacks Tag 0EXB (AlgebraicGeometry.frobeniusColimitVectEquivalence) and Stacks Tag 0EXA (AlgebraicGeometry.frobeniusColimitVectModelEquivalence) identify that category with colim_F Vect(U), and the identification passes to cores.

def frobeniusVectorBundleGroupoidFiberEquivCoreColimitVect (U : BigHOver B S hS)
    [CompactSpace ((BigHOver.toScheme B S hS).obj U)]
    [QuasiSeparatedSpace ((BigHOver.toScheme B S hS).obj U)] :
    (frobeniusVectorBundleGroupoidFibration B S hS p hpS).Fiber U ≌
      Core (frobeniusColimitVect ((BigHOver.toScheme B S hS).obj U) p
        (isInCharacteristic_bigHOver B S hS p hpS U))

AlgebraicGeometry.frobeniusVectorBundleGroupoidFibration_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusColimitVectorBundleStack.lean, line 67. The attribute's comment: “stack in groupoids”.

Stacks Project, Tag 0EXE. Let p be a prime number and let S be a scheme in characteristic p. Then the category fibred in groupoids p : 𝒮 ⟶ (Sch/S)_h whose fibre category over U is the category of finite locally free colim_F 𝒪_U-modules over U (with its isomorphisms) is a stack in groupoids.

Here (Sch/S)_h is the big h site AlgebraicGeometry.BigHOver B S hS of an arbitrary big h site B containing S, and "stack in groupoids" is Stacks 02ZI for its h topology.

theorem frobeniusVectorBundleGroupoidFibration_isStackInGroupoids
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (p : ℕ) [Fact p.Prime]
    (hpS : IsInCharacteristic S p) :
    (frobeniusVectorBundleGroupoidFibration B S hS p hpS).IsStackInGroupoids.{u + 1}
      (BigHOver.topology B S hS)

Tag 0EXF, a lemma

Tag 0EXF in the Stacks Project.

Stacks.AlgebraicGeometry.FreenessOverDVR.exists_thickening_exponent_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FreenessOverDVR/FreenessCriterion.lean, line 190. The attribute's comment: “without the hypothesis that the fibres are geometrically connected, which the proof does not use”.

Stacks, Tag 0EXF. Let f : X ⟶ S be a proper morphism where S = Spec A is the spectrum of a discrete valuation ring. Denote η ∈ S the generic point and Xₙ ⊆ X the closed subscheme cut out by the n-th power of a uniformizer. Then there exists an integer n such that any finite locally free 𝒪_X-module 𝓔 such that 𝓔|_{X_η} and 𝓔|_{Xₙ} are free, is free.

The integer is n = k + 1 + e. Here k bounds the π-power torsion of the local rings of X (exists_forall_germ_pow_mul_eq_zero), and e bounds the π-power torsion of H¹(X, πᵏ 𝒪_X^r) for every rank r at once (exists_pow_smul_cohomology_adicSub_free_eq_zero). Comparing the lengths of H⁰(X, πᵏ (𝓔 / πᵏ⁺ᵐ 𝓔)) and H⁰(X, πᵏ (𝒪_X^r / πᵏ⁺ᵐ 𝒪_X^r)) at m = e and m = e + 1, which agree because 𝓔 / πⁿ 𝓔 ≅ 𝒪_X^r / πⁿ 𝒪_X^r, transfers that bound to H¹(X, πᵏ 𝓔) (torsionBy_cohomology_eq_bot_of_adicQuotientIso); the free ranks of the two H⁰ agree by the generic fibre. The basis sections of 𝒪_X^r / πⁿ 𝒪_X^r then lift, modulo πᵏ⁺¹, to global sections of 𝓔 (exists_sections_lift), and the resulting 𝒪_X^r ⟶ 𝓔 is an isomorphism modulo πᵏ⁺¹, hence an isomorphism since f is proper over a local base (isIso_of_comp_adicProj).

The source's hypothesis that the fibres of f be geometrically connected is not used: the source needs it only to reduce to the case where f has a section, and the argument above does not pass through a section.

theorem exists_thickening_exponent_free (A : Type u) [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [IsProper f] :
    ∃ n : ℕ, 0 < n ∧ ∀ E : X.Modules, E.IsFiniteLocallyFree →
      IsFreeOfFiniteRank (genericFibreRestrict A f E) →
      IsFreeOfFiniteRank (thickeningRestrict A f n E) →
      IsFreeOfFiniteRank E

Stacks.AlgebraicGeometry.FreenessOverDVR.exists_thickening_exponent_free_of_free_generic_and_thickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FreenessOverDVR/Triviality.lean, line 308. The attribute's comment: “conditional on TrivialityInput, which carries the source's cited input [Stacks, Tag 02O6] (finiteness of the cohomology of a proper morphism, open in this library), the reduction to the case of a section — whose last step, invertibility of a determinant invertible at one point of each fibre, the source itself leaves to the reader — and the derived comparison RΓ(X, 𝓔) ⊗^L A/π^m ≅ RΓ(X, 𝒪_X^r) ⊗^L A/π^m read on cohomology. Of the inputs of that comparison the library does carry the subsheaf of sections supported on the special fibre ([Stacks, Tag 084L]), the quotients 𝓔/π^j 𝓔, the Artin-Rees exponent ([Stacks, Tag 01YA]), the two-term complex (𝓔 --π^m--> 𝓔) in D(𝒪_X) with its distinguished triangle, and RΓ(X, -) : D(𝒪_X) ⥤ D(A); what it lacks is the reduction formula Hⁱ(K ⊗^L A/π^m) = Hⁱ(K)/π^m ⊕ Hⁱ⁺¹(K)[π^m], which is a step of the source's proof and not a tag. Proved here: the construction of both exponents and hence of n, the summand-counting transfer of the exponent bound from 𝒪_X to 𝓔 (torsionExponentTransfer), and the two Nakayama steps that turn surjectivity modulo π^{e+1} into freeness. The hypotheses are satisfiable: exists_thickening_exponent_free_specPowerSeries discharges all of them over k⟦X⟧”.

Stacks, Tag 0EXF. Let f : X ⟶ Spec A be proper with geometrically connected fibres over a discrete valuation ring A, let η be the generic point of Spec A and let X_n ⊆ X be the closed subscheme cut out by the n-th power of a uniformizer π. There is an integer n, independent of the module, such that every finite locally free 𝒪_X-module which is free on X_η and on X_n is free.

The integer produced is e + 1 + k, which is the source's k + e + 1: k is the Artin-Rees exponent carried by TrivialityInput.comparison, and e is an exponent annihilating the π-power torsion of H⁰(X, 𝒪_X) and H¹(X, 𝒪_X), both of which depend only on X.

theorem exists_thickening_exponent_free_of_free_generic_and_thickening
    {π : A} (hπ : Irreducible π) (h : TrivialityInput A f π) :
    ∃ n : ℕ, 0 < n ∧ ∀ E : X.Modules, E.IsFiniteLocallyFree →
      IsFreeOfFiniteRank (genericFibreRestrict A f E) →
      IsFreeOfFiniteRank (thickeningRestrict A f n E) →
      IsFreeOfFiniteRank E

Tag 0EXG, a lemma

Tag 0EXG in the Stacks Project.

AlgebraicGeometry.VectorBundleCodimensionOne.exists_isFiniteLocallyFree_pullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/VectorBundleCodimensionOne/FreeOverLocalBase.lean, line 61. The attribute's comment: “corrected: freeness is also required at generic points of S with no codimension-1 specialization; as stated the lemma fails for X = ℙ¹_k over Spec k with ℰ = 𝒪(1)”.

Let f : X ⟶ S be flat and proper with 𝒪_S = f_*𝒪_X, let S be a normal Noetherian scheme, and let ℰ be a finite locally free 𝒪_X-module whose pullback to X ×_S Spec 𝒪_{S,s} is free for every point s ∈ S of codimension one, and also for every point s of codimension zero that does not specialize to a point of codimension one. Then ℰ is isomorphic to the pullback of a finite locally free 𝒪_S-module.

The two conditions hfree and hfree₀ together are equivalent to freeness over the local scheme at every point of codimension at most one. The condition hfree₀ is not in the source, and the statement is false without it (not_forall_exists_isFiniteLocallyFree_pullback_iso_of_codimOne): for a field k, take S = Spec k, X = ℙ¹_k and ℰ = 𝒪(1); then S has no point of codimension one, but 𝒪(1) is not the pullback of a k-vector space. When every irreducible component of S has a point of codimension one, hfree₀ is vacuous.

Codimension of a point is the Krull dimension of its local ring, and freeness after base change to the local scheme at s means an isomorphism with some free module 𝒪^{(I)}, the index set being arbitrary. The hypothesis 𝒪_S = f_*𝒪_X is invertibility of the comparison map f.toLRSHom.toHom.c.

public theorem exists_isFiniteLocallyFree_pullback_iso {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [IsProper f] [IsNoetherian S] [IsNormal S] (E : X.Modules)
    [SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] (hO : IsIso f.toLRSHom.toHom.c)
    (hfree : ∀ s : S, ringKrullDim (S.presheaf.stalk s) = 1 →
      ∃ I : Type u, Nonempty
        ((Scheme.Modules.pullback (pullback.fst f (S.fromSpecStalk s))).obj E ≅
          SheafOfModules.free I))
    (hfree₀ : ∀ s : S, ringKrullDim (S.presheaf.stalk s) = 0 →
      (∀ t : S, s ⤳ t → ringKrullDim (S.presheaf.stalk t) ≠ 1) →
      ∃ I : Type u, Nonempty
        ((Scheme.Modules.pullback (pullback.fst f (S.fromSpecStalk s))).obj E ≅
          SheafOfModules.free I)) :
    ∃ M : S.Modules, SheafOfModules.IsFiniteLocallyFree.{u, u, u} M ∧
      Nonempty ((Scheme.Modules.pullback f).obj M ≅ E)

Tag 0EXH, a theorem

Tag 0EXH in the Stacks Project.

AlgebraicGeometry.frobeniusColimitVectModelPullback_full_faithful_and_descends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FrobeniusDescentVectorBundles.lean, line 48.

Descent of vector bundles in positive characteristic (Stacks Tag 0EXH). Let p be a prime, Y a quasi-compact quasi-separated scheme over 𝐅_p and f : X ⟶ Y a proper surjective morphism of finite presentation with geometrically connected fibres. Then the pullback functor colim_F Vect(Y) ⥤ colim_F Vect(X) is fully faithful, and if ℰ is a finite locally free 𝒪_X-module such that for all y ∈ Y there are n_y, r_y ≥ 0 with F^{n_y,*}ℰ|_{X_{y,red}} ≅ 𝒪_{X_{y,red}}^{⊕ r_y}, then for some n ≥ 0 the Frobenius power pullback F^{n,*}ℰ is the pullback of a finite locally free 𝒪_Y-module.

theorem frobeniusColimitVectModelPullback_full_faithful_and_descends (p : ℕ) [Fact p.Prime]
    {X Y : Scheme.{u}} (hY : IsInCharacteristic Y p) (f : X ⟶ Y) [CompactSpace Y]
    [QuasiSeparatedSpace Y] [IsProper f] [Surjective f] [LocallyOfFinitePresentation f]
    [GeometricallyConnected f] :
    ((frobeniusColimitVectModelPullback f p (isInCharacteristic_of_hom f p hY) hY).Full ∧
      (frobeniusColimitVectModelPullback f p (isInCharacteristic_of_hom f p hY) hY).Faithful) ∧
    ∀ E : X.Vect,
      (∀ y : Y, ∃ n r : ℕ, Nonempty
        ((Scheme.Modules.pullback ((f.fiber y).reductionι ≫ f.fiberι y)).obj
            ((frobeniusPullbackIter X p (isInCharacteristic_of_hom f p hY) n).obj E).obj ≅
          SheafOfModules.free (ULift.{u} (Fin r)))) →
      ∃ (n : ℕ) (G : Y.Vect), Nonempty
        ((frobeniusPullbackIter X p (isInCharacteristic_of_hom f p hY) n).obj E ≅
          (Scheme.Vect.pullback f).obj G)

Sources

LeanAlgebraicGeometry.frobeniusColimitVectModelEquivalence · AlgebraicGeometry.exists_frobeniusColimitVect_obj_eq · AlgebraicGeometry.frobeniusColimitVectModelHomIsColimit · AlgebraicGeometry.frobeniusColimitVectHomEquiv · AlgebraicGeometry.frobeniusColimitVectModelShiftIso · AlgebraicGeometry.frobeniusColimitVect · AlgebraicGeometry.frobeniusColimitVectEquivalence · AlgebraicGeometry.colimVectComparison_isEquivalence

Section38.40 Blowing up complexes #

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

Tag 0ESP, a lemma

Tag 0ESP in the Stacks Project.

AlgebraicGeometry.fittingIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FittingIdeal.lean, line 429. The attribute's comment: “the quasi-coherent ideal sheaf Fit_{p,k}(E)”.

The (p, k)-th Fitting ideal sheaf of a pseudo-coherent object of D(𝒪_X), the largest quasi-coherent sheaf of ideals which on every affine open is contained in the ideal of minors of d_p computed from every bounded-above finite free model, over U, of every complex representing E.

noncomputable def fittingIdealSheaf {X : Scheme.{u}} [HasDerivedCategory.{w} X.Modules]
    (E : DerivedCategory X.Modules) (p k : ℤ) : X.IdealSheafData

AlgebraicGeometry.ideal_fittingIdealSheaf_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FittingIdeal.lean, line 439. The attribute's comment: “the local description, the inclusion into the ideal of minors”.

On an affine open U over which a complex representing E has a bounded-above finite free model, the Fitting ideal sheaf is contained in the ideal generated by the minors of the matrix of d_p of size -k + n_{p+1} - n_{p+2} + ⋯ + (-1)^{b-p+1} n_b.

theorem ideal_fittingIdealSheaf_le {X : Scheme.{u}} [HasDerivedCategory.{w} X.Modules]
    (E : DerivedCategory X.Modules) (p k : ℤ) (U : X.affineOpens)
    (K : CochainComplex X.Modules ℤ) (hK : Nonempty (DerivedCategory.Q.obj K ≅ E))
    (M : FreeModel K U.1) :
    (fittingIdealSheaf E p k).ideal U ≤
      minorIdeal (M.matrix p) (M.toFreeData.minorSize p k).toNat

AlgebraicGeometry.fittingIdealSheafOfDerivedModels_isFiniteType_and_ideal_eq_minorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/FittingIdealLocalEquality.lean, line 158. The attribute's comment: “the finite type ideal sheaf Fit_{p,k}(E) and the minors of d_p generating it”.

Stacks Project, Tag 0ESP. Let X be a scheme and let E be a pseudo-coherent object of D(𝒪_X). For all integers p, k the Fitting ideal sheaf Fit_{p,k}(E) ⊆ 𝒪_X is a finite type quasi-coherent sheaf of ideals whose restriction to an open U over which E is isomorphic to a bounded-above complex of finite free modules ⋯ → 𝒪_U^{n_{b-1}} → 𝒪_U^{n_b} → 0 is generated by the minors of the matrix of d_p of size -k + n_{p+1} - n_{p+2} + ⋯ + (-1)^{b-p+1} n_b: on an affine U it is the ideal of those minors, and on an arbitrary U it is, over every affine open inside U, the ideal generated by their images. In particular the ideal of minors is the same for every such complex and every such model, which is the independence the source's proof establishes.

theorem fittingIdealSheafOfDerivedModels_isFiniteType_and_ideal_eq_minorIdeal
    (E : DerivedCategory X.Modules)
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E) (p k : ℤ) :
    (fittingIdealSheafOfDerivedModels E p k).IsFiniteType ∧
      (∀ (U : X.affineOpens) (K : CochainComplex X.Modules ℤ)
        (_ : Nonempty (DerivedCategory.Q.obj K ≅ E)) (M : DerivedFreeModel K U.1),
        (fittingIdealSheafOfDerivedModels E p k).ideal U =
          minorIdeal (M.matrix p) (M.toFreeData.minorSize p k).toNat) ∧
      ∀ (U : X.Opens) (K : CochainComplex X.Modules ℤ)
        (_ : Nonempty (DerivedCategory.Q.obj K ≅ E)) (M : DerivedFreeModel K U)
        (V : X.affineOpens) (hVU : V.1 ≤ U),
        (fittingIdealSheafOfDerivedModels E p k).ideal V =
          Ideal.map (X.presheaf.map (homOfLE hVU).op).hom
            (minorIdeal (M.matrix p) (M.toFreeData.minorSize p k).toNat)

Tag 0ESQ, a lemma

Tag 0ESQ in the Stacks Project.

AlgebraicGeometry.ComplexAndDivisorSituation.isAdmissibleBlowup_fittingIdealProdOfRanks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/PerfectComplexAdmissibleBlowup.lean, line 319. The attribute's comment: “the U-admissible blowup, in the product of the Fitting ideals of the complex”.

The blowup in the product of the Fitting ideal sheaves is U-admissible: the centre is of finite type and its support, the union of the supports of the factors, avoids U.

theorem isAdmissibleBlowup_fittingIdealProdOfRanks {m : ℤ} (hm : ∀ j, m < j → r j = 0)
    (hlf : LocallyFinite fun i => ((fittingIdealOfRanks hE r m i).support : Set X)) :
    Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase (fittingIdealProdOfRanks hE r m hlf))

AlgebraicGeometry.ComplexAndDivisorSituation.isEffectiveCartierDivisor_comap_fittingIdealOfRanks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/PerfectComplexAdmissibleBlowup.lean, line 333. The attribute's comment: “the Fitting ideals of the complex become effective Cartier divisors”.

On the blowup in the product of the Fitting ideal sheaves, the inverse image of each Fit_{i, k_i}(E) is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_comap_fittingIdealOfRanks {m : ℤ}
    (hlf : LocallyFinite fun i => ((fittingIdealOfRanks hE r m i).support : Set X)) (i : ℤ) :
    Stacks.Divisors.IsEffectiveCartierDivisor
      ((fittingIdealOfRanks hE r m i).comap
        (blowUpToBase (fittingIdealProdOfRanks hE r m hlf)))

AlgebraicGeometry.exists_admissibleBlowup_forall_isHomologyPerfectTorLEOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/PerfectComplexAdmissibleBlowup.lean, line 505.

Let X be a scheme, let E ∈ D(𝒪_X) be perfect, and let U ⊆ X be a scheme-theoretically dense open subscheme such that H^i(E|_U) is finite locally free of constant rank r_i for every i. Then there is a U-admissible blowup b : X' ⟶ X such that H^i(Lb^*E) is a perfect 𝒪_{X'}-module of Tor dimension at most one for every i.

theorem exists_admissibleBlowup_forall_isHomologyPerfectTorLEOne {X : Scheme.{u}}
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace)) (U : X.Opens)
    (dense : Scheme.Opens.IsSchemeTheoreticallyDense U) (perfect : IsPerfect.{u, u, u + 1} E)
    (r : ℤ → ℕ)
    (homology_rank : ∀ i : ℤ, SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((DerivedCategory.homologyFunctor (OXMod.{u, u} U.toScheme.toRingedSpace) i).obj
        ((derivedPullback U.ι.toLRSHom.toShHom).obj E)) (r i)) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X),
      Stacks.Blowup.IsAdmissibleBlowup U b ∧ ∀ i : ℤ, IsHomologyPerfectTorLEOne E b i

Tag 0ESR, a lemma

Tag 0ESR in the Stacks Project.

AlgebraicGeometry.exists_nonempty_open_admissibleBlowup_forall_isHomologyPerfectTorLEOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/IntegralPerfectComplexBlowup.lean, line 98.

Stacks Project, Tag 0ESR. Let X be an integral scheme and let E ∈ D(𝒪_X) be perfect. Then there is a nonempty open U ⊆ X such that H^i(E|_U) is finite locally free of constant rank r_i for every i, and a U-admissible blowup b : X' ⟶ X such that H^i(Lb^*E) is a perfect 𝒪_{X'}-module of Tor dimension at most one for every i.

theorem exists_nonempty_open_admissibleBlowup_forall_isHomologyPerfectTorLEOne
    (X : Scheme.{u}) [IsIntegral X] (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (perfect : IsPerfect.{u, u, u + 1} E) :
    ∃ (U : X.Opens) (r : ℤ → ℕ), (U : Set X).Nonempty ∧
      (∀ i : ℤ, SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
        ((DerivedCategory.homologyFunctor (OXMod.{u, u} U.toScheme.toRingedSpace) i).obj
          ((derivedPullback U.ι.toLRSHom.toShHom).obj E)) (r i)) ∧
      ∃ (X' : Scheme.{u}) (b : X' ⟶ X),
        Stacks.Blowup.IsAdmissibleBlowup U b ∧ ∀ i : ℤ, IsHomologyPerfectTorLEOne E b i

Tag 0F8J, a remark

Tag 0F8J in the Stacks Project.

CochainComplex.nonempty_truncLE_truncLE_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/TruncationShortExactSequence.lean, line 48. The attribute's comment: “the left-hand row of the display is the preceding truncation”.

The first row of the display of Stacks 0F8J. Truncating K above degree n and then above a degree m ≤ n returns the truncation of K above degree m.

public theorem nonempty_truncLE_truncLE_iso (K : CochainComplex C ℤ) {m n : ℤ} (h : m ≤ n) :
    Nonempty ((K.truncLE n).truncLE m ≅ K.truncLE m)

CochainComplex.nonempty_Q_shortComplexTruncLE_X₃_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/TruncationShortExactSequence.lean, line 72. The attribute's comment: “the right-hand row of the display is the shifted cohomology object”.

The right-hand row of the display of Stacks 0F8J. The quotient of the truncation of K above degree k - 1 inside the truncation of K above degree k is the cohomology object H^k(K) placed in degree k.

public theorem nonempty_Q_shortComplexTruncLE_X₃_iso (K : CochainComplex C ℤ) (k : ℤ) :
    Nonempty (DerivedCategory.Q.obj ((K.truncLE k).shortComplexTruncLE (k - 1)).X₃ ≅
      (DerivedCategory.singleFunctor C k).obj (K.homology k))

CochainComplex.nonempty_triangleOfSES_truncLE_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/TruncationShortExactSequence.lean, line 108. The attribute's comment: “the truncation triangle is the triangle of the displayed short exact sequence”.

Stacks 0F8J. The canonical truncation triangle τ_{≤k-1}K ⟶ τ_{≤k}K ⟶ H^k(K)[-k] ⟶ (τ_{≤k-1}K)[1] is the triangle of the short exact sequence of complexes 0 ⟶ τ_{≤k-1}(τ_{≤k}K) ⟶ τ_{≤k}K ⟶ Q ⟶ 0, morphisms included.

public theorem nonempty_triangleOfSES_truncLE_iso (K : CochainComplex C ℤ) (k : ℤ) :
    Nonempty (DerivedCategory.triangleOfSES
      ((K.truncLE k).shortComplexTruncLE_shortExact (k - 1)) ≅
      (DerivedCategory.TStructure.t.triangleLEGT (k - 1)).obj
        (DerivedCategory.Q.obj (K.truncLE k)))

Stacks.FiniteLocallyFree.isFiniteLocallyFree_cycles, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/BoundedComplex.lean, line 189. The attribute's comment: “the kernels of the differentials, for a complex of finite locally free modules on a scheme vanishing above a degree, with the cohomology sheaves perfect of tor amplitude in [-1, 0]”.

[Stacks, Tag 0F8J], the kernels. Let ℰ be a complex of finite locally free 𝒪_X-modules vanishing above degree b, each of whose cohomology sheaves is a perfect 𝒪_X-module of tor amplitude in [-1, 0]. Then Ker(d^n) is finite locally free for every n.

Boundedness below is not needed for this: the induction descends from b, and each step consumes only the degree above.

theorem isFiniteLocallyFree_cycles
    (hterm : ∀ n : ℤ, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (P.X n))
    (hperf : ∀ n : ℤ, IsPerfect.{u, u, u + 1}
      ((DerivedCategory.singleFunctor X.Modules 0).obj (P.homology n)))
    (htor : ∀ n : ℤ, HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor X.Modules 0).obj (P.homology n)) (-1) 0)
    (b : ℤ) [P.IsStrictlyLE b] (n : ℤ) :
    IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (P.cycles n)

Stacks.FiniteLocallyFree.isFiniteLocallyFree_kernel_homologyπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/BoundedComplex.lean, line 215. The attribute's comment: “the images of the differentials, presented as the kernels of the projections from the cocycles onto the cohomology, for a complex of finite locally free modules on a scheme vanishing above a degree, with the cohomology sheaves perfect of tor amplitude in [-1, 0]”.

[Stacks, Tag 0F8J], the images. Under the hypotheses of Stacks.FiniteLocallyFree.isFiniteLocallyFree_cycles, the image Im(d^{n-1}) of the differential into degree n is finite locally free.

That image is written here as kernel (P.homologyπ n), the kernel of the projection from the cocycles in degree n onto the cohomology there — the presentation StacksDraft.CartanEilenbergResolutions.cochainGluingData uses, and the one that is indexed by n with no subtraction. It is the image in the categorical sense too: StacksDraft.CartanEilenbergResolutions.exists_imageIso_of_cochainGluingData exhibits an isomorphism CategoryTheory.Limits.image (P.dFrom (n - 1)) ≅ kernel (P.homologyπ n) compatible with the factorisation of the differential through it.

theorem isFiniteLocallyFree_kernel_homologyπ
    (hterm : ∀ n : ℤ, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (P.X n))
    (hperf : ∀ n : ℤ, IsPerfect.{u, u, u + 1}
      ((DerivedCategory.singleFunctor X.Modules 0).obj (P.homology n)))
    (htor : ∀ n : ℤ, HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor X.Modules 0).obj (P.homology n)) (-1) 0)
    (b : ℤ) [P.IsStrictlyLE b] (n : ℤ) :
    IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (kernel (P.homologyπ n))

Stacks.FiniteLocallyFree.boundedComplexSplitting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/BoundedComplex.lean, line 246. The attribute's comment: “the degreewise exactness datum of a bounded complex of finite locally free modules on a scheme, assembled from the two displayed short exact sequences, with the cohomology sheaves perfect of tor amplitude in [-1, 0]”.

[Stacks, Tag 0F8J] assembled: the degreewise exactness datum of a bounded complex of finite locally free 𝒪_X-modules with perfect cohomology of tor dimension at most one.

This is the source's conclusion in the form its consumers need. Stacks.Chow defines the Chern classes, the power sums and the Chern character of a complex against a Stacks.Chow.BoundedComplexSplitting — the family of short exact sequences 0 ⟶ Ker(d^n) ⟶ ℰ^n ⟶ Im(d^n) ⟶ 0 together with finite local freeness of every kernel and every image — and before this nothing produced one. The finite local freeness of the kernels and of the images is precisely what the source takes from this tag; the rest of the datum is the degreewise presentation of the complex, supplied by StacksDraft.CartanEilenbergResolutions.cochainGluingData.

The two vanishing conditions at the ends of the range are the boundedness of the complex: nothing enters degree a because ℰ^{a-1} vanishes, and nothing leaves degree a + k because ℰ^{a+k+1} does.

def boundedComplexSplitting (a : ℤ) (k : ℕ)
    [P.IsStrictlyGE a] [P.IsStrictlyLE (a + (k : ℤ))]
    (hterm : ∀ n : ℤ, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (P.X n))
    (hperf : ∀ n : ℤ, IsPerfect.{u, u, u + 1}
      ((DerivedCategory.singleFunctor X.Modules 0).obj (G.H n)))
    (htor : ∀ n : ℤ, HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor X.Modules 0).obj (G.H n)) (-1) 0) :
    Stacks.Chow.BoundedComplexSplitting X P a k

StacksDraft.Perfect.isFiniteLocallyFree_range_and_ker_of_torDimensionLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/TorDimensionOneCohomology.lean, line 291. The attribute's comment: “the images and kernels of the differentials”.

Stacks 0F8J. Let X be a scheme and let E ∈ D(𝒪_X) be such that every cohomology module H^i(E) is a perfect 𝒪_X-module of Tor dimension at most one, that is, H^i(E) placed in degree zero is a perfect object with Tor amplitude in [-1, 0]. Let ℰ^• be a complex of finite locally free 𝒪_X-modules which vanishes above degree b and represents E. Then Im(d^i) and Ker(d^i) are finite locally free 𝒪_X-modules for every i.

The source takes E perfect and ℰ^• bounded; neither the perfectness of E nor a lower bound on ℰ^• is used.

public theorem isFiniteLocallyFree_range_and_ker_of_torDimensionLE_one
    (E : DerivedCategory X.Modules) (K : CochainComplex X.Modules ℤ)
    (e : DerivedCategory.Q.obj K ≅ E) (b : ℤ) [K.IsStrictlyLE b]
    (hterm : ∀ i : ℤ,
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (K.X i))
    (hH : ∀ i : ℤ,
      IsPerfect.{u, u, u + 1} ((DerivedCategory.singleFunctor X.Modules 0).obj
        ((DerivedCategory.homologyFunctor X.Modules i).obj E)) ∧
      HasTorAmplitude X.toRingedSpace ((DerivedCategory.singleFunctor X.Modules 0).obj
        ((DerivedCategory.homologyFunctor X.Modules i).obj E)) (-1) 0)
    (i : ℤ) :
    Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf)
        (image (K.d i (i + 1)) : X.Modules) ∧
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf)
        (kernel (K.d i (i + 1)) : X.Modules)

StacksDraft.Perfect.isFiniteLocallyFree_truncLE_X_of_torDimensionLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/TorDimensionOneCohomology.lean, line 319. The attribute's comment: “the rows of the short exact sequences representing the truncation triangles”.

Stacks 0F8J, the truncation rows. Under the hypotheses of StacksDraft.Perfect.isFiniteLocallyFree_range_and_ker_of_torDimensionLE_one, fix k and let 0 ⟶ τ_{≤k-1}(τ_{≤k}ℰ^•) ⟶ τ_{≤k}ℰ^• ⟶ Q ⟶ 0 be the short exact sequence of successive canonical truncations. Every term of each of its three rows is a finite locally free 𝒪_X-module.

The rows are ℰ^a → ⋯ → ℰ^{k-2} → Ker(d^{k-1}), ℰ^a → ⋯ → ℰ^{k-1} → Ker(d^k) and Im(d^{k-1}) → Ker(d^k), as displayed in the source. This short exact sequence represents the distinguished triangle τ_{≤k-1}E ⟶ τ_{≤k}E ⟶ H^k(E)[-k] ⟶ (τ_{≤k-1}E)[1], which is CochainComplex.nonempty_triangleOfSES_truncLE_iso.

public theorem isFiniteLocallyFree_truncLE_X_of_torDimensionLE_one
    (E : DerivedCategory X.Modules) (K : CochainComplex X.Modules ℤ)
    (e : DerivedCategory.Q.obj K ≅ E) (b : ℤ) [K.IsStrictlyLE b]
    (hterm : ∀ i : ℤ,
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (K.X i))
    (hH : ∀ i : ℤ,
      IsPerfect.{u, u, u + 1} ((DerivedCategory.singleFunctor X.Modules 0).obj
        ((DerivedCategory.homologyFunctor X.Modules i).obj E)) ∧
      HasTorAmplitude X.toRingedSpace ((DerivedCategory.singleFunctor X.Modules 0).obj
        ((DerivedCategory.homologyFunctor X.Modules i).obj E)) (-1) 0)
    (k i : ℤ) :
    Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf)
        (((K.truncLE k).shortComplexTruncLE (k - 1)).X₁.X i) ∧
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf)
        (((K.truncLE k).shortComplexTruncLE (k - 1)).X₂.X i) ∧
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf)
        (((K.truncLE k).shortComplexTruncLE (k - 1)).X₃.X i)

Sources

LeanAlgebraicGeometry.fittingIdealSheaf · AlgebraicGeometry.ideal_fittingIdealSheaf_le · AlgebraicGeometry.fittingIdealSheafOfDerivedModels_isFiniteType_and_ideal_eq_minorIdeal · AlgebraicGeometry.ComplexAndDivisorSituation.isAdmissibleBlowup_fittingIdealProdOfRanks · AlgebraicGeometry.ComplexAndDivisorSituation.isEffectiveCartierDivisor_comap_fittingIdealOfRanks · AlgebraicGeometry.exists_admissibleBlowup_forall_isHomologyPerfectTorLEOne · AlgebraicGeometry.exists_nonempty_open_admissibleBlowup_forall_isHomologyPerfectTorLEOne · CochainComplex.nonempty_truncLE_truncLE_iso

Section38.41 Blowing up perfect modules #

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

Tag 0ESS, a lemma

Tag 0ESS in the Stacks Project.

AlgebraicGeometry.isIso_derivedPullbackComparison_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/PerfectPullback.lean, line 618. The attribute's comment: “derived pullback agrees with ordinary pullback”.

Stacks 0ESS, the derived pullback. For an 𝒪_X-module of Tor dimension at most one the canonical comparison Lb^*ℱ ⟶ b^*ℱ along the blowup of X in a quasi-coherent ideal is invertible.

A two-term flat resolution of ℱ exists by Stacks 08CI; it is K-flat by Stacks 06YQ, so the comparison is invertible on it by Stacks 06YJ, and its degreewise pullback is again a resolution of b^*ℱ because pullback to the blowup keeps the injection of its first term injective.

theorem isIso_derivedPullbackComparison_blowUpToBase (F : OXMod.{u, u} X.toRingedSpace)
    (htor : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
    IsIso ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullbackComparison
      (blowUpToBase I).toLRSHom.toShHom).app
      ((HomotopyCategory.quotient (OXMod.{u, u} X.toRingedSpace) (.up ℤ)).obj
        ((CochainComplex.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F)))

AlgebraicGeometry.derivedPullbackBlowUpToBaseIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/PerfectPullback.lean, line 667. The attribute's comment: “derived pullback is the ordinary pullback”.

Stacks 0ESS, the identification Lb^*ℱ = b^*ℱ. For an 𝒪_X-module of Tor dimension at most one, the derived pullback to the blowup of X in a quasi-coherent ideal is the ordinary pullback, placed in degree 0.

noncomputable def derivedPullbackBlowUpToBaseIso (F : OXMod.{u, u} X.toRingedSpace)
    (htor : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
    (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (blowUpToBase I).toLRSHom.toShHom).obj
        ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) ≅
      (DerivedCategory.singleFunctor (OXMod.{u, u} (blowUp I).toRingedSpace) 0).obj
        ((modulePullback (blowUpToBase I).toLRSHom.toShHom).obj F)

AlgebraicGeometry.isPerfect_modulePullback_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/PerfectPullback.lean, line 698. The attribute's comment: “the ordinary pullback is perfect”.

Stacks 0ESS, perfectness. The ordinary pullback of a perfect 𝒪_X-module of Tor dimension at most one to a blowup is perfect.

theorem isPerfect_modulePullback_blowUpToBase (F : OXMod.{u, u} X.toRingedSpace)
    (hperfect : Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, u + 1}
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F))
    (htor : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
    Stacks.Cohomology.PerfectComplexes.IsPerfect.{u, u, u + 1}
      ((DerivedCategory.singleFunctor (OXMod.{u, u} (blowUp I).toRingedSpace) 0).obj
        ((modulePullback (blowUpToBase I).toLRSHom.toShHom).obj F))

AlgebraicGeometry.hasTorAmplitude_modulePullback_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/PerfectPullback.lean, line 714. The attribute's comment: “the ordinary pullback has Tor dimension at most one”.

Stacks 0ESS, Tor dimension. The ordinary pullback to a blowup of an 𝒪_X-module of Tor dimension at most one again has Tor dimension at most one.

theorem hasTorAmplitude_modulePullback_blowUpToBase (F : OXMod.{u, u} X.toRingedSpace)
    (htor : Stacks.Cohomology.TorAmplitude.HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude (blowUp I).toRingedSpace
      ((DerivedCategory.singleFunctor (OXMod.{u, u} (blowUp I).toRingedSpace) 0).obj
        ((modulePullback (blowUpToBase I).toLRSHom.toShHom).obj F)) (-1) 0

Tag 0EST, a lemma

Tag 0EST in the Stacks Project.

AlgebraicGeometry.exists_isAdmissibleBlowup_shortExact_strictTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingNormalForm.lean, line 541.

Stacks Project, Tag 0EST. Let ℱ be a perfect 𝒪_X-module of Tor dimension at most one which is finite locally free of constant rank r on a scheme-theoretically dense open U. Then there is a U-admissible blowup b : X' ⟶ X and a short exact sequence

0 ⟶ 𝒦 ⟶ b^*ℱ ⟶ 𝒬 ⟶ 0

with 𝒬 finite locally free of rank r and 𝒦 finitely presented, perfect, of Tor dimension at most one, and zero over U.

The witnesses are canonical: X' is the base change along the identity of X of the blowup of the r-th Fitting ideal of ℱ, 𝒬 is the strict transform of ℱ and 𝒦 is the kernel of the canonical surjection onto it. The finite presentation of ℱ, which the Fitting ideals need, is not assumed: it follows from perfectness (AlgebraicGeometry.isFinitePresentation_of_isPerfect_single).

theorem exists_isAdmissibleBlowup_shortExact_strictTransform
    (U : X.Opens) (hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
    (hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback U.ι).obj F) r)
    (hperfect : IsPerfect.{u, u, u + 1}
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F))
    (htor : HasTorAmplitude X.toRingedSpace
      ((DerivedCategory.singleFunctor (OXMod.{u, u} X.toRingedSpace) 0).obj F) (-1) 0) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X), Stacks.Blowup.IsAdmissibleBlowup U b ∧
      ∃ (K Q : X'.Modules) (i : K ⟶ (Scheme.Modules.pullback b).obj F)
        (p : (Scheme.Modules.pullback b).obj F ⟶ Q) (w : i ≫ p = 0),
        (ShortComplex.mk i p w).ShortExact ∧
          SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} Q r ∧
            K.IsFinitePresentation ∧
              IsPerfect.{u, u, u + 1}
                ((DerivedCategory.singleFunctor (OXMod.{u, u} X'.toRingedSpace) 0).obj K) ∧
                HasTorAmplitude X'.toRingedSpace
                  ((DerivedCategory.singleFunctor (OXMod.{u, u} X'.toRingedSpace) 0).obj K)
                  (-1) 0 ∧
                IsZero ((Scheme.Modules.pullback (b ⁻¹ᵁ U).ι).obj K)

Tag 0ESU, a lemma

Tag 0ESU in the Stacks Project.

AlgebraicGeometry.isAdmissibleBlowup_blowUpToBase_fittingIdealProd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingProduct.lean, line 193. The attribute's comment: “the U-admissible blowup, in the product of the Fitting ideals up to N”.

Stacks Project, Tag 0ESU, the blowup. For a finitely presented 𝒪_X-module vanishing on an open U, the blowup of X in the product of the Fitting ideals of index at most N is a U-admissible blowup: that product is of finite type and supported away from U.

theorem isAdmissibleBlowup_blowUpToBase_fittingIdealProd [F.IsFinitePresentation] (U : X.Opens)
    (hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback U.ι).obj F) 0) (N : ℕ) :
    Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase (fittingIdealProd F N))

AlgebraicGeometry.isEffectiveCartierDivisor_fittingIdeal_pullback_fittingIdealProd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingProduct.lean, line 226. The attribute's comment: “the Fitting ideals of index at most N become effective Cartier divisors”.

Stacks Project, Tag 0ESU, the effective Cartier divisors. On the blowup of X in the product of the Fitting ideals of index at most N, the k-th Fitting ideal of the pulled back module is an effective Cartier divisor for every k ≤ N.

The inverse image of the whole product is the exceptional divisor of the blowup, hence an effective Cartier divisor by tag 02OS, and each factor of it is one by tag 07ZV; the k-th Fitting ideal of the pullback is the inverse image of the k-th Fitting ideal by tag 0C3D.

theorem isEffectiveCartierDivisor_fittingIdeal_pullback_fittingIdealProd
    [F.IsFinitePresentation] (N : ℕ) {k : ℕ} (hk : k ≤ N) :
    Stacks.Divisors.IsEffectiveCartierDivisor
      (fittingIdeal ((Scheme.Modules.pullback (blowUpToBase (fittingIdealProd F N))).obj F)
        (k : ℤ))

AlgebraicGeometry.isAdmissibleBlowup_blowUpToBase_fittingIdealProdAll, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingProductAll.lean, line 272. The attribute's comment: “the U-admissible blowup, in the product of all the Fitting ideals”.

For a finitely presented 𝒪_X-module vanishing on an open U, the blowup of X in the product of all the Fitting ideals is a U-admissible blowup: that product is of finite type and supported away from U.

theorem isAdmissibleBlowup_blowUpToBase_fittingIdealProdAll [F.IsFinitePresentation]
    (U : X.Opens)
    (hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback U.ι).obj F) 0) :
    Stacks.Blowup.IsAdmissibleBlowup U (blowUpToBase (fittingIdealProdAll F))

AlgebraicGeometry.isEffectiveCartierDivisor_fittingIdeal_pullback_fittingIdealProdAll, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingProductAll.lean, line 321. The attribute's comment: “every Fitting ideal becomes an effective Cartier divisor on the blowup”.

On the blowup of X in the product of all the Fitting ideals, the k-th Fitting ideal of the pulled back module is an effective Cartier divisor for every k ≥ 0.

theorem isEffectiveCartierDivisor_fittingIdeal_pullback_fittingIdealProdAll
    [F.IsFinitePresentation] (k : ℕ) :
    Stacks.Divisors.IsEffectiveCartierDivisor
      (fittingIdeal ((Scheme.Modules.pullback (blowUpToBase (fittingIdealProdAll F))).obj F)
        (k : ℤ))

AlgebraicGeometry.exists_isAdmissibleBlowup_isEffectiveCartierDivisor_fittingIdeal_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/Transform/FittingProductAll.lean, line 336. The attribute's comment: “the U-admissible blowup making every Fitting ideal effective Cartier, for ℱ|_U = 0”.

For a finitely presented 𝒪_X-module ℱ with ℱ|_U = 0 there is a U-admissible blowup b : X' → X on which every Fitting ideal of b^*ℱ is an effective Cartier divisor.

theorem exists_isAdmissibleBlowup_isEffectiveCartierDivisor_fittingIdeal_pullback
    [F.IsFinitePresentation] (U : X.Opens)
    (hzero : CategoryTheory.Limits.IsZero ((Scheme.Modules.pullback U.ι).obj F)) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X), Stacks.Blowup.IsAdmissibleBlowup U b ∧
      ∀ k : ℕ, Stacks.Divisors.IsEffectiveCartierDivisor
        (fittingIdeal ((Scheme.Modules.pullback b).obj F) (k : ℤ))

AlgebraicGeometry.exists_isAdmissibleBlowup_canonicalFiltrations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DivisorSum/CanonicalFiltrations.lean, line 94. The attribute's comment: “the blowup, the divisors, both canonical filtrations and every graded piece's rank”.

Stacks Project, Tag 0ESU. Let ℱ be an 𝒪_X-module of finite presentation vanishing on an open U ⊆ X. Then there is a U-admissible blowup b : X' → X and a locally finite family of effective Cartier divisors D_j on X' such that the pullback b^*ℱ has two locally finite filtrations
0 = F⁰ ⊆ F¹ ⊆ ⋯ ⊆ b^*ℱ        and        b^*ℱ = F₁ ⊇ F₂ ⊇ ⋯ ⊇ 0
— the global subsheaves AlgebraicGeometry.fittingIncr and AlgebraicGeometry.fittingDecr of the family — whose graded pieces are, on the divisor D i, the direct images of modules finite locally free of rank i + 1 there. Both filtrations are invariant under every automorphism of b^*ℱ, and around every point an affine open with local equations e_1, …, e_N for the divisors describes them as the multiples of e_{i+1} ⋯ e_N and the sections killed by e_{i+1} ⋯ e_N.

Finite presentation is more general than the source's hypothesis that ℱ be perfect of Tor dimension at most one: a perfect module of Tor dimension at most one is of finite presentation, and the conclusion here is the source's for every module of finite presentation.

In the indexing of this directory D j is the source's D_{j+1}, so the rank i + 1 on D i is the source's rank i on D_i.

theorem exists_isAdmissibleBlowup_canonicalFiltrations [F.IsFinitePresentation] (U : X.Opens)
    (hzero : IsZero ((Scheme.Modules.pullback U.ι).obj F)) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X) (_ : Stacks.Blowup.IsAdmissibleBlowup U b)
      (_ : ((Scheme.Modules.pullback b).obj F).IsQuasicoherent)
      (D : ℕ → X'.IdealSheafData),
      (∀ j, IsEffectiveCartierDivisor (D j)) ∧
      IsLocallyFiniteFamily D ∧
      (∀ x : X', ∃ V : X'.Opens, x ∈ (V : Set X') ∧ ∃ m : ℕ, ∀ n ≥ m,
        Disjoint (V : Set X') ((D n).support : Set X')) ∧
      (∀ k : ℕ, fittingIdeal ((Scheme.Modules.pullback b).obj F) (k : ℤ) =
        locallyFiniteSum D fun j => (j + 1) - k) ∧
      Monotone (fittingIncr D ((Scheme.Modules.pullback b).obj F)) ∧
      Antitone (fittingDecr D ((Scheme.Modules.pullback b).obj F)) ∧
      fittingIncr D ((Scheme.Modules.pullback b).obj F) 0 = ⊥ ∧
      fittingDecr D ((Scheme.Modules.pullback b).obj F) 1 = ⊤ ∧
      (∀ x : X', ∃ V : X'.Opens, x ∈ (V : Set X') ∧ ∃ m : ℕ, ∀ n ≥ m,
        IsZero ((Scheme.Modules.pullback V.ι).obj (cokernel (C := X'.Modules)
          (fittingIncr D ((Scheme.Modules.pullback b).obj F) n).ι))) ∧
      (∀ x : X', ∃ V : X'.Opens, x ∈ (V : Set X') ∧ ∃ m : ℕ, ∀ n ≥ m,
        IsZero ((Scheme.Modules.pullback V.ι).obj
          (fittingDecr D ((Scheme.Modules.pullback b).obj F) n).asModules)) ∧
      (∀ (i : ℕ) (hle : fittingIncr D ((Scheme.Modules.pullback b).obj F) i ≤
          fittingIncr D ((Scheme.Modules.pullback b).obj F) (i + 1)),
        ∃ G : (D i).subscheme.Modules,
          SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} G (i + 1) ∧
          Nonempty (submoduleGraded hle ≅
            (Scheme.Modules.pushforward (D i).subschemeι).obj G)) ∧
      (∀ (i : ℕ) (hle : fittingDecr D ((Scheme.Modules.pullback b).obj F) (i + 2) ≤
          fittingDecr D ((Scheme.Modules.pullback b).obj F) (i + 1)),
        ∃ G : (D i).subscheme.Modules,
          SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} G (i + 1) ∧
          Nonempty (submoduleGraded hle ≅
            (Scheme.Modules.pushforward (D i).subschemeι).obj G)) ∧
      (∀ (e : (Scheme.Modules.pullback b).obj F ≅ (Scheme.Modules.pullback b).obj F) (i : ℕ),
        Scheme.Modules.rangeSubmodule
            ((fittingIncr D ((Scheme.Modules.pullback b).obj F) i).ιModules ≫ e.hom) =
          fittingIncr D ((Scheme.Modules.pullback b).obj F) i) ∧
      (∀ (e : (Scheme.Modules.pullback b).obj F ≅ (Scheme.Modules.pullback b).obj F) (i : ℕ),
        Scheme.Modules.rangeSubmodule
            ((fittingDecr D ((Scheme.Modules.pullback b).obj F) i).ιModules ≫ e.hom) =
          fittingDecr D ((Scheme.Modules.pullback b).obj F) i) ∧
      ∀ x : X', ∃ V : X'.affineOpens, x ∈ (V.1 : Set X') ∧
        ∃ (N : ℕ) (e : ℕ → Γ(X', V.1)),
          (∀ j, j + 1 ≤ N → (D j).ideal V = Ideal.span {e (j + 1)}) ∧
          (∀ j, N ≤ j → (D j).ideal V = ⊤) ∧
          (∀ j, e j ∈ nonZeroDivisors Γ(X', V.1)) ∧
          (∀ j, N < j → IsUnit (e j)) ∧
          (∀ k : ℕ, (fittingIdeal ((Scheme.Modules.pullback b).obj F) (k : ℤ)).ideal V =
            ∏ j ∈ Finset.Icc (k + 1) N, Ideal.span {e j} ^ (j - k)) ∧
          (∀ (i : ℕ) (s : Γ((Scheme.Modules.pullback b).obj F, V.1)),
            s ∈ (fittingIncr D ((Scheme.Modules.pullback b).obj F) i).toSubmodule.obj (op V.1) ↔
              ∃ t : Γ((Scheme.Modules.pullback b).obj F, V.1),
                (∏ j ∈ Finset.Icc (i + 1) N, e j) • t = s) ∧
          (∀ (i : ℕ) (s : Γ((Scheme.Modules.pullback b).obj F, V.1)),
            s ∈ (fittingDecr D ((Scheme.Modules.pullback b).obj F)
                (i + 1)).toSubmodule.obj (op V.1) ↔
              (∏ j ∈ Finset.Icc (i + 1) N, e j) • s = 0)

Stacks.Divisors.isEffectiveCartierDivisor_locallyFiniteSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DivisorSum/LocallyFinite.lean, line 176. The attribute's comment: “the locally finite sum E_k = D_{k+1} + 2D_{k+2} + ⋯ is effective Cartier”. References: EGA IV (21.2.7), “partial”.

The sum of a locally finite family of effective Cartier divisors is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_locallyFiniteSum {ι : Type*} {D : ι → X.IdealSheafData}
    (hD : IsLocallyFiniteFamily D) (hcart : ∀ i, IsEffectiveCartierDivisor (D i)) (n : ι → ℕ) :
    IsEffectiveCartierDivisor (locallyFiniteSum D n)

fittingIdeal_quotient_span_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/ScaledPresentation.lean, line 151. The attribute's comment: “the Fitting ideals of a presentation matrix divided by f”.

Stacks Project, Tag 0ESU, the Fitting ideals of a scaled presentation. If A = f • B is an n-row presentation matrix of 𝓕 and B presents 𝓕', then Fit_k(𝓕) = (f)^{n-k} Fit_k(𝓕').

theorem fittingIdeal_quotient_span_smul {n : ℕ} {J : Type*} (B : Matrix (Fin n) J R) (f : R)
    (k : ℕ) :
    fittingIdeal (M := (Fin n → R) ⧸ (f • B).columnSpan) (k : ℤ) =
      Ideal.span {f} ^ (n - k) * fittingIdeal (M := (Fin n → R) ⧸ B.columnSpan) (k : ℤ)

Stacks.ScaledPresentation.fittingIdeal_cokernel_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/ScaledPresentation.lean, line 406. The attribute's comment: “the Fitting ideals of a square presentation matrix divided by f”.

Stacks Project, Tag 0ESU, the Fitting ideals of a square presentation matrix divided by f: if 𝓕 is presented by f • B and 𝓕' by B, then Fit_k(𝓕) = (f)^{n-k} Fit_k(𝓕').

theorem fittingIdeal_cokernel_smul (k : ℕ) :
    fittingIdeal (M := Cokernel (f • B)) (k : ℤ) =
      Ideal.span {f} ^ (n - k) * fittingIdeal (M := Cokernel B) (k : ℤ)

Stacks.ScaledPresentation.shortExact_ofFree_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/ScaledPresentation.lean, line 425. The attribute's comment: “the canonical sequence 0 → 𝒪_{D_n}^{⊕n} → ℱ → ℱ' → 0 of a local presentation”.

Stacks Project, Tag 0ESU, the first canonical short exact sequence of a local presentation. For A = f • B with B injective, writing 𝓕 = Rⁿ / A Rⁿ and 𝓕' = Rⁿ / B Rⁿ, the sequence
0 → (R ⧸ (f))ⁿ → 𝓕 → 𝓕' → 0
is exact, and when f is a nonzerodivisor its submodule is Ker(f : 𝓕 → 𝓕), which is what makes the sequence canonical. Here R ⧸ (f) is the structure sheaf of the effective Cartier divisor cut out by f.

theorem shortExact_ofFree_toBase (hf : f ∈ nonZeroDivisors R)
    (hB : Function.Injective B.mulVecLin) :
    Function.Injective (ofFree B f) ∧
      LinearMap.range (ofFree B f) = LinearMap.ker (toBase B f) ∧
      Function.Surjective (toBase B f) ∧
      LinearMap.range (ofFree B f) = LinearMap.ker (LinearMap.lsmul R (Cokernel (f • B)) f)

Stacks.ScaledPresentation.shortExact_ofBase_toFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/ScaledPresentation.lean, line 443. The attribute's comment: “the canonical sequence 0 → ℱ' → ℱ → 𝒪_{D_n}^{⊕n} → 0 of a local presentation”.

Stacks Project, Tag 0ESU, the second canonical short exact sequence of a local presentation. For A = f • B with f a nonzerodivisor, writing 𝓕 = Rⁿ / A Rⁿ and 𝓕' = Rⁿ / B Rⁿ, the sequence
0 → 𝓕' → 𝓕 → (R ⧸ (f))ⁿ → 0
is exact, and its submodule is the image of multiplication by f on 𝓕, so that its quotient is Coker(f : 𝓕 → 𝓕); this is what makes the sequence canonical.

theorem shortExact_ofBase_toFree (hf : f ∈ nonZeroDivisors R) :
    Function.Injective (ofBase B f) ∧
      LinearMap.range (ofBase B f) = LinearMap.ker (toFree B f) ∧
      Function.Surjective (toFree B f) ∧
      LinearMap.range (ofBase B f) = LinearMap.range (LinearMap.lsmul R (Cokernel (f • B)) f)

Stacks.ScaledPresentation.exists_eq_smul_and_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/ScaledPresentation.lean, line 496. The attribute's comment: “the local step: a principal Fit_{n-1} gives A = f A' and the two sequences”.

Stacks Project, Tag 0ESU, the local step of the induction. Let 𝓕 = R^{n} / A R^{n} be presented by a square matrix A with n = m + 1 rows, with A injective, and suppose Fit_{n-1}(𝓕) is generated by a nonzerodivisor f. Then A = f A' for a square matrix A' which is again injective, so that 𝓕' = R^{n} / A' R^{n} is presented by an exact sequence of the same shape, and 𝓕 sits in the two canonical short exact sequences
0 → (R ⧸ (f))ⁿ → 𝓕 → 𝓕' → 0    and    0 → 𝓕' → 𝓕 → (R ⧸ (f))ⁿ → 0
whose free term is the structure sheaf of the divisor cut out by f — the divisor D_n of the source — and whose submodule and quotient are Ker(f : 𝓕 → 𝓕) and Coker(f : 𝓕 → 𝓕).

theorem exists_eq_smul_and_shortExact {m : ℕ}
    (A : Matrix (Fin (m + 1)) (Fin (m + 1)) R) (hf : f ∈ nonZeroDivisors R)
    (hA : Function.Injective A.mulVecLin)
    (hfit : fittingIdeal (M := Cokernel A) (m : ℤ) = Ideal.span {f}) :
    ∃ A' : Matrix (Fin (m + 1)) (Fin (m + 1)) R, A = f • A' ∧
      Function.Injective A'.mulVecLin ∧
      (Function.Injective (ofFree A' f) ∧
        LinearMap.range (ofFree A' f) = LinearMap.ker (toBase A' f) ∧
        Function.Surjective (toBase A' f) ∧
        LinearMap.range (ofFree A' f) =
          LinearMap.ker (LinearMap.lsmul R (Cokernel (f • A')) f)) ∧
      (Function.Injective (ofBase A' f) ∧
        LinearMap.range (ofBase A' f) = LinearMap.ker (toFree A' f) ∧
        Function.Surjective (toFree A' f) ∧
        LinearMap.range (ofBase A' f) =
          LinearMap.range (LinearMap.lsmul R (Cokernel (f • A')) f))

Stacks.ScaledPresentation.fittingIdeal_cokernel_eq_top_of_fittingIdeal_smul_eq_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/ScaledPresentation.lean, line 541. The attribute's comment: “the entries of A' generate the unit ideal”.

Stacks Project, Tag 0ESU: the entries of A' generate the unit ideal. If 𝓕 is presented by A = f A' with A' square of size n = m + 1 and Fit_{n-1}(𝓕) is generated by the nonzerodivisor f, then Fit_{n-1}(𝓕') = R for 𝓕' = R^{n} / A' R^{n}: the scaling identity gives (f) = (f) · Fit_{n-1}(𝓕'), and f cancels. Since Fit_{n-1}(𝓕') is the ideal of 1 × 1 minors of A', this says the entries of A' generate the unit ideal, which is the hypothesis under which the source invokes Algebra, Lemma 10.102.2 (tag 00MT) to drop the number of generators by one.

theorem fittingIdeal_cokernel_eq_top_of_fittingIdeal_smul_eq_span_singleton {m : ℕ}
    (A' : Matrix (Fin (m + 1)) (Fin (m + 1)) R) (hf : f ∈ nonZeroDivisors R)
    (hfit : fittingIdeal (M := Cokernel (f • A')) (m : ℤ) = Ideal.span {f}) :
    fittingIdeal (R := R) (M := Cokernel A') (m : ℤ) = ⊤

Stacks.ScaledPresentation.exists_cokernel_equiv_of_isUnit_entry, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/UnitEntryDescent.lean, line 225. The attribute's comment: “dropping a generator: a unit relation entry gives a smaller presentation”.

If some entry of a square matrix A of size n = m + 1 is a unit, then the module Rⁿ / A Rⁿ presented by A is the module presented by a square matrix of size m, which is again injective if A is.

theorem exists_cokernel_equiv_of_isUnit_entry {m : ℕ}
    (A : Matrix (Fin (m + 1)) (Fin (m + 1)) R) (a b : Fin (m + 1)) (hu : IsUnit (A a b)) :
    ∃ ψ : Matrix (Fin m) (Fin m) R,
      Nonempty (Cokernel A ≃ₗ[R] Cokernel ψ) ∧
        (Function.Injective A.mulVecLin → Function.Injective ψ.mulVecLin)

Stacks.ScaledPresentation.exists_cover_cokernel_equiv_of_fittingIdeal_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Fitting/UnitEntryDescent.lean, line 281. The attribute's comment: “the Zariski cover on which ℱ' needs only n-1 generators”.

Let 𝓕 be presented by a square matrix A of size n = m + 1 with Fit_{n-1}(𝓕) = R. Then the entries of A generate the unit ideal — so the basic opens D(A i j) cover Spec R — and over each of those basic opens the module presented by A is the cokernel of a square matrix of size m, and hence is generated by m = n - 1 elements.

theorem exists_cover_cokernel_equiv_of_fittingIdeal_eq_top {m : ℕ}
    (A : Matrix (Fin (m + 1)) (Fin (m + 1)) R)
    (hfit : fittingIdeal (R := R) (M := Cokernel A) (m : ℤ) = ⊤) :
    Ideal.span (Set.range fun p : Fin (m + 1) × Fin (m + 1) => A p.1 p.2) = ⊤ ∧
      ∀ p : Fin (m + 1) × Fin (m + 1),
        ∃ ψ : Matrix (Fin m) (Fin m) (Localization.Away (A p.1 p.2)),
          Nonempty (Cokernel (A.map (algebraMap R (Localization.Away (A p.1 p.2)))) ≃ₗ[
              Localization.Away (A p.1 p.2)] Cokernel ψ) ∧
            ∃ s : Fin m → Cokernel (A.map (algebraMap R (Localization.Away (A p.1 p.2)))),
              Submodule.span (Localization.Away (A p.1 p.2)) (Set.range s) = ⊤

Tag 0ESV, a lemma

Tag 0ESV in the Stacks Project.

AlgebraicGeometry.exists_admissibleBlowup_isPerfectTorLEOne_ker_im_coker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/PerfectHomomorphismFittingBlowup.lean, line 164. The attribute's comment: “the U-admissible blowup after which the kernel, image and cokernel of the pullback of φ are perfect of Tor dimension ≤ 1”.

Stacks Project, Tag 0ESV. Let X be a scheme and φ : ℱ ⟶ 𝒢 a homomorphism of perfect 𝒪_X-modules of Tor dimension at most one. Let U ⊆ X be a scheme-theoretically dense open with ℱ|_U = 0 and 𝒢|_U = 0. Then there is a U-admissible blowup b : X' ⟶ X such that the kernel, the image and the cokernel of b^*φ are perfect 𝒪_{X'}-modules of Tor dimension at most one.

The blowup is the blowup of X in the zeroth Fitting ideal of Coker(φ). That cokernel is finitely presented: it is the H^0 of the cone E of φ[0] — the source's object (ℱ ⟶ 𝒢) of D(𝒪_X), which is perfect by tag 08CR and hence pseudo-coherent — and E has no cohomology in positive degrees, so tag 08DN (2) applies. It vanishes over U because ℱ and 𝒢 do and pullback is right exact, hence is finite locally free of rank 0 there. Tag 0ESN (1) therefore makes the blowup U-admissible and tag 0ESN (4) makes b^*Coker(φ) perfect of Tor dimension at most one; right exactness of pullback identifies that module with the cokernel of b^*φ. The pullbacks b^*ℱ and b^*𝒢 are perfect of Tor dimension at most one by tag 0ESS, after which the image — the source's "kernel of the cokernel" — and then the kernel are AlgebraicGeometry.isPerfectTorLEOne_abelianImage_of_cokernel and AlgebraicGeometry.isPerfectTorLEOne_kernel.

theorem exists_admissibleBlowup_isPerfectTorLEOne_ker_im_coker {X : Scheme.{u}}
    (F G : OXMod.{u, u} X.toRingedSpace) (φ : F ⟶ G)
    (hF : IsPerfectTorLEOne X F) (hG : IsPerfectTorLEOne X G)
    (U : X.Opens) (hU : Scheme.Opens.IsSchemeTheoreticallyDense U)
    (_hFU : IsZero ((modulePullback U.ι.toLRSHom.toShHom).obj F))
    (hGU : IsZero ((modulePullback U.ι.toLRSHom.toShHom).obj G)) :
    ∃ (X' : Scheme.{u}) (b : X' ⟶ X), Stacks.Blowup.IsAdmissibleBlowup U b ∧
      IsPerfectTorLEOne X' (kernel ((modulePullback b.toLRSHom.toShHom).map φ)) ∧
      IsPerfectTorLEOne X' (Abelian.image ((modulePullback b.toLRSHom.toShHom).map φ)) ∧
      IsPerfectTorLEOne X' (cokernel ((modulePullback b.toLRSHom.toShHom).map φ))

Sources

LeanAlgebraicGeometry.isIso_derivedPullbackComparison_blowUpToBase · AlgebraicGeometry.derivedPullbackBlowUpToBaseIso · AlgebraicGeometry.isPerfect_modulePullback_blowUpToBase · AlgebraicGeometry.hasTorAmplitude_modulePullback_blowUpToBase · AlgebraicGeometry.exists_isAdmissibleBlowup_shortExact_strictTransform · AlgebraicGeometry.isAdmissibleBlowup_blowUpToBase_fittingIdealProd · AlgebraicGeometry.isEffectiveCartierDivisor_fittingIdeal_pullback_fittingIdealProd · AlgebraicGeometry.isAdmissibleBlowup_blowUpToBase_fittingIdealProdAll

Section38.42 An operator introduced by Berthelot and Ogus #

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

Tag 0F8M, a lemma

Tag 0F8M in the Stacks Project.

Stacks.Divisors.Eta.etaSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EtaAffineComparison.lean, line 863. The attribute's comment: “the affine comparison of eta complexes”.

[Stacks, Tag 0F8M], second assertion. Let Y be a scheme, let D ⊆ Y be an effective Cartier divisor with ideal sheaf I ⊆ 𝒪_Y, and let F^• be a complex of quasi-coherent 𝒪_Y-modules whose terms are I-torsion free. If U ⊆ Y is affine open and D ∩ U = V(f), then η_f(F^•(U)) is canonically isomorphic to (η_I F^•)(U).

noncomputable def etaSectionsIso (D : Y.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor D]
    (F : CochainComplex (SheafOfModules.{u} Oᵧ) ℤ)
    (_hqc : ∀ n : ℤ, (F.X n).IsQuasicoherent)
    (htf : ∀ n : ℤ,
      Stacks.IdealTorsion.IsIdealTorsionFree Y.toRingedSpace (idealSheafι D) (F.X n))
    (U : Y.Opens) (_hU : IsAffineOpen U)
    (g : (idealSheaf D).val.obj (op U))
    (hg : Stacks.IdealTorsion.GeneratesIdealOn Y.toRingedSpace U g) :
    EtaComplex.etaObject
        (Stacks.IdealTorsion.Eta.generatorSection Y.toRingedSpace (idealSheafι D) U g)
        (Stacks.IdealTorsion.Eta.sectionsComplex Y.toRingedSpace F U) ≅
      Stacks.IdealTorsion.Eta.sectionsComplex Y.toRingedSpace
        (etaObj Y.toRingedSpace (idealSheaf D) (idealSheafι D) F htf) U

Stacks.Divisors.Eta.isQuasicoherent_etaObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EtaQuasicoherent.lean, line 245. The attribute's comment: “eta is a complex of quasi-coherent modules”.

[Stacks, Tag 0F8M], first assertion. Let X be a scheme, let D ⊆ X be an effective Cartier divisor with ideal sheaf I ⊆ 𝒪_X, and let F^• be a complex of quasi-coherent 𝒪_X-modules whose terms are I-torsion free. Then η_I F^• is a complex of quasi-coherent 𝒪_X-modules.

theorem isQuasicoherent_etaObj (D : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor D] (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hqc : ∀ n : ℤ, (F.X n).IsQuasicoherent)
    (htf : ∀ n : ℤ,
      Stacks.IdealTorsion.IsIdealTorsionFree X.toRingedSpace (idealSheafι D) (F.X n))
    (n : ℤ) :
    ((etaObj X.toRingedSpace (idealSheaf D) (idealSheafι D) F htf).X n).IsQuasicoherent

Tag 0GTV, a lemma

Tag 0GTV in the Stacks Project.

Stacks.Divisors.Eta.derivedEta_isQuasicoherent_and_affineComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EtaDerivedBerthelotOgus.lean, line 151.

[Stacks, Tag 0GTV]. Let X be a scheme and let D ⊆ X be an effective Cartier divisor with ideal sheaf I ⊆ 𝒪_X. The functor Lη_I : D(𝒪_X) ⥤ D(𝒪_X) of [Stacks, Tag 0F8Q] sends D_QCoh(𝒪_X) into itself: if every cohomology sheaf H^n(K) of K is quasi-coherent, so is every cohomology sheaf of Lη_I K. Moreover, if X = Spec(A) is affine and D = V(f) — the ideal of D in A = Γ(X, 𝒪_X) is generated by f — then the functor Lη_f on D(A) of [Stacks, Tag 0F7R] and the functor Lη_I correspond via the equivalence (-)^~ : D(A) ≌ D_QCoh(𝒪_X) of [Stacks, Tag 06Z0]: (-)^~ ⋙ Lη_I ≅ Lη_f ⋙ (-)^~.

The functor Lη_f is defined because f is a nonzerodivisor, which follows from the hypotheses (Stacks.Divisors.Eta.mem_nonZeroDivisors_of_ideal_top_eq_span).

theorem derivedEta_isQuasicoherent_and_affineComparison :
    (∀ (X : Scheme.{u}) (D : X.IdealSheafData) [Stacks.Divisors.IsEffectiveCartierDivisor D]
        (K : DerivedCategory X.Modules),
        (∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) →
          ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj
            ((derivedEtaData D).functor.obj K)).IsQuasicoherent) ∧
      ∀ (R : CommRingCat.{u}) (D : (Spec R).IdealSheafData)
        [Stacks.Divisors.IsEffectiveCartierDivisor D] (f : GammaTop R)
        (hf : D.ideal ⟨⊤, isAffineOpen_top (Spec R)⟩ = Ideal.span {f}),
        Nonempty (derivedTildeGamma R ⋙ (derivedEtaData D).functor ≅
          Stacks.Eta.DerivedDescent.moduleDerivedEta f
              (mem_nonZeroDivisors_of_ideal_top_eq_span R D hf) ⋙
            derivedTildeGamma R)

AlgebraicGeometry.ComplexAndDivisorSituation.chartDecalage_of_derivedEta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/BlowUpSquare/ChartDecalageExistence.lean, line 395. The attribute's comment: “the second assertion, on an affine chart with principal determinantal ideals”.

The derived décalage of a triple on its affine charts with principal determinantal ideals, for every triple (X, D, M) and every derived décalage Lη_I of its divisor: on such a chart (U, A, f, M^•) the restriction of Lη_I M to U is the complex of 𝒪_U-modules associated with η_f M^•, as a roof of quasi-isomorphisms. The comparison is AlgebraicGeometry.ComplexAndDivisorSituation.AffineChart.nonempty_restrictModules_derivedEta_iso, which holds on every affine chart. For the derived décalage Stacks.Divisors.Eta.derivedEtaData of a triple at the standard model this is AlgebraicGeometry.ComplexAndDivisorSituation.chartDecalage.

theorem chartDecalage_of_derivedEta (S : ComplexAndDivisorSituation.{u, d})
    (E : Stacks.Divisors.Eta.DerivedEta S.D) : ChartDecalage S E

Sources

LeanStacks.Divisors.Eta.etaSectionsIso · Stacks.Divisors.Eta.isQuasicoherent_etaObj · Stacks.Divisors.Eta.derivedEta_isQuasicoherent_and_affineComparison · AlgebraicGeometry.ComplexAndDivisorSituation.chartDecalage_of_derivedEta

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

38.34 The h topology to 38.42 An operator introduced by…

Section38.34 The h topology#

Tag 0ETR, a lemma

Tag 0ETS, a definition

Tag 0ETT, a lemma

Tag 0H45, a lemma

Tag 0ETU, a lemma

Tag 0ETV, a lemma

Tag 0ETW, a lemma

Tag 0ETX, a lemma

Tag 0ETY, a lemma

Tag 0ETZ, a definition

Tag 0EUY, a definition

Tag 0EU0, a lemma

Tag 0EU1, a definition

Tag 0EU2, a lemma

Tag 0EU3, a lemma

Tag 0EU4, a lemma

Tag 0EU5, a lemma

Tag 0EU6, a lemma

Tag 0EU7, a lemma

Sources

Section38.35 More on the h topology#

Tag 0EV0, an example

Tag 0EV1, an example

Tag 0EV2, a lemma

Tag 0EV3, a lemma

Sources

Section38.36 Blow up squares and the ph topology#

Tag 0EV5, an equation

Tag 0EW1, a lemma

Tag 0EW2, a lemma

Sources

Section38.37 Almost blow up squares and the h topology#

Tag 0EV6, an equation

Tag 0EV7, a lemma

Tag 0EV8, a lemma

Tag 0EV9, a lemma

Tag 0EVA, a lemma

Tag 0EVB, a lemma

Tag 0EVC, a lemma

Tag 0EVD, a lemma

Tag 0EVE, a lemma

Tag 0EVF, a proposition

Tag 0EVG, an example

Tag 0EVH, an example

Tag 0EVI, a lemma

Tag 0EX9, a lemma

Sources

Section38.38 Absolute weak normalization and h coverings#

Tag 0EVJ, a lemma

Tag 0EVK, a lemma

Tag 0EVL, a lemma

Tag 0EVT, a lemma

Tag 0EVU, a lemma

Tag 0EVV, a lemma

Tag 0EVW, a lemma

Sources

Section38.39 Descent vector bundles in positive characteristic#

Tag 0EXA, the section

Tag 0EXB, a lemma

Tag 0EXC, a lemma

Tag 0EXD, a lemma

Tag 0EXE, a proposition

Tag 0EXF, a lemma

Tag 0EXG, a lemma

Tag 0EXH, a theorem

Sources

Section38.40 Blowing up complexes#

Tag 0ESP, a lemma

Tag 0ESQ, a lemma

Tag 0ESR, a lemma

Tag 0F8J, a remark

Sources

Section38.41 Blowing up perfect modules#

Tag 0ESS, a lemma

Tag 0EST, a lemma

Tag 0ESU, a lemma

Tag 0ESV, a lemma

Sources

Section38.34 The h topology #

Section38.35 More on the h topology #

Section38.36 Blow up squares and the ph topology #

Section38.37 Almost blow up squares and the h topology #

Section38.38 Absolute weak normalization and h coverings #

Section38.39 Descent vector bundles in positive characteristic #

Section38.40 Blowing up complexes #

Section38.41 Blowing up perfect modules #

Section38.42 An operator introduced by Berthelot and Ogus #