34.10 The V topology to 34.13 Extending functors

Section34.10 The V topology#

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

Tag 0ETB, a definition

Tag 0ETB in the Stacks Project.

AlgebraicGeometry.IsStandardVCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/StandardCoverings.lean, line 68.

A finite family of morphisms from affine schemes to an affine scheme is a standard V covering if every morphism from the spectrum of a valuation ring lifts to one member after an extension of valuation rings.

public def IsStandardVCovering {T : Scheme.{u}} [IsAffine T] {I : Type v} [Finite I]
    (X : I → Scheme.{u}) [∀ i, IsAffine (X i)] (f : ∀ i, X i ⟶ T) : Prop
Tag 0ETC, a lemma

Tag 0ETC in the Stacks Project.

AlgebraicGeometry.isStandardVCovering_of_flat_affineCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/StandardFpqcCoverings.lean, line 41.

A standard fpqc covering of an affine scheme is a standard V covering.

theorem isStandardVCovering_of_flat_affineCover
    {T : Scheme.{u}} [IsAffine T] (𝒰 : T.AffineCover.{v} @Flat) [Finite 𝒰.I₀] :
    AlgebraicGeometry.IsStandardVCovering (fun i ↦ Spec (𝒰.X i)) 𝒰.f
Tag 0ETD, a lemma

Tag 0ETD in the Stacks Project.

AlgebraicGeometry.StandardPHCovering.isStandardVCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/PhComparison.lean, line 50.

A standard ph covering is a standard V covering.

public theorem StandardPHCovering.isStandardVCovering
    {T : Scheme.{u}} [IsAffine T] {I : Type v} {X : I → Scheme.{u}}
    {f : ∀ i, X i ⟶ T} (hf : StandardPHCovering f) :
    @IsStandardVCovering T _ I hf.finite X hf.isAffine f
Tag 0ETE, a lemma

Tag 0ETE in the Stacks Project.

AlgebraicGeometry.isStandardVCovering_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/StandardCoverings.lean, line 91.

A standard V covering of an affine scheme remains a standard V covering after pullback along a morphism from another affine scheme.

public lemma isStandardVCovering_pullback
    {T T' : Scheme.{u}} [IsAffine T] [IsAffine T']
    {I : Type v} [Finite I] (X : I → Scheme.{u}) [∀ i, IsAffine (X i)]
    (f : ∀ i, X i ⟶ T) (g : T' ⟶ T)
    (hf : IsStandardVCovering X f) :
    IsStandardVCovering (fun i ↦ pullback (f i) g)
      (fun i ↦ pullback.snd (f i) g)
Tag 0ETF, a lemma

Tag 0ETF in the Stacks Project.

AlgebraicGeometry.IsStandardVCovering.comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/StandardCoverings.lean, line 107.

Composing a standard V covering with a standard V covering of each member gives a standard V covering.

public lemma IsStandardVCovering.comp
    {T : Scheme.{u}} [IsAffine T]
    {J : Type v} [Finite J] (X : J → Scheme.{u}) [∀ j, IsAffine (X j)]
    (f : ∀ j, X j ⟶ T) (hf : IsStandardVCovering X f)
    {I : J → Type w} [∀ j, Finite (I j)]
    (Y : ∀ j, I j → Scheme.{u}) [∀ j i, IsAffine (Y j i)]
    (g : ∀ j i, Y j i ⟶ X j)
    (hg : ∀ j, IsStandardVCovering (Y j) (g j)) :
    IsStandardVCovering (fun ji : Σ j, I j ↦ Y ji.1 ji.2)
      (fun ji ↦ g ji.1 ji.2 ≫ f ji.1)
Tag 0ETG, a lemma

Tag 0ETG in the Stacks Project.

AlgebraicGeometry.isStandardVCovering_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/StandardCoverings.lean, line 150.

A finite family of affine schemes over an affine scheme is a standard V covering if and only if it admits a refining standard V covering, if and only if the morphism from the disjoint union of the family is a standard V covering.

public theorem isStandardVCovering_tfae {T : Scheme.{u}} [IsAffine T]
    {I : Type v} [Finite I] (X : I → Scheme.{u}) [∀ i, IsAffine (X i)]
    (f : ∀ i, X i ⟶ T) :
    List.TFAE [
      IsStandardVCovering X f,
      ∃ (K : Type v) (_ : Finite K) (Y : K → Scheme.{u}) (_ : ∀ k, IsAffine (Y k))
          (g : ∀ k, Y k ⟶ T),
        IsStandardVCovering Y g ∧
          Nonempty
            (({ I₀ := K, X := Y, f := g } : PreZeroHypercover T).Hom
              ({ I₀ := I, X := X, f := f } : PreZeroHypercover T)),
      IsStandardVCovering
        (fun _ : Unit ↦ ∐ X) (fun _ ↦ Sigma.desc f)]
Tag 0ETH, a definition

Tag 0ETH in the Stacks Project.

AlgebraicGeometry.IsVCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/Coverings.lean, line 48.

Stacks 0ETH. A family of morphisms of schemes is a V covering if, over every affine open of the target, a finite standard V covering by affine schemes refines the pullback of the family.

public noncomputable def IsVCovering {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T) : Prop
Tag 0ETI, a lemma

Tag 0ETI in the Stacks Project.

AlgebraicGeometry.isVCovering_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/VCoveringRefinement.lean, line 241.

A family of morphisms of schemes is a V covering if and only if a V covering refines it, if and only if its disjoint-union morphism is a V covering.

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

Tag 0ETJ in the Stacks Project.

AlgebraicGeometry.isVCovering_of_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/Permanence.lean, line 69. The attribute's comment: “isomorphism”.

An isomorphism of schemes, regarded as a singleton family, is a V covering.

lemma isVCovering_of_isIso {T' T : Scheme.{u}} (f : T' ⟶ T) [IsIso f] :
    AlgebraicGeometry.IsVCovering (fun _ : Unit ↦ T') (fun _ ↦ f)

AlgebraicGeometry.isVCovering_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/Permanence.lean, line 89. The attribute's comment: “base_change”.

The pullback of a V covering along any morphism of schemes is a V covering.

lemma isVCovering_pullback {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T) {T' : Scheme.{u}}
    (g : T' ⟶ T) (hf : AlgebraicGeometry.IsVCovering X f) :
    AlgebraicGeometry.IsVCovering
      (fun i ↦ pullback (f i) g)
      (fun i ↦ pullback.snd (f i) g)

AlgebraicGeometry.IsVCovering.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/Permanence.lean, line 192. The attribute's comment: “composition”.

Composing a V covering with V coverings of each of its members gives a V covering.

theorem IsVCovering.comp {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : AlgebraicGeometry.IsVCovering X f) {J : I → Type w}
    (Y : ∀ i, J i → Scheme.{u}) (g : ∀ i j, Y i j ⟶ X i)
    (hg : ∀ i, AlgebraicGeometry.IsVCovering (Y i) (g i)) :
    AlgebraicGeometry.IsVCovering
      (fun ij : Σ i, J i ↦ Y ij.1 ij.2)
      (fun ij ↦ g ij.1 ij.2 ≫ f ij.1)
Tag 0ETK, a lemma

Tag 0ETK in the Stacks Project.

AlgebraicGeometry.isVCovering_of_mem_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FpqcComparison.lean, line 66. The attribute's comment: “fpqc_v”.

Stacks 0ETK. Every fpqc covering is a V covering.

Above an affine open of the target, Stacks 022E refines the base change of the family by a standard fpqc covering, and Stacks 0ETC says that a standard fpqc covering is a standard V covering.

public theorem isVCovering_of_mem_fpqcPrecoverage {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage T) :
    IsVCovering X f

AlgebraicGeometry.isVCovering_of_mem_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FpqcComparison.lean, line 89. The attribute's comment: “fppf_v”.

Stacks 0ETK. Every fppf covering is a V covering, being an fpqc covering by Stacks 022C.

public theorem isVCovering_of_mem_fppfPrecoverage {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈ Scheme.fppfPrecoverage T) :
    IsVCovering X f

AlgebraicGeometry.isVCovering_of_mem_syntomicPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FpqcComparison.lean, line 98. The attribute's comment: “syntomic_v”.

Stacks 0ETK. Every syntomic covering is a V covering, being an fpqc covering by Stacks 022C.

public theorem isVCovering_of_mem_syntomicPrecoverage {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈
      Scheme.precoverage (@Syntomic : MorphismProperty Scheme.{u}) T) :
    IsVCovering X f

AlgebraicGeometry.isVCovering_of_mem_smoothPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FpqcComparison.lean, line 108. The attribute's comment: “smooth_v”.

Stacks 0ETK. Every smooth covering is a V covering, being an fpqc covering by Stacks 022C.

public theorem isVCovering_of_mem_smoothPrecoverage {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈
      Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}) T) :
    IsVCovering X f

AlgebraicGeometry.isVCovering_of_mem_etalePrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FpqcComparison.lean, line 118. The attribute's comment: “etale_v”.

Stacks 0ETK. Every étale covering is a V covering, being an fpqc covering by Stacks 022C.

public theorem isVCovering_of_mem_etalePrecoverage {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈ Scheme.etalePrecoverage T) :
    IsVCovering X f

AlgebraicGeometry.isVCovering_of_mem_zariskiPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FpqcComparison.lean, line 127. The attribute's comment: “zariski_v”.

Stacks 0ETK. Every Zariski covering is a V covering, being an fpqc covering by Stacks 022C.

public theorem isVCovering_of_mem_zariskiPrecoverage {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈ Scheme.zariskiPrecoverage T) :
    IsVCovering X f

AlgebraicGeometry.isVCovering_of_isPHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/PhComparison.lean, line 162. The attribute's comment: “ph_v”.

Stacks 0ETK. Every ph covering is a V covering. It needs no finiteness hypothesis on the members of the family.

This is also one half of Stacks 0ETR, which for a family locally of finite presentation asserts that being a ph covering and being a V covering are equivalent; it carries no 0ETR registration. The two conditions 0ETR compares are the numbered items of one assertion, that equivalence, so a single implication is a fragment of that assertion and not a part of it; 0ETR belongs where the equivalence is stated in full, which is AlgebraicGeometry.isPHCovering_iff_isVCovering in StacksFrontier/AlgebraicGeometry/Topologies/V/PhVFlatteningModification.lean. The converse implication is AlgebraicGeometry.isPHCovering_of_isVCovering, which carries AlgebraicGeometry.StandardVCoveringHasPHRefinement; the inputs the Stacks argument needs for that predicate are the generic flatness stratification of the base (Stacks 0H3Z), AlgebraicGeometry.finitePresentationHasFlatStratification, and the Raynaud-Gruson flattening theorem for an admissible blowup (Stacks 0815), and both are available.

public theorem isVCovering_of_isPHCovering {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hph : IsPHCovering X f) :
    IsVCovering X f
Tag 0ETL, a definition

Tag 0ETL in the Stacks Project.

AlgebraicGeometry.IsVSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/Coverings.lean, line 72.

Stacks 0ETL. A set-valued presheaf on schemes is a sheaf for the V topology if it satisfies the sheaf condition for every V covering family.

public abbrev IsVSheaf (F : Scheme.{u}ᵒᵖ ⥤ Type w) : Prop
Tag 0ETM, a lemma

Tag 0ETM in the Stacks Project.

AlgebraicGeometry.isVSheaf_iff_zariski_and_standard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/Sheaves.lean, line 471. The attribute's comment: “Zariski and standard V criterion”.

Stacks Project, Tag 0ETM. The V sheaf condition is equivalent to the Zariski sheaf condition together with the sheaf condition for all standard V coverings.

theorem isVSheaf_iff_zariski_and_standard
    (F : Scheme.{u}ᵒᵖ ⥤ Type w) :
    AlgebraicGeometry.IsVSheaf.{u, max u v, w} F ↔
      (∀ (T : Scheme.{u}) (𝒰 : T.OpenCover.{max u v}),
        (Presieve.ofArrows 𝒰.X 𝒰.f).IsSheafFor F) ∧
      (∀ (T : Scheme.{u}) [IsAffine T] (I : Type (max u v)) [Finite I]
        (X : I → Scheme.{u}) [∀ i, IsAffine (X i)] (f : ∀ i, X i ⟶ T),
        AlgebraicGeometry.IsStandardVCovering X f →
          (Presieve.ofArrows X f).IsSheafFor F)

AlgebraicGeometry.isStandardVSheaf_iff_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/Sheaves.lean, line 526. The attribute's comment: “single-arrow standard V criterion”.

Stacks Project, Tag 0ETM, moreover. Under the Zariski sheaf condition, the sheaf condition for standard V coverings can be tested on one-arrow standard V coverings.

theorem isStandardVSheaf_iff_singleton
    (F : Scheme.{u}ᵒᵖ ⥤ Type w)
    (hZ : ∀ (T : Scheme.{u}) (𝒰 : T.OpenCover.{max u v}),
      (Presieve.ofArrows 𝒰.X 𝒰.f).IsSheafFor F) :
    (∀ (T : Scheme.{u}) [IsAffine T] (I : Type (max u v)) [Finite I]
      (X : I → Scheme.{u}) [∀ i, IsAffine (X i)] (f : ∀ i, X i ⟶ T),
      AlgebraicGeometry.IsStandardVCovering X f →
        (Presieve.ofArrows X f).IsSheafFor F) ↔
    (∀ (T X : Scheme.{u}) [IsAffine T] [IsAffine X] (f : X ⟶ T),
      AlgebraicGeometry.IsStandardVCovering (fun _ : Unit ↦ X) (fun _ ↦ f) →
        (Presieve.ofArrows (fun _ : Unit ↦ X) (fun _ ↦ f)).IsSheafFor F)
Tag 0ETN, a lemma

Tag 0ETN in the Stacks Project.

AlgebraicGeometry.isVCovering_iff_valuation_lifting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/QuasiCompactCoverings.lean, line 157. The attribute's comment: “part (1) iff part (2)”.

A quasi-compact morphism is a singleton V covering exactly when every map from a valuation spectrum lifts after an extension of valuation rings.

theorem isVCovering_iff_valuation_lifting {X Y : Scheme.{u}} (f : X ⟶ Y)
    [QuasiCompact f] :
    AlgebraicGeometry.IsVCovering (fun _ : Unit ↦ X) (fun _ ↦ f) ↔
      (∀ (V : Type u) [CommRing V] [IsDomain V] [ValuationRing V]
        (g : Spec (.of V) ⟶ Y),
        ∃ (W : Type u) (_ : CommRing W) (_ : IsDomain W) (_ : ValuationRing W)
          (e : V →+* W),
          AlgebraicGeometry.IsExtensionOfValuationRings e ∧
            ∃ (h : Spec (.of W) ⟶ X),
              Spec.map (CommRingCat.ofHom e) ≫ g = h ≫ f)

AlgebraicGeometry.valuation_lifting_iff_specialization_lifting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/QuasiCompactCoverings.lean, line 252. The attribute's comment: “part (2) iff part (3)”.

Valuation-ring lifting is equivalent to lifting every specialization after arbitrary base change.

theorem valuation_lifting_iff_specialization_lifting {X Y : Scheme.{u}}
    (f : X ⟶ Y) :
    (∀ (V : Type u) [CommRing V] [IsDomain V] [ValuationRing V]
      (g : Spec (.of V) ⟶ Y),
      ∃ (W : Type u) (_ : CommRing W) (_ : IsDomain W) (_ : ValuationRing W)
        (e : V →+* W),
        AlgebraicGeometry.IsExtensionOfValuationRings e ∧
          ∃ (h : Spec (.of W) ⟶ X),
            Spec.map (CommRingCat.ofHom e) ≫ g = h ≫ f) ↔
      (∀ (Z : Scheme.{u}) (g : Z ⟶ Y) (z' z : Z),
        z' ⤳ z →
          ∃ (w' w : (pullback g f : Scheme.{u})),
            (w' ⤳ w) ∧
              (pullback.fst g f) w' = z' ∧
                (pullback.fst g f) w = z)
Tag 0ETP, a lemma

Tag 0ETP in the Stacks Project.

AlgebraicGeometry.isVCovering_universallySubmersive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/VCoveringSubmersive.lean, line 191.

Stacks Project, Tag 0ETP. The morphism from the disjoint union of a V covering to its target is universally submersive.

public theorem isVCovering_universallySubmersive {T : Scheme.{u}} {I : Type v}
    [Small.{u} I] (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : IsVCovering X f) :
    universally (topologically @Topology.IsQuotientMap) (Sigma.desc f)
Sources
LeanAlgebraicGeometry.IsStandardVCovering · AlgebraicGeometry.isStandardVCovering_of_flat_affineCover · AlgebraicGeometry.StandardPHCovering.isStandardVCovering · AlgebraicGeometry.isStandardVCovering_pullback · AlgebraicGeometry.IsStandardVCovering.comp · AlgebraicGeometry.isStandardVCovering_tfae · AlgebraicGeometry.IsVCovering · AlgebraicGeometry.isVCovering_tfae

Section34.11 Change of topologies#

Section 34.11 of the Stacks Project, Tag 03FE. 1 tag here is carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03FF, a remark

Tag 03FF in the Stacks Project.

AlgebraicGeometry.BigFppfSite.isSite_covBounded_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 200. The attribute's comment: “Zariski site axioms”.

The Zariski coverings of a big fppf site's category whose index type meets its covering bound satisfy the site axioms.

theorem isSite_covBounded_isZariskiCovering :
    IsSite (CovBounded (IsZariskiCovering (κ := B.cutoff)) B.coveringBound)

AlgebraicGeometry.BigFppfSite.isSite_covBounded_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 208. The attribute's comment: “étale site axioms”.

The étale coverings of a big fppf site's category whose index type meets its covering bound satisfy the site axioms.

theorem isSite_covBounded_isEtaleCovering :
    IsSite (CovBounded (IsEtaleCovering (κ := B.cutoff)) B.coveringBound)

AlgebraicGeometry.BigFppfSite.isSite_covBounded_smoothCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 217. The attribute's comment: “smooth site axioms”.

The smooth coverings of a big fppf site's category whose index type meets its covering bound satisfy the site axioms.

theorem isSite_covBounded_smoothCovering :
    IsSite (CovBounded (SmoothCovering B.cutoff) B.coveringBound)

AlgebraicGeometry.BigFppfSite.isSite_covBounded_syntomicCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 226. The attribute's comment: “syntomic site axioms”.

The syntomic coverings of a big fppf site's category whose index type meets its covering bound satisfy the site axioms.

theorem isSite_covBounded_syntomicCovering :
    IsSite (CovBounded (SyntomicCovering B.cutoff) B.coveringBound)

AlgebraicGeometry.BigFppfSite.toBigZariskiSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 242. The attribute's comment: “the big Zariski site”.

The big Zariski site carried by a chosen big fppf site: the same size-bounded category of schemes, with the chosen fppf covering families which are Zariski coverings.

def toBigZariskiSite : BigZariskiSite.{u}

AlgebraicGeometry.BigFppfSite.toBigEtaleSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 268. The attribute's comment: “the big étale site”.

The big étale site carried by a chosen big fppf site: the same size-bounded category of schemes, with the chosen fppf covering families which are étale coverings.

def toBigEtaleSite : BigEtaleSite.{u}

AlgebraicGeometry.BigFppfSite.toBigSmoothSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 295. The attribute's comment: “the big smooth site”.

The big smooth site carried by a chosen big fppf site: the same size-bounded category of schemes, with the chosen fppf covering families which are smooth coverings.

def toBigSmoothSite : BigSmoothSite.{u}

AlgebraicGeometry.BigFppfSite.toBigSyntomicSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenCoarserSites.lean, line 324. The attribute's comment: “the big syntomic site”.

The big syntomic site carried by a chosen big fppf site: the same size-bounded category of schemes, with the chosen fppf covering families which are syntomic coverings.

def toBigSyntomicSite : BigSyntomicSite.{u}

AlgebraicGeometry.etaleCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenEtaleSite.lean, line 207. The attribute's comment: “étale coverings”.

The selected étale coverings on the underlying category of a chosen big fppf site: the families selected by the fppf site which are étale coverings.

public abbrev etaleCovering (B : BigFppfSite.{u})
    (E : Covering B.Schemes) : Prop

AlgebraicGeometry.etaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenEtaleSite.lean, line 217. The attribute's comment: “étale topology”.

The big étale topology on the underlying category of a chosen big fppf site.

public abbrev etaleTopology (B : BigFppfSite.{u}) : GrothendieckTopology B.Schemes

AlgebraicGeometry.etaleCovering_isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenEtaleSite.lean, line 240. The attribute's comment: “étale site”.

Stacks 03FF. The étale subcollection of a chosen big fppf site satisfies the site axioms.

public theorem etaleCovering_isSite (B : BigFppfSite.{u}) :
    IsSite (etaleCovering B)

AlgebraicGeometry.etaleCovering_has_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenEtaleSite.lean, line 249. The attribute's comment: “étale covering representatives”.

Stacks 03FF. Every étale covering of the common category is combinatorially equivalent to a selected étale covering.

public theorem etaleCovering_has_representative (B : BigFppfSite.{u})
    (E : Covering B.Schemes) (hE : IsEtaleCovering E) :
    ∃ E' : Covering B.Schemes,
      etaleCovering B E' ∧ Covering.CombEquiv E E'

AlgebraicGeometry.BigFppfSite.carriedIsCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/RingedChangeOfTopologies.lean, line 159. The attribute's comment: “the chosen covering families of the big τ-site carried by a big fppf site”.

Stacks 03FF. The chosen covering families of the big τ-site carried by B, as a predicate on the covering families of B's own category.

public def carriedIsCovering : CoveringTopology → Covering B.Schemes → Prop

AlgebraicGeometry.BigFppfSite.carriedIsCovering_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/RingedChangeOfTopologies.lean, line 231. The attribute's comment: “the chosen covering families are nested along the chain of topologies”.

Stacks 03FF, the nesting of the four coarser systems. A chosen τ'-covering family is a chosen τ-covering family when τ is finer than τ': the covering bound is B's own in every one of the five cases, so only the morphism property changes, and the five properties are nested.

public theorem carriedIsCovering_mono (h : τ.IsFiner τ') {E : Covering B.Schemes}
    (hE : B.carriedIsCovering τ' E) : B.carriedIsCovering τ E

AlgebraicGeometry.BigFppfSite.zariskiCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 65. The attribute's comment: “Zariski coverings”.

The chosen Zariski covering families of Sch_κ are the chosen fppf covering families which are Zariski coverings.

abbrev zariskiCovering (E : Covering B.Schemes) : Prop

AlgebraicGeometry.BigFppfSite.etaleCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 71. The attribute's comment: “étale coverings”. References: SGA 4 VII (1.2), “Cov X: étale coverings”.

The chosen étale covering families of Sch_κ are the chosen fppf covering families which are étale coverings.

abbrev etaleCovering (E : Covering B.Schemes) : Prop

AlgebraicGeometry.BigFppfSite.smoothCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 77. The attribute's comment: “smooth coverings”.

The chosen smooth covering families of Sch_κ are the chosen fppf covering families which are smooth coverings.

abbrev smoothCovering (E : Covering B.Schemes) : Prop

AlgebraicGeometry.BigFppfSite.syntomicCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 83. The attribute's comment: “syntomic coverings”.

The chosen syntomic covering families of Sch_κ are the chosen fppf covering families which are syntomic coverings.

abbrev syntomicCovering (E : Covering B.Schemes) : Prop

AlgebraicGeometry.BigFppfSite.zariskiTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 114. The attribute's comment: “Zariski topology”.

The big Zariski topology carried by a chosen big fppf site.

abbrev zariskiTopology : GrothendieckTopology B.Schemes

AlgebraicGeometry.BigFppfSite.etaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 119. The attribute's comment: “étale topology”. References: SGA 4 VII (1.2), “étale topology on (Sch)”.

The big étale topology carried by a chosen big fppf site.

abbrev etaleTopology : GrothendieckTopology B.Schemes

AlgebraicGeometry.BigFppfSite.smoothTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 124. The attribute's comment: “smooth topology”.

The big smooth topology carried by a chosen big fppf site.

abbrev smoothTopology : GrothendieckTopology B.Schemes

AlgebraicGeometry.BigFppfSite.syntomicTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 129. The attribute's comment: “syntomic topology”.

The big syntomic topology carried by a chosen big fppf site.

abbrev syntomicTopology : GrothendieckTopology B.Schemes

AlgebraicGeometry.BigFppfSite.zariskiCovering_has_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/ChosenCoverings.lean, line 144. The attribute's comment: “Zariski representatives”.

Every Zariski covering family of Sch_κ is combinatorially equivalent to a chosen Zariski covering family.

theorem zariskiCovering_has_representative (E : Covering B.Schemes)
    (hE : IsZariskiCovering E) :
    ∃ E' : Covering B.Schemes, B.zariskiCovering E' ∧ Covering.CombEquiv E E'
Sources
LeanAlgebraicGeometry.BigFppfSite.isSite_covBounded_isZariskiCovering · AlgebraicGeometry.BigFppfSite.isSite_covBounded_isEtaleCovering · AlgebraicGeometry.BigFppfSite.isSite_covBounded_smoothCovering · AlgebraicGeometry.BigFppfSite.isSite_covBounded_syntomicCovering · AlgebraicGeometry.BigFppfSite.toBigZariskiSite · AlgebraicGeometry.BigFppfSite.toBigEtaleSite · AlgebraicGeometry.BigFppfSite.toBigSmoothSite · AlgebraicGeometry.BigFppfSite.toBigSyntomicSite

Section34.12 Change of big sites#

Section 34.12 of the Stacks Project, Tag 022I. 2 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 022J, a lemma

Tag 022J in the Stacks Project.

AlgebraicGeometry.exists_common_bigZariskiSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/CommonBigSites.lean, line 235. The attribute's comment: “big Zariski sites”.

A set-sized family of big Zariski sites admits a common enlargement of both its scheme cutoffs and covering-family bounds.

public theorem exists_common_bigZariskiSite {ι : Type v} [Small.{u} ι]
    (B : ι → BigZariskiSite.{u}) :
    ∃ C : BigZariskiSite.{u},
      ∀ i, (B i).schemeCardinal ≤ C.schemeCardinal ∧
        (B i).coveringCardinal ≤ C.coveringCardinal

AlgebraicGeometry.exists_common_bigFppfSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/CommonBigSites.lean, line 271. The attribute's comment: “big fppf sites”.

A set-sized family of big fppf sites admits a common enlargement of both its scheme cutoffs and covering-family bounds.

public theorem exists_common_bigFppfSite {ι : Type v} [Small.{u} ι]
    (B : ι → AlgebraicGeometry.BigFppfSite.{u}) :
    ∃ C : AlgebraicGeometry.BigFppfSite.{u},
      ∀ i, (B i).cutoff ≤ C.cutoff ∧ (B i).coveringBound ≤ C.coveringBound

AlgebraicGeometry.exists_common_bigEtaleSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/CommonBigSites.lean, line 306. The attribute's comment: “big étale sites”.

A set-sized family of big étale sites admits a common enlargement of both its scheme cutoffs and covering-family bounds.

public theorem exists_common_bigEtaleSite {ι : Type v} [Small.{u} ι]
    (B : ι → AlgebraicGeometry.BigEtaleSite.{u}) :
    ∃ C : AlgebraicGeometry.BigEtaleSite.{u},
      ∀ i, (B i).cutoff ≤ C.cutoff ∧ (B i).coveringBound ≤ C.coveringBound
Tag 022K, a lemma

Tag 022K in the Stacks Project.

AlgebraicGeometry.hasFiniteLimits_siteCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 313. The attribute's comment: “existence of finite limits in the big sites”.

The underlying category of any of the five big sites has a terminal object and fibre products.

public instance hasFiniteLimits_siteCategory {τ : CoveringTopology}
    (B : BigSite.{u} τ) : HasFiniteLimits (siteCategory B)

AlgebraicGeometry.inclusion_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 321. The attribute's comment: “the inclusion is cocontinuous”.

public theorem inclusion_isCocontinuous {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B') :
    (inclusion (Classical.choose h)).IsCocontinuous (siteTopology τ B) (siteTopology τ B')

AlgebraicGeometry.inclusion_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 371. The attribute's comment: “the inclusion preserves finite limits”.

public theorem inclusion_preservesFiniteLimits {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B') :
    PreservesFiniteLimits (inclusion (Classical.choose h))

AlgebraicGeometry.inclusion_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 416. The attribute's comment: “the inclusion is a morphism of sites”.

public theorem inclusion_isMorphismOfSites {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B') :
    _root_.IsMorphismOfSites.{u + 1} (inclusion (Classical.choose h))
      (siteTopology τ B) (siteTopology τ B')

AlgebraicGeometry.inclusionOver_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 467. The attribute's comment: “the localized inclusion is cocontinuous”.

public theorem inclusionOver_isCocontinuous {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B')
    (S : Scheme.{u}) (hS : S.size < cutoff τ B) :
    (inclusionOver h S hS).IsCocontinuous
      (overTopology τ B S hS)
      (overTopology τ B' S (largerContains h hS))

AlgebraicGeometry.inclusionOver_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 485. The attribute's comment: “the localized inclusion is a morphism of sites”.

public theorem inclusionOver_isMorphismOfSites {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B')
    (S : Scheme.{u}) (hS : S.size < cutoff τ B) :
    _root_.IsMorphismOfSites.{u + 1} (inclusionOver h S hS)
      (overTopology τ B S hS)
      (overTopology τ B' S (largerContains h hS))

AlgebraicGeometry.inclusionOver_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 502. The attribute's comment: “the localized inclusion preserves finite limits”.

public theorem inclusionOver_preservesFiniteLimits {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B')
    (S : Scheme.{u}) (hS : S.size < cutoff τ B) :
    PreservesFiniteLimits (inclusionOver h S hS)

AlgebraicGeometry.toposRetraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 533. The attribute's comment: “the retraction of big topoi”.

public noncomputable def toposRetraction {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B') :
    let J := siteTopology τ B
    let K := siteTopology τ B'
    let F := inclusion (Classical.choose h)
    let : F.IsCocontinuous J K := inclusion_isCocontinuous B B' h
    let : F.IsContinuous J K := (inclusion_isMorphismOfSites B B' h).toIsContinuous
    ToposRetraction (siteCategory B) (siteCategory B') J K F

AlgebraicGeometry.toposRetractionOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ChangeOfBigSites.lean, line 577. The attribute's comment: “the retraction of localized topoi”.

public noncomputable def toposRetractionOver {τ : CoveringTopology}
    (B B' : BigSite.{u} τ) (h : IsContained B B')
    (S : Scheme.{u}) (hS : S.size < cutoff τ B) :
    let J := overTopology τ B S hS
    let K := overTopology τ B' S (largerContains h hS)
    let F := inclusionOver h S hS
    let : F.IsCocontinuous J K := inclusionOver_isCocontinuous B B' h S hS
    let : F.IsContinuous J K := (inclusionOver_isMorphismOfSites B B' h S hS).toIsContinuous
    ToposRetraction (Over (base B S hS))
      (Over (base B' S (largerContains h hS))) J K F

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.exists_common_bigZariskiSite · AlgebraicGeometry.exists_common_bigFppfSite · AlgebraicGeometry.exists_common_bigEtaleSite · AlgebraicGeometry.hasFiniteLimits_siteCategory · AlgebraicGeometry.inclusion_isCocontinuous · AlgebraicGeometry.inclusion_preservesFiniteLimits · AlgebraicGeometry.inclusion_isMorphismOfSites · AlgebraicGeometry.inclusionOver_isCocontinuous

Section34.13 Extending functors#

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

Tag 0EUW, a lemma

Tag 0EUW in the Stacks Project.

AlgebraicGeometry.ExtendingFunctors.extension_hom_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctors.lean, line 304. The attribute's comment: “uniqueness: a morphism between two extensions satisfying the analogues of (a) and (b) is determined by the identifications of their restrictions with the original functor”.

Stacks 0EUW. The extension of F to Sch/S is unique: a morphism between two extensions of F which both satisfy the analogues of (a) and (b) is determined by its restriction to the full subcategory.

theorem extension_hom_unique {P : ObjectProperty (Over S)}
    (_hP1 : HasAffineOpens P) (hP2 : HasFinitePresentationAffines P)
    {F : P.FullSubcategoryᵒᵖ ⥤ Type w}
    (_haF : IsZariskiSheafOnSubcategory P F)
    (_hbF : PreservesAffineLimitsOnSubcategory P F)
    {F₁ F₂ : (Over S)ᵒᵖ ⥤ Type w}
    (_ha₁ : IsZariskiSheaf F₁) (hb₁ : PreservesAffineLimits F₁)
    (ha₂ : IsZariskiSheaf F₂) (_hb₂ : PreservesAffineLimits F₂)
    {α : P.ι.op ⋙ F₁ ≅ F} {β : P.ι.op ⋙ F₂ ≅ F} (θ θ' : F₁ ⟶ F₂)
    (hθ : Functor.whiskerLeft P.ι.op θ ≫ β.hom = α.hom)
    (hθ' : Functor.whiskerLeft P.ι.op θ' ≫ β.hom = α.hom) :
    θ = θ'

AlgebraicGeometry.ExtendingFunctors.extension_iso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctors.lean, line 327. The attribute's comment: “uniqueness: two extensions satisfying the analogues of (a) and (b) admit at most one isomorphism compatible with the identifications of their restrictions with the original functor”.

Stacks 0EUW. The extension of F to Sch/S is unique: two extensions of F which both satisfy the analogues of (a) and (b) admit at most one isomorphism compatible with the identifications of their restrictions with F.

theorem extension_iso_unique {P : ObjectProperty (Over S)}
    (hP1 : HasAffineOpens P) (hP2 : HasFinitePresentationAffines P)
    {F : P.FullSubcategoryᵒᵖ ⥤ Type w}
    (haF : IsZariskiSheafOnSubcategory P F)
    (hbF : PreservesAffineLimitsOnSubcategory P F)
    {F₁ F₂ : (Over S)ᵒᵖ ⥤ Type w}
    (ha₁ : IsZariskiSheaf F₁) (hb₁ : PreservesAffineLimits F₁)
    (ha₂ : IsZariskiSheaf F₂) (hb₂ : PreservesAffineLimits F₂)
    {α : P.ι.op ⋙ F₁ ≅ F} {β : P.ι.op ⋙ F₂ ≅ F} (ε ε' : F₁ ≅ F₂)
    (hε : Functor.whiskerLeft P.ι.op ε.hom ≫ β.hom = α.hom)
    (hε' : Functor.whiskerLeft P.ι.op ε'.hom ≫ β.hom = α.hom) :
    ε = ε'

AlgebraicGeometry.ExtendingFunctors.exists_unique_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsLimits/Uniqueness.lean, line 610.

Stacks 0EUW. For a scheme S and a full subcategory 𝒞 of Sch/S which contains, up to isomorphism, the affine opens of its objects and the affine schemes of finite presentation over the affine opens of S, a functor F : 𝒞ᵒᵖ ⥤ Set which is a Zariski sheaf and takes directed inverse limits of affine objects to filtered colimits extends to Sch/S in a unique way: there is a functor F' on Sch/S which is a Zariski sheaf, takes directed inverse limits of affine schemes over S to filtered colimits, restricts to F on 𝒞, and is isomorphic to any other functor with these three properties.

theorem exists_unique_extension (hP1 : HasAffineOpens P)
    (hP2 : HasFinitePresentationAffines P)
    {F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1))}
    (haF : IsZariskiSheafOnSubcategory P F)
    (hbF : PreservesAffineLimitsOnSubcategory P F) :
    ∃ (F' : (Over S)ᵒᵖ ⥤ Type (max w (u + 1))) (_ : IsZariskiSheaf F')
      (_ : PreservesAffineLimits F') (_ : P.ι.op ⋙ F' ≅ F),
      ∀ (F'' : (Over S)ᵒᵖ ⥤ Type (max w (u + 1))), IsZariskiSheaf F'' →
        PreservesAffineLimits F'' → (P.ι.op ⋙ F'' ≅ F) → Nonempty (F' ≅ F'')

AlgebraicGeometry.ExtendingFunctors.isZariskiSheaf_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsSheaf/ZariskiSheaf.lean, line 156. The attribute's comment: “the analogue of condition (a) for the extension AlgebraicGeometry.ExtendingFunctors.extension: the extension is a Zariski sheaf on Sch/S”.

The analogue of condition (a) of Stacks 0EUW for the extension. The extension is a Zariski sheaf on Sch/S: its value at X is the limit of the colimit formula over the affine objects over affine opens of S mapping to X, and a section is built over each such object by gluing, using the sheaf condition for the colimit formula on affine objects.

theorem isZariskiSheaf_extension (hP1 : HasAffineOpens P)
    (hP2 : HasFinitePresentationAffines P) (haF : IsZariskiSheafOnSubcategory P F) :
    IsZariskiSheaf (extension P F)
Tag 049N, a lemma

Tag 049N in the Stacks Project.

AlgebraicGeometry.exists_isStandardCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardCoveringLimitDescent.lean, line 75. The attribute's comment: “covering_existence, stated once for AlgebraicGeometry.IsStandardCovering rather than separately in the idiom native to each of the five topologies”.

Stacks 049N (1), uniformly in the topology. Let T = lim Tᵢ be an affine scheme written as an inverse limit of a cofiltered system of affine schemes. A standard τ-covering of T is, member by member, the base change along T ⟶ Tᵢ of a standard τ-covering of Tᵢ for some stage i, for each of the five topologies.

theorem exists_isStandardCovering_of_isLimit (τ : CoveringTopology)
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [IsAffine c.pt] [∀ i, IsAffine (D.obj i)]
    {J : Type w} (U : J → Scheme.{u}) (f : ∀ j, U j ⟶ c.pt)
    (h : IsStandardCovering τ U f) :
    ∃ (i : I) (Uᵢ : J → Scheme.{u}) (fᵢ : ∀ j, Uᵢ j ⟶ D.obj i),
      IsStandardCovering τ Uᵢ fᵢ ∧
        ∀ j : J, Nonempty ((Over.pullback (c.π.app i)).obj (Over.mk (fᵢ j)) ≅
          Over.mk (f j))

AlgebraicGeometry.exists_standardZariskiCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringExistence.lean, line 743. The attribute's comment: “covering_existence”.

A finite standard Zariski covering of an affine inverse limit descends to a standard Zariski covering at some stage.

theorem exists_standardZariskiCovering_of_isLimit
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [IsAffine c.pt] [∀ i, IsAffine (D.obj i)]
    (𝒰 : c.pt.Cover.{w} Scheme.zariskiPrecoverage)
    (h𝒰 : AlgebraicGeometry.IsStandardZariskiCovering 𝒰) :
    ∃ (i : I) (𝒰ᵢ : (D.obj i).Cover.{w} Scheme.zariskiPrecoverage)
      (_h𝒰ᵢ : AlgebraicGeometry.IsStandardZariskiCovering 𝒰ᵢ)
      (e : 𝒰.I₀ ≃ 𝒰ᵢ.I₀),
      ∀ j : 𝒰.I₀,
        Nonempty ((Over.pullback (c.π.app i)).obj (Over.mk (𝒰ᵢ.f (e j))) ≅
          Over.mk (𝒰.f j))

AlgebraicGeometry.exists_standardEtaleCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringExistence.lean, line 807. The attribute's comment: “covering_existence”.

A finite standard étale covering of an affine inverse limit descends to a standard étale covering at some stage.

theorem exists_standardEtaleCovering_of_isLimit
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [IsAffine c.pt] [∀ i, IsAffine (D.obj i)]
    (𝒰 : c.pt.AffineCover.{w} @Etale) [Finite 𝒰.I₀] :
    ∃ (i : I) (𝒰ᵢ : (D.obj i).AffineCover.{w} @Etale)
      (_ : Finite 𝒰ᵢ.I₀) (e : 𝒰.I₀ ≃ 𝒰ᵢ.I₀),
      ∀ j : 𝒰.I₀,
        Nonempty ((Over.pullback (c.π.app i)).obj (Over.mk (𝒰ᵢ.f (e j))) ≅
          Over.mk (𝒰.f j))

AlgebraicGeometry.exists_standardSmoothCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringExistence.lean, line 850. The attribute's comment: “covering_existence”.

A finite standard smooth covering of an affine inverse limit descends to a standard smooth covering at some stage.

theorem exists_standardSmoothCovering_of_isLimit
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [IsAffine c.pt] [∀ i, IsAffine (D.obj i)]
    {J : Type w} [Finite J]
    (U : J → Scheme.{u}) [∀ j, IsAffine (U j)]
    (f : ∀ j, U j ⟶ c.pt)
    (hf : IsStandardSmoothCovering U f) :
    ∃ (i : I) (Uᵢ : J → Scheme.{u})
      (hUᵢ : ∀ j, IsAffine (Uᵢ j)) (fᵢ : ∀ j, Uᵢ j ⟶ D.obj i),
      (letI : ∀ j, IsAffine (Uᵢ j) := hUᵢ
       IsStandardSmoothCovering Uᵢ fᵢ) ∧
        ∀ j : J,
          Nonempty ((Over.pullback (c.π.app i)).obj (Over.mk (fᵢ j)) ≅
            Over.mk (f j))

AlgebraicGeometry.exists_standardSyntomicCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringExistence.lean, line 880. The attribute's comment: “covering_existence”.

A finite standard syntomic covering of an affine inverse limit descends to a standard syntomic covering at some stage.

theorem exists_standardSyntomicCovering_of_isLimit
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ i, IsAffine (D.obj i)]
    {J : Type w} (U : J → Scheme.{u}) (f : ∀ j, U j ⟶ c.pt)
    (hf : IsStandardSyntomicCovering U f) :
    ∃ (i : I) (Uᵢ : J → Scheme.{u}) (fᵢ : ∀ j, Uᵢ j ⟶ D.obj i),
      IsStandardSyntomicCovering Uᵢ fᵢ ∧
        ∀ j : J,
          Nonempty ((Over.pullback (c.π.app i)).obj (Over.mk (fᵢ j)) ≅
            Over.mk (f j))

AlgebraicGeometry.exists_standardFppfCovering_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringExistence.lean, line 912. The attribute's comment: “covering_existence”.

A finite standard fppf covering of an affine inverse limit descends to a standard fppf covering at some stage.

theorem exists_standardFppfCovering_of_isLimit
    {I : Type v} [Category.{v} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ i, IsAffine (D.obj i)]
    {J : Type w} (U : J → Scheme.{u}) (f : ∀ j, U j ⟶ c.pt)
    (hf : IsStandardFppfCovering U f) :
    ∃ (i : I) (Uᵢ : J → Scheme.{u}) (fᵢ : ∀ j, Uᵢ j ⟶ D.obj i),
      IsStandardFppfCovering Uᵢ fᵢ ∧
        ∀ j : J,
          Nonempty ((Over.pullback (c.π.app i)).obj (Over.mk (fᵢ j)) ≅
            Over.mk (f j))

AlgebraicGeometry.eventually_familyHom_eq_of_baseChange_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringMorphisms.lean, line 99. The attribute's comment: “covering_morphism_equality”. References: SGA 3 VIB (10.0), “(i)”; SGA 4 VII (5.2), “a, special case”.

Equality of morphisms of finite families of affine, flat, finitely presented schemes over a limit holds already at some finite stage.

theorem eventually_familyHom_eq_of_baseChange_eq
    {I : Type v} [Category.{a} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    (hD : ∀ i, IsAffine (D.obj i)) (i : I)
    (E : PreZeroHypercover.{w} (D.obj i))
    (F : PreZeroHypercover.{w'} (D.obj i)) [Finite E.I₀]
    (hE : ∀ j, IsAffineFlatOfFinitePresentation (Over.mk (E.f j)))
    (hF : ∀ j, IsAffineFlatOfFinitePresentation (Over.mk (F.f j)))
    (f g : E.Hom F) (hfg : FamilyHom.BaseChangeEq (c.π.app i) E F f g) :
    ∃ (j : I) (e : j ⟶ i), FamilyHom.BaseChangeEq (D.map e) E F f g

AlgebraicGeometry.exists_familyHom_after_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Vtopology/CoveringMorphisms.lean, line 264. The attribute's comment: “covering_morphisms”.

A morphism of finite standard covering families of an affine inverse limit descends to a morphism at a finite stage, with its given index map unchanged.

theorem exists_familyHom_after_baseChange
    {I : Type v} [Category.{a} I] [IsCofiltered I] [EssentiallySmall.{u} I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    (hD : ∀ i, IsAffine (D.obj i)) (i : I)
    (E : PreZeroHypercover.{w} (D.obj i))
    (F : PreZeroHypercover.{w'} (D.obj i))
    [Finite E.I₀]
    (hE : ∀ k, IsAffineFlatOfFinitePresentation (Over.mk (E.f k)))
    (hF : ∀ k, IsAffineFlatOfFinitePresentation (Over.mk (F.f k)))
    (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))),
      g.s₀ = f.s₀ ∧ ∀ k : E.I₀,
        ∃ (α : (Over.pullback (c.π.app j)).obj
            ((Over.pullback (D.map e)).obj (Over.mk (E.f k))) ≅
              (Over.pullback (c.π.app i)).obj (Over.mk (E.f k)))
          (β : (Over.pullback (c.π.app j)).obj
            ((Over.pullback (D.map e)).obj (Over.mk (F.f (g.s₀ k)))) ≅
              (Over.pullback (c.π.app i)).obj (Over.mk (F.f (g.s₀ k)))),
          (α.hom.left ≫ pullback.fst (E.f k) (c.π.app i) =
            pullback.fst ((Over.pullback (D.map e)).obj (Over.mk (E.f k))).hom
              (c.π.app j) ≫ pullback.fst (E.f k) (D.map e)) ∧
          (β.hom.left ≫ pullback.fst (F.f (g.s₀ k)) (c.π.app i) =
            pullback.fst ((Over.pullback (D.map e)).obj
              (Over.mk (F.f (g.s₀ k)))).hom (c.π.app j) ≫
                pullback.fst (F.f (g.s₀ k)) (D.map e)) ∧
          HEq (α.hom.left ≫ f.h₀ k)
            (((Over.pullback (c.π.app j)).map
              (show Over.mk ((E.pullback₂ (D.map e)).f k) ⟶
                  Over.mk ((F.pullback₂ (D.map e)).f (g.s₀ k)) from
                Over.homMk (g.h₀ k) (g.w₀ k))).left ≫ β.hom.left)
Tag 0GDW, a lemma

Tag 0GDW in the Stacks Project.

AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_extension_of_isStandardAffineSheafOnSubcategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsStandardAffineInterchange.lean, line 722. The attribute's comment: “the extension of a functor satisfying conditions (a), (b) and (c) from a full subcategory satisfying conditions (1) and (2) of Tag 0EUW is a sheaf for every τ-covering of Sch/S, for each of the five topologies”.

Stacks 0GDW. Let S be a scheme, let 𝒞 be a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW and let F : 𝒞ᵒᵖ ⥤ Set satisfy conditions (a), (b) and (c). Then the extension F' = AlgebraicGeometry.ExtendingFunctors.extension of F to Sch/S is a sheaf for each of the five topologies — Zariski, étale, smooth, syntomic and fppf.

This is the unconditional form of AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_extension, whose hypothesis hstd is supplied by AlgebraicGeometry.ExtendingFunctors.isStandardAffineSheaf_extension.

theorem isCoveringSheaf_extension_of_isStandardAffineSheafOnSubcategory (τ : CoveringTopology)
    (P : ObjectProperty (Over S)) (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1)))
    (hP1 : HasAffineOpens P) (hP2 : HasFinitePresentationAffines P)
    (haF : IsZariskiSheafOnSubcategory P F) (hbF : PreservesAffineLimitsOnSubcategory P F)
    (hcF : IsStandardAffineSheafOnSubcategory.{max w (u + 1), u, v} τ P F) :
    IsCoveringSheaf.{max w (u + 1), u, v} τ (extension P F)

AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_of_isStandardAffineSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsStandardTopologies.lean, line 380. The attribute's comment: “the general case of the source's proof: a Zariski sheaf on Sch/S which is a sheaf for the standard τ-coverings of the affine objects lying over an affine open of the base is a sheaf for every τ-covering”.

The reduction of Stacks 0GDW to the standard affine case. A Zariski sheaf on Sch/S which satisfies the sheaf condition for the standard τ-coverings of the affine objects lying over an affine open of S satisfies the sheaf condition for every τ-covering.

This is the general case of the proof of the source. An object of Sch/S is covered by its affine opens lying over affine opens of S; over each of them the given covering is refined by a standard τ-covering, which produces a local section (AlgebraicGeometry.ExtendingFunctors.exists_section_of_isStandardAffineSheaf); the local sections agree on the pairwise intersections because both restrictions are computed by the given family over the base change of the covering to the intersection, and they glue by the Zariski sheaf condition.

theorem isCoveringSheaf_of_isStandardAffineSheaf (τ : CoveringTopology)
    {G : (Over S)ᵒᵖ ⥤ Type w} (haG : IsZariskiSheaf G)
    (hG : IsStandardAffineSheaf.{w, u, v} τ G) : IsCoveringSheaf.{w, u, v} τ G

AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsStandardTopologies.lean, line 454. The attribute's comment: “the general case: the extension is a sheaf for every τ-covering once it is one for the standard τ-coverings of the affine objects lying over an affine open of the base, which is carried as a hypothesis”.

Stacks 0GDW, the general case of the source's proof, at the extension. Let S be a scheme, let 𝒞 be a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW and let F : 𝒞ᵒᵖ ⥤ Set satisfy condition (a). Then the extension F' = AlgebraicGeometry.ExtendingFunctors.extension of F to Sch/S satisfies the sheaf condition for every τ-covering as soon as it satisfies the sheaf condition for the standard τ-coverings of the affine objects of Sch/S lying over an affine open of S.

The source deduces the latter from its condition (c) by writing such an affine object as a directed limit of affines of finite presentation over an affine open of S (Stacks 00QN), descending the standard covering to a stage of that limit (Stacks 049N) and passing to the filtered colimit; that deduction is not formalized here, so the restricted sheaf condition is carried as the hypothesis hstd.

theorem isCoveringSheaf_extension (τ : CoveringTopology) (P : ObjectProperty (Over S))
    (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1))) (hP1 : HasAffineOpens P)
    (hP2 : HasFinitePresentationAffines P) (haF : IsZariskiSheafOnSubcategory P F)
    (hstd : IsStandardAffineSheaf.{max w (u + 1), u, v} τ (extension P F)) :
    IsCoveringSheaf.{max w (u + 1), u, v} τ (extension P F)
Tag 0EUX, a lemma

Tag 0EUX in the Stacks Project.

AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_zariski_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsCoveringSheaf.lean, line 606. The attribute's comment: “τ = Zariski”.

Stacks 0EUX for τ = Zariski. Let S be a scheme, let 𝒞 be a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW — the big Zariski site (Sch/S)_Zar is such a subcategory — and let F : 𝒞ᵒᵖ ⥤ Set be a Zariski sheaf on 𝒞. Then the extension F' of F to all schemes over S satisfies the sheaf condition for all Zariski coverings.

Property (b) of Stacks 0EUW, which the source assumes, is not needed for this clause: the extension is a Zariski sheaf whatever F does to directed limits of affines, and a Zariski sheaf is a sheaf for every Zariski covering. It is property (b) that makes AlgebraicGeometry.ExtendingFunctors.extension deserve the name F', by identifying its restriction to 𝒞 with F; the conclusion below is about that same functor, assumed or not.

theorem isCoveringSheaf_zariski_extension (P : ObjectProperty (Over S))
    (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1)))
    (hP1 : HasAffineOpens P) (hP2 : HasFinitePresentationAffines P)
    (hF : IsCoveringSheafOnSubcategory.{max w (u + 1), u, u} .zariski P F) :
    IsCoveringSheaf.{max w (u + 1), u, v} .zariski (extension P F)

AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_extension_of_isCoveringSheafOnSubcategory', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsStandardAffineInterchange.lean, line 794. The attribute's comment: “all five topologies: Zariski, étale, smooth, syntomic and fppf”.

Stacks 0EUX. Let τ be one of Zariski, étale, smooth, syntomic and fppf, let S be a scheme, let 𝒞 be a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW — the big site (Sch/S)_τ is such a subcategory — and let F : 𝒞ᵒᵖ ⥤ Set be a τ-sheaf on 𝒞 satisfying property (b) of Stacks 0EUW. Then the extension F' of F to all schemes over S satisfies the sheaf condition for all τ-coverings.

This is the unconditional form of AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_extension_of_isCoveringSheafOnSubcategory, which carries the sheaf condition of the extension for the standard τ-coverings of the affine objects of Sch/S lying over an affine open of S as a hypothesis only because that condition is proved in this file, which sits above it in the import order. The ingredients are conditions (a) and (c) of Stacks 0GDW, which a τ-sheaf on 𝒞 satisfies by AlgebraicGeometry.ExtendingFunctors.isZariskiSheafOnSubcategory_of_isCoveringSheafOnSubcategory and ExtendingFunctors.isStandardAffineSheafOnSubcategory_of_isCoveringSheafOnSubcategory, and Stacks 0GDW itself, ExtendingFunctors.isCoveringSheaf_extension_of_isStandardAffineSheafOnSubcategory.

Condition (a) is read on open coverings indexed by the points of a scheme, so the τ-sheaf condition is asked of F for index types of Type (max u v), where u is the universe of the objects of Sch/S and Type v is the universe of the index types for which the conclusion is drawn. For v = u — the case of the big site (Sch/S)_τ, whose coverings are indexed in the universe of its objects, which is the situation of the source — hypothesis and conclusion are both read on index types of Type u.

theorem isCoveringSheaf_extension_of_isCoveringSheafOnSubcategory'
    (τ : CoveringTopology) (P : ObjectProperty (Over S))
    (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1)))
    (hP1 : HasAffineOpens P) (hP2 : HasFinitePresentationAffines P)
    (hF : IsCoveringSheafOnSubcategory.{max w (u + 1), u, max u v} τ P F)
    (hbF : PreservesAffineLimitsOnSubcategory P F) :
    IsCoveringSheaf.{max w (u + 1), u, v} τ (extension P F)

AlgebraicGeometry.ExtendingFunctors.isCoveringSheaf_extension_of_isCoveringSheafOnSubcategory_of_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsStandardAffineInterchange.lean, line 823. The attribute's comment: “all five topologies, for coverings indexed in the universe of the objects of Sch/S, which is the big site of the source”.

Stacks 0EUX for the big site. Let τ be one of Zariski, étale, smooth, syntomic and fppf, let S be a scheme, let 𝒞 be a full subcategory of Sch/S satisfying conditions (1) and (2) of Stacks 0EUW, and let F : 𝒞ᵒᵖ ⥤ Set be a τ-sheaf on 𝒞 satisfying property (b) of Stacks 0EUW. Then the extension F' of F to all schemes over S satisfies the sheaf condition for all τ-coverings.

This is ExtendingFunctors.isCoveringSheaf_extension_of_isCoveringSheafOnSubcategory' read on index types of Type u, the universe of the objects of Sch/S. That is the situation of the source: the subcategory it takes is the big site (Sch/S)_τ, whose covering families are indexed in the universe of its own objects, so the τ-sheaf condition hypothesis and the sheaf condition concluded are read on the same index types.

theorem isCoveringSheaf_extension_of_isCoveringSheafOnSubcategory_of_univ
    (τ : CoveringTopology) (P : ObjectProperty (Over S))
    (F : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1)))
    (hP1 : HasAffineOpens P) (hP2 : HasFinitePresentationAffines P)
    (hF : IsCoveringSheafOnSubcategory.{max w (u + 1), u, u} τ P F)
    (hbF : PreservesAffineLimitsOnSubcategory P F) :
    IsCoveringSheaf.{max w (u + 1), u, u} τ (extension P F)
Sources
LeanAlgebraicGeometry.ExtendingFunctors.extension_hom_unique · AlgebraicGeometry.ExtendingFunctors.extension_iso_unique · AlgebraicGeometry.ExtendingFunctors.exists_unique_extension · AlgebraicGeometry.ExtendingFunctors.isZariskiSheaf_extension · AlgebraicGeometry.exists_isStandardCovering_of_isLimit · AlgebraicGeometry.exists_standardZariskiCovering_of_isLimit · AlgebraicGeometry.exists_standardEtaleCovering_of_isLimit · AlgebraicGeometry.exists_standardSmoothCovering_of_isLimit

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.