7.44 Sheaves of algebraic… to 7.52 Points and topologies

Section7.44 Sheaves of algebraic structures#

Section 7.44 of the Stacks Project, Tag 00YR. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00YS, a definition

Tag 00YS in the Stacks Project.

Declarations registered for the tag:

Tag 00YT, a lemma

Tag 00YT in the Stacks Project.

AlgebraicGeometry.smallEtaleUnderlyingSetCommutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreAbelian.lean, line 95. The attribute's comment: “the forgetful functor from abelian groups to sets, on the small étale sites over X: inverse image along small étale base change commutes with passing to the underlying sheaf of sets”.

On the small étale sites of the objects of B over X, inverse image along small étale base change to any T ⟶ X commutes with passing from an abelian sheaf to its underlying sheaf of sets.

public theorem smallEtaleUnderlyingSetCommutes : SmallEtaleUnderlyingSetCommutes B X

CategoryTheory.Functor.isIso_mateEquiv_sheafAdjunctionContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Presheaf/AlgebraicStructure/Sheaves.lean, line 405. The attribute's comment: “The sheaf level, for an arbitrary s : A ⥤ B: for a continuous, representably flat u : C ⥤ D and a functor s preserving filtered colimits and sheafification, the pullback f^{-1} of A-valued sheaves commutes with postcomposition by s, in that the canonical mate f^{-1}(s ∘ F) ⟶ s ∘ (f^{-1} F) of the pushforward square is an isomorphism. The tag is the case B = Type u, s the underlying-set functor of a type of algebraic structure. The presheaf level, u_p (F ⋙ s) ≅ (u_p F) ⋙ s, is lanCompIsoOfPreserves at L = u.op, which mentions no topology.”. References: SGA 4 III (1.7), “4) diagram commutes”; SGA 4 III (2.4), “underlying sheaf of sets”; SGA 4 IV (3.1.2), “u^* preserves structures”.

Let (C, J) and (D, K) be sites, let u : C ⥤ D be continuous and representably flat — the latter holds under the hypotheses of Stacks 00X6 — and let s : A ⥤ B be a functor such that A and B have filtered colimits, s preserves them, A- and B-valued presheaves on D can be sheafified, sheafification commutes with s, and an A-valued presheaf is a sheaf as soon as its image under s is.

Then the pullback functor f^{-1} on A-valued sheaves commutes with postcomposition by s: the mate, under the adjunction f^{-1} ⊣ f_*, of the identity square expressing that the pushforward f_* = u^s is restriction along u.op on both sides, namely the canonical map f^{-1}(s ∘ F) ⟶ s ∘ (f^{-1} F), is an isomorphism.

For B = Type u and s the underlying-set functor of a type of algebraic structure, this says that the pullback of sheaves of algebraic structures commutes with taking the underlying sheaf of sets.

At the level of presheaves the corresponding assertion, that u_p commutes with postcomposition by s, is Functor.lanCompIsoOfPreserves for L = u.op, which needs neither topology.

public theorem isIso_mateEquiv_sheafAdjunctionContinuous {C : Type u} [SmallCategory C]
    {D : Type u} [SmallCategory D] (u : C ⥤ D) (J : GrothendieckTopology C)
    (K : GrothendieckTopology D) [u.IsContinuous J K] [RepresentablyFlat u] {A : Type w}
    [Category.{v} A] {B : Type w'} [Category.{v'} B] (s : A ⥤ B)
    [HasFilteredColimitsOfSize.{u, u} A] [HasFilteredColimitsOfSize.{u, u} B]
    [PreservesFilteredColimitsOfSize.{u, u} s] [HasWeakSheafify K A] [HasWeakSheafify K B]
    [J.HasSheafCompose s] [K.HasSheafCompose s] [K.PreservesSheafification s] :
    IsIso
      ((mateEquiv (u.sheafAdjunctionContinuous A J K) (u.sheafAdjunctionContinuous B J K)).symm
          (TwoSquare.mk (u.sheafPushforwardContinuous A J K) (sheafCompose K s) (sheafCompose J s)
            (u.sheafPushforwardContinuous B J K) (𝟙 _))).natTrans
Tag 00YV, a proposition

Tag 00YV in the Stacks Project.

CategoryTheory.Adjunction.leftExactWhiskerRight, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Presheaf/AlgebraicStructure/Sheaves.lean, line 550. The attribute's comment: “Stated for an arbitrary theory T of algebraic structures defined by finite projective limits — structures of type T in E being the left exact functors T ⥤ E — rather than for the seven listed types of algebraic structure separately, and for an arbitrary adjunction between left exact functors rather than for a morphism of topoi: postcomposition with f⁻¹ and with f_* is an adjoint pair on structures, compatible with taking the underlying sheaf of sets by construction.”. References: SGA 4 IV (3.1.2), “finite proj lim structs”; SGA 4 III (1.7), “special case”.

Let T be a theory of algebraic structures defined by finite projective limits, so that a structure of that type in a category E is a left exact functor T ⥤ E, its underlying object being its value at the sort. Let f = (f⁻¹, f_*) be a morphism of topoi, that is, an adjunction f⁻¹ ⊣ f_* whose left adjoint f⁻¹ is left exact (the right adjoint f_* then being left exact for free).

Then postcomposition with f⁻¹ and with f_* are functors on structures of type T, and they form an adjoint pair. Since they are postcomposition, they commute with taking the underlying object — for E, E' categories of sheaves of sets, the underlying sheaf of sets — on the nose.

public noncomputable def leftExactWhiskerRight (T : Type u₁) [Category.{v₁} T] {E : Type u₂}
    [Category.{v₂} E] {E' : Type u₃} [Category.{v₃} E'] {f : E ⥤ₗ E'} {g : E' ⥤ₗ E}
    (adj : f.obj ⊣ g.obj) :
    (LeftExactFunctor.whiskeringRight T E E').obj f ⊣
      (LeftExactFunctor.whiskeringRight T E' E).obj g
Tag 00YU, a remark

Tag 00YU in the Stacks Project.

Stacks.Presheaf.AbelianVersusSets.not_universally_agrees, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Presheaf/AlgebraicStructure/AbelianVersusSetsCounterexample.lean, line 159.

Main Statement (Tag 00YU). Agreement does not hold in general: there exist categories C, D, a functor u : C ⥤ D, a presheaf of abelian groups F on C, and an object V of D such that the comparison map θ_{F,V} is not a bijection.

theorem not_universally_agrees :
    ∃ (C D : Type) (_ : SmallCategory C) (_ : SmallCategory D) (u' : C ⥤ D)
      (F : Cᵒᵖ ⥤ AddCommGrpCat.{0}) (V : Dᵒᵖ),
      ¬ Function.Bijective ((theta u' F).app V)
Sources
LeanCategoryTheory.Functor.whiskeringLeft · CategoryTheory.Functor.sheafPushforwardContinuous · AlgebraicGeometry.smallEtaleUnderlyingSetCommutes · CategoryTheory.Functor.isIso_mateEquiv_sheafAdjunctionContinuous · CategoryTheory.Adjunction.leftExactWhiskerRight · Stacks.Presheaf.AbelianVersusSets.not_universally_agrees

Section7.45 Pullback maps#

Section 7.45 of the Stacks Project, Tag 06UM. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06UM, the section

Tag 06UM in the Stacks Project.

AlgebraicGeometry.Stack.locallyQuasicoherentStructurePullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasicoherentTensorPushforward.lean, line 180. The attribute's comment: “the relative pullback map w_𝒪_𝒲 ⟶ f_𝒪_𝒬 at the structure sheaf of the middle stack of a factorization 𝒬 ⟶ 𝒲 ⟶ 𝒳 of algebraic stacks, on LQCoh^fbc, for direct images wStar, fStar and an adjunction adjPr with an identification cmp : prStar ⋙ wStar ≅ fStar”.

The relative pullback map on LQCoh^fbc at the structure sheaf. For a factorization 𝒬 --pr--> 𝒲 --w--> 𝒳 of 1-morphisms of algebraic stacks with direct images wStar, fStar on LQCoh^fbc identified by cmp : pr_* ⋙ w_* ≅ f_*, the relative pullback map at the structure sheaf of 𝒲, followed by f_* of the identification pr^*𝒪_𝒲 ≅ 𝒪_𝒬 of AlgebraicGeometry.Stack.locallyQuasicoherentStructureSheafPullbackIso:

w_*𝒪_𝒲 ⟶ f_*(pr^*𝒪_𝒲) ⟶ f_*𝒪_𝒬.

def locallyQuasicoherentStructurePullbackMap :
    wStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒲.val.val.p 𝒲.val.property hincW).obj
        (FibredSite.quasicoherentTensorUnit B S hS 𝒲.val.val.p 𝒲.val.property)) ⟶
      fStar.obj ((quasicoherentToFlatBaseChange B E hE S hS
          𝒬.val.val.p 𝒬.val.property hincP).obj
        (FibredSite.quasicoherentTensorUnit B S hS 𝒬.val.val.p 𝒬.val.property))

AlgebraicGeometry.Stack.quasicoherentRelativePullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasicoherentTensorPushforward.lean, line 221. The attribute's comment: “the relative pullback map w_{QCoh,}𝒪_𝒲 ⟶ f_{QCoh,}𝒪_𝒬 in QCoh(𝒪_𝒳), the coherator of Lemma 0778 applied to the map on LQCoh^fbc, over the same data of Proposition 0771 together with the coherator inputs hincX, hclosed, hpres, hls, hlsD, hwp, hsep of Lemma 0778”.

The relative pullback map in QCoh(𝒪_𝒳) at the structure sheaf. The coherator Q of Lemma 0778 applied to AlgebraicGeometry.Stack.locallyQuasicoherentStructurePullbackMap. Its source and target are the three-step composite Q ∘ w_* ∘ i of Stacks 077A at the structure sheaf, so this is a map

w_{QCoh, *}𝒪_𝒲 ⟶ f_{QCoh, *}𝒪_𝒬

in QCoh(𝒪_𝒳).

def quasicoherentRelativePullbackMap :
    (flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed hpres
          hls hlsD hwp hsep).obj
        (wStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒲.val.val.p 𝒲.val.property
          hincW).obj (FibredSite.quasicoherentTensorUnit B S hS 𝒲.val.val.p 𝒲.val.property))) ⟶
      (flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed hpres
          hls hlsD hwp hsep).obj
        (fStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒬.val.val.p 𝒬.val.property
          hincP).obj (FibredSite.quasicoherentTensorUnit B S hS 𝒬.val.val.p 𝒬.val.property)))

CategoryTheory.Adjunction.relativePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePullbackMap.lean, line 89. The attribute's comment: “the relative pullback map g_ℱ ⟶ h_f^{-1}ℱ of a commutative triangle of morphisms of topoi, stated for an adjunction f^{-1} ⊣ f_, two direct images and an isomorphism f_ ⋙ g_ ≅ h_ in place of the source's equality of functors”.

The relative pullback map of a commutative triangle. For an adjunction f^{-1} ⊣ f_* and direct images g_*, h_* to a third category identified by c : f_* ⋙ g_* ≅ h_*, the map

g_*ℱ ⟶ h_*f^{-1}ℱ

is g_* applied to the unit ℱ ⟶ f_*f^{-1}ℱ, followed by c at f^{-1}ℱ.

def relativePullback : gstar ⟶ finv ⋙ hstar

CategoryTheory.Adjunction.relativePullbackMapOfHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePullbackMap.lean, line 111. The attribute's comment: “the variant g_ℱ ⟶ h_𝒢 of the relative pullback map attached to a morphism f^{-1}ℱ ⟶ 𝒢”.

The relative pullback map attached to a morphism f^{-1}ℱ ⟶ 𝒢. The pullback map g_*ℱ ⟶ h_*f^{-1}ℱ followed by h_*φ.

def relativePullbackMapOfHom (F : 𝒞) {G : 𝒟} (φ : finv.obj F ⟶ G) :
    gstar.obj F ⟶ hstar.obj G
Tag 06UN, a definition

Tag 06UN in the Stacks Project.

CategoryTheory.Presheaf.isTerminalConstPUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/GlobalSections.lean, line 38.

The presheaf constant at a singleton is the final object of the category of presheaves on C.

def isTerminalConstPUnit :
    IsTerminal ((Functor.const Cᵒᵖ).obj (PUnit.{w + 1}))

CategoryTheory.Presheaf.globalSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/GlobalSections.lean, line 45.

The global sections of a presheaf of sets F on C: the set Γ(C, F) = Mor_{PSh(C)}(*, F) of morphisms of presheaves from the final presheaf * to F.

abbrev globalSections (F : Cᵒᵖ ⥤ Type w) : Type _
Tag 0792, a lemma

Tag 0792 in the Stacks Project.

Stacks.Sites.GlobalSectionsAsEqualizer.globalSectionsForkIsLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/GlobalSections/AsEqualizer.lean, line 186.

Stacks Tag 0792: Γ(C, F) is the equalizer of a^*, b^*.

noncomputable def globalSectionsForkIsLimit {V U : C} (a b : V ⟶ U)
    (h : IsColimit (Cofork.ofπ (shYonedaTerminal J U) (shYoneda_fork_commutes J a b)))
    (F : Sheaf J (Type u)) :
    IsLimit (Fork.ofι (evalAt J F U) (evalAt_eq J a b F))
Tag 0F6X, a remark

Tag 0F6X in the Stacks Project.

ToposBaseChange.main, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/GlobalSections/BaseChangeComposition.lean, line 111. References: SGA 4 XII (4.4), “more general”.

Tag 0F6X (vertical composition of base change maps). The base change map \beta_rect of the outer rectangle equals the pasted composite obtained from \beta_bot and \beta_top, namely the horizontal composite of natural transformations 

  m^{-1} \circ g_* \circ f_*
    --> g'_* \circ l^{-1} \circ f_*     (β_bot whiskered by f_* on the right)
    --> g'_* \circ f'_* \circ k^{-1}    (β_top whiskered by g'_* on the left)
In Mathlib's notation this two-step whiskered composite is exactly (βtop).hComp (βbot) (the horizontal composition of the two TwoSquares).

theorem main :
    βrect adjf adjf' adjg adjg' χtop χbot
      = (βtop adjf adjf' χtop).hComp (βbot adjg adjg' χbot)
Sources
LeanAlgebraicGeometry.Stack.locallyQuasicoherentStructurePullbackMap · AlgebraicGeometry.Stack.quasicoherentRelativePullbackMap · CategoryTheory.Adjunction.relativePullback · CategoryTheory.Adjunction.relativePullbackMapOfHom · CategoryTheory.Presheaf.isTerminalConstPUnit · CategoryTheory.Presheaf.globalSections · Stacks.Sites.GlobalSectionsAsEqualizer.globalSectionsForkIsLimit · ToposBaseChange.main

Section7.47 Topologies#

Section 7.47 of the Stacks Project, Tag 00YW. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 12 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00YX, a definition

Tag 00YX in the Stacks Project.

Declarations registered for the tag:

Tag 00YY, an equation

Tag 00YY in the Stacks Project.

Declarations registered for the tag:

Tag 00YZ, a lemma

Tag 00YZ in the Stacks Project.

CategoryTheory.sieveSetEmbedding, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 49. The attribute's comment: “(1)”.

Stacks 00YZ (1). A sieve on U is a subpresheaf of h_U, so it is determined by the family of subsets {f : V ⟶ U | f ∈ S} of h_U(V) = Hom(V, U). Thus the collection of sieves on U injects into ∏_V 𝒫(Hom(V, U)), which is the source's proof that it is a set.

def sieveSetEmbedding (U : C) : Sieve U ↪ ∀ V : C, Set (V ⟶ U)

CategoryTheory.Sieve.le_iff_forall_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 59. The attribute's comment: “(2)”. References: SGA 3 IV (4.1.1), “special case”; SGA 4 I (4.3.2).

Stacks 00YZ (2). The partial order on sieves on U is inclusion: S ≤ T holds exactly when the subset of Hom(V, U) cut out by S is contained in the one cut out by T, for every V.

theorem le_iff_forall_subset {S T : Sieve U} :
    S ≤ T ↔ ∀ V : C, sieveSetEmbedding U S V ⊆ sieveSetEmbedding U T V

CategoryTheory.Sieve.iSup_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 66. The attribute's comment: “(3)”. References: SGA 4 I (4.3.2), “union”.

Stacks 00YZ (3). The union of a family of sieves on U is a sieve, namely their supremum: an arrow lies in ⨆ i, S i exactly when it lies in some S i.

theorem iSup_apply {I : Type w} (S : I → Sieve U) {V : C} (f : V ⟶ U) :
    (⨆ i, S i) f ↔ ∃ i, S i f

CategoryTheory.Sieve.iInf_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 73. The attribute's comment: “(3)”. References: SGA 4 I (4.3.2), “intersection”.

Stacks 00YZ (3). The intersection of a family of sieves on U is a sieve, namely their infimum: an arrow lies in ⨅ i, S i exactly when it lies in every S i.

theorem iInf_apply {I : Type w} (S : I → Sieve U) {V : C} (f : V ⟶ U) :
    (⨅ i, S i) f ↔ ∀ i, S i f

CategoryTheory.Sieve.isLeast_ofArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 81. The attribute's comment: “(4)”.

Stacks 00YZ (4). Given a family {Y i ⟶ U} of morphisms with target U, the sieve Sieve.ofArrows it generates — the union of the images of the maps h_{Y i} → h_U — is the smallest sieve on U containing every f i.

theorem isLeast_ofArrows {I : Type w} (Y : I → C) (f : ∀ i, Y i ⟶ U) :
    IsLeast {S : Sieve U | ∀ i, S (f i)} (Sieve.ofArrows Y f)

CategoryTheory.Sieve.existsUnique_isLeast_arrows_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 93. The attribute's comment: “(4)”. References: SGA 4 I (4.3.3), “generated sieve”; SGA 4½ Arcata (1.6.1), “sieve generated by U_i”.

Stacks 00YZ (4). The smallest sieve on U containing a given family {Y i ⟶ U} of morphisms with target U is unique.

theorem existsUnique_isLeast_arrows_mem {I : Type w} (Y : I → C) (f : ∀ i, Y i ⟶ U) :
    ∃! S : Sieve U, IsLeast {S : Sieve U | ∀ i, S (f i)} S

CategoryTheory.Sieve.isGreatest_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 100. The attribute's comment: “(5)”.

Stacks 00YZ (5). The sieve h_U, which contains every arrow with target U (CategoryTheory.Sieve.top_apply), is the maximal sieve on U.

theorem isGreatest_top : IsGreatest (Set.univ : Set (Sieve U)) ⊤

CategoryTheory.Sieve.isLeast_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveLattice.lean, line 106. The attribute's comment: “(6)”.

Stacks 00YZ (6). The empty subpresheaf of h_U, which contains no arrow at all (CategoryTheory.Sieve.bot_apply), is the minimal sieve on U.

theorem isLeast_bot : IsLeast (Set.univ : Set (Sieve U)) ⊥

Declarations registered for the tag:

Tag 00Z1, a definition

Tag 00Z1 in the Stacks Project.

Declarations registered for the tag:

Tag 00Z2, a definition

Tag 00Z2 in the Stacks Project.

Declarations registered for the tag:

Tag 00Z3, a lemma

Tag 00Z3 in the Stacks Project.

Declarations registered for the tag:

Tag 00Z8, a definition

Tag 00Z8 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.Sieve · CategoryTheory.Sieve.downward_closed · CategoryTheory.sieveSetEmbedding · CategoryTheory.Sieve.le_iff_forall_subset · CategoryTheory.Sieve.iSup_apply · CategoryTheory.Sieve.iInf_apply · CategoryTheory.Sieve.isLeast_ofArrows · CategoryTheory.Sieve.existsUnique_isLeast_arrows_mem

Section7.48 The topology defined by a site#

Section 7.48 of the Stacks Project, Tag 00ZB. 1 tag here is carried by 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00ZD, a definition

Tag 00ZD in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.Coverage.toGrothendieck

Section7.49 Sheafification in a topology#

Section 7.49 of the Stacks Project, Tag 00ZG. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 12 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00ZH, a lemma

Tag 00ZH in the Stacks Project.

statement1_map_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 212. The attribute's comment: “(1)”. References: SGA 4 II (3.0.5), “LF presheaf: id law”.

Stacks 00ZH (1), identity law: restriction in F⁺ along an identity arrow is the identity, one half of F⁺ being a presheaf.

theorem statement1_map_id (F : Cᵒᵖ ⥤ Type u) (U : Cᵒᵖ) :
    (J.plusObj F).map (𝟙 U) = 𝟙 ((J.plusObj F).obj U)

statement1_map_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 219. The attribute's comment: “(1)”. References: SGA 4 II (3.0.5), “LF presheaf: comp law”.

Stacks 00ZH (1), composition law: restricting in F⁺ along f ≫ g is restricting along f and then along g, the other half of F⁺ being a presheaf.

theorem statement1_map_comp (F : Cᵒᵖ ⥤ Type u)
    {U V W : Cᵒᵖ} (f : U ⟶ V) (g : V ⟶ W) :
    (J.plusObj F).map (f ≫ g) = (J.plusObj F).map f ≫ (J.plusObj F).map g

statement2_ell_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 227. The attribute's comment: “(2)”. References: SGA 4 II (3.0.5), “ℓ(F):F→LF is natural”.

Stacks 00ZH (2): ℓ : F ⟶ F⁺ is a morphism of presheaves, i.e. its components commute with restriction along any arrow f.

theorem statement2_ell_natural (F : Cᵒᵖ ⥤ Type u) {U V : Cᵒᵖ} (f : U ⟶ V) :
    F.map f ≫ (J.toPlus F).app V = (J.toPlus F).app U ≫ (J.plusObj F).map f

statement3a_map_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 234. The attribute's comment: “(3)”.

Stacks 00ZH (3), identity law for F ↦ F⁺ as an operation on presheaves: (𝟙 F)⁺ = 𝟙 F⁺.

theorem statement3a_map_id (F : Cᵒᵖ ⥤ Type u) :
    (J.plusFunctor (Type u)).map (𝟙 F) = 𝟙 ((J.plusFunctor (Type u)).obj F)

statement3a_map_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 241. The attribute's comment: “(3)”.

Stacks 00ZH (3), composition law for F ↦ F⁺ as an operation on presheaves: (α ≫ β)⁺ = α⁺ ≫ β⁺.

theorem statement3a_map_comp {F G H : Cᵒᵖ ⥤ Type u} (α : F ⟶ G) (β : G ⟶ H) :
    (J.plusFunctor (Type u)).map (α ≫ β) =
      (J.plusFunctor (Type u)).map α ≫ (J.plusFunctor (Type u)).map β

statement3b_ell_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 249. The attribute's comment: “(3)”.

Stacks 00ZH (3), naturality of ℓ in the presheaf variable: the square α ≫ ℓ G = ℓ F ≫ α⁺ commutes, so ℓ is a natural transformation 𝟭 ⟶ plusFunctor.

theorem statement3b_ell_natural {F G : Cᵒᵖ ⥤ Type u} (α : F ⟶ G) :
    α ≫ J.toPlus G = J.toPlus F ≫ J.plusMap α

statement4_preserves_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 257. The attribute's comment: “(4)”. References: SGA 3 IV (4.3.10.0).

Stacks 00ZH (4): if α : F ⟶ G is injective on sections over every object, then so is α⁺. The sections of F⁺ over U form a filtered colimit of multiequalizers, and injectivity survives both diagramNatTrans and the filtered colimit.

theorem statement4_preserves_mono
    {F G : Cᵒᵖ ⥤ Type u} (α : F ⟶ G)
    (hα : ∀ U : Cᵒᵖ, Function.Injective (α.app U)) :
    ∀ U : Cᵒᵖ, Function.Injective ((J.plusMap α).app U)

statement5_local_representability, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/PlusProperties.lean, line 270. The attribute's comment: “(5)”.

Stacks 00ZH (5): every section s of F⁺ over U is locally in the image of ℓ — there is a covering sieve S ∈ J U and a φ : S.functor ⟶ F with φ ≫ J.toPlus F equal to the restriction of s to S, expressed via S.functorInclusion and yonedaEquiv.symm s.

theorem statement5_local_representability
    (F : Cᵒᵖ ⥤ Type u) (U : C) (s : (J.plusObj F).obj (op U)) :
    ∃ (S : Sieve U) (_ : S ∈ J U) (φ : S.functor ⟶ F),
      φ ≫ J.toPlus F =
        S.functorInclusion ≫ (CategoryTheory.yonedaEquiv.symm s)
Tag 00ZI, a definition

Tag 00ZI in the Stacks Project.

Declarations registered for the tag:

Tag 00ZJ, a theorem

Tag 00ZJ in the Stacks Project.

Declarations registered for the tag:

Tag 00ZL, a definition

Tag 00ZL in the Stacks Project.

Declarations registered for the tag:

Tag 00ZM, a proposition

Tag 00ZM in the Stacks Project.

Declarations registered for the tag:

Sources
Leanstatement1_map_id · statement1_map_comp · statement2_ell_natural · statement3a_map_id · statement3a_map_comp · statement3b_ell_natural · statement4_preserves_mono · statement5_local_representability

Section7.50 Topologies and sheaves#

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

Tag 00ZO, a lemma

Tag 00ZO in the Stacks Project.

sieve_sheafification_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SieveSheafification.lean, line 42. References: SGA 4 II (5.3), “sieve inclusion S→h_U”; SGA 3 IV (4.3.12), “special case”; SGA 4 II (4.6.1), “more general”; SGA 4 II (5.1), “special case”; SGA 4 II (5.5), “Ψ ∘ Φ = id”.

Stacks 00ZO. A sieve S on U is a covering sieve for the topology J if and only if the sheafification S^# ⟶ h_U^# of its inclusion S ↪ h_U (i.e. the image under the associated-sheaf functor of S.functorInclusion) is an isomorphism.

theorem sieve_sheafification_iff {C : Type u} [SmallCategory C] (J : GrothendieckTopology C)
    (U : C) (S : Sieve U) :
    S ∈ J U ↔ IsIso ((presheafToSheaf J (Type u)).map S.functorInclusion)
Tag 00ZP, a theorem

Tag 00ZP in the Stacks Project.

Declarations registered for the tag:

Tag 00ZQ, a lemma

Tag 00ZQ in the Stacks Project.

le_iff_isSheaf_imp_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topology/SupOfSheaves.lean, line 55.

Stacks 00ZQ. For Grothendieck topologies J, J' on a category C, we have J ≤ J' (every J-covering sieve is J'-covering) if and only if every sheaf for J' is a sheaf for J.

theorem le_iff_isSheaf_imp_isSheaf :
    J ≤ J' ↔
      ∀ (P : Cᵒᵖ ⥤ Type (max u v)),
        Presheaf.IsSheaf J' P → Presheaf.IsSheaf J P
Sources
Leansieve_sheafification_iff · CategoryTheory.topology_eq_iff_same_sheaves · le_iff_isSheaf_imp_isSheaf

Section7.52 Points and topologies#

Section 7.52 of the Stacks Project, Tag 00ZS. 1 tag here is carried by 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00ZT, a definition

Tag 00ZT in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.GrothendieckTopology.Point

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.