18.40 Locally ringed topoi to 18.44 Localizing sheaves of…

Section18.40 Locally ringed topoi#

Section 18.40 of the Stacks Project, Tag 04ER. 13 tags here are carried by 48 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04ES, a lemma

Tag 04ES in the Stacks Project.

Stacks.Sheaves.LocallyRingedSite.condition1_iff_condition2_and_condition2_iff_condition3, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/LocalUnitConditions.lean, line 302. References: SGA 4 IV (13.9), “b) (ii) <=> (iii)”.

Theorem (Stacks Tag 04ES). For a ringed site (C, O), conditions (1), (2), (3) are equivalent. We state the equivalence as the conjunction of the two biconditionals (1) ↔ (2) and (2) ↔ (3).

theorem condition1_iff_condition2_and_condition2_iff_condition3
    (O : Sheaf J CommRingCat.{v}) :
    (Condition1 O ↔ Condition2 O) ∧ (Condition2 O ↔ Condition3 O)

Tag 04ET, a lemma

Tag 04ET in the Stacks Project.

AlgebraicGeometry.RingedSite.stalksAreZeroOrLocal_of_locallyUnitOrOneSubUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Defs.lean, line 177. The attribute's comment: “(1) implies (2)”. References: SGA 4 IV (13.9), “b) (iii) => (iv)”.

The local unit-or-unit-complement condition makes every stalk of the structure sheaf either the zero ring or a local ring.

theorem stalksAreZeroOrLocal_of_locallyUnitOrOneSubUnit (X : RingedSite.{u, u, u})
    (h : LocallyUnitOrOneSubUnit X) : StalksAreZeroOrLocal X

AlgebraicGeometry.RingedSite.locallyUnitOrOneSubUnit_iff_stalksAreZeroOrLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Defs.lean, line 219. The attribute's comment: “equivalence when the site has enough points”. References: SGA 4 IV (13.9), “b) (iii) <=> (iv)”.

On a site with a conservative family of points, the local unit-or-unit-complement condition is equivalent to all stalks of the structure sheaf being zero rings or local rings.

theorem locallyUnitOrOneSubUnit_iff_stalksAreZeroOrLocal (X : RingedSite.{u, u, u})
    (hX : X.J.HasConservativeFamily.{u}) :
    LocallyUnitOrOneSubUnit X ↔ StalksAreZeroOrLocal X

Tag 05D7, an equation

Tag 05D7 in the Stacks Project.

AlgebraicGeometry.RingedSite.oneIsNeverZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Defs.lean, line 308.

The canonical morphism from the empty sheaf to the equalizer of the zero and one sections of the structure sheaf.

noncomputable def oneIsNeverZero (X : RingedSite.{u, v, w}) :
    ⊥_ (Sheaf X.J (Type w)) ⟶ equalizer (zeroSection X) (oneSection X)

Stacks.Sheaves.LocallyRingedSite.oneIsNeverZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/OneIsNeverZero.lean, line 156. The attribute's comment: “the displayed morphism from the empty sheaf to the equalizer of 0 and 1”.

The canonical morphism of sheaves of sets

∅^# ⟶ Equalizer(0, 1 : * ⟶ O)

from the initial sheaf to the equalizer of the zero and one sections of the structure sheaf. The first condition in the definition of a locally ringed site (Tag 04EU) is that it be an isomorphism.

noncomputable def oneIsNeverZero (O : Sheaf J CommRingCat.{w}) :
    ⊥_ (Sheaf J (Type w)) ⟶ equalizer (zeroSection J O) (oneSection J O)

Stacks.Sheaves.LocallyRingedSite.isIso_oneIsNeverZero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/OneIsNeverZero.lean, line 187. The attribute's comment: “the equivalent sections-level form: 0 ≠ 1 over every object the empty sieve does not cover”.

The canonical morphism ∅^# ⟶ Equalizer(0, 1) is an isomorphism exactly when, for every object U that is not sheaf-theoretically empty, the sections 0 and 1 of O(U) are distinct.

theorem isIso_oneIsNeverZero_iff (O : Sheaf J CommRingCat.{w}) :
    IsIso (oneIsNeverZero J O) ↔
      ∀ U : C, (⊥ : Sieve U) ∉ J U → (0 : O.obj.obj (op U)) ≠ 1

Tag 05D8, a lemma

Tag 05D8 in the Stacks Project.

AlgebraicGeometry.RingedSite.nontrivial_stalk_of_isIso_oneIsNeverZero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Defs.lean, line 450. The attribute's comment: “the implication (1) ⇒ (2)”.

If zero and one are nowhere equal, then the stalk of the structure sheaf at every point is a nonzero ring.

lemma nontrivial_stalk_of_isIso_oneIsNeverZero (X : RingedSite.{v, u, u})
    [IsIso (oneIsNeverZero X)] (p : X.J.Point.{u}) :
    Nontrivial ((p.presheafFiber (A := CommRingCat.{u})).obj X.O.obj)

AlgebraicGeometry.RingedSite.isIso_oneIsNeverZero_iff_forall_nontrivial_stalk, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Defs.lean, line 458. The attribute's comment: “the equivalence (1) ⇔ (2) when the site has enough points”.

On a site with a conservative family of points, zero and one are nowhere equal if and only if every stalk of the structure sheaf is a nonzero ring.

lemma isIso_oneIsNeverZero_iff_forall_nontrivial_stalk (X : RingedSite.{v, u, u})
    (hX : X.J.HasConservativeFamily.{u}) :
    IsIso (oneIsNeverZero X) ↔
      ∀ p : X.J.Point.{u}, Nontrivial ((p.presheafFiber (A := CommRingCat.{u})).obj X.O.obj)

Stacks.Sheaves.LocallyRingedSite.nontrivial_stalkRingObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/OneIsNeverZero.lean, line 263. The attribute's comment: “(1) implies (2): if the morphism of 05D7 is an isomorphism then no stalk of the structure sheaf is the zero ring”.

If the morphism of Tag 05D7 is an isomorphism then for every point p of the site the stalk O_p is not the zero ring.

theorem nontrivial_stalkRingObj (h : IsIso (oneIsNeverZero X.J X.O))
    (p : Stacks.Sheaves.LocallyRingedTopos.Point X) : Nontrivial p.stalkRingObj

Tag 04EU, a definition

Tag 04EU in the Stacks Project.

AlgebraicGeometry.RingedSite.IsLocallyRinged, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Defs.lean, line 344.

A ringed site is locally ringed when the sections 0 and 1 of its structure sheaf are nowhere equal and every section is locally either a unit or has unit complement.

abbrev IsLocallyRinged (X : RingedSite.{u, v, w}) : Prop

Stacks.Sheaves.LocallyRingedSite.isLocallyRingedSite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/OneIsNeverZero.lean, line 240. The attribute's comment: “Definition 18.40.4 in the source's spelling (05D7 an isomorphism, plus 04ES)”.

Definition 18.40.4 in the source's own spelling (the morphism of Tag 05D7 is an isomorphism, and the equivalent conditions of Tag 04ES hold) is equivalent to the sections-level predicate IsLocallyRingedSite.

theorem isLocallyRingedSite_iff :
    IsIso (oneIsNeverZero X.J X.O) ∧ Stacks.Sheaves.LocallyRingedSite.Condition1 X.O ↔
      LocalizedRingedTopos.IsLocallyRingedSite X

Tag 04H7, a lemma

Tag 04H7 in the Stacks Project.

AlgebraicGeometry.RingedSite.isLocallyRinged_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedTopoi/InverseImage.lean, line 394. The attribute's comment: “part (1)”.

Stacks Project, Tag 04H7, part (1). The inverse image of a locally ringed site by a morphism of topoi is locally ringed.

theorem isLocallyRinged_inverseImage (hY : IsLocallyRinged Y) :
    IsLocallyRinged
      ({ C := C, J := J, O := (inverseImageCommRingFunctor f).obj Y.O } :
        RingedSite.{u, u, u})

AlgebraicGeometry.RingedToposHom.isLocallyRinged_iff_of_ringedToposEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedTopoi/InverseImage.lean, line 437. The attribute's comment: “part (2)”.

Stacks Project, Tag 04H7, part (2). An equivalence of ringed topoi preserves and reflects local ringedness.

theorem isLocallyRinged_iff_of_ringedToposEquivalence (f : RingedToposHom X Y)
    [f.toToposHom.inverseImage.IsEquivalence] [IsIso f.fSharp] :
    RingedSite.IsLocallyRinged ({ C := Y.C, J := Y.J, O := Y.O } : RingedSite.{v, v, v}) ↔
      RingedSite.IsLocallyRinged ({ C := X.C, J := X.J, O := X.O } : RingedSite.{u, u, u})

Tag 04H8, a definition

Tag 04H8 in the Stacks Project.

Stacks.Sheaves.LocallyRingedSite.isLocallyRingedSite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/OneIsNeverZero.lean, line 240. The attribute's comment: “a ringed topos is locally ringed exactly when its underlying ringed site is”.

Definition 18.40.4 in the source's own spelling (the morphism of Tag 05D7 is an isomorphism, and the equivalent conditions of Tag 04ES hold) is equivalent to the sections-level predicate IsLocallyRingedSite.

theorem isLocallyRingedSite_iff :
    IsIso (oneIsNeverZero X.J X.O) ∧ Stacks.Sheaves.LocallyRingedSite.Condition1 X.O ↔
      LocalizedRingedTopos.IsLocallyRingedSite X

AlgebraicGeometry.RingedTopos.IsLocallyRinged, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedTopoi/Defs.lean, line 63.

Stacks Project, Tag 04H8. A ringed topos is locally ringed when the ringed site presenting it is a locally ringed site.

abbrev RingedTopos.IsLocallyRinged (X : RingedTopos.{v, u, w}) : Prop

AlgebraicGeometry.RingedTopos.isLocallyRinged_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedTopoi/Defs.lean, line 76. The attribute's comment: “well-posedness: invariance under an equivalence of ringed topoi”.

Stacks Project, Tag 04H8, well-posedness. Being locally ringed is a property of a ringed topos and not of a site presenting it: by Stacks 04H7 part (2) an equivalence of ringed topoi preserves and reflects it.

theorem RingedTopos.isLocallyRinged_iff_of_equivalence {X : RingedTopos.{u, u, u}}
    {Y : RingedTopos.{v, v, v}} (f : RingedToposHom X Y)
    [f.toToposHom.inverseImage.IsEquivalence] [IsIso f.fSharp] :
    Y.IsLocallyRinged ↔ X.IsLocallyRinged

Tag 0B8Q, a lemma

Tag 0B8Q in the Stacks Project.

AlgebraicGeometry.RingedSite.isInvertible_of_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InvertibleRankOne.lean, line 485. The attribute's comment: “locally free of rank one implies invertible”.

Stacks Project, Tag 0B8Q, the unconditional clause. On the ringed topos of a ringed site, a sheaf of modules which is locally free of rank one is invertible.

theorem isInvertible_of_isFiniteLocallyFreeOfRank_one
    (X : AlgebraicGeometry.RingedSite.{u, v, max u v w})
    (L : SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hL : AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRank X L 1) :
    Stacks.SheafOfModules.IsInvertible X.O.obj
      (Stacks.SheafOfModules.Tensor.ringSheaf X.O).property L

AlgebraicGeometry.RingedSite.isInvertible_iff_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InvertibleRankOne.lean, line 733. The attribute's comment: “characterization for locally ringed sites”.

Stacks Project, Tag 0B8Q, the characterization clause. On a locally ringed site, a sheaf of modules is invertible exactly when it is locally free of rank one.

theorem isInvertible_iff_isFiniteLocallyFreeOfRank_one
    (X : AlgebraicGeometry.RingedSite.{u, max u v, max u v})
    (L : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hX : AlgebraicGeometry.RingedSite.IsLocallyRinged X) :
    Stacks.SheafOfModules.IsInvertible X.O.obj
      (Stacks.SheafOfModules.Tensor.ringSheaf X.O).property L ↔
      AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRank X L 1

AlgebraicGeometry.RingedSite.exists_isInvertible_not_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InvertibleRankOne.lean, line 870. The attribute's comment: “the converse fails in general”.

Stacks Project, Tag 0B8Q, the parenthetical clause. Without local ringedness the converse fails: there is a ringed site carrying an invertible sheaf of modules which is not locally free of rank one.

theorem exists_isInvertible_not_isFiniteLocallyFreeOfRank_one :
    ∃ (X : AlgebraicGeometry.RingedSite.{u, v, w})
      (L : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)),
      Stacks.SheafOfModules.IsInvertible X.O.obj
        (Stacks.SheafOfModules.Tensor.ringSheaf X.O).property L ∧
        ¬ AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRank X L 1

Tag 04H9, a lemma

Tag 04H9 in the Stacks Project.

AlgebraicGeometry.RingedSite.HomGeneral.reflectsUnitsObj_of_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/IsLocallyRingedCriterion.lean, line 209. The attribute's comment: “(1)⇒(3), independent universes”. References: SGA 4 IV (13.9), “c) (i) ⇒ (ii)”.

Stacks 04H9, (1) ⇒ (3) at independent universes. If a morphism of ringed sites is locally ringed, then every left exact functor to sets reflects units for the induced morphism f⁻¹O_Y ⟶ O_X; at a stalk functor this is locality of the induced map of stalk rings.

theorem reflectsUnitsObj_of_isLocallyRinged (hf : f.IsLocallyRinged)
    (P : Sheaf X.J (Type w) ⥤ Type t) [PreservesFiniteLimits P] :
    RingedTopos.ReflectsUnitsObj P f.fSharpRingMap

AlgebraicGeometry.RingedSite.HomGeneral.isLocallyRinged_iff_reflectsUnitsObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/IsLocallyRingedCriterion.lean, line 221. The attribute's comment: “(1)⇔(3) at a conservative family, independent universes”. References: SGA 4 IV (13.9), “c) (i)⇔(ii) enough pts”.

Stacks 04H9, (1) ⇔ (3) at independent universes. For a family of left exact functors to sets which detects isomorphisms — in practice the stalk functors at a conservative family of points — a morphism of ringed sites is locally ringed exactly when each member reflects units for f⁻¹O_Y ⟶ O_X.

theorem isLocallyRinged_iff_reflectsUnitsObj {ι : Type*}
    (P : ι → Sheaf X.J (Type w) ⥤ Type t) (hP : ∀ i, PreservesFiniteLimits (P i))
    [HasPullback (RingedTopos.unitsιOf X.O)
      (RingedTopos.forgetRingMap f.fSharpRingMap)]
    (hcons : ∀ {F G : Sheaf X.J (Type w)} (ψ : F ⟶ G), (∀ i, IsIso ((P i).map ψ)) → IsIso ψ) :
    f.IsLocallyRinged ↔ ∀ i, RingedTopos.ReflectsUnitsObj (P i) f.fSharpRingMap

Stacks.Sheaves.LocallyRingedTopos.condition1_imp_condition2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/StalkCriterion.lean, line 572. The attribute's comment: “(1)⇒(2)”. References: SGA 4 IV (13.9), “c) (i) => (ii)”.

Theorem, part 1: (1) ⇒ (2) always holds (no hypotheses beyond Definition 1).

Each stalk functor (.)_p = p^{-1} is exact, hence preserves the cartesian square of condition (1); together with the identifications (f^{-1} O_D)_p = O_{D,q} and (f^{-1} O_D^*)_p = O_{D,q}^*, this yields condition (2).

theorem condition1_imp_condition2 (f : RingedToposHom X Y)
    (h : Condition1 f) : Condition2 f

Stacks.Sheaves.LocallyRingedTopos.condition1_of_condition2OnFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/StalkCriterion.lean, line 589. The attribute's comment: “(2)-family⇒(1)”. References: SGA 4 IV (13.9), “c) (ii)⇒(i) conserv fam”.

Theorem, part 4 (general case): (2) on a conservative family implies (1).

If condition (2) holds for every point of a conservative family of points of C, then condition (1) holds (the family detects cartesianness of the sheaf square).

theorem condition1_of_condition2OnFamily (f : RingedToposHom X Y)
    (P : ConservativeFamily X) (h : Condition2OnFamily f P) :
    Condition1 f

Stacks.Sheaves.LocallyRingedTopos.condition1_iff_condition2_of_enoughPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/StalkCriterion.lean, line 657. The attribute's comment: “(1)⇔(2)”. References: SGA 4 IV (13.9), “c) (i) <=> (ii)”.

Theorem, part 2: if C has enough points, then (1) ⇔ (2).

Forward is part 1. Conversely a conservative family of points detects whether a square of sheaves is cartesian (cartesianness is preserved and reflected by the exact, jointly-conservative stalk functors), so condition (2) forces condition (1).

theorem condition1_iff_condition2_of_enoughPoints (f : RingedToposHom X Y)
    (hC : HasEnoughPoints X) :
    Condition1 f ↔ Condition2 f

Stacks.Sheaves.LocallyRingedTopos.condition2_iff_condition3_of_locallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/StalkCriterion.lean, line 911. The attribute's comment: “(2)⇔(3)”.

Theorem, part 3: in the locally ringed case, (2) ⇔ (3).

When both topoi are locally ringed, every stalk O_{C,p} and O_{D,q} is a local ring (via IsLocallyRinged.isLocalRing_stalk, with no enough-points assumption on either C or D), so condition (2) at p — the cartesianness of the stalk-of-units-sheaves square — is, via the identifications (O^*)_p = (O_p)^* (stalkUnitsIso), exactly the statement that the unit-inclusion square of phi_p is cartesian, which by the algebraic core lemma is equivalent to phi_p being a local ring map.

theorem condition2_iff_condition3_of_locallyRinged (f : RingedToposHom X Y)
    (hlrC : IsLocallyRinged X) (hlrD : IsLocallyRinged Y) :
    Condition2 f ↔ Condition3 f

Stacks.Sheaves.LocallyRingedTopos.condition1_of_condition3OnFamily_of_locallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/StalkCriterion.lean, line 926. The attribute's comment: “(3)-family⇒(1)”. References: SGA 4 IV (13.9), “c) (ii)⇒(i) conserv fam”.

Theorem, part 4 (locally ringed case): (3) on a conservative family implies (1).

If both topoi are locally ringed and phi_p is a local ring map for every point p of a conservative family of points of C, then condition (1) holds. No enough-points assumption on D is needed.

theorem condition1_of_condition3OnFamily_of_locallyRinged (f : RingedToposHom X Y)
    (hlrC : IsLocallyRinged X) (hlrD : IsLocallyRinged Y)
    (P : ConservativeFamily X) (h : Condition3OnFamily f P) :
    Condition1 f

AlgebraicGeometry.RingedTopos.isLocalHom_sheafFiber_iff_reflectsUnitsObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/StalkReflectsUnits.lean, line 276. The attribute's comment: “that the two spellings of condition (3) at a single point of the site agree, at independent universes: reflection of units by the set-valued fibre functor is locality of the fibre ring map. Neither implication between conditions (1), (2) and (3) is proved here — the forward half of this equivalence is proved in this file and the converse alongside it; what the statement supplies is the bridge at a site with C : Type u, Category.{v} C and sections at w all independent, which the collapsed formulation of StalkCriterion.lean cannot state”.

Stacks 04H9, reflection of units and locality of the stalk map are equivalent, at independent universes. The fibre functor of Φ on sheaves of sets reflects units for φ exactly when the fibre of φ at Φ taken in commutative rings is a local ring homomorphism.

theorem isLocalHom_sheafFiber_iff_reflectsUnitsObj {C : Type u} [Category.{v} C]
    {J : GrothendieckTopology C} (Φ : J.Point.{w}) {O₁ O₂ : Sheaf J CommRingCat.{w}}
    (φ : O₁ ⟶ O₂)
    [LocallySmall.{w} C] [J.HasSheafCompose (forget RingCat.{w})]
    [J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})] :
    IsLocalHom ((Φ.sheafFiber (A := CommRingCat.{w})).map φ).hom ↔
      ReflectsUnitsObj (Φ.sheafFiber (A := Type w)) φ

Tag 04HA, a definition

Tag 04HA in the Stacks Project.

AlgebraicGeometry.RingedToposHom.IsLocallyRinged, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Morphisms.lean, line 100. The attribute's comment: “morphisms of locally ringed topoi”.

A morphism of ringed topoi is locally ringed when its square of units subsheaves, over the structure map fSharpSet f, is cartesian.

abbrev IsLocallyRinged (f : RingedToposHom X Y) : Prop

AlgebraicGeometry.RingedSite.Hom.exists_associatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Morphisms.lean, line 156. The attribute's comment: “associated ringed-topos morphism of a ringed-site morphism”. References: SGA 4 IV (13.3.1), “site ⇒ topos morphism”.

A morphism of ringed sites induces a morphism of ringed topoi whose underlying morphism of topoi and whose structure map on underlying sheaves of sets are the given ones.

theorem exists_associatedRingedToposHom (f : RingedSite.Hom X Y) :
    ∃ g : RingedToposHom (toRingedTopos X) (toRingedTopos Y),
      (g.toToposHom = f.isMorphismOfSites.morphismOfTopoi) ∧
      HEq (RingedToposHom.fSharpSet g) (fSharpSet f)

AlgebraicGeometry.RingedSite.Hom.IsLocallyRinged, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Morphisms.lean, line 191. The attribute's comment: “morphisms of locally ringed sites”.

A morphism of ringed sites is locally ringed when the units square for its associated morphism of ringed topoi is cartesian.

abbrev IsLocallyRinged (f : RingedSite.Hom X Y) : Prop

AlgebraicGeometry.RingedSite.HomGeneral.IsLocallyRinged, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/MorphismsGeneral.lean, line 239. The attribute's comment: “morphisms of locally ringed sites, independent universes”.

Stacks 04HA at independent universes. A morphism of ringed sites is locally ringed when its square

  f⁻¹(O_Y^*) ---> O_X^*
      |             |
      v             v
  f⁻¹(O_Y)  ---> O_X

of units subsheaves is cartesian, the bottom arrow being the structure map on underlying sheaves of sets. The top arrow is not part of the data: the inclusion of units is a monomorphism, so an arrow making the square commute is unique if it exists, which is AlgebraicGeometry.RingedSite.HomGeneral.isLocallyRinged_iff_existsUnique.

abbrev IsLocallyRinged (f : HomGeneral X Y) : Prop

AlgebraicGeometry.RingedSite.HomGeneral.exists_associatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/MorphismsGeneral.lean, line 291. The attribute's comment: “associated ringed-topos morphism, independent universes”. References: SGA 4 IV (13.3.1), “special case”.

Stacks 04HA at independent universes. A morphism of ringed sites induces a morphism of ringed topoi whose underlying morphism of topoi is HomGeneral.toposHom and whose structure map on underlying sheaves of sets is HomGeneral.fSharpSet.

As in AlgebraicGeometry.RingedSite.Hom.exists_associatedRingedToposHom, the statement is existential rather than a construction: the structure map of a morphism of ringed sites lands in the restriction u^s O_X along the site functor, whereas a morphism of ringed topoi needs it in the direct image f_* O_X along the induced morphism of topoi, and those agree only up to Stacks.Sheaves.ToposPullback.restrictionCommRingIso, which is the identity on underlying sheaves of sets but not the identity map of sheaves of commutative rings.

theorem HomGeneral.exists_associatedRingedToposHom (f : HomGeneral X Y) :
    ∃ g : RingedToposHom (toRingedTopos X) (toRingedTopos Y),
      (g.toToposHom = f.toposHom) ∧ HEq (RingedToposHom.fSharpSet g) f.fSharpSet

Tag 04IG, a lemma

Tag 04IG in the Stacks Project.

AlgebraicGeometry.RingedToposHom.isLocallyRinged_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedTopoi/CompositionOfLocallyRingedMorphisms.lean, line 87.

Stacks 04IG. A composite of locally ringed morphisms of ringed topoi is locally ringed.

theorem isLocallyRinged_comp (g : RingedToposHom Y Z) (f : RingedToposHom X Y)
    (hg : IsLocallyRinged g) (hf : IsLocallyRinged f) :
    IsLocallyRinged (g.comp f)

Tag 04KR, a lemma

Tag 04KR in the Stacks Project.

AlgebraicGeometry.inverseImage_units_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheafInverseImage.lean, line 432. The attribute's comment: “inverse image of the units subsheaf”.

Stacks 04KR: the inverse image of the units subsheaf. There is exactly one isomorphism of the inverse image of the units subsheaf of Y with the units subsheaf of the inverse-image ringed topos compatible with the inclusions into the structure sheaves; it is therefore the canonical one.

theorem inverseImage_units_iso :
    ∃! e : f.inverseImage.obj (RingedTopos.units Y) ≅
        RingedTopos.units (inverseImageRingedTopos C J Y f),
      e.hom ≫ RingedTopos.unitsι (inverseImageRingedTopos C J Y f) =
        f.inverseImage.map (RingedTopos.unitsι Y) ≫ (inverseImageForgetIso J Y f).hom

AlgebraicGeometry.inverseImageRingedToposHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheafInverseImage.lean, line 458. The attribute's comment: “canonical morphism of locally ringed topoi”.

Stacks 04KR: the canonical morphism is a morphism of locally ringed topoi. Its structure map on underlying sheaves of sets is an isomorphism, so its square of units subsheaves is cartesian as soon as the comparison of units subsheaves exists.

theorem inverseImageRingedToposHom_isLocallyRinged :
    RingedToposHom.IsLocallyRinged (inverseImageRingedToposHom C J Y f)

Declarations registered for the tag:

• AlgebraicGeometry.inverseImageRingedToposHom, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheafInverseImage.lean, line 480 (StacksFrontier): “canonical ringed-topos morphism”.

Tag 04IH, a lemma

Tag 04IH in the Stacks Project.

Stacks.Sheaves.LocalizedRingedTopos.isLocallyRingedSite_localizedRingedTopos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalizedRingedToposLocallyRinged.lean, line 75. The attribute's comment: “(5), first assertion: the localization at a sheaf is again locally ringed”.

The localization of a locally ringed topos at a sheaf is again a locally ringed topos.

theorem isLocallyRingedSite_localizedRingedTopos (X :
  Stacks.Sheaves.LocallyRingedTopos.RingedTopos.{u})
    (F : X.Topos) (hX : IsLocallyRingedSite X) :
    IsLocallyRingedSite (localizedRingedTopos X F)

AlgebraicGeometry.RingedSite.localizationRingedToposHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizationMorphismsLocallyRinged.lean, line 90. The attribute's comment: “(1), second assertion: the localization morphism (j_U, j_U♯) is a morphism of locally ringed topoi”.

Stacks 04IH (1), second assertion. The localization morphism (j_U, j_U♯) of a ringed site at an object U is a morphism of locally ringed topoi: its structure map is the identity on underlying sheaves of sets, and the inverse image of the units subsheaf is the units subsheaf, so the units square is a square of identities.

theorem localizationRingedToposHom_isLocallyRinged (U : X.C) :
    (X.localizationRingedToposHom U).IsLocallyRinged

AlgebraicGeometry.RingedSite.relocalizationRingedToposHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizationMorphismsLocallyRinged.lean, line 112. The attribute's comment: “(2): the morphism (j, j♯) of 04IY is a morphism of locally ringed topoi”.

Stacks 04IH (2). The morphism (j, j♯) : (Sh(C/V), O_V) → (Sh(C/U), O_U) of Stacks 04IY, the relocalization of a ringed site along a morphism f : V ⟶ U of its underlying category, is a morphism of locally ringed topoi. As for the localization morphism, the units square is a square of identities.

theorem relocalizationRingedToposHom_isLocallyRinged (f : V ⟶ U) :
    (X.relocalizationRingedToposHom f).IsLocallyRinged

AlgebraicGeometry.RingedTopos.localizationMorphism_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizationMorphismsLocallyRinged.lean, line 139. The attribute's comment: “(5), second assertion: the localization morphism (j_F, j_F♯) is a morphism of locally ringed topoi”.

Stacks 04IH (5), second assertion. The localization morphism (j_F, j_F♯) : (Sh(C)/F, O_F) → (Sh(C), O) of a ringed topos at a sheaf is a morphism of locally ringed topoi: the site of elements carries the restriction of the structure sheaf, so the structure map is the identity on underlying sheaves of sets and the units square is a square of identities.

theorem localizationMorphism_isLocallyRinged :
    (localizationMorphism X F).IsLocallyRinged

AlgebraicGeometry.RingedSite.Hom.localized_isLocallyRinged_sites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizedMorphismLocallyRinged.lean, line 198. The attribute's comment: “part (3): the localization of a morphism of locally ringed sites”.

For a morphism of locally ringed sites (f, f^#) and an object V of the target, the two localized sites (C/U, O_U) and (D/V, O'_V) are locally ringed sites and the localized morphism (f', (f')^#) of Stacks 04J0 is a locally ringed morphism.

theorem localized_isLocallyRinged_sites (hX : RingedSite.IsLocallyRinged X)
    (hY : RingedSite.IsLocallyRinged Y) (hf : f.IsLocallyRinged) :
    RingedSite.IsLocallyRinged (X.over (f.u.obj V)) ∧
      RingedSite.IsLocallyRinged (Y.over V) ∧ (f.localized V).IsLocallyRinged

AlgebraicGeometry.RingedSite.Hom.localizedRingedToposHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizedMorphismsLocallyRinged.lean, line 203. The attribute's comment: “(3): the localized morphism f' of 04J0 is a morphism of locally ringed sites”.

Stacks 04IH (3). The localized morphism (f', (f')♯) of Stacks 04J0 is a morphism of locally ringed sites as soon as (f, f♯) is: its units square is the image under the exact functor j_U^{-1} of the units square of f, with the two bottom edges matched by Stacks 03CF's clause (b).

The units subsheaf of a localization, and its inclusion, are the restrictions of those of the original ringed site on the nose, so the only comparison entering is clause (b), whose two components form a square of isomorphisms on the left of the pasting.

theorem Hom.localizedRingedToposHom_isLocallyRinged (V : Y.C)
    (hf : f.ringedToposHom.IsLocallyRinged) :
    (f.localizedRingedToposHom V).IsLocallyRinged

AlgebraicGeometry.RingedSite.Hom.relocalized_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizedMorphismsLocallyRinged.lean, line 224. The attribute's comment: “(4): the relocalized morphism f_c of 04J1 is a morphism of locally ringed topoi”.

Stacks 04IH (4). The relocalized morphism (f_c, f_c♯) of Stacks 04J1 is a morphism of locally ringed topoi as soon as (f, f♯) is a morphism of locally ringed sites.

This is Stacks' "follows formally on combining (2) and (3)": f_c is by definition the localized morphism of Stacks 04J0 composed with the relocalization morphism of Stacks 04IY along c, the first locally ringed by clause (3) and the second by clause (2), and a composite of locally ringed morphisms is locally ringed by Stacks 04IG.

theorem Hom.relocalized_isLocallyRinged {U : X.C} {V : Y.C} (c : U ⟶ f.u.obj V)
    (hf : f.ringedToposHom.IsLocallyRinged) :
    (f.relocalized c).IsLocallyRinged

AlgebraicGeometry.RingedToposHom.localized_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizedMorphismsLocallyRinged.lean, line 282. The attribute's comment: “(7): the localized morphism f' of 04IF is a morphism of locally ringed topoi”.

Stacks 04IH (7). The localized morphism (f', (f')♯) of Stacks 04IF is a morphism of locally ringed topoi as soon as (f, f♯) is: its units square is the image under the exact functor j_{f⁻¹G}⁻¹ of the units square of f, with the two bottom edges matched by 04IF's comparison of inverse images.

The units subsheaf of a localization, and its inclusion, are the inverse image of those of the original ringed topos on the nose, so the only comparison entering is 04IF's, whose two components form a square of isomorphisms on the left of the pasting.

theorem localized_isLocallyRinged (hf : f.IsLocallyRinged) :
    (f.localized G).IsLocallyRinged

AlgebraicGeometry.RingedToposHom.relocalized_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/LocalizedMorphismsLocallyRinged.lean, line 300. The attribute's comment: “(8): the relocalized morphism f_s of 04J8 is a morphism of locally ringed topoi”.

Stacks 04IH (8). The relocalized morphism (f_s, f_s♯) of Stacks 04J8 is a morphism of locally ringed topoi as soon as (f, f♯) is.

Stacks 04J8 defines f_s as the morphism of 04IF composed with the relocalization morphism of 04J4 along s, the first locally ringed by clause (7) and the second by clause (6), and a composite of locally ringed morphisms is locally ringed by Stacks 04IG.

theorem relocalized_isLocallyRinged {F : X.Topos}
    (s : F ⟶ f.toToposHom.inverseImage.obj G) (hf : f.IsLocallyRinged) :
    (f.relocalized s).IsLocallyRinged

AlgebraicGeometry.RingedTopos.localizedRingedTopos_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/ToposLocalizationLocallyRinged.lean, line 81. The attribute's comment: “(5), first assertion: the localization (Sh(C)/F, O_F) of a locally ringed topos at a sheaf is again a locally ringed topos, in the categorical spelling of local ringedness”.

Stacks 04IH (5), first assertion. The localization (Sh(C)/F, O_F) of a locally ringed topos at a sheaf of sets is again a locally ringed topos: its structure sheaf is the inverse image of O along the localization morphism of topoi, and local ringedness passes to an inverse image.

theorem localizedRingedTopos_isLocallyRinged (X : RingedTopos.{u, u, u}) (F : X.Topos)
    (hX : RingedSite.IsLocallyRinged (toRingedSite X)) :
    RingedSite.IsLocallyRinged (toRingedSite (localizedRingedTopos X F))

AlgebraicGeometry.RingedTopos.relocalizationMorphism_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/ToposRelocalization.lean, line 206. The attribute's comment: “(6): the morphism (j, j♯) of 04J4 is a morphism of locally ringed topoi”.

Stacks 04IH (6). The morphism (j, j♯) : (Sh(C)/G, O_G) → (Sh(C)/F, O_F) of Stacks 04J4, the relocalization of a ringed topos along a morphism s : G ⟶ F of sheaves, is a morphism of locally ringed topoi: its structure map is the identity on underlying sheaves of sets and the inverse image of the units subsheaf is the units subsheaf, so the units square is a square of identities.

theorem relocalizationMorphism_isLocallyRinged (s : G ⟶ F) :
    (X.relocalizationMorphism s).IsLocallyRinged

AlgebraicGeometry.RingedSite.isLocallyRinged_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/Localization.lean, line 140. The attribute's comment: “(1), first assertion: the localization (C/U, O_U) of a locally ringed site is again a locally ringed site”.

Stacks 04IH (1), first assertion. A localization (C/U, O_U) of a locally ringed site is again a locally ringed site.

theorem isLocallyRinged_over (X : RingedSite.{u, v, w}) (U : X.C)
    (hX : IsLocallyRinged X) : IsLocallyRinged (X.over U)

Stacks.Sheaves.LocallyRingedSite.localizedRingedTopos_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/LocallyRingedSites/OneIsNeverZero.lean, line 249. The attribute's comment: “(5), first assertion, with condition (1) in the source's sheaf-level spelling of 05D7”.

If the morphism of Tag 05D7 is an isomorphism for X and the conditions of Tag 04ES hold, then both hold for the localization of X at a sheaf F.

theorem localizedRingedTopos_isLocallyRinged (F : X.Topos)
    (hX : IsIso (oneIsNeverZero X.J X.O) ∧ Stacks.Sheaves.LocallyRingedSite.Condition1 X.O) :
    IsIso (oneIsNeverZero (LocalizedRingedTopos.localizedRingedTopos X F).J
        (LocalizedRingedTopos.localizedRingedTopos X F).O) ∧
      Stacks.Sheaves.LocallyRingedSite.Condition1 (LocalizedRingedTopos.localizedRingedTopos X F).O

Sources

• Section 18.40, Tag 04ER
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Sheaves.LocallyRingedSite.condition1_iff_condition2_and_condition2_iff_condition3 · AlgebraicGeometry.RingedSite.stalksAreZeroOrLocal_of_locallyUnitOrOneSubUnit · AlgebraicGeometry.RingedSite.locallyUnitOrOneSubUnit_iff_stalksAreZeroOrLocal · AlgebraicGeometry.RingedSite.oneIsNeverZero · Stacks.Sheaves.LocallyRingedSite.oneIsNeverZero · Stacks.Sheaves.LocallyRingedSite.isIso_oneIsNeverZero_iff · AlgebraicGeometry.RingedSite.nontrivial_stalk_of_isIso_oneIsNeverZero · AlgebraicGeometry.RingedSite.isIso_oneIsNeverZero_iff_forall_nontrivial_stalk

Section18.41 Lower shriek for modules#

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

Tag 0797, a lemma

Tag 0797 in the Stacks Project.

Stacks.SheafOfModules.lowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriek.lean, line 85. References: SGA 4 IV (14.2), “j_!”.

Stacks 0797. Lower shriek g_! : Mod(O_C) ⥤ Mod(O_D) for the morphism of topoi associated with a continuous and cocontinuous functor of sites, where O_C = g^{-1} O_D: a sheaf of O_C-modules is pushed forward as a presheaf of modules and the result is sheafified.

def lowerShriek [u.IsCocontinuous J K] :
    _root_.SheafOfModules.{v} (inverseImageRing J K u O) ⥤ _root_.SheafOfModules.{v} O

Stacks.SheafOfModules.lowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriek.lean, line 95. References: SGA 4 IV (14.2), “j_! ⊣ j^*”.

Stacks 0797. Lower shriek is left adjoint to the inverse image g^* = g^{-1} of sheaves of modules, for the morphism of topoi associated with a continuous and cocontinuous functor of sites.

def lowerShriekAdjunction [u.IsCocontinuous J K] :
    lowerShriek.{v} J K u O ⊣ inverseImage.{v} J K u O

AlgebraicGeometry.smallEtaleModuleProjectionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ModuleProjectionPullback.lean, line 194. The attribute's comment: “the adjunction at the inclusion of the small étale site of a scheme into its big étale site, at the module universe of Stacks 0DDH part (6)”.

Stacks 0797 at the small étale inclusion. π_S^* is left adjoint to π_{S,*}, which is AlgebraicGeometry.smallEtaleModuleRestriction B S S (𝟙 S).

public def smallEtaleModuleProjectionAdjunction :
    smallEtaleModuleProjectionPullback B S ⊣ smallEtaleModuleRestriction B S S (𝟙 S)

Tag 0798, a remark

Tag 0798 in the Stacks Project.

Stacks.SheafOfModules.lowerShriekForgetComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 81. The attribute's comment: “comparison_transformation”.

The canonical natural transformation from lower shriek applied to the underlying abelian sheaf to the underlying abelian sheaf of lower shriek on modules.

noncomputable def lowerShriekForgetComparison :
    _root_.SheafOfModules.toSheaf.{w} S ⋙
        F.sheafPullback AddCommGrpCat.{w} J K ⟶
      _root_.SheafOfModules.pullback.{w} phi ⋙ _root_.SheafOfModules.toSheaf.{w} R

Stacks.SheafOfModules.lowerShriekForgetComparison_homEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 133. The attribute's comment: “comparison_transformation”.

The comparison map is adjoint to the forgotten unit of the module lower-shriek adjunction.

theorem lowerShriekForgetComparison_homEquiv (M : _root_.SheafOfModules.{w} S) :
    (F.sheafAdjunctionContinuous AddCommGrpCat.{w} J K).homEquiv
        ((_root_.SheafOfModules.toSheaf.{w} S).obj M)
        ((_root_.SheafOfModules.toSheaf.{w} R).obj
          ((_root_.SheafOfModules.pullback.{w} phi).obj M))
        ((lowerShriekForgetComparison F phi).app M) =
      (_root_.SheafOfModules.toSheaf.{w} S).map
        ((_root_.SheafOfModules.pullbackPushforwardAdjunction.{w} phi).unit.app M)

Stacks.SheafOfModules.lowerShriekForget_not_isomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 448. The attribute's comment: “noncommutativity”.

The lower shriek of modules may differ, even as an abelian sheaf, from lower shriek of the underlying abelian sheaf.

theorem lowerShriekForget_not_isomorphic :
    ∃ (J : GrothendieckTopology PUnit) (K : GrothendieckTopology Bool)
      (F : PUnit ⥤ Bool) (R : Sheaf K RingCat.{0})
      (hF : F.IsContinuous J K) (_hFc : F.IsCocontinuous J K),
      letI : F.IsContinuous J K := hF
      let S : Sheaf J RingCat.{0} :=
        (F.sheafPushforwardContinuous RingCat.{0} J K).obj R
      let φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{0} J K).obj R := 𝟙 S
      ∃ (hAb : (F.sheafPushforwardContinuous AddCommGrpCat.{0} J K).IsRightAdjoint)
        (hMod : (SheafOfModules.pushforward.{0} φ).IsRightAdjoint),
      letI : (F.sheafPushforwardContinuous AddCommGrpCat.{0} J K).IsRightAdjoint := hAb
      letI : (SheafOfModules.pushforward.{0} φ).IsRightAdjoint := hMod
      ∃ M : SheafOfModules.{0} S,
        ¬ Nonempty
          (((SheafOfModules.toSheaf.{0} S ⋙
              F.sheafPullback AddCommGrpCat.{0} J K).obj M) ≅
            ((SheafOfModules.pullback.{0} φ ⋙
              SheafOfModules.toSheaf.{0} R).obj M))

Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 653. The attribute's comment: “the criterion: agreement iff the comparison is invertible at every j_{U!} O_U”.

The canonical comparison between lower shriek on sheaves of modules and lower shriek on the underlying abelian sheaves is an isomorphism if and only if it is an isomorphism at the extension by zero j_{U!} O_U of the structure sheaf for every object U of the source site.

theorem isIso_lowerShriekForgetComparison_iff :
    IsIso (lowerShriekForgetComparison F phi) ↔
      ∀ U : C, IsIso ((lowerShriekForgetComparison F phi).app
        (extensionByZeroUnit.{u₁, v₁, u, max u₂ v₂ t} S U))

Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_iff_of_isos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 697. The attribute's comment: “the criterion, at any family isomorphic to the extensions by zero of the structure sheaf”.

If a family G of sheaves of modules is isomorphic, object by object, to the extensions by zero of the structure sheaf, then the comparison is an isomorphism exactly when it is an isomorphism at every G U.

theorem isIso_lowerShriekForgetComparison_iff_of_isos
    (G : C → _root_.SheafOfModules.{max u₁ v₁ u₂ v₂ u t} S)
    (e : ∀ U : C, extensionByZeroUnit.{u₁, v₁, u, max u₂ v₂ t} S U ≅ G U) :
    IsIso (lowerShriekForgetComparison F phi) ↔
      ∀ U : C, IsIso ((lowerShriekForgetComparison F phi).app (G U))

Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_iff_extensionByZeroUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForget.lean, line 778. The attribute's comment: “the criterion in the source's form: the comparison is an isomorphism iff g_!^{Ab} j_{U!} O_U ⟶ j_{u(U)!} O_{u(U)} is one for every U, the target being identified by Stacks 07AC”.

The canonical comparison between lower shriek on sheaves of modules and lower shriek on the underlying abelian sheaves is an isomorphism if and only if, for every object U of the source site, the canonical map

g_!^{Ab} j_{U!} O_U ⟶ j_{u(U)!} O_{u(U)}

is an isomorphism.

theorem isIso_lowerShriekForgetComparison_iff_extensionByZeroUnit :
    IsIso (lowerShriekForgetComparison u (structureMap J K u O)) ↔
      ∀ V : C, IsIso ((lowerShriekForgetComparison u (structureMap J K u O)).app
            (extensionByZeroUnit (inverseImageRing J K u O) V) ≫
          (_root_.SheafOfModules.toSheaf O).map
            (pullbackExtensionByZeroUnitIso.{t, u₁, u₂, v₁, v₂} J K u O V).hom)

Stacks.SheafOfModules.lowerShriekForgetComparison_app_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForgetCounit.lean, line 52. The attribute's comment: “the comparison on counits”.

The lower-shriek forget comparison carries the forgotten counit of the module lower-shriek adjunction to the counit of the abelian one: both sides are maps from the abelian lower shriek of the direct image of N to the abelian sheaf underlying N, the left one going through the module lower shriek of the direct image.

theorem lowerShriekForgetComparison_app_comp_counit (N : _root_.SheafOfModules.{w} R) :
    (lowerShriekForgetComparison F phi).app
          ((_root_.SheafOfModules.pushforward.{w} phi).obj N) ≫
        (_root_.SheafOfModules.toSheaf.{w} R).map
          ((_root_.SheafOfModules.pullbackPushforwardAdjunction.{w} phi).counit.app N) =
      (F.sheafAdjunctionContinuous AddCommGrpCat.{w} J K).counit.app
        ((_root_.SheafOfModules.toSheaf.{w} R).obj N)

Stacks.SheafOfModules.abelianShriekOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForgetLocalized.lean, line 103. The attribute's comment: “g_!^{Ab} j_{U!} = j_{u(U)!} (g')^{Ab}_!, the consequence of the localized square of Stacks 03EG that the remark uses”.

Lower shriek of abelian sheaves commutes with localization: with V = u(U) and g' : Sh(C/U) ⟶ Sh(D/V) the morphism of topoi induced by the localized functor u' = Over.post u of Stacks 03EG,

g_!^{Ab} ∘ j_{U!} ≅ j_{V!} ∘ (g')^{Ab}_!.

def abelianShriekOverIso :
    (Over.forget U).sheafPullback AddCommGrpCat.{w} (J.over U) J ⋙
        u.sheafPullback AddCommGrpCat.{w} J K ≅
      (Over.post u : Over U ⥤ Over (u.obj U)).sheafPullback AddCommGrpCat.{w}
          (J.over U) (K.over (u.obj U)) ⋙
        (Over.forget (u.obj U)).sheafPullback AddCommGrpCat.{w} (K.over (u.obj U)) K

Stacks.SheafOfModules.homEquiv_comp_lowerShriekForgetComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForgetLocalized.lean, line 567. The attribute's comment: “the composition law for the comparison transformation g_!^{Ab} ∘ forget ⟶ forget ∘ g_!”.

The composition law for the comparison transformation of Stacks 0798. For a composite a ⋙ b of continuous functors of sites, with the structure sheaves the successive restrictions of a sheaf of rings on the target, the composite

b_!^{Ab} (c^a) ≫ c^b

of the two comparison transformations is the adjoint transpose, under the composite of the two lower-shriek adjunctions for abelian sheaves, of the forgotten unit of the composite of the two lower-shriek adjunctions for modules, written with the two units separated.

theorem homEquiv_comp_lowerShriekForgetComparison
    (M : _root_.SheafOfModules.{w} (inverseImageRing JA JB a (inverseImageRing JB JE b O))) :
    ((a.sheafAdjunctionContinuous AddCommGrpCat.{w} JA JB).comp
        (b.sheafAdjunctionContinuous AddCommGrpCat.{w} JB JE)).homEquiv _ _
      ((b.sheafPullback AddCommGrpCat.{w} JB JE).map
          ((lowerShriekForgetComparison a
            (structureMap JA JB a (inverseImageRing JB JE b O))).app M) ≫
        (lowerShriekForgetComparison b (structureMap JB JE b O)).app
          ((_root_.SheafOfModules.pullback.{w}
            (structureMap JA JB a (inverseImageRing JB JE b O))).obj M)) =
      (_root_.SheafOfModules.toSheaf.{w}
            (inverseImageRing JA JB a (inverseImageRing JB JE b O))).map
          ((_root_.SheafOfModules.pullbackPushforwardAdjunction.{w}
            (structureMap JA JB a (inverseImageRing JB JE b O))).unit.app M) ≫
        (a.sheafPushforwardContinuous AddCommGrpCat.{w} JA JB).map
          ((_root_.SheafOfModules.toSheaf.{w} (inverseImageRing JB JE b O)).map
            ((_root_.SheafOfModules.pullbackPushforwardAdjunction.{w}
              (structureMap JB JE b O)).unit.app
              ((_root_.SheafOfModules.pullback.{w}
                (structureMap JA JB a (inverseImageRing JB JE b O))).obj M)))

Stacks.SheafOfModules.localizedStructureSheafComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForgetLocalized.lean, line 1064. The attribute's comment: “the canonical map of equation 0799, κ_U : (g')_!^{Ab} O_U ⟶ O_{u(U)}”.

The canonical map (g')_!^{Ab} O_U ⟶ O_{u(U)} of Stacks 0798: lower shriek of abelian sheaves applied to the underlying abelian sheaf of the structure sheaf of the localized source site, mapping to the underlying abelian sheaf of the structure sheaf of the localized target site. It is the comparison transformation of Stacks 0798 for the localized functor, evaluated at the structure sheaf, followed by the canonical map g'_! O_U ⟶ O_{u(U)} of sheaves of modules.

def localizedStructureSheafComparison :
    ((Over.post (X := V) u).sheafPullback AddCommGrpCat.{w} (J.over V) (K.over (u.obj V))).obj
        ((_root_.SheafOfModules.toSheaf.{w} (inverseImageRing (J.over V) (K.over (u.obj V))
            (Over.post (X := V) u) (O.over (u.obj V)))).obj
          (_root_.SheafOfModules.unit _)) ⟶
      (_root_.SheafOfModules.toSheaf.{w} (O.over (u.obj V))).obj
        (_root_.SheafOfModules.unit (O.over (u.obj V)))

Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_of_localizedStructureSheafComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekForgetLocalized.lean, line 1154. The attribute's comment: “the criterion: g_! = g_!^{Ab} if the canonical map of equation 0799 is an isomorphism for every object U”.

Lower shriek on sheaves of modules agrees with lower shriek on the underlying abelian sheaves, that is, the comparison transformation Stacks.SheafOfModules.lowerShriekForgetComparison is an isomorphism, as soon as, for every object U of the source site, the canonical map

(g')_!^{Ab} O_U ⟶ O_{u(U)}

of Stacks.SheafOfModules.localizedStructureSheafComparison is an isomorphism, g' being the morphism of topoi induced by the localized functor u' = Over.post u : C/U ⥤ D/u(U) of Stacks 03EG.

theorem isIso_lowerShriekForgetComparison_of_localizedStructureSheafComparison
    (h : ∀ V : C, IsIso (localizedStructureSheafComparison J K u O V)) :
    IsIso (lowerShriekForgetComparison u (structureMap J K u O))

AlgebraicGeometry.Space.isIso_etaleLowerShriekForgetComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModuleExtensionByZeroForget.lean, line 68. The attribute's comment: “postcomposition along an étale morphism of algebraic spaces”.

Stacks 0798 for postcomposition along an étale morphism of algebraic spaces: the comparison from extension by zero of the underlying abelian sheaf to the underlying abelian sheaf of extension by zero of modules is an isomorphism, because every slice functor of postcomposition is an equivalence and the structure morphism of rings is the identity.

instance isIso_etaleLowerShriekForgetComparison (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    IsIso (Stacks.SheafOfModules.lowerShriekForgetComparison.{u, u}
      (smallEtalePostcomp B S hS f hf)
      (Stacks.SheafOfModules.structureMap (SmallEtale.topology B S hS X.1)
        (SmallEtale.topology B S hS Y.1) (smallEtalePostcomp B S hS f hf)
        (etaleRingSheaf B S hS Y)))

AlgebraicGeometry.Space.etaleModuleShriekForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModuleShriekForgetStalk.lean, line 91. The attribute's comment: “extension by zero of modules and of abelian sheaves, for an étale morphism”.

Tag 0798 for an étale morphism of algebraic spaces. The abelian sheaf underlying the extension by zero of a sheaf of 𝒪_X-modules is the extension by zero of the abelian sheaf underlying it.

This is AlgebraicGeometry.Space.etaleModuleShriekForgetIsoRaw repackaged: the two isomorphisms have the same components, and only the spelling of the functors differs. The repackaging is what makes the structure sheaf of rings of X appear as AlgebraicGeometry.Space.etaleRingSheaf rather than as the restriction along postcomposition of that of Y, and the module categories appear as AlgebraicGeometry.Space.Modules; without it every rewrite below is rejected for being type-incorrect at the transparency rewriting uses.

def etaleModuleShriekForgetIso :
    SheafOfModules.toSheaf (etaleRingSheaf B S hS X) ⋙
        abelianEtaleExtensionByZero B S hS f hf ≅
      etaleModuleLowerShriek B S hS f hf ⋙
        SheafOfModules.toSheaf (etaleRingSheaf B S hS Y)

AlgebraicGeometry.Space.etaleModuleShriekForgetIso_hom_app_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModuleShriekForgetStalk.lean, line 114. The attribute's comment: “the comparison on counits, for an étale morphism”.

The comparison of Tag 0798 carries the forgotten counit of the module extension-by-zero adjunction to the counit of the abelian one.

theorem etaleModuleShriekForgetIso_hom_app_comp_counit
    (N : Modules.{u, u} B S hS Y.1 Y.2) :
    (etaleModuleShriekForgetIso B S hS f hf).hom.app
          ((etaleModulePullback.{u, u} B S hS f hf).obj N) ≫
        (SheafOfModules.toSheaf (etaleRingSheaf B S hS Y)).map
          ((etaleModuleLowerShriekAdjunction B S hS f hf).counit.app N) =
      (abelianEtaleExtensionByZeroAdjunction B S hS f hf).counit.app
        ((SheafOfModules.toSheaf (etaleRingSheaf B S hS Y)).obj N)

Tag 0FN3, a lemma

Tag 0FN3 in the Stacks Project.

Stacks.SheafOfModules.inverseImageCompCocontinuousPushforwardOfIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekCocontinuousSquare.lean, line 444. The attribute's comment: “first conclusion: f'_* ∘ (g')^* ≅ g^* ∘ f_* on sheaves of modules, for a commutative square of ringed topoi whose four functors u, u', v, v' are cocontinuous, with v, v' continuous as well, with the comparison functors of the index categories of Section 00XF cofinal, and with g^{-1} O_D = O_{D'}, (g')^{-1} O_C = O_{C'}. An isomorphism rather than an equality, the sheaf-level comparison of Stacks 0FN1 being a base change of right Kan extensions. The direct images of sheaves of modules along the cocontinuous u and u' are the canonical ones attached to the structure map f^♯ : O_D → {}_su O_C of the morphism of ringed topoi, whose underlying sheaves of abelian groups are {}_su, {}_su'.”.

Stacks 0FN3, first conclusion, for the canonical direct images. For a commutative square of ringed topoi as in the module docstring — all four functors cocontinuous giving f, f', g, g', the functors v, v' continuous as well as cocontinuous, u' ⋙ v = v' ⋙ u, the comparison functors {}^{u'}_{V'} I ⥤ {}^u_{v(V')} I all cofinal, and g^{-1} O_D = O_{D'}, (g')^{-1} O_C = O_{C'} — we have f'_* ∘ (g')^* ≅ g^* ∘ f_* on sheaves of modules.

The direct images of sheaves of modules are the canonical ones: f_* is Stacks.SheafOfModules.pushforwardCocontinuous for the given structure map f^♯ : O_D ⟶ {}_su O_C, and f'_* is the same construction for the structure map (f')^♯ : O_{D'} ⟶ {}_su' O_{C'} that f^♯ induces by restriction along v and base change. For these the linearity hypothesis of Stacks.SheafOfModules.nonempty_inverseImage_comp_cocontinuousPushforward_iso is a theorem, Stacks.SheafOfModules.ranSMul_squareComparison, so no hypothesis beyond the square, the cofinality and the structure map remains, and the isomorphism itself is available: it is the inverse of Stacks.SheafOfModules.squareComparison.

def inverseImageCompCocontinuousPushforwardOfIso
    (fSharp : OD ⟶ (u.sheafPushforwardCocontinuous RingCat.{r} J K).obj OC)
    (hsq : u' ⋙ v = v' ⋙ u)
    (hfinal : ∀ V' : D',
      (CostructuredArrow.map₂ (S := u') (T := V') (U := u) (V := v.obj V') (F := v') (G := v)
        (eqToHom hsq.symm) (𝟙 (v.obj V'))).Final) :
    inverseImage.{v} J' J v' OC ⋙
        (CocontinuousPushforward.of.{v} J' K' u'
          (structureMapSquare (J' := J') (K' := K') fSharp hsq)).functor ≅
      (CocontinuousPushforward.of.{v} J K u fSharp).functor ⋙ inverseImage.{v} K' K v OD

Stacks.SheafOfModules.lowerShriekCompLeftAdjointOfIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekCocontinuousSquare.lean, line 501. The attribute's comment: “second conclusion: g'_! ∘ (f')⁻¹ ≅ f⁻¹ ∘ g_! on sheaves of modules, for a commutative square of ringed topoi whose four functors u, u', v, v' are cocontinuous, with v, v' continuous as well, with the comparison functors of the index categories of Section 00XF cofinal, and with g^{-1} O_D = O_{D'}, (g')^{-1} O_C = O_{C'}. Deduced from the first conclusion by uniqueness of left adjoints, so an isomorphism and not an equality. g_! and g'_! are the lower shriek of Stacks 0797, and f^{-1}, (f')^{-1} the inverse image f^* G = O_C ⊗_{f^{-1}O_D} f^{-1}G of Stacks.SheafOfModules.inverseImageCocontinuous: all four are constructed, none assumed, so the source's condition (1) — a cocontinuous functor giving rise to a morphism of ringed topoi — is a theorem here. The direct images along u and u' are the canonical ones attached to the structure map f^♯ : O_D → {}_su O_C.”.

Stacks 0FN3, second conclusion, for the canonical direct images. In the situation of Stacks.SheafOfModules.inverseImageCompCocontinuousPushforwardOfIso we have g'_! ∘ (f')^{-1} ≅ f^{-1} ∘ g_!. The composite g'_! ∘ (f')^{-1} is left adjoint to f'_* ∘ (g')^* and f^{-1} ∘ g_! is left adjoint to g^* ∘ f_*; by the first conclusion those two right adjoints are isomorphic, so uniqueness of left adjoints identifies the two composites. The left adjoints g_! and g'_! of g^* and (g')^* are the concrete lower shriek of Stacks 0797, and the inverse images f^{-1} and (f')^{-1} of the two canonical direct images along the cocontinuous u and u' — which is condition (1) — are Stacks.SheafOfModules.inverseImageCocontinuous, constructed by Stacks.SheafOfModules.inverseImageCocontinuousAdjunction. All four exist by the UnivLE, HasWeakSheafify and WEqualsLocallyBijective hypotheses of this section.

def lowerShriekCompLeftAdjointOfIso
    (fSharp : OD ⟶ (u.sheafPushforwardCocontinuous RingCat.{r} J K).obj OC)
    (hsq : u' ⋙ v = v' ⋙ u)
    (hfinal : ∀ V' : D',
      (CostructuredArrow.map₂ (S := u') (T := V') (U := u) (V := v.obj V') (F := v') (G := v)
        (eqToHom hsq.symm) (𝟙 (v.obj V'))).Final) :
    (CocontinuousPushforward.of.{v} J' K' u'
          (structureMapSquare (J' := J') (K' := K') fSharp hsq)).functor.leftAdjoint ⋙
        lowerShriek.{v} J' J v' OC ≅
      lowerShriek.{v} K' K v OD ⋙
        (CocontinuousPushforward.of.{v} J K u fSharp).functor.leftAdjoint

Tag 0FN4, a lemma

Tag 0FN4 in the Stacks Project.

Stacks.SheafOfModules.inverseImage_comp_pushforward_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekContinuousSquare.lean, line 139. The attribute's comment: “first conclusion: f'_* ∘ (g')^* = g^* ∘ f_* on sheaves of modules, for a commutative square of ringed topoi whose horizontal functors u, u' are continuous and whose vertical functors v, v' are continuous as well as cocontinuous, with g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}”.

Stacks 0FN4, first conclusion. For a commutative square of ringed topoi as in the module docstring — u, u' continuous giving f, f', the functors v, v' continuous as well as cocontinuous giving g, g', v ⋙ u = u' ⋙ v', and g^{-1} O_D = O_{D'}, (g')^{-1} O_C = O_{C'} — we have f'_* ∘ (g')^* = g^* ∘ f_* on sheaves of modules. Both sides are restriction along one of the two sides of the square together with restriction of scalars along the corresponding composite structure map, and the square says those agree.

theorem inverseImage_comp_pushforward_eq (hsq : v ⋙ u = u' ⋙ v')
    (hcomm : f'Sharp = restrictStructureMap J' J K' K u u' v v' OC OD fSharp hsq) :
    inverseImage.{v} J' J v' OC ⋙ _root_.SheafOfModules.pushforward.{v} f'Sharp =
      _root_.SheafOfModules.pushforward.{v} fSharp ⋙ inverseImage.{v} K' K v OD

Stacks.SheafOfModules.pullbackCompLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LowerShriekContinuousSquare.lean, line 176. The attribute's comment: “second conclusion: g'_! ∘ (f')⁻¹ ≅ f⁻¹ ∘ g_! on sheaves of modules, for a commutative square of ringed topoi whose horizontal functors u, u' are continuous and whose vertical functors v, v' are continuous as well as cocontinuous, with g^{-1} O_D = O_{D'} and (g')^{-1} O_C = O_{C'}; a canonical isomorphism rather than an equality, uniqueness of left adjoints giving no more. g_! and g'_! are the lower shriek of Stacks 0797 and f⁻¹, (f')⁻¹ the pullback of Stacks 03D7; the existence of all four is proved, not assumed.”.

Stacks 0FN4, second conclusion. In the situation of Stacks.SheafOfModules.inverseImage_comp_pushforward_eq we have g'_! ∘ (f')^{-1} ≅ f^{-1} ∘ g_!, where g_! and g'_! are the lower shriek Stacks.SheafOfModules.lowerShriek of Stacks 0797 and f^{-1}, (f')^{-1} are the pullbacks SheafOfModules.pullback of Stacks 03D7. The composite g'_! ∘ (f')^{-1} is left adjoint to f'_* ∘ (g')^* and f^{-1} ∘ g_! is left adjoint to g^* ∘ f_*; by the first conclusion those two right adjoints are the same functor, so uniqueness of left adjoints identifies the two composites.

Nothing beyond the square is assumed: the four adjunctions are Stacks.SheafOfModules.lowerShriekAdjunction of Stacks 0797 and SheafOfModules.pullbackPushforwardAdjunction of Stacks 03D7, which the UnivLE, HasWeakSheafify and WEqualsLocallyBijective hypotheses of this section make available.

def pullbackCompLowerShriekIso (hsq : v ⋙ u = u' ⋙ v')
    (hcomm : f'Sharp = restrictStructureMap J' J K' K u u' v v' OC OD fSharp hsq) :
    _root_.SheafOfModules.pullback.{v} f'Sharp ⋙ lowerShriek.{v} J' J v' OC ≅
      lowerShriek.{v} K' K v OD ⋙ _root_.SheafOfModules.pullback.{v} fSharp

Sources

• Section 18.41, Tag 0796
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.lowerShriek · Stacks.SheafOfModules.lowerShriekAdjunction · AlgebraicGeometry.smallEtaleModuleProjectionAdjunction · Stacks.SheafOfModules.lowerShriekForgetComparison · Stacks.SheafOfModules.lowerShriekForgetComparison_homEquiv · Stacks.SheafOfModules.lowerShriekForget_not_isomorphic · Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_iff · Stacks.SheafOfModules.isIso_lowerShriekForgetComparison_iff_of_isos

Section18.42 Constant sheaves#

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

Tag 093J, a lemma

Tag 093J in the Stacks Project.

Stacks.ConstantSheaf.surjective_constantSections_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafModules.lean, line 288. The attribute's comment: “surjectivity”.

Stacks Tag 093J, surjectivity half. If f : M ⟶ N is a surjection of R-modules then the induced map on the sections over U of the associated constant sheaves is surjective.

theorem surjective_constantSections_map {M N : ModuleCat.{x} R} (f : M ⟶ N)
    (hf : Function.Surjective f.hom) (U : C) :
    Function.Surjective ((constantSections J U).map f).hom

Stacks.ConstantSheaf.injective_constantSections_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafModules.lean, line 323. The attribute's comment: “injectivity”.

Stacks Tag 093J, injectivity half. constantSections takes injections of modules to injections.

theorem injective_constantSections_map {M N : ModuleCat.{x} R} (f : M ⟶ N)
    (hf : Function.Injective f.hom) (U : C) :
    Function.Injective ((constantSections J U).map f).hom

Stacks.ConstantSheaf.range_constantSections_map_eq_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafModules.lean, line 388.

Stacks Tag 093J. The functor of sections of a constant sheaf of modules is exact: an exact pair of morphisms of R-modules is taken to an exact pair.

theorem range_constantSections_map_eq_ker (U : C) {A B D : ModuleCat.{x} R}
    (α : A ⟶ B) (β : B ⟶ D) (h : LinearMap.range α.hom = LinearMap.ker β.hom) :
    LinearMap.range ((constantSections J U).map α).hom =
      LinearMap.ker ((constantSections J U).map β).hom

constantSheaf_shortExact_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Sheafification/ConstantAbelianSheaf.lean, line 174. References: EGA 0 (12.1.3), “special case”; EGA IV (10.2.8), “special case”.

(1) Exactness as abelian sheaves.

Given a short exact sequence 0 → A → B → C → 0 of abelian groups (a short complex S with S.ShortExact), applying the constant sheaf functor yields a short exact sequence of abelian sheaves 0 → A → B → C → 0 on the site C.

theorem constantSheaf_shortExact_of_shortExact
    (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) :
    (S.map (constantSheaf J AddCommGrpCat.{u})).ShortExact

constantSheaf_sections_shortExact_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Sheafification/ConstantAbelianSheaf.lean, line 279.

(2) Exactness as abelian presheaves.

The same induced sequence of constant sheaves is exact as a sequence of abelian presheaves: for every object U of C, the sequence of abelian groups obtained by taking sections over U is short exact. In particular B → C is objectwise surjective on sections.

theorem constantSheaf_sections_shortExact_of_shortExact
    (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (U : C) :
    ((S.map (constantSheaf J AddCommGrpCat.{u})).map
        ((sheafSections J AddCommGrpCat.{u}).obj (op U))).ShortExact

Tag 093K, a lemma

Tag 093K in the Stacks Project.

Stacks.ConstantSheaf.bijective_tensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafModules.lean, line 560.

Stacks Tag 093K. Tensoring with a finitely presented external module commutes with taking sections of a constant sheaf: the canonical comparison is bijective.

theorem bijective_tensorComparison (M : ModuleCat.{x} R) (Q : ModuleCat.{y} R)
    [Module.FinitePresentation R Q] (N : ModuleCat.{x} R)
    (e : TensorProduct R M Q ≃ₗ[R] N) (U : C) :
    Function.Bijective (tensorComparison J M Q N e U).1

Tag 093L, a lemma

Tag 093L in the Stacks Project.

Stacks.ConstantSheaf.flat_constantSections, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafModules.lean, line 709.

Stacks Tag 093L. On every object of a site, the sections of the constant sheaf associated to a flat module over a coherent ring form a flat module.

instance flat_constantSections [IsCoherentRing R] (M : ModuleCat.{x} R) [Module.Flat R M]
    (U : C) : Module.Flat R ((constantSections J U).obj M)

Tag 093M, a lemma

Tag 093M in the Stacks Project.

Stacks.ConstantSheaf.completedConstantSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletion.lean, line 126. The attribute's comment: “the completed constant sheaf lim (R/Iⁿ)̲”.

The completed constant sheaf R̲^∧ = lim (R/Iⁿ)̲.

noncomputable def completedConstantSheaf : Sheaf J (ModuleCat.{w} R)

Stacks.ConstantSheaf.completedConstantSheafStructureMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletion.lean, line 141. The attribute's comment: “the canonical map from the constant sheaf to its completion”.

The canonical map R̲ ⟶ R̲^∧ from the constant sheaf to its completion.

noncomputable def completedConstantSheafStructureMap :
    (constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R R) ⟶ completedConstantSheaf J I

Stacks.ConstantSheaf.completedConstantIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletion.lean, line 277. The attribute's comment: “the completed ideal sheaf I̲^∧ = lim (I/Iⁿ)̲”.

The completed constant ideal sheaf I̲^∧ = lim (I/Iⁿ)̲.

noncomputable def completedConstantIdealSheaf : Sheaf J (ModuleCat.{w} R)

Stacks.ConstantSheaf.flat_completedConstantSheaf_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletion.lean, line 384. The attribute's comment: “Γ(U, R̲^∧) is a flat R-module for every U, the first step of the flatness proof”.

On every object of the site the sections of the completed constant sheaf form a flat R-module.

theorem flat_completedConstantSheaf_sections (U : C) :
    Module.Flat R
      (((sheafSections J (ModuleCat.{w} R)).obj (op U)).obj (completedConstantSheaf J I))

Stacks.ConstantSheaf.isFlat_completedConstantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletion.lean, line 420. The attribute's comment: “R̲^∧ is flat over R̲”.

The completed constant sheaf R̲^∧ = lim (R/Iⁿ)̲ is flat over the constant sheaf of rings R̲. By Tags 03ES and 03ET this follows from the objectwise flatness of flat_completedConstantSheaf_sections.

theorem isFlat_completedConstantSheaf :
    AlgebraicGeometry.SheafOfModules.IsFlat (completedConstantSheafOverConstantRing J I)

Stacks.ConstantSheaf.constantTensorAction_comp_completedConstantSheafResidueMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionConstantIdealAction.lean, line 234. The attribute's comment: “I̲ Λ̂ ⊂ Δ.

Stacks 093M, the inclusion I̲ · R̲^∧ ⊂ I̲^∧: the canonical map R̲^∧ ⟶ (R/I)̲, read over Osharp, kills the multiplication I̲ ⊗_{Osharp} R̲^∧ ⟶ R̲^∧. Since I̲^∧ is the kernel of that canonical map, this says that the product of the constant sheaf of ideals with the completed constant sheaf is contained in the completed constant ideal sheaf.

The multiplication is killed by any map annihilating every constant multiple, and the residue map is such a map: an element of I acts as zero on (R/I)̲, hence a (m) acts as zero on its bridge.

theorem constantTensorAction_comp_completedConstantSheafResidueMap :
    constantTensorAction J a (ModuleCat.ofHom I.subtype) (completedConstantSheaf J I) ≫
        sheafOfModulesOfConstantRingMap J (associatedRingMap J a)
          (completedConstantSheafResidueMap J I) = 0

Stacks.ConstantSheaf.idealSmulMap_comp_of_constantTensorAction_comp_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionConstantIdealAction.lean, line 264. The attribute's comment: “I Λ̂ ⊂ I̲ Λ̂”.

Stacks 093M, the inclusion I F ⊂ I̲ · F: a map out of F over Osharp which kills the multiplication I̲ ⊗_{Osharp} F ⟶ F also kills the map ∐_{f ∈ I} F ⟶ F of multiplication by the elements of I, whose image is I F.

Multiplying by a single element of I is tested on the images of the sheafification unit, where the multiplication's value is known; the passage from the elements of I to the single map out of the coproduct is the preservation of coproducts by the bridge, read off its adjunction.

theorem idealSmulMap_comp_of_constantTensorAction_comp_eq_zero (F : Sheaf J (ModuleCat.{w} R))
    {Z : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Osharp)}
    (g : (sheafOfModulesOfConstantRingFunctor J (associatedRingMap J a)).obj F ⟶ Z)
    (hg : constantTensorAction J a (ModuleCat.ofHom I.subtype) F ≫ g = 0) :
    (sheafOfModulesOfConstantRingFunctor J (associatedRingMap J a)).map
        (idealSmulMap J I F) ≫ g = 0

Stacks.ConstantSheaf.isColimitCokernelCoforkConstantTensorAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionConstantIdealAction.lean, line 345. The attribute's comment: “Λ̂/I̲ Λ̂ = (Λ/I)̲”.

Stacks 093M, the identification R̲^∧/I̲ · R̲^∧ = (R/I)̲: the canonical map R̲^∧ ⟶ (R/I)̲, read as a map of sheaves of modules over Osharp, is a cokernel of the multiplication I̲ ⊗_{Osharp} R̲^∧ ⟶ R̲^∧ by the constant sheaf of ideals I̲.

A map out of the bridge of R̲^∧ which kills the multiplication kills the multiplications by the elements of I as well, so its transpose across the bridge adjunction factors through (R/I)̲ by the identification R̲^∧/I R̲^∧ = (R/I)̲; transposing back gives the factorisation, which is unique because the canonical map is an epimorphism.

noncomputable def isColimitCokernelCoforkConstantTensorAction :
    IsColimit (CokernelCofork.ofπ
      ((sheafOfModulesOfConstantRingFunctor J (associatedRingMap J a)).map
        (completedConstantSheafResidueMap J I))
      (constantTensorAction_comp_completedConstantSheafResidueMap J a I))

Stacks.ConstantSheaf.completedConstantSheaf_quotientByConstantIdealSmul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionConstantIdealAction.lean, line 393. The attribute's comment: “Λ̂/I̲ Λ̂ = (Λ/I)̲”.

Stacks 093M. The canonical isomorphism R̲^∧/I̲ · R̲^∧ ≅ (R/I)̲ from the quotient of the completed constant sheaf by the product of the constant sheaf of ideals with it to the constant sheaf of the quotient ring, as sheaves of modules over Osharp.

noncomputable def completedConstantSheaf_quotientByConstantIdealSmul :
    cokernel (constantTensorAction J a (ModuleCat.ofHom I.subtype)
        (completedConstantSheaf J I)) ≅
      (sheafOfModulesOfConstantRingFunctor J (associatedRingMap J a)).obj
        ((constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R (R ⧸ I)))

Stacks.ConstantSheaf.completedConstantSheaf_quotientByConstantIdealSmul_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionConstantIdealAction.lean, line 407. The attribute's comment: “Λ̂/I̲ Λ̂ = (Λ/I)̲”.

Stacks 093M. The isomorphism R̲^∧/I̲ · R̲^∧ ≅ (R/I)̲ intertwines the cokernel projection with the canonical map R̲^∧ ⟶ (R/I)̲, so it is the identification of Tag 093M and not a bare existence statement.

theorem completedConstantSheaf_quotientByConstantIdealSmul_hom_comp :
    cokernel.π (constantTensorAction J a (ModuleCat.ofHom I.subtype)
          (completedConstantSheaf J I)) ≫
        (completedConstantSheaf_quotientByConstantIdealSmul J a I).hom =
      (sheafOfModulesOfConstantRingFunctor J (associatedRingMap J a)).map
        (completedConstantSheafResidueMap J I)

Stacks.ConstantSheaf.range_sections_completedConstantIdealSheafInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionIdealAction.lean, line 293. The attribute's comment: “I Λ̂(U) = Î(U) on every object”.

On every object U of the site the sections of the completed constant ideal sheaf inside Γ(U, R̲^∧) are exactly I · Γ(U, R̲^∧).

theorem range_sections_completedConstantIdealSheafInclusion (U : C) :
    LinearMap.range (((sheafSections J (ModuleCat.{w} R)).obj (op U)).map
        (completedConstantIdealSheafInclusion J I)).hom =
      I • (⊤ : Submodule R (((sheafSections J (ModuleCat.{w} R)).obj (op U)).obj
        (completedConstantSheaf J I)))

Stacks.ConstantSheaf.epi_completedConstantIdealSheafLift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionIdealAction.lean, line 363. The attribute's comment: “I Λ̂ = Δ.

The elements of I generate the completed constant ideal sheaf over the completed constant sheaf: the factorisation of ∐_{f ∈ I} R̲^∧ ⟶ R̲^∧ through I̲^∧ is an epimorphism, i.e. I · R̲^∧ = I̲^∧ as subsheaves of R̲^∧.

instance epi_completedConstantIdealSheafLift : Epi (completedConstantIdealSheafLift J I)

Stacks.ConstantSheaf.completedConstantSheaf_quotientByIdealSmul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionIdealAction.lean, line 378. The attribute's comment: “Λ̂/IΛ̂ = (Λ/I)̲”.

The canonical isomorphism R̲^∧/I R̲^∧ ≅ (R/I)̲ from the quotient of the completed constant sheaf by the ideal it is completed at to the constant sheaf of the quotient ring.

noncomputable def completedConstantSheaf_quotientByIdealSmul :
    cokernel (idealSmulMap J I (completedConstantSheaf J I)) ≅
      (constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R (R ⧸ I))

Stacks.ConstantSheaf.completedConstantSheaf_quotientByIdealSmul_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionIdealAction.lean, line 389. The attribute's comment: “Λ̂/IΛ̂ = (Λ/I)̲”.

The isomorphism R̲^∧/I R̲^∧ ≅ (R/I)̲ carries the cokernel projection to the canonical map R̲^∧ ⟶ (R/I)̲.

theorem completedConstantSheaf_quotientByIdealSmul_hom_comp :
    cokernel.π (idealSmulMap J I (completedConstantSheaf J I)) ≫
        (completedConstantSheaf_quotientByIdealSmul J I).hom =
      completedConstantSheafResidueMap J I

Stacks.ConstantSheaf.completedConstantSheafResidueMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionQuotient.lean, line 337. The attribute's comment: “the canonical map from the completion to the constant sheaf of Λ/I”.

The canonical map R̲^∧ ⟶ (R/I)̲ from the completed constant sheaf to the constant sheaf of the quotient ring: the projection to the level n = 1 of the completion, followed by the identification R/I¹ = R/I.

noncomputable def completedConstantSheafResidueMap :
    completedConstantSheaf J I ⟶
      (constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R (R ⧸ I))

Stacks.ConstantSheaf.shortExact_completedConstantIdealShortComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionQuotient.lean, line 514. The attribute's comment: “the completed ideal sheaf is the kernel of the map from the completion to (Λ/I)̲”.

The sequence 0 → I̲^∧ → R̲^∧ → (R/I)̲ → 0 of sheaves of R-modules is short exact.

theorem shortExact_completedConstantIdealShortComplex :
    (completedConstantIdealShortComplex J I).ShortExact

Stacks.ConstantSheaf.completedConstantSheaf_quotientByCompletedIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionQuotient.lean, line 522. The attribute's comment: “Λ̂/Î = (Λ/I)̲”.

The canonical isomorphism R̲^∧/I̲^∧ ≅ (R/I)̲ from the quotient of the completed constant sheaf by the completed constant ideal sheaf to the constant sheaf of the quotient ring.

noncomputable def completedConstantSheaf_quotientByCompletedIdeal :
    cokernel (completedConstantIdealSheafInclusion J I) ≅
      (constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R (R ⧸ I))

Stacks.ConstantSheaf.completedConstantSheaf_quotientByCompletedIdeal_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafCompletionQuotient.lean, line 531. The attribute's comment: “Λ̂/Î = (Λ/I)̲”.

The isomorphism R̲^∧/I̲^∧ ≅ (R/I)̲ intertwines the cokernel projection with the canonical map R̲^∧ ⟶ (R/I)̲.

theorem completedConstantSheaf_quotientByCompletedIdeal_hom_comp :
    cokernel.π (completedConstantIdealSheafInclusion J I) ≫
        (completedConstantSheaf_quotientByCompletedIdeal J I).hom =
      completedConstantSheafResidueMap J I

Stacks.ConstantSheaf.constantSheaf_idealAction_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafQuotient.lean, line 91. The attribute's comment: “sections of the ideal subsheaf”.

The image of the constant ideal sheaf on each object is the ideal acting on sections of the constant ring sheaf.

theorem constantSheaf_idealAction_sections (U : C) :
    LinearMap.range
      ((constantSheaf J (ModuleCat.{w} R) ⋙
        (sheafSections J (ModuleCat.{w} R)).obj (op U)).map
          (ModuleCat.ofHom I.subtype)).hom =
      I • (⊤ : Submodule R
        ((constantSheaf J (ModuleCat.{w} R) ⋙
          (sheafSections J (ModuleCat.{w} R)).obj (op U)).obj (ModuleCat.of R R)))

Stacks.ConstantSheaf.constantSheaf_quotientByConstantIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafQuotient.lean, line 198. The attribute's comment: “quotient by the constant ideal sheaf”.

The canonical isomorphism from the quotient by the constant ideal sheaf to the constant sheaf of the quotient ring.

noncomputable def constantSheaf_quotientByConstantIdeal :
    let f := (constantSheaf J (ModuleCat.{w} R)).map (ModuleCat.ofHom I.subtype)
    cokernel f ≅ (constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R (R ⧸ I))

Stacks.ConstantSheaf.constantSheaf_quotientByConstantIdeal_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafQuotient.lean, line 220. The attribute's comment: “quotient by the constant ideal sheaf”.

The quotient isomorphism intertwines the cokernel projection with the constant sheaf of the ring quotient map.

theorem constantSheaf_quotientByConstantIdeal_hom_comp :
    let f := (constantSheaf J (ModuleCat.{w} R)).map (ModuleCat.ofHom I.subtype)
    cokernel.π f ≫ (constantSheaf_quotientByConstantIdeal J I).hom =
      (constantSheaf J (ModuleCat.{w} R)).map (ModuleCat.ofHom I.mkQ)

Stacks.ConstantSheaf.constantSheaf_quotientByIdealAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafQuotient.lean, line 258. The attribute's comment: “quotient by the ideal subsheaf”.

The canonical isomorphism from the quotient by the image ideal subsheaf, equivalently the ideal generated by I in the constant ring sheaf, to the constant sheaf of the quotient ring.

noncomputable def constantSheaf_quotientByIdealAction :
    let f := (constantSheaf J (ModuleCat.{w} R)).map (ModuleCat.ofHom I.subtype)
    cokernel (image.ι f) ≅
      (constantSheaf J (ModuleCat.{w} R)).obj (ModuleCat.of R (R ⧸ I))

Stacks.ConstantSheaf.constantSheaf_quotientByIdealAction_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafQuotient.lean, line 269. The attribute's comment: “quotient by the ideal subsheaf”.

The image-ideal quotient isomorphism intertwines its quotient projection with the constant sheaf of the ring quotient map.

theorem constantSheaf_quotientByIdealAction_hom_comp :
    let f := (constantSheaf J (ModuleCat.{w} R)).map (ModuleCat.ofHom I.subtype)
    cokernel.π (image.ι f) ≫ (constantSheaf_quotientByIdealAction J I).hom =
      (constantSheaf J (ModuleCat.{w} R)).map (ModuleCat.ofHom I.mkQ)

Tag 093N, a lemma

Tag 093N in the Stacks Project.

Stacks.SheafOfModules.Constant.constantModuleSheaf_isFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafFiniteness.lean, line 870. The attribute's comment: “finite_type”.

Stacks Project, Tag 093N, part (1). On a site whose topos is not empty, a constant sheaf of modules is of finite type if and only if its value is a finitely generated module.

theorem constantModuleSheaf_isFiniteType_iff
    [∀ U : C, HasWeakSheafify (J.over U) AddCommGrpCat.{w}]
    [∀ U : C, (J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (hJ : ∃ U : C, ¬ (⊥ : Sieve U) ∈ J U) (M : ModuleCat.{w} R) :
    SheafOfModules.IsFiniteType (constantModuleSheaf J M) ↔ ModuleCat.isFG R M

Stacks.SheafOfModules.Constant.constantModuleSheaf_isFinitePresentation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafFinitePresentation.lean, line 141. The attribute's comment: “finite_presentation”.

Stacks Project, Tag 093N, part (2). On a site with an object that is not sheaf theoretically empty, a constant sheaf of modules is of finite presentation if and only if its value is a finitely presented module.

theorem constantModuleSheaf_isFinitePresentation_iff
    (hJ : ∃ U : C, ¬ (⊥ : Sieve U) ∈ J U) (M : ModuleCat.{w} R) :
    SheafOfModules.IsFinitePresentation (constantModuleSheaf J M) ↔
      Module.FinitePresentation R M

Sources

• Section 18.42, Tag 093I
• AxiomMath/Stacks at 5ed82d14

LeanStacks.ConstantSheaf.surjective_constantSections_map · Stacks.ConstantSheaf.injective_constantSections_map · Stacks.ConstantSheaf.range_constantSections_map_eq_ker · constantSheaf_shortExact_of_shortExact · constantSheaf_sections_shortExact_of_shortExact · Stacks.ConstantSheaf.bijective_tensorComparison · Stacks.ConstantSheaf.flat_constantSections · Stacks.ConstantSheaf.completedConstantSheaf

Section18.43 Locally constant sheaves#

Section 18.43 of the Stacks Project, Tag 093P. 6 tags here are carried by 34 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 093Q, a definition

Tag 093Q in the Stacks Project.

Stacks.ConstantSheaf.IsLocallyConstant, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/Defs.lean, line 73. The attribute's comment: “part (2)”. References: EGA 0 (3.6.1), “locally simple”; SGA 3 X (9.2.1), “(2), (4)”; SGA 4 IX (2.0), “locally constant”.

Stacks 093Q (2). A sheaf is locally constant if every object of the site has a covering on each member of which its restriction is a constant sheaf.

class IsLocallyConstant [∀ U : C, HasWeakSheafify (J.over U) D] (F : Sheaf J D) : Prop

Stacks.ConstantSheaf.IsFiniteLocallyConstant, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/Defs.lean, line 86. The attribute's comment: “part (3)”.

Stacks 093Q (3). A sheaf with values in a concrete category is finite locally constant if every object of the site has a covering on each member of which it is a constant sheaf with finite underlying value. For Type and Grp, this is respectively the source's notion for sheaves of sets and sheaves of groups.

class IsFiniteLocallyConstant {FD : D → D → Type*} {CD : D → Type w}
    [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD]
    [∀ U : C, HasWeakSheafify (J.over U) D] (F : Sheaf J D) : Prop

Declarations registered for the tag:

• CategoryTheory.Sheaf.IsConstant registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/LocallyConstant/Defs.lean, line 59 (StacksFrontier): “part (1): a constant sheaf is an object in the essential image of the constant sheaf functor”. References: EGA 0 (3.6.1); SGA 4 IV (2.7.5); SGA 4 IV (4.3.4); SGA 4 IX (2.0).

Tag 093R, a lemma

Tag 093R in the Stacks Project.

MorphismOfTopoi.isConstant_inverseImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantPullback/ConstantInverseImage.lean, line 198. The attribute's comment: “constant sheaves of sets, for an arbitrary morphism of topoi”.

Stacks 093R, the constant case. The inverse image of a constant sheaf of sets along a morphism of topoi is constant.

public lemma isConstant_inverseImage (G : Sheaf K (Type w)) [Sheaf.IsConstant K G] :
    Sheaf.IsConstant J (f.inverseImage.obj G)

Stacks.ConstantSheaf.isLocallyConstant_sheafPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantPullback/InverseImageFiniteLocallyConstant.lean, line 420. The attribute's comment: “locally constant sheaves with arbitrary coefficients, for the inverse image along a morphism of sites”.

Tag 093R, for a morphism of sites. The inverse image of a locally constant sheaf along a continuous functor of sites is locally constant, for arbitrary coefficients.

The trivializing covering is taken over the final object of C, whose image is final in D because G is left exact; no object with a final image has to be supplied.

The source states the tag for an arbitrary morphism of topoi, whose inverse image need not be induced by a functor between the two sites; the attribute is qualified accordingly.

public lemma isLocallyConstant_sheafPullback (F : Sheaf J A) [hF : IsLocallyConstant J F] :
    IsLocallyConstant K ((G.sheafPullback A J K).obj F)

Stacks.ConstantSheaf.isFiniteLocallyConstant_sheafPullback_of_coverPreserving, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantPullback/InverseImageFiniteLocallyConstant.lean, line 450. The attribute's comment: “finite locally constant sheaves with arbitrary concrete coefficients, for the inverse image along a morphism of sites”.

Tag 093R. The inverse image of a finite locally constant sheaf along a continuous functor of sites is finite locally constant, for arbitrary concrete coefficients. In particular this holds for sheaves of abelian groups, which is the case Tag 03RZ (2) needs.

One trivializing covering {X i ⟶ ⊤_C} is enough, by Stacks.ConstantSheaf.isFiniteLocallyConstant_of_cover. Its image under G covers G.obj ⊤_C, which is final in D because G is left exact, and on a member the restriction of G^* F is constant with the same finite value, by Stacks.ConstantSheaf.constantIsoOverPullbackSheafPullback.

public lemma isFiniteLocallyConstant_sheafPullback_of_coverPreserving (F : Sheaf J A)
    [hF : IsFiniteLocallyConstant (FD := FA) (CD := CA) J F] :
    IsFiniteLocallyConstant (FD := FA) (CD := CA) K ((G.sheafPullback A J K).obj F)

MorphismOfTopoi.isConstant_abelianInverseImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/AbelianConstantInverseImage.lean, line 213. The attribute's comment: “constant sheaves of abelian groups, for an arbitrary morphism of topoi”.

Stacks 093R, the constant abelian case. The inverse image of a constant sheaf of abelian groups along a morphism of topoi is constant.

public lemma isConstant_abelianInverseImage (G : Sheaf K AddCommGrpCat.{w}) [Sheaf.IsConstant K G] :
    Sheaf.IsConstant J ((CategoryTheory.Sites.abelianInverseImage f).obj G)

MorphismOfTopoi.isFiniteLocallyConstant_abelianInverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/AbelianInverseImageMorphismOfTopoi.lean, line 88. The attribute's comment: “finite locally constant sheaves of abelian groups, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”.

Tag 093R, the finite abelian case. The inverse image of a finite locally constant sheaf of abelian groups along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is finite locally constant.

No functor between the two sites is assumed. Finite local constancy of an abelian sheaf is a property of its underlying sheaf of sets by Stacks.ConstantSheaf.isFiniteLocallyConstant_iff_forget, the underlying sheaf of sets of the abelian inverse image is the geometric inverse image of the underlying sheaf of sets, and the latter preserves finite local constancy by MorphismOfTopoi.isFiniteLocallyConstant_inverseImage_of_smallSites.

public lemma isFiniteLocallyConstant_abelianInverseImage_of_smallSites
    [∀ U : C, HasWeakSheafify (J.over U) AddCommGrpCat.{w}]
    [∀ V : D, HasWeakSheafify (K.over V) AddCommGrpCat.{w}]
    (G : Sheaf K AddCommGrpCat.{w}) [hG : IsFiniteLocallyConstant K G] :
    IsFiniteLocallyConstant J ((CategoryTheory.Sites.abelianInverseImage f).obj G)

MorphismOfTopoi.isLocallyConstant_abelianInverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/AbelianLocallyConstantInverseImage.lean, line 215. The attribute's comment: “locally constant sheaves of abelian groups, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”.

Tag 093R for locally constant sheaves of abelian groups. The inverse image of a locally constant sheaf of abelian groups along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is locally constant.

No functor between the two sites, no final object in either, and no finiteness of the local values is assumed. The covering of an object U of C is the one Stacks.Topos.exists_cover_inverseImage_sections produces for the family of sheaves represented by the objects of D over which G is trivialized as an abelian sheaf, and on a member V of it the section it carries trivializes the abelian inverse image over V, with the same trivializing group, by MorphismOfTopoi.abelianConstantIsoOverPullbackInverseImageOfSection.

public lemma isLocallyConstant_abelianInverseImage_of_smallSites
    (G : Sheaf K AddCommGrpCat.{w}) [hG : IsLocallyConstant K G] :
    IsLocallyConstant J ((CategoryTheory.Sites.abelianInverseImage f).obj G)

MorphismOfTopoi.isLocallyConstant_grpInverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/GrpLocallyConstantInverseImage.lean, line 211. The attribute's comment: “locally constant sheaves of groups, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”.

Tag 093R for locally constant sheaves of groups. The inverse image of a locally constant sheaf of groups along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is locally constant.

No functor between the two sites, no final object in either, no commutativity of the local values and no finiteness of them is assumed. The covering of an object U of C is the one Stacks.Topos.exists_cover_inverseImage_sections produces for the family of sheaves represented by the objects of D over which G is trivialized as a sheaf of groups, and on a member V of it the section it carries trivializes the inverse image over V, with the same trivializing group, by MorphismOfTopoi.grpConstantIsoOverPullbackInverseImageOfSection.

public lemma isLocallyConstant_grpInverseImage_of_smallSites
    (G : Sheaf K GrpCat.{w}) [hG : IsLocallyConstant K G] :
    IsLocallyConstant J ((CategoryTheory.Sites.grpInverseImage f).obj G)

MorphismOfTopoi.isLocallyConstant_moduleInverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/ModuleLocallyConstantInverseImage.lean, line 435. The attribute's comment: “locally constant sheaves of modules over a fixed ring, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”.

Tag 093R for locally constant sheaves of modules over a fixed ring. The inverse image of a locally constant sheaf of Λ-modules along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is locally constant.

No functor between the two sites, no final object in either, no commutativity of Λ and no finiteness of the local values is assumed. The covering of an object U of C is the one Stacks.Topos.exists_cover_inverseImage_sections produces for the family of sheaves represented by the objects of D over which G is trivialized as a sheaf of Λ-modules, and on a member V of it the section it carries trivializes the inverse image over V, with the same trivializing module, by MorphismOfTopoi.moduleConstantIsoOverPullbackInverseImageOfSection.

public lemma isLocallyConstant_moduleInverseImage_of_smallSites (Λ : Type r) [Ring Λ]
    (G : Sheaf K (ModuleCat.{w} Λ)) [hG : IsLocallyConstant K G] :
    IsLocallyConstant J ((CategoryTheory.Sites.moduleInverseImage f Λ).obj G)

MorphismOfTopoi.isLocallyConstant_inverseImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/MorphismOfTopoiPullback.lean, line 168. The attribute's comment: “locally constant sheaves of sets, for a morphism of topoi equipped with a localization datum along a functor of sites”.

Tag 093R. The inverse image of a locally constant sheaf of sets along a morphism of topoi which is equipped with a localization datum is locally constant.

A trivializing covering of the distinguished object of the target site is carried forward by cover preservation to a covering of a final object of the source site, which is enough for local constancy there (Stacks.ConstantSheaf.isLocallyConstant_of_cover), and on a member the restriction of f⁻¹G is constant by MorphismOfTopoi.LocalizationDatum.isConstant_overPullback_inverseImage.

public lemma isLocallyConstant_inverseImage (d : LocalizationDatum f) (G : Sheaf K (Type w))
    [hG : IsLocallyConstant K G] : IsLocallyConstant J (f.inverseImage.obj G)

MorphismOfTopoi.isFiniteLocallyConstant_inverseImage, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/MorphismOfTopoiPullback.lean, line 184. The attribute's comment: “finite locally constant sheaves of sets, for a morphism of topoi equipped with a localization datum along a functor of sites”.

Tag 093R. The inverse image of a finite locally constant sheaf of sets along a morphism of topoi which is equipped with a localization datum is finite locally constant.

The constant values are unchanged by MorphismOfTopoi.LocalizationDatum.constantIsoOverPullbackInverseImage, so their finiteness needs no argument.

public lemma isFiniteLocallyConstant_inverseImage {FA : Type w → Type w → Type*}
    {CA : Type w → Type wc} [∀ P Q, FunLike (FA P Q) (CA P) (CA Q)]
    [ConcreteCategory.{wc} (Type w) FA]
    (d : LocalizationDatum f) (G : Sheaf K (Type w))
    [hG : IsFiniteLocallyConstant (FD := FA) (CD := CA) K G] :
    IsFiniteLocallyConstant (FD := FA) (CD := CA) J (f.inverseImage.obj G)

MorphismOfTopoi.isLocallyConstant_inverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/MorphismOfTopoiSectionRelocalization.lean, line 264. The attribute's comment: “locally constant sheaves of sets, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”. References: SGA 3 X (9.2.1), “(4)”.

Tag 093R. The inverse image of a locally constant sheaf of sets along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is locally constant.

No functor between the two sites, and no final object in either, is assumed: the covering of an object U of C is the one Stacks.Topos.exists_cover_inverseImage_sections produces for the family of sheaves represented by the objects over which G is trivialized, and on a member of it the section it carries trivializes (f⁻¹G)|_V by MorphismOfTopoi.constantIsoOverPullbackInverseImageOfSection.

public lemma isLocallyConstant_inverseImage_of_smallSites (G : Sheaf K (Type w))
    [hG : IsLocallyConstant K G] : IsLocallyConstant J (f.inverseImage.obj G)

MorphismOfTopoi.isFiniteLocallyConstant_inverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/MorphismOfTopoiSectionRelocalization.lean, line 294. The attribute's comment: “finite locally constant sheaves of sets, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”.

Tag 093R. The inverse image of a finite locally constant sheaf of sets along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is finite locally constant.

The constant values are unchanged by MorphismOfTopoi.constantIsoOverPullbackInverseImageOfSection, so their finiteness needs no argument; the covering is the one of MorphismOfTopoi.isLocallyConstant_inverseImage_of_smallSites, taken for the objects over which G becomes constant with a finite value.

public lemma isFiniteLocallyConstant_inverseImage_of_smallSites {FA : Type w → Type w → Type*}
    {CA : Type w → Type wc} [∀ P Q, FunLike (FA P Q) (CA P) (CA Q)]
    [ConcreteCategory.{wc} (Type w) FA] (G : Sheaf K (Type w))
    [hG : IsFiniteLocallyConstant (FD := FA) (CD := CA) K G] :
    IsFiniteLocallyConstant (FD := FA) (CD := CA) J (f.inverseImage.obj G)

MorphismOfTopoi.isLocallyConstant_ringInverseImage_of_smallSites, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/RingLocallyConstantInverseImage.lean, line 209. The attribute's comment: “locally constant sheaves of rings, for an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites”.

Tag 093R for locally constant sheaves of rings. The inverse image of a locally constant sheaf of rings along an arbitrary morphism of topoi between the topoi of sheaves of sets on two small sites is locally constant.

No functor between the two sites, no final object in either, no commutativity of the local values and no finiteness of them is assumed. The covering of an object U of C is the one Stacks.Topos.exists_cover_inverseImage_sections produces for the family of sheaves represented by the objects of D over which G is trivialized as a sheaf of rings, and on a member V of it the section it carries trivializes the inverse image over V, with the same trivializing ring, by MorphismOfTopoi.ringConstantIsoOverPullbackInverseImageOfSection.

public lemma isLocallyConstant_ringInverseImage_of_smallSites
    (G : Sheaf K RingCat.{w}) [hG : IsLocallyConstant K G] :
    IsLocallyConstant J ((CategoryTheory.Sites.ringInverseImage f).obj G)

Tag 093S, a lemma

Tag 093S in the Stacks Project.

Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_abelian, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantAbelian/Morphisms.lean, line 358. The attribute's comment: “part (2), sheaves of abelian groups; assumes pointwise right Kan extensions along the localization functors, a limit-existence side condition implied by fibre products in the site”. References: SGA 4 IX (2.1), “(ii) map, abelian”.

A morphism of locally constant sheaves of abelian groups whose source is finite locally constant is, on a covering of any object, obtained from a homomorphism of abelian groups.

lemma exists_cover_restrict_eq_constantSheaf_map_abelian
    (F G : Sheaf J Ab.{w}) (φ : F ⟶ G)
    [hF : IsFiniteLocallyConstant J F] [hG : IsLocallyConstant J G] (U : C) :
    ∃ (I : Type (max u v)) (X : I → C) (f : ∀ i, X i ⟶ U),
      Sieve.ofArrows X f ∈ J U ∧ ∀ i,
        ∃ (A B : Ab.{w}), Finite (A : Type w) ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf (J.over (X i)) Ab.{w}).obj A ≅
              (J.overPullback Ab.{w} (X i)).obj F)
            (eG : (constantSheaf (J.over (X i)) Ab.{w}).obj B ≅
              (J.overPullback Ab.{w} (X i)).obj G),
              (constantSheaf (J.over (X i)) Ab.{w}).map g ≫ eG.hom =
                eF.hom ≫ (J.overPullback Ab.{w} (X i)).map φ

Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_abelian_smallSite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantAbelian/Morphisms.lean, line 392. The attribute's comment: “part (2), sheaves of abelian groups”. References: SGA 4 IX (2.1), “(ii) map, abelian”.

On a small site C : Type u, with the abelian groups in the universe u, a morphism of locally constant sheaves of abelian groups whose source is finite locally constant is, on a covering of any object, obtained from a homomorphism of abelian groups.

lemma exists_cover_restrict_eq_constantSheaf_map_abelian_smallSite
    {C : Type u} [SmallCategory C] (J : GrothendieckTopology C)
    (F G : Sheaf J Ab.{u}) (φ : F ⟶ G)
    [IsFiniteLocallyConstant J F] [IsLocallyConstant J G] (U : C) :
    ∃ (I : Type u) (X : I → C) (f : ∀ i, X i ⟶ U),
      Sieve.ofArrows X f ∈ J U ∧ ∀ i,
        ∃ (A B : Ab.{u}), Finite (A : Type u) ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf (J.over (X i)) Ab.{u}).obj A ≅
              (J.overPullback Ab.{u} (X i)).obj F)
            (eG : (constantSheaf (J.over (X i)) Ab.{u}).obj B ≅
              (J.overPullback Ab.{u} (X i)).obj G),
              (constantSheaf (J.over (X i)) Ab.{u}).map g ≫ eG.hom =
                eF.hom ≫ (J.overPullback Ab.{u} (X i)).map φ

Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_modules, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantModules/Morphisms.lean, line 477. The attribute's comment: “part (3), sheaves of Λ-modules, with of finite type in the equivalent locally-constant-with-finitely-generated-values form of Tag 093N; assumes pointwise right Kan extensions along the localization functors, a limit-existence side condition implied by fibre products in the site”. References: SGA 4 IX (2.1).

Stacks 093S (3). A morphism of locally constant sheaves of R-modules whose source is locally constant of finite type is, on a covering of any object, obtained from a homomorphism of R-modules.

Carries one hypothesis the source does not state: the family of pointwise right Kan extensions along (Over.map t).op out of which Stacks.ConstantSheaf.constantSheafOverMapIso is built. It is a limit-existence side condition on the coefficient category, implied both by UnivLE.{max u v, w} and by fibre products in the site; see this file's implementation notes, and Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_modules_of_hasPullbacks for the form carrying no universe condition at all. Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_modules_smallSite is the form on a small site, where that side condition is a theorem rather than a hypothesis, and is what part (3) of the tag is registered on.

lemma exists_cover_restrict_eq_constantSheaf_map_modules
    (F G : Sheaf J (ModuleCat.{w} R)) (φ : F ⟶ G)
    (hF : IsFiniteTypeLocallyConstant R J F) [hG : IsLocallyConstant J G] (U : C) :
    ∃ (I : Type (max u v)) (X : I → C) (f : ∀ i, X i ⟶ U),
      Sieve.ofArrows X f ∈ J U ∧ ∀ i,
        ∃ (A B : ModuleCat.{w} R), ModuleCat.isFG R A ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf (J.over (X i)) (ModuleCat.{w} R)).obj A ≅
              (J.overPullback (ModuleCat.{w} R) (X i)).obj F)
            (eG : (constantSheaf (J.over (X i)) (ModuleCat.{w} R)).obj B ≅
              (J.overPullback (ModuleCat.{w} R) (X i)).obj G),
              (constantSheaf (J.over (X i)) (ModuleCat.{w} R)).map g ≫ eG.hom =
                eF.hom ≫ (J.overPullback (ModuleCat.{w} R) (X i)).map φ

Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_modules_smallSite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantModules/Morphisms.lean, line 542. The attribute's comment: “part (3), sheaves of Λ-modules, with of finite type in the equivalent locally-constant-with-finitely-generated-values form of Tag 093N”. References: SGA 4 IX (2.1).

Stacks 093S (3). A morphism of locally constant sheaves of R-modules whose source is locally constant of finite type is, on a covering of any object, obtained from a homomorphism of R-modules.

Stated on a small site, C : Type u with SmallCategory C and the modules in the same universe, which is the setting of the source and this library's convention for a small site. In it the statement carries no hypothesis beyond the source's: the pointwise right Kan extensions along the localization functors (Over.map t).op, which Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map_modules takes as an input, are limits over u-small index categories and so exist in ModuleCat.{u} R by ModuleCat.hasLimitsOfShape; sheafification on each localized site is automatic for the same reason. Neither UnivLE nor fibre products in the site are needed.

lemma exists_cover_restrict_eq_constantSheaf_map_modules_smallSite
    {R : Type r} [Ring R] {C : Type u} [SmallCategory C] (J : GrothendieckTopology C)
    (F G : Sheaf J (ModuleCat.{u} R)) (φ : F ⟶ G)
    (hF : IsFiniteTypeLocallyConstant R J F) [IsLocallyConstant J G] (U : C) :
    ∃ (I : Type u) (X : I → C) (f : ∀ i, X i ⟶ U),
      Sieve.ofArrows X f ∈ J U ∧ ∀ i,
        ∃ (A B : ModuleCat.{u} R), ModuleCat.isFG R A ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf (J.over (X i)) (ModuleCat.{u} R)).obj A ≅
              (J.overPullback (ModuleCat.{u} R) (X i)).obj F)
            (eG : (constantSheaf (J.over (X i)) (ModuleCat.{u} R)).obj B ≅
              (J.overPullback (ModuleCat.{u} R) (X i)).obj G),
              (constantSheaf (J.over (X i)) (ModuleCat.{u} R)).map g ≫ eG.hom =
                eF.hom ≫ (J.overPullback (ModuleCat.{u} R) (X i)).map φ

Stacks.ConstantSheaf.exists_cover_restrict_eq_constantSheaf_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/Morphisms.lean, line 533. The attribute's comment: “sets”. References: SGA 4 IX (2.1), “(i)”.

A morphism of locally constant sheaves of sets whose source is finite locally constant is, on a covering of any object, obtained from a map of sets.

lemma exists_cover_restrict_eq_constantSheaf_map
    (F G : Sheaf J (Type w)) (φ : F ⟶ G)
    [IsFiniteLocallyConstant J F] [IsLocallyConstant J G] (U : C) :
    ∃ (I : Type (max u v)) (X : I → C) (f : ∀ i, X i ⟶ U),
      Sieve.ofArrows X f ∈ J U ∧ ∀ i,
        ∃ (A B : Type w), Finite A ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf (J.over (X i)) (Type w)).obj A ≅
              (J.overPullback (Type w) (X i)).obj F)
            (eG : (constantSheaf (J.over (X i)) (Type w)).obj B ≅
              (J.overPullback (Type w) (X i)).obj G),
              (constantSheaf (J.over (X i)) (Type w)).map g ≫ eG.hom =
                eF.hom ≫ (J.overPullback (Type w) (X i)).map φ

Tag 093T, a lemma

Tag 093T in the Stacks Project.

Stacks.ConstantSheaf.constantSheafHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafHom.lean, line 533. The attribute's comment: “constant_hom”.

Stacks Project, Tag 093T (1). For a finitely presented Λ-module M and any Λ-module N, the constant sheaf on Hom_Λ(M, N) is the internal hom of the constant sheaves on M and on N: Hom_Λ(M, N)̲ ≅ SheafHom_{Λ̲}(M̲, N̲), as sheaves of Λ-modules. The module E is any representative of Hom_Λ(M, N), supplied with the identification e.

noncomputable def constantSheafHomIso
    [Module.FinitePresentation Λ (M : Type (max u v x))] :
    (constantSheaf J (ModuleCat.{max u v x} Λ)).obj E ≅
      moduleSheafHom J Λ ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj M)
        ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj N)

Stacks.ConstantSheaf.constantSheafHomIso_hom_app_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafHom.lean, line 548. The attribute's comment: “constant_hom”. References: SGA 3 VIII (1.4), “partial”.

Stacks Project, Tag 093T (1), the comparison is the canonical one. The section of the internal hom over X which the isomorphism assigns to the constant section determined by a homomorphism f : M ⟶ N is the restriction to the slice site C/X of the morphism of constant sheaves induced by f.

theorem constantSheafHomIso_hom_app_apply
    [Module.FinitePresentation Λ (M : Type (max u v x))] (X : Cᵒᵖ) (f : M ⟶ N) :
    ((constantSheafHomIso J Λ M N E e).hom.hom.app X).hom
        (((constantUnit J Λ E).app X).hom (e (ModuleCat.homLinearEquiv (S := Λ) f))) =
      (J.overPullback (ModuleCat.{max u v x} Λ) X.unop).map
        ((constantSheaf J (ModuleCat.{max u v x} Λ)).map f)

Stacks.ConstantSheaf.constantSheafHomIso_hom_app_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafHom.lean, line 592. The attribute's comment: “constant_hom”.

Stacks Project, Tag 093T (1), applied to the identity: the comparison sends the constant section given by 𝟙 M to the identity on every slice.

theorem constantSheafHomIso_hom_app_id
    [Module.FinitePresentation Λ (M : Type (max u v x))] (E' : ModuleCat.{max u v x} Λ)
    (e' : ((M : Type (max u v x)) →ₗ[Λ] (M : Type (max u v x))) ≃ₗ[Λ] E') (X : Cᵒᵖ) :
    ((constantSheafHomIso J Λ M M E' e').hom.hom.app X).hom
        (((constantUnit J Λ E').app X).hom (e' (ModuleCat.homLinearEquiv (S := Λ) (𝟙 M)))) =
      𝟙 ((J.overPullback (ModuleCat.{max u v x} Λ) X.unop).obj
        ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj M))

Stacks.ConstantSheaf.constantSheafHomIso_hom_app_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafHom.lean, line 605. The attribute's comment: “constant_hom”.

Stacks Project, Tag 093T (1), applied to a composition: the comparison respects composition of constant homomorphisms on every slice.

theorem constantSheafHomIso_hom_app_comp
    [Module.FinitePresentation Λ (M : Type (max u v x))]
    [Module.FinitePresentation Λ (N : Type (max u v x))] (P : ModuleCat.{max u v x} Λ)
    (E₁ E₂ : ModuleCat.{max u v x} Λ)
    (e₁ : ((N : Type (max u v x)) →ₗ[Λ] (P : Type (max u v x))) ≃ₗ[Λ] E₁)
    (e₂ : ((M : Type (max u v x)) →ₗ[Λ] (P : Type (max u v x))) ≃ₗ[Λ] E₂)
    (X : Cᵒᵖ) (f : M ⟶ N) (g : N ⟶ P) :
    ((constantSheafHomIso J Λ M P E₂ e₂).hom.hom.app X).hom
        (((constantUnit J Λ E₂).app X).hom
          (e₂ (ModuleCat.homLinearEquiv (S := Λ) (f ≫ g)))) =
      ((constantSheafHomIso J Λ M N E e).hom.hom.app X).hom
          (((constantUnit J Λ E).app X).hom (e (ModuleCat.homLinearEquiv (S := Λ) f))) ≫
        ((constantSheafHomIso J Λ N P E₁ e₁).hom.hom.app X).hom
          (((constantUnit J Λ E₁).app X).hom
            (e₁ (ModuleCat.homLinearEquiv (S := Λ) g)))

Stacks.ConstantSheaf.constantSheafHomIsoOfHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafHom.lean, line 637. The attribute's comment: “constant_hom”.

Stacks Project, Tag 093T (1), with Hom_Λ(M, N) represented by the morphism type of the category of Λ-modules rather than by an abstract representative.

noncomputable def constantSheafHomIsoOfHom (M N : ModuleCat.{max u v x} Λ)
    [Module.FinitePresentation Λ (M : Type (max u v x))] :
    (constantSheaf J (ModuleCat.{max u v x} Λ)).obj (ModuleCat.of Λ (M ⟶ N)) ≅
      moduleSheafHom J Λ ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj M)
        ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj N)

Stacks.ConstantSheaf.constantSheafIsomHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafIsom.lean, line 412. The attribute's comment: “constant Isom”.

The canonical map of Stacks Tag 093T (2), Isom_Λ(M, N)̲ ⟶ Isom_{Λ̲}(M̲, N̲): the map which sends a linear equivalence to the isomorphism of constant sheaves it induces, factored through the constant sheaf by the universal property of sheafification. That it is an isomorphism, which is the content of part (2), is Stacks.ConstantSheaf.constantSheafIsomIso.

noncomputable def constantSheafIsomHom :
    (constantSheaf J (Type (max u v x))).obj
        ((M : Type (max u v x)) ≃ₗ[Λ] (N : Type (max u v x))) ⟶
      moduleSheafIsom J Λ ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj M)
        ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj N)

Stacks.ConstantSheaf.constantSheafIsomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafIsom.lean, line 464. The attribute's comment: “constant Isom”.

Stacks Project, Tag 093T (2). Isom_Λ(M, N)̲ ≅ Isom_{Λ̲}(M̲, N̲) for finitely presented M and N, as sheaves of sets. The comparison is the canonical one: it sends the constant section given by a linear equivalence e to the restriction of the isomorphism of constant sheaves e̲, which is Stacks.ConstantSheaf.toSheafify_constantSheafIsomHom together with Stacks.ConstantSheaf.constantIsomNatTrans_app_apply.

noncomputable def constantSheafIsomIso
    [Module.FinitePresentation Λ (M : Type (max u v x))]
    [Module.FinitePresentation Λ (N : Type (max u v x))] :
    (constantSheaf J (Type (max u v x))).obj
        ((M : Type (max u v x)) ≃ₗ[Λ] (N : Type (max u v x))) ≅
      moduleSheafIsom J Λ ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj M)
        ((constantSheaf J (ModuleCat.{max u v x} Λ)).obj N)

Stacks.ConstantSheaf.isLocallyConstant_moduleSheafIsom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ConstantSheafIsom.lean, line 616. The attribute's comment: “Isom of locally constant sheaves”.

If F and G are locally constant sheaves of Λ-modules of finite presentation, then Isom_{Λ̲}(F, G) is a locally constant sheaf of sets. The assertion is local on C, so F and G may be trivialized simultaneously; over a member of the resulting covering they are the constant sheaves on finitely presented modules M and N, and then Stacks.ConstantSheaf.constantSheafIsomIso identifies Isom_{Λ̲}(F, G) with the constant sheaf on M ≃ₗ[Λ] N.

theorem isLocallyConstant_moduleSheafIsom (F G : Sheaf J (ModuleCat.{max u v x} Λ))
    (hF : IsFinitePresentationLocallyConstantModuleSheaf J Λ F)
    (hG : IsFinitePresentationLocallyConstantModuleSheaf J Λ G) :
    IsLocallyConstant J (moduleSheafIsom J Λ F G)

Stacks.ConstantSheaf.isLocallyConstant_moduleSheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyConstantSheafHom.lean, line 249. The attribute's comment: “sheafHom of locally constant sheaves”.

Stacks Project, Tag 093T (3). If F is a locally constant sheaf of Λ-modules of finite presentation and G is a locally constant sheaf of Λ-modules, then the internal hom SheafHom_{Λ̲}(F, G) is a locally constant sheaf of Λ-modules.

theorem isLocallyConstant_moduleSheafHom (F G : Sheaf J (ModuleCat.{max u v x} Λ))
    (hF : IsFinitePresentationLocallyConstantModuleSheaf J Λ F) [IsLocallyConstant J G] :
    IsLocallyConstant J (moduleSheafHom J Λ F G)

Stacks.ConstantSheaf.moduleSheafIsom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ModuleSheafIsom.lean, line 235. The attribute's comment: “the sheaf Isom”.

The sheaf of isomorphisms of two sheaves of Λ-modules, i.e. Stacks's Isom_{Λ̲}(F, G): the subsheaf of Stacks.ConstantSheaf.moduleSheafHom of those sections which have an inverse in Stacks.ConstantSheaf.moduleSheafHom taken in the other order. The sections of the internal hom of sheaves of Λ-modules over X are the morphisms F|_X ⟶ G|_X of sheaves of Λ-modules, which are also the sections of CategoryTheory.sheafHom, so this is the subobject Stacks describes.

def moduleSheafIsom (F G : Sheaf J (ModuleCat.{max u v x} Λ)) :
    Sheaf J (Type (max u v x))

Tag 093U, a lemma

Tag 093U in the Stacks Project.

Stacks.ConstantSheaf.isWeakSerreClass_isFiniteTypeLocallyConstantModuleSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyConstantExtensions.lean, line 793. The attribute's comment: “finite_type_modules”. References: SGA 4 IX (2.1), “(ii) ker/coker, (iii)”.

Stacks Tag 093U (3). On a site, the finite type locally constant sheaves of modules over a Noetherian ring form a weak Serre subcategory of the category of sheaves of modules.

The five conditions of Tag 0754 are: strict fullness (Stacks.ConstantSheaf.isClosedUnderIsomorphisms_isFiniteTypeLocallyConstantModuleSheaf), containment of 0 (Stacks.ConstantSheaf.containsZero_isFiniteTypeLocallyConstantModuleSheaf), closure under kernels and under cokernels (Stacks.ConstantSheaf.isClosedUnderKernels_isFiniteTypeLocallyConstantModuleSheaf and Stacks.ConstantSheaf.isClosedUnderCokernels_isFiniteTypeLocallyConstantModuleSheaf), and closure under extensions (Stacks.ConstantSheaf.isClosedUnderExtensions_isFiniteTypeLocallyConstantModuleSheaf).

instance isWeakSerreClass_isFiniteTypeLocallyConstantModuleSheaf :
    ObjectProperty.IsWeakSerreClass
      (IsFiniteTypeLocallyConstantModuleSheaf.{v, u, w} J Λ)

Stacks.ConstantSheaf.isWeakSerreClass_isFiniteLocallyConstantAbelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/AbelianWeakSerre.lean, line 439. The attribute's comment: “finite_abelian”. References: SGA 4 IX (2.1), “(ii) ker/coker, (iii)”.

Stacks Tag 093U (2). On a site, the finite locally constant sheaves of abelian groups form a weak Serre subcategory of the category of all abelian sheaves.

The clause proved here is part (2). It is not an instance of part (3), Stacks.ConstantSheaf.isWeakSerreClass_isFiniteTypeLocallyConstantModuleSheaf: there the finiteness is finiteness of type over a Noetherian coefficient ring, here it is finiteness of the local value itself. Part (3) over ℤ is however what the proof reduces to, together with the local annihilation invariant Stacks.ConstantSheaf.IsLocallyAnnihilated.

theorem isWeakSerreClass_isFiniteLocallyConstantAbelianSheaf :
    (isFiniteLocallyConstantAbelianSheaf.{v, u, w} J).IsWeakSerreClass

Stacks.ConstantSheaf.isClosedUnderFiniteLimits_and_finiteColimits_isFiniteLocallyConstantSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/FiniteLimits.lean, line 743. The attribute's comment: “sets”.

On a site, the finite locally constant sheaves of sets are closed under finite limits and under finite colimits inside the category of all sheaves of sets.

The clause of the tag proved here is part (1), about sheaves of sets whose local constant values are finite sets. It is not an instance of part (3), which is Stacks.ConstantSheaf.isWeakSerreClass_isFiniteTypeLocallyConstantModuleSheaf: there the finiteness is finiteness of type over a Noetherian coefficient ring, here it is finiteness of the local value itself.

theorem isClosedUnderFiniteLimits_and_finiteColimits_isFiniteLocallyConstantSetSheaf :
    ObjectProperty.IsClosedUnderFiniteLimits
        (isFiniteLocallyConstantSetSheaf.{v, u, w} J) ∧
      ObjectProperty.IsClosedUnderFiniteColimits
        (isFiniteLocallyConstantSetSheaf.{v, u, w} J)

Tag 093V, a lemma

Tag 093V in the Stacks Project.

Stacks.ConstantSheaf.isLocallyConstant_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/TensorProduct.lean, line 159. References: SGA 5 VI (1.4.5), “locally constant claim”.

The tensor product of two locally constant sheaves of Λ-modules on a site is a locally constant sheaf of Λ-modules.

theorem isLocallyConstant_tensor (F G : Sheaf J (ModuleCat.{w} Λ))
    [IsLocallyConstant J F] [IsLocallyConstant J G] : IsLocallyConstant J (F ⊗ G)

Sources

• Section 18.43, Tag 093P
• AxiomMath/Stacks at 5ed82d14

LeanStacks.ConstantSheaf.IsLocallyConstant · Stacks.ConstantSheaf.IsFiniteLocallyConstant · CategoryTheory.Sheaf.IsConstant · MorphismOfTopoi.isConstant_inverseImage · Stacks.ConstantSheaf.isLocallyConstant_sheafPullback · Stacks.ConstantSheaf.isFiniteLocallyConstant_sheafPullback_of_coverPreserving · MorphismOfTopoi.isConstant_abelianInverseImage · MorphismOfTopoi.isFiniteLocallyConstant_abelianInverseImage_of_smallSites

Section18.44 Localizing sheaves of rings#

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

Tag 0EMC, a lemma

Tag 0EMC in the Stacks Project.

AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.toLocalizationSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/StructureSheafLocalization.lean, line 110. The attribute's comment: “canonical homomorphism of sheaves of rings”.

The canonical map from the ring sheaf to the sheafified localization.

noncomputable def toLocalizationSheaf (S : MultiplicativeSubpresheaf X)
    [HasWeakSheafify X.J CommRingCat.{w}] :
    X.O ⟶ (presheafToSheaf X.J CommRingCat.{w}).obj S.localizationPresheaf

AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.isUnit_toLocalizationSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/StructureSheafLocalization.lean, line 154. The attribute's comment: “inversion of the prescribed sections”.

The canonical map sends each prescribed section to a unit.

theorem isUnit_toLocalizationSheaf (S : MultiplicativeSubpresheaf X)
    [HasWeakSheafify X.J CommRingCat.{w}]
    (U : X.Cᵒᵖ) (s : S.obj U) :
    IsUnit (((S.toLocalizationSheaf).hom.app U).hom (s : X.O.obj.obj U))

AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.existsUnique_lift_toLocalizationSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/StructureSheafLocalization.lean, line 165. The attribute's comment: “universal property”.

A morphism inverting every prescribed section factors uniquely through the sheafified sectionwise localization.

theorem existsUnique_lift_toLocalizationSheaf (S : MultiplicativeSubpresheaf X)
    [HasWeakSheafify X.J CommRingCat.{w}]
    (A : Sheaf X.J CommRingCat.{w}) (f : X.O ⟶ A)
    (hf : ∀ (U : X.Cᵒᵖ) (s : S.obj U),
      IsUnit ((f.hom.app U).hom (s : X.O.obj.obj U))) :
    ∃! g : (presheafToSheaf X.J CommRingCat.{w}).obj S.localizationPresheaf ⟶ A,
      S.toLocalizationSheaf ≫ g = f

Tag 0EMD, a lemma

Tag 0EMD in the Stacks Project.

AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.existsUnique_lift_localizationModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ModuleSheafLocalization.lean, line 443. The attribute's comment: “localization_universal_property”. References: EGA 0 (1.2.4), “more general”.

The universal property of (S⁻¹F)^#. A map of sheaves of O_X-modules φ : F ⟶ G such that each prescribed local section of S acts invertibly on G factors uniquely through the canonical map F ⟶ (S⁻¹F)^#.

theorem existsUnique_lift_localizationModuleSheaf
    {F G : SheafOfModules.{max w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)} (φ : F ⟶ G)
    (hG : ∀ (U : X.Cᵒᵖ) (s : S.obj U),
      letI : Module (X.O.obj.obj U) (G.val.obj U) := (G.val.obj U).isModule
      Function.Bijective fun t : G.val.obj U ↦ (s : X.O.obj.obj U) • t) :
    ∃! ψ : S.localizationModuleSheaf F ⟶ G, S.toLocalizationModuleSheaf F ≫ ψ = φ

AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.localizationModuleSheafIsoTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ModuleSheafLocalization.lean, line 478. The attribute's comment: “localization_tensor_iso”.

(S⁻¹F)^# = (S⁻¹O_X)^# ⊗_{O_X} F as sheaves of (S⁻¹O_X)^#-modules. The sheafification of the sectionwise localization of F is the extension of scalars of F along O_X ⟶ (S⁻¹O_X)^#.

def localizationModuleSheafIsoTensor
    (F : SheafOfModules.{max w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    (PresheafOfModules.sheafification σ).obj (S.localizationModulePresheaf F.val) ≅
      (SheafOfModules.pullback (S.localizationRingSheafHom σ)).obj F

AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.unit_comp_localizationModuleSheafIsoTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ModuleSheafLocalization.lean, line 489. The attribute's comment: “localization_tensor_iso”.

The identification (S⁻¹F)^# = (S⁻¹O_X)^# ⊗_{O_X} F is compatible with the canonical maps out of F: the unit of the pullback--pushforward adjunction corresponds to the sectionwise localization map followed by the sheafification unit.

theorem unit_comp_localizationModuleSheafIsoTensor
    (F : SheafOfModules.{max w z} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    (SheafOfModules.pullbackPushforwardAdjunction
        (S.localizationRingSheafHom σ)).unit.app F ≫
      (SheafOfModules.pushforward (S.localizationRingSheafHom σ)).map
        (S.localizationModuleSheafIsoTensor σ F).inv =
      toPushforwardSheafification _ σ (changeOfRingsAdjunction S.toLocalizationPresheaf) F

Sources

• Section 18.44, Tag 0EMB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.toLocalizationSheaf · AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.isUnit_toLocalizationSheaf · AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.existsUnique_lift_toLocalizationSheaf · AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.existsUnique_lift_localizationModuleSheaf · AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.localizationModuleSheafIsoTensor · AlgebraicGeometry.RingedSite.MultiplicativeSubpresheaf.unit_comp_localizationModuleSheafIsoTensor

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.