63.2 Growing sections to 63.5 Weightings and trace maps…

Section63.2 Growing sections#

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

Tag 0F6F, a lemma

Tag 0F6F in the Stacks Project.

AlgebraicGeometry.SmallEtale.supportedSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportedSections/ClosedSupportEquiv.lean, line 421. The attribute's comment: “canonical bijection”.

The canonical bijection between sections supported on corresponding closed subschemes of two étale neighborhoods.

public noncomputable def supportedSectionsEquiv
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U U' : SmallEtale B S hS) (φ : U' ⟶ U)
    (Z' : Scheme.{u})
    (i : Z' ⟶ (SmallEtale.toScheme B S hS).obj U')
    [IsClosedImmersion i]
    [IsClosedImmersion (i ≫ (SmallEtale.toScheme B S hS).map φ)] :
    {s : F.obj.obj (op U) //
        supportSection B S hS F U s ⊆
          Set.range (i ≫ (SmallEtale.toScheme B S hS).map φ).base} ≃
      {s' : F.obj.obj (op U') //
        supportSection B S hS F U' s' ⊆
          Set.range i.base}

AlgebraicGeometry.SmallEtale.supportedSectionsEquiv_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportedSections/LocallyClosed.lean, line 70. The attribute's comment: “restriction characterization”.

The canonical bijection is restriction on any étale test object on which the inverse images of the two closed subsets coincide.

public theorem supportedSectionsEquiv_restrict
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U U' : SmallEtale B S hS) (φ : U' ⟶ U)
    (Z' : Scheme.{u})
    (i : Z' ⟶ (SmallEtale.toScheme B S hS).obj U')
    [IsClosedImmersion i]
    [IsClosedImmersion (i ≫ (SmallEtale.toScheme B S hS).map φ)]
    (V : SmallEtale B S hS) (f : V ⟶ U')
    (h : Set.preimage ((SmallEtale.toScheme B S hS).map (f ≫ φ)).base
        (Set.range (i ≫ (SmallEtale.toScheme B S hS).map φ).base) =
      Set.preimage ((SmallEtale.toScheme B S hS).map f).base
        (Set.range i.base))
    (s : {s : F.obj.obj (op U) //
      supportSection B S hS F U s ⊆
        Set.range (i ≫ (SmallEtale.toScheme B S hS).map φ).base}) :
    F.obj.map f.op (supportedSectionsEquiv B S hS F U U' φ Z' i s).val =
      F.obj.map (f ≫ φ).op s.val

AlgebraicGeometry.SmallEtale.locallyClosedSupportEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportedSections/LocallyClosed.lean, line 355. The attribute's comment: “locally closed support”.

The canonical bijection of Tag 0F6G (merged into 0F6F), including its abelian-group structure. Both opens contain the given support as a closed subset.

public noncomputable def locallyClosedSupportEquiv
    (W : SmallEtale B S hS) (Z : Set ((SmallEtale.toScheme B S hS).obj W))
    (U V : ((SmallEtale.toScheme B S hS).obj W).Opens)
    (hZU : Z ⊆ U) (hZV : Z ⊆ V)
    (hUc : IsClosed (U.ι.base ⁻¹' Z)) (hVc : IsClosed (V.ι.base ⁻¹' Z)) :
    supportedSectionsOnOpen B S hS F W Z U ≃+
      supportedSectionsOnOpen B S hS F W Z V

AlgebraicGeometry.SmallEtale.locallyClosedSupportEquiv_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportedSections/LocallyClosed.lean, line 378. The attribute's comment: “locally closed support, restriction”.

For nested opens the canonical identification is restriction.

public theorem locallyClosedSupportEquiv_restrict
    (W : SmallEtale B S hS) (Z : Set ((SmallEtale.toScheme B S hS).obj W))
    (U V : ((SmallEtale.toScheme B S hS).obj W).Opens)
    (hZU : Z ⊆ U) (hZV : Z ⊆ V)
    (hUc : IsClosed (U.ι.base ⁻¹' Z)) (hVc : IsClosed (V.ι.base ⁻¹' Z))
    (h : V ≤ U) (s : supportedSectionsOnOpen B S hS F W Z U) :
    (locallyClosedSupportEquiv B S hS F W Z U V hZU hZV hUc hVc s).val =
      F.obj.map (openObjectHomOfLE B S hS W h).op s.val
Tag 0F6G, a lemma

Tag 0F6G in the Stacks Project.

AlgebraicGeometry.SmallEtale.locallyClosedSupportEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportedSections/LocallyClosed.lean, line 355. The attribute's comment: “the canonical bijection”.

The canonical bijection of Tag 0F6G (merged into 0F6F), including its abelian-group structure. Both opens contain the given support as a closed subset.

public noncomputable def locallyClosedSupportEquiv
    (W : SmallEtale B S hS) (Z : Set ((SmallEtale.toScheme B S hS).obj W))
    (U V : ((SmallEtale.toScheme B S hS).obj W).Opens)
    (hZU : Z ⊆ U) (hZV : Z ⊆ V)
    (hUc : IsClosed (U.ι.base ⁻¹' Z)) (hVc : IsClosed (V.ι.base ⁻¹' Z)) :
    supportedSectionsOnOpen B S hS F W Z U ≃+
      supportedSectionsOnOpen B S hS F W Z V

AlgebraicGeometry.SmallEtale.locallyClosedSupportEquiv_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportedSections/LocallyClosed.lean, line 378. The attribute's comment: “the canonical bijection”.

For nested opens the canonical identification is restriction.

public theorem locallyClosedSupportEquiv_restrict
    (W : SmallEtale B S hS) (Z : Set ((SmallEtale.toScheme B S hS).obj W))
    (U V : ((SmallEtale.toScheme B S hS).obj W).Opens)
    (hZU : Z ⊆ U) (hZV : Z ⊆ V)
    (hUc : IsClosed (U.ι.base ⁻¹' Z)) (hVc : IsClosed (V.ι.base ⁻¹' Z))
    (h : V ≤ U) (s : supportedSectionsOnOpen B S hS F W Z U) :
    (locallyClosedSupportEquiv B S hS F W Z U V hZU hZV hUc hVc s).val =
      F.obj.map (openObjectHomOfLE B S hS W h).op s.val
Sources
LeanAlgebraicGeometry.SmallEtale.supportedSectionsEquiv · AlgebraicGeometry.SmallEtale.supportedSectionsEquiv_restrict · AlgebraicGeometry.SmallEtale.locallyClosedSupportEquiv · AlgebraicGeometry.SmallEtale.locallyClosedSupportEquiv_restrict

Section63.3 Sections with compact support#

Section 63.3 of the Stacks Project, Tag 0F4W. 17 tags here are carried by 44 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0F4X, a lemma

Tag 0F4X in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekSubsheaf.lean, line 152. The attribute's comment: “the proper support condition”.

Stacks 0F4X. The condition that a section of the small-étale direct image of F over an étale test object V ⟶ Y has proper support over V: its support in X ×_Y V is proper over V.

public def properSupportSections (V : SmallEtale B Y.obj Y.property)
    (s : F.obj.obj (op ((smallEtaleBaseChange B f).obj V))) : Prop

AlgebraicGeometry.SmallEtale.properSupportSections_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekSubsheaf.lean, line 211. The attribute's comment: “stability under restriction”.

Stacks 0F4X. The proper-support condition is stable under restriction along an arrow of the small étale site of Y.

public theorem properSupportSections_restrict [LocallyOfFiniteType (B.inclusion.map f)]
    (U V : SmallEtale B Y.obj Y.property) (a : V ⟶ U)
    (s : F.obj.obj (op ((smallEtaleBaseChange B f).obj U)))
    (hs : properSupportSections B f F U s) :
    properSupportSections B f F V (F.obj.map ((smallEtaleBaseChange B f).map a).op s)

AlgebraicGeometry.SmallEtale.properSupportSections_descend, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekSubsheaf.lean, line 251. The attribute's comment: “locality of the proper support condition”.

Stacks 0F4X. The proper-support condition is local for the fpqc topology on the test object.

public theorem properSupportSections_descend [LocallyOfFiniteType (B.inclusion.map f)]
    (V : SmallEtale B Y.obj Y.property)
    (s : F.obj.obj (op ((smallEtaleBaseChange B f).obj V)))
    {ι : Type w} (W : ι → SmallEtale B Y.obj Y.property) (a : ∀ i, W i ⟶ V)
    (hcover : Presieve.ofArrows
      (fun i => (SmallEtale.toScheme B Y.obj Y.property).obj (W i))
      (fun i => (SmallEtale.toScheme B Y.obj Y.property).map (a i)) ∈
        Scheme.fpqcPrecoverage ((SmallEtale.toScheme B Y.obj Y.property).obj V))
    (hloc : ∀ i, properSupportSections B f F (W i)
      (F.obj.map ((smallEtaleBaseChange B f).map (a i)).op s)) :
    properSupportSections B f F V s

AlgebraicGeometry.SmallEtale.fShriekSubsheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekSubsheaf.lean, line 477. References: SGA 4 XVII (6.3.16), “f_! as subsheaf of f_*”; SGA 4 XVII (6.1.2), “abelian sheaves”.

Stacks 0F4X. The abelian subsheaf f_! F of the small-étale direct image f_* F consisting exactly of the sections whose support is proper over the étale base, bundled with the sectionwise description of its image.

public def fShriekSubsheaf [LocallyOfFiniteType (B.inclusion.map f)] :
    {G : MonoOver ((smallEtaleBaseChange B f).sheafPushforwardContinuous
        AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
          (SmallEtale.topology B X.obj X.property) |>.obj F) //
      ∀ (V : SmallEtale B Y.obj Y.property)
        (s : ((smallEtaleBaseChange B f).sheafPushforwardContinuous
          AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
            (SmallEtale.topology B X.obj X.property)).obj F |>.obj.obj (op V)),
          s ∈ Set.range (G.arrow.hom.app (op V)) ↔
            properSupportSections B f F V s}

AlgebraicGeometry.SmallEtale.mem_range_fShriekSubsheaf_arrow_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekSubsheaf.lean, line 511. The attribute's comment: “the sectionwise characterization”.

Stacks 0F4X. The sections of f_! F over an étale test object are exactly the sections of f_* F whose support is proper over that object.

public theorem mem_range_fShriekSubsheaf_arrow_iff [LocallyOfFiniteType (B.inclusion.map f)]
    (V : SmallEtale B Y.obj Y.property)
    (s : (directImageSheaf B f F).obj.obj (op V)) :
    s ∈ Set.range ((fShriekSubsheaf B f F).val.arrow.hom.app (op V)) ↔
      properSupportSections B f F V s
Tag 0F4Y, a lemma

Tag 0F4Y in the Stacks Project.

AlgebraicGeometry.SmallEtale.abelianExtensionByZeroToPushforward_range_eq_fShriekSubsheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekExtensionByZero.lean, line 945.

Stacks 0F4Y. For a separated étale morphism, the image of extension by zero in the direct image is precisely the proper-support subsheaf.

public theorem abelianExtensionByZeroToPushforward_range_eq_fShriekSubsheaf
    (B : BigEtaleSite.{u}) (X : Scheme.{u}) (hX : B.Contains X) (U : SmallEtale B X hX)
    [IsSeparated (B.inclusion.map U.obj.hom)]
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1})
    (V : SmallEtale B X hX) :
    Set.range (((abelianExtensionByZeroToPushforward B X hX U).app F).hom.app (op V)) =
      Set.range (((fShriekSubsheaf B U.obj.hom F).val.arrow).hom.app (op V))
Tag 0F4Z, a definition

Tag 0F4Z in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekSubsheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekSubsheaf.lean, line 477. The attribute's comment: “the subsheaf f_! F of f_ F, the direct image with compact support”. References: SGA 4 XVII (6.3.16), “f_! as subsheaf of f_”; SGA 4 XVII (6.1.2), “abelian sheaves”.

Stacks 0F4X. The abelian subsheaf f_! F of the small-étale direct image f_* F consisting exactly of the sections whose support is proper over the étale base, bundled with the sectionwise description of its image.

public def fShriekSubsheaf [LocallyOfFiniteType (B.inclusion.map f)] :
    {G : MonoOver ((smallEtaleBaseChange B f).sheafPushforwardContinuous
        AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
          (SmallEtale.topology B X.obj X.property) |>.obj F) //
      ∀ (V : SmallEtale B Y.obj Y.property)
        (s : ((smallEtaleBaseChange B f).sheafPushforwardContinuous
          AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
            (SmallEtale.topology B X.obj X.property)).obj F |>.obj.obj (op V)),
          s ∈ Set.range (G.arrow.hom.app (op V)) ↔
            properSupportSections B f F V s}
Tag 0F51, a lemma

Tag 0F51 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportIsoPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 185. The attribute's comment: “natural isomorphism f_! ≅ f_* for proper f”.

For a proper morphism the proper-support direct image is the ordinary direct image, naturally in the abelian étale sheaf.

public def properSupportIsoPushforward [IsProper (B.inclusion.map g)] :
    properSupportFunctor.{u, v} B g ≅ etalePushforward.{u, v} B g

AlgebraicGeometry.SmallEtale.fShriekSubsheaf_arrow_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekProper.lean, line 76.

Stacks 0F51. For a proper morphism, the canonical inclusion of the proper-support direct image f_! F into the ordinary direct image f_* F is an isomorphism.

public theorem fShriekSubsheaf_arrow_isIso [IsProper (B.inclusion.map f)] :
    IsIso ((fShriekSubsheaf B f F).val.arrow)
Tag 0F53, a remark

Tag 0F53 in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekFunctorial.lean, line 65. The attribute's comment: “open_inclusion_compatibility: induced maps”.

The induced map on proper-support direct images, characterized by its inclusion into ordinary direct image.

public noncomputable def fShriekMap
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F H : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (φ : F ⟶ H) :
    let G := (SmallEtale.fShriekSubsheaf B f F).val
    let K := (SmallEtale.fShriekSubsheaf B f H).val
    let push := (smallEtaleBaseChange B f).sheafPushforwardContinuous AddCommGrpCat.{v}
      (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B X.obj X.property)
    {m : G.obj.left ⟶ K.obj.left // m ≫ K.arrow = G.arrow ≫ push.map φ}

AlgebraicGeometry.SmallEtale.fShriekMap_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekFunctorial.lean, line 219. The attribute's comment: “open_inclusion_compatibility: identity”.

The proper-support direct image takes identity morphisms to identities.

public theorem fShriekMap_id
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    (fShriekMap B f F F (𝟙 F)).val = 𝟙 _

AlgebraicGeometry.SmallEtale.fShriekMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekFunctorial.lean, line 236. The attribute's comment: “open_inclusion_compatibility: composition”.

The proper-support direct image respects composition of sheaf morphisms.

public theorem fShriekMap_comp
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F H K : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (φ : F ⟶ H) (ψ : H ⟶ K) :
    (fShriekMap B f F K (φ ≫ ψ)).val =
      (fShriekMap B f F H φ).val ≫ (fShriekMap B f H K ψ).val

AlgebraicGeometry.SmallEtale.openInclusionShriekMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekFunctorial.lean, line 647. The attribute's comment: “open_inclusion_compatibility”.

Extension by zero from an open subscheme is natural in the abelian sheaf.

public theorem openInclusionShriekMap_naturality
    (B : BigEtaleSite.{u}) {X' X Y : B.Scheme}
    (j : X' ⟶ X) (f : X ⟶ Y)
    [IsOpenImmersion (B.inclusion.map j)]
    [IsSeparated (B.inclusion.map f)]
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F H : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (φ : F ⟶ H) :
    letI : LocallyOfFiniteType (B.inclusion.map (j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map j ≫ B.inclusion.map f)
      infer_instance
    let pull := (smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)
    (fShriekMap B (j ≫ f) (pull.obj F) (pull.obj H) (pull.map φ)).val ≫
      (openInclusionShriekMap B j f H).val =
        (openInclusionShriekMap B j f F).val ≫
        (fShriekMap B f F H φ).val

AlgebraicGeometry.SmallEtale.openInclusionShriekMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenInclusion/ShriekMap.lean, line 524. The attribute's comment: “open_inclusion_mono”.

The canonical injection from the proper-support direct image on an open subscheme, with its sectionwise extension-by-zero characterization.

public noncomputable def openInclusionShriekMap
    (B : BigEtaleSite.{u}) {X' X Y : B.Scheme}
    (j : X' ⟶ X) (f : X ⟶ Y)
    [IsOpenImmersion (B.inclusion.map j)]
    [IsSeparated (B.inclusion.map f)]
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    letI : LocallyOfFiniteType (B.inclusion.map (j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map j ≫ B.inclusion.map f)
      infer_instance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    let G' := (SmallEtale.fShriekSubsheaf B (j ≫ f) F').val
    let G := (SmallEtale.fShriekSubsheaf B f F).val
    {α : G'.obj.left ⟶ G.obj.left //
      Mono α ∧
      ∀ (V : SmallEtale B Y.obj Y.property) (a : G'.obj.left.obj.obj (op V)),
        let W := (smallEtaleBaseChange B f).obj V
        let e := (smallEtaleBaseChange_compIso B X' X Y j f).val
        let s := G.arrow.hom.app (op V) (α.hom.app (op V) a)
        let s' := G'.arrow.hom.app (op V) a
        let s'W := F'.obj.map (e.hom.app V).op s'
        (F'.obj.map (e.hom.app V).op s' =
          (((smallEtaleBaseChange B j).sheafAdjunctionContinuous AddCommGrpCat.{v}
            (SmallEtale.topology B X.obj X.property)
            (SmallEtale.topology B X'.obj X'.property)).unit.app F).hom.app (op W) s) ∧
        (SmallEtale.supportSection B X.obj X.property F W s =
          (B.inclusion.map (pullback.fst W.obj.hom j)).base ''
            SmallEtale.supportSection B X'.obj X'.property F'
              ((smallEtaleBaseChange B j).obj W) s'W)}

AlgebraicGeometry.SmallEtale.openInclusionShriekCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenInclusionComp.lean, line 383. The attribute's comment: “open_inclusion_trans”.

Stacks 0F53. Restricting an abelian sheaf to a nested open subscheme in two steps or in one gives canonically isomorphic proper-support direct images.

public noncomputable def openInclusionShriekCompIso
    (B : BigEtaleSite.{u}) {X'' X' X Y : B.Scheme}
    (i : X'' ⟶ X') (j : X' ⟶ X) (f : X ⟶ Y)
    [IsOpenImmersion (B.inclusion.map i)]
    [IsOpenImmersion (B.inclusion.map j)]
    [IsSeparated (B.inclusion.map f)]
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    letI : IsOpenImmersion (B.inclusion.map (i ≫ j)) := by
      change IsOpenImmersion (B.inclusion.map i ≫ B.inclusion.map j)
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map j ≫ B.inclusion.map f)
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (i ≫ j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map i ≫ B.inclusion.map (j ≫ f))
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map ((i ≫ j) ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map (i ≫ j) ≫ B.inclusion.map f)
      infer_instance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    let F'' := ((smallEtaleBaseChange B i).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X'.obj X'.property)
      (SmallEtale.topology B X''.obj X''.property)).obj F'
    let Fd := ((smallEtaleBaseChange B (i ≫ j)).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X''.obj X''.property)).obj F
    (fShriekSubsheaf B (i ≫ j ≫ f) F'').val.obj.left ≅
      (fShriekSubsheaf B ((i ≫ j) ≫ f) Fd).val.obj.left

AlgebraicGeometry.SmallEtale.openInclusionShriekCompIso_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenInclusionComp.lean, line 419. The attribute's comment: “open_inclusion_trans”.

Stacks 0F53. The comparison of proper-support direct images is the comparison of restrictions, read inside the ordinary direct images.

public theorem openInclusionShriekCompIso_ambient
    (B : BigEtaleSite.{u}) {X'' X' X Y : B.Scheme}
    (i : X'' ⟶ X') (j : X' ⟶ X) (f : X ⟶ Y)
    [IsOpenImmersion (B.inclusion.map i)]
    [IsOpenImmersion (B.inclusion.map j)]
    [IsSeparated (B.inclusion.map f)]
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    letI : IsOpenImmersion (B.inclusion.map (i ≫ j)) := by
      change IsOpenImmersion (B.inclusion.map i ≫ B.inclusion.map j)
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map j ≫ B.inclusion.map f)
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (i ≫ j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map i ≫ B.inclusion.map (j ≫ f))
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map ((i ≫ j) ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map (i ≫ j) ≫ B.inclusion.map f)
      infer_instance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    let F'' := ((smallEtaleBaseChange B i).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X'.obj X'.property)
      (SmallEtale.topology B X''.obj X''.property)).obj F'
    let Fd := ((smallEtaleBaseChange B (i ≫ j)).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X''.obj X''.property)).obj F
    let Pi := (smallEtaleBaseChange B (i ≫ j ≫ f)).sheafPushforwardContinuous
      AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B X''.obj X''.property)
    let Pd := (smallEtaleBaseChange B ((i ≫ j) ≫ f)).sheafPushforwardContinuous
      AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B X''.obj X''.property)
    let restrictionIso := (smallEtaleSheafPullbackCompIso B X'' X' X i j
      AddCommGrpCat.{v}).app F
    let pushforwardIso : Pi ≅ Pd :=
      eqToIso (congrArg (fun g : X'' ⟶ Y =>
        (smallEtaleBaseChange B g).sheafPushforwardContinuous
          AddCommGrpCat.{v} (SmallEtale.topology B Y.obj Y.property)
          (SmallEtale.topology B X''.obj X''.property))
        (Category.assoc i j f).symm)
    (openInclusionShriekCompIso B i j f F).hom ≫
        (fShriekSubsheaf B ((i ≫ j) ≫ f) Fd).val.arrow =
      (fShriekSubsheaf B (i ≫ j ≫ f) F'').val.arrow ≫
        (Pi.mapIso restrictionIso ≪≫ pushforwardIso.app Fd).hom

AlgebraicGeometry.SmallEtale.openInclusionShriekMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenInclusionComp.lean, line 478. The attribute's comment: “open_inclusion_trans”.

Stacks 0F53. Extension by zero is transitive: for nested open subschemes X'' ⟶ X' ⟶ X of the source of a separated morphism locally of finite type, the canonical map from the proper-support direct image on X'' is the composite of the two successive canonical maps, once the two proper-support direct images on X'' are identified.

public theorem openInclusionShriekMap_comp
    (B : BigEtaleSite.{u}) {X'' X' X Y : B.Scheme}
    (i : X'' ⟶ X') (j : X' ⟶ X) (f : X ⟶ Y)
    [IsOpenImmersion (B.inclusion.map i)]
    [IsOpenImmersion (B.inclusion.map j)]
    [IsSeparated (B.inclusion.map f)]
    [LocallyOfFiniteType (B.inclusion.map f)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    letI : IsOpenImmersion (B.inclusion.map (i ≫ j)) := by
      change IsOpenImmersion (B.inclusion.map i ≫ B.inclusion.map j)
      infer_instance
    letI : IsSeparated (B.inclusion.map (j ≫ f)) := by
      change IsSeparated (B.inclusion.map j ≫ B.inclusion.map f)
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map j ≫ B.inclusion.map f)
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (i ≫ j ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map i ≫ B.inclusion.map (j ≫ f))
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map ((i ≫ j) ≫ f)) := by
      change LocallyOfFiniteType (B.inclusion.map (i ≫ j) ≫ B.inclusion.map f)
      infer_instance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    (openInclusionShriekCompIso B i j f F).hom ≫
        (openInclusionShriekMap B (i ≫ j) f F).val =
      (openInclusionShriekMap B i (j ≫ f) F').val ≫
        (openInclusionShriekMap B j f F).val
Tag 0F52, a lemma

Tag 0F52 in the Stacks Project.

AlgebraicGeometry.SmallEtale.compactificationProperSupportIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 224. The attribute's comment: “natural isomorphism of proper-support functors”.

The canonical comparison f_! ⟶ f̄_! ∘ j_! of proper-support direct images through a compactification j : X ⟶ X̄ of X over Y, as a natural isomorphism of functors on abelian étale sheaves.

public def compactificationProperSupportIso
    [LocallyOfFiniteType (B.inclusion.map U.obj.hom)] :
    properSupportFunctor.{u, u + 1} B (U.obj.hom ≫ fbar) ≅
      abelianExtensionByZero B Xbar.obj Xbar.property U ⋙
        properSupportFunctor.{u, u + 1} B fbar

AlgebraicGeometry.SmallEtale.fShriekFunctorIsoCompactification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 243. The attribute's comment: “f_! = f̄_* ∘ j_!”.

f_! = f̄_* ∘ j_!: the direct image with compact support along f = j ≫ f̄, for j : X ⟶ X̄ an open immersion and f̄ : X̄ ⟶ Y proper, is extension by zero along j followed by the ordinary direct image along f̄.

public def fShriekFunctorIsoCompactification
    [LocallyQuasiFinite (B.inclusion.map fbar)] :
    fShriekFunctor.{u, u} B (U.obj.hom ≫ fbar) ≅
      abelianExtensionByZero B Xbar.obj Xbar.property U ⋙
        etalePushforward.{u, u + 1} B fbar

AlgebraicGeometry.SmallEtale.compactificationFShriekMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactification.lean, line 322. The attribute's comment: “canonical comparison”.

Stacks 0F52. The canonical map f_! F ⟶ f̄_!(j_! F) for an open immersion j : X ⟶ X̄ with f = j ≫ f̄: the extension-by-zero unit, which identifies F with the restriction of j_! F, followed by the open-inclusion comparison of Stacks 0F53. The subtype records that factorisation, which is what pins the map down.

public noncomputable def compactificationFShriekMap :
    letI : IsSeparated (B.inclusion.map fbar) := inferInstance
    letI : LocallyOfFiniteType (B.inclusion.map fbar) := inferInstance
    letI : LocallyOfFiniteType (B.inclusion.map (U.obj.hom ≫ fbar)) := by
      change LocallyOfFiniteType (B.inclusion.map U.obj.hom ≫ B.inclusion.map fbar)
      infer_instance
    let Fbar := (abelianExtensionByZero B Xbar.obj Xbar.property U).obj F
    let pull := (smallEtaleBaseChange B U.obj.hom).sheafPullback AddCommGrpCat.{u + 1}
      (SmallEtale.topology B Xbar.obj Xbar.property)
      (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
    let push := (smallEtaleBaseChange B (U.obj.hom ≫ fbar)).sheafPushforwardContinuous
      AddCommGrpCat.{u + 1} (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
    let Gsrc := (fShriekSubsheaf B (U.obj.hom ≫ fbar) F).val
    let Gpull := (fShriekSubsheaf B (U.obj.hom ≫ fbar) (pull.obj Fbar)).val
    let Gtgt := (fShriekSubsheaf B fbar Fbar).val
    {α : Gsrc.obj.left ⟶ Gtgt.obj.left //
      ∃ i : Gsrc.obj.left ≅ Gpull.obj.left,
        let unit := (abelianExtensionByZeroAdjunction B Xbar.obj Xbar.property U).unit.app F
        let e := unit ≫ (openRestrictionIso.{u, u} B U.obj.hom).hom.app Fbar
        (i.hom ≫ Gpull.arrow = Gsrc.arrow ≫ push.map e) ∧
        (α = i.hom ≫ (openInclusionShriekMap B U.obj.hom fbar Fbar).val)}

AlgebraicGeometry.SmallEtale.compactificationFShriekMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactification.lean, line 521. The attribute's comment: “isomorphism”.

Stacks 0F52. The canonical compactification comparison is an isomorphism.

public theorem compactificationFShriekMap_isIso :
    IsIso (compactificationFShriekMap B fbar U F).val

AlgebraicGeometry.SmallEtale.compactificationFShriekMap_to_pushforward_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactification.lean, line 581. The attribute's comment: “ordinary direct image”.

Stacks 0F52. Since the compactification is proper, the same canonical map identifies f_! F with the ordinary direct image f̄_*(j_! F).

public theorem compactificationFShriekMap_to_pushforward_isIso :
    letI : LocallyOfFiniteType (B.inclusion.map fbar) := inferInstance
    let Fbar := (abelianExtensionByZero B Xbar.obj Xbar.property U).obj F
    IsIso ((compactificationFShriekMap B fbar U F).val ≫
      (fShriekSubsheaf B fbar Fbar).val.arrow)

AlgebraicGeometry.SmallEtale.compactificationFShriekMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactification.lean, line 597. The attribute's comment: “naturality and functor comparison”.

Stacks 0F52. The compactification comparison commutes with morphisms of abelian étale sheaves, hence identifies the two direct-image functors naturally.

public theorem compactificationFShriekMap_naturality
    (H : Sheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property) AddCommGrpCat.{u + 1})
    (phi : F ⟶ H) :
    letI : IsSeparated (B.inclusion.map fbar) := inferInstance
    letI : LocallyOfFiniteType (B.inclusion.map fbar) := inferInstance
    letI : LocallyOfFiniteType (B.inclusion.map (U.obj.hom ≫ fbar)) := by
      change LocallyOfFiniteType (B.inclusion.map U.obj.hom ≫ B.inclusion.map fbar)
      infer_instance
    let ext := abelianExtensionByZero B Xbar.obj Xbar.property U
    let push := (smallEtaleBaseChange B (U.obj.hom ≫ fbar)).sheafPushforwardContinuous
      AddCommGrpCat.{u + 1} (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
    let pushbar := (smallEtaleBaseChange B fbar).sheafPushforwardContinuous
      AddCommGrpCat.{u + 1} (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B Xbar.obj Xbar.property)
    let GF := (fShriekSubsheaf B (U.obj.hom ≫ fbar) F).val
    let GH := (fShriekSubsheaf B (U.obj.hom ≫ fbar) H).val
    let GbarF := (fShriekSubsheaf B fbar (ext.obj F)).val
    let GbarH := (fShriekSubsheaf B fbar (ext.obj H)).val
    ∀ (a : GF.obj.left ⟶ GH.obj.left) (b : GbarF.obj.left ⟶ GbarH.obj.left),
      (a ≫ GH.arrow = GF.arrow ≫ push.map phi) →
      (b ≫ GbarH.arrow = GbarF.arrow ≫ pushbar.map (ext.map phi)) →
      (a ≫ (compactificationFShriekMap B fbar U H).val =
        (compactificationFShriekMap B fbar U F).val ≫ b)
Tag 0F72, a definition

Tag 0F72 in the Stacks Project.

AlgebraicGeometry.SmallEtale.compactlySupportedSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupport.lean, line 62.

Stacks 0F72. The subgroup of global sections of an abelian sheaf on the small étale site whose support is proper over the base field.

public def compactlySupportedSections :
    AddSubgroup (F.obj.obj (op (SmallEtale.final B X hX)))
Tag 0F73, a lemma

Tag 0F73 in the Stacks Project.

AlgebraicGeometry.SmallEtale.compactlySupportedSections_eq_top_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekProper.lean, line 101.

Stacks 0F73. On a scheme proper over a field, every global section of an abelian sheaf on the small étale site has compact support.

public theorem compactlySupportedSections_eq_top_of_isProper :
    compactlySupportedSections k X f B hX F = ⊤
Tag 0F74, a remark

Tag 0F74 in the Stacks Project.

AlgebraicGeometry.SmallEtale.compactlySupportedSections_openInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpen.lean, line 474. The attribute's comment: “canonical injection”.

Stacks 0F74. Extension by zero gives a canonical injection on compactly supported sections along an open immersion, characterised by the restriction of its value back to the open subscheme and by the equality of supports.

public noncomputable def compactlySupportedSections_openInclusion {X' X : B.Scheme}
    (j : X' ⟶ X) (f : X.obj ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f]
    [IsOpenImmersion (B.inclusion.map j)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    letI : LocallyOfFiniteType (B.inclusion.map j ≫ f) := inferInstance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    {φ : compactlySupportedSections k X'.obj (B.inclusion.map j ≫ f) B X'.property F' →+
        compactlySupportedSections k X.obj f B X.property F //
      Function.Injective φ ∧
      ∀ s, (F'.obj.map ((SmallEtale.finalIsTerminal B X'.obj X'.property).from
            ((smallEtaleBaseChange B j).obj (SmallEtale.final B X.obj X.property))).op s.1 =
          (((smallEtaleBaseChange B j).sheafAdjunctionContinuous AddCommGrpCat.{v}
            (SmallEtale.topology B X.obj X.property)
            (SmallEtale.topology B X'.obj X'.property)).unit.app F).hom.app
              (op (SmallEtale.final B X.obj X.property)) (φ s).1) ∧
        (supportSection B X.obj X.property F (SmallEtale.final B X.obj X.property) (φ s).1 =
          (B.inclusion.map j).base ''
            supportSection B X'.obj X'.property F'
              (SmallEtale.final B X'.obj X'.property) s.1)}

AlgebraicGeometry.SmallEtale.compactlySupportedSections_openInclusion_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpen.lean, line 508. The attribute's comment: “precosheaf identity”.

Stacks 0F74. For the identity open immersion extension by zero is surjective on compactly supported sections, hence an isomorphism: the unit of the restriction adjunction along an identity is an isomorphism, and the characterising restriction equation identifies the injection with it.

public theorem compactlySupportedSections_openInclusion_id (X : B.Scheme)
    (f : X.obj ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    Function.Surjective (compactlySupportedSections_openInclusion k B (𝟙 X) f F).1

AlgebraicGeometry.SmallEtale.compactlySupportedSections_openInclusion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpen.lean, line 632. The attribute's comment: “precosheaf composition”.

Stacks 0F74. Extension by zero on compactly supported sections is transitive for composable open immersions, once the two restrictions of the sheaf to the smallest open subscheme are identified by the canonical comparison of inverse images.

public theorem compactlySupportedSections_openInclusion_comp {X'' X' X : B.Scheme}
    (i : X'' ⟶ X') (j : X' ⟶ X) (f : X.obj ⟶ Spec (.of k))
    [IsSeparated f] [LocallyOfFiniteType f]
    [IsOpenImmersion (B.inclusion.map i)] [IsOpenImmersion (B.inclusion.map j)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v}) :
    letI : IsOpenImmersion (B.inclusion.map (i ≫ j)) := by
      change IsOpenImmersion (B.inclusion.map i ≫ B.inclusion.map j)
      infer_instance
    letI : IsSeparated (B.inclusion.map j ≫ f) := by infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map j ≫ f) := by infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map i ≫ (B.inclusion.map j ≫ f)) := by
      infer_instance
    letI : LocallyOfFiniteType (B.inclusion.map (i ≫ j) ≫ f) := by
      change LocallyOfFiniteType (B.inclusion.map i ≫ B.inclusion.map j ≫ f)
      infer_instance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    let F'' := ((smallEtaleBaseChange B i).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X'.obj X'.property)
      (SmallEtale.topology B X''.obj X''.property)).obj F'
    let Fd := ((smallEtaleBaseChange B (i ≫ j)).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X''.obj X''.property)).obj F
    ∀ (s : compactlySupportedSections k X''.obj (B.inclusion.map i ≫ (B.inclusion.map j ≫ f))
        B X''.property F''),
      ∃ (t : compactlySupportedSections k X''.obj (B.inclusion.map (i ≫ j) ≫ f) B X''.property
        Fd),
        (((smallEtaleSheafPullbackCompIso B X'' X' X i j AddCommGrpCat.{v}).app F).hom.hom.app
            (op (SmallEtale.final B X''.obj X''.property)) s.1 = t.1) ∧
        ((compactlySupportedSections_openInclusion k B j f F).1
          ((compactlySupportedSections_openInclusion k B i (B.inclusion.map j ≫ f) F').1 s) =
          (compactlySupportedSections_openInclusion k B (i ≫ j) f F).1 t)

AlgebraicGeometry.SmallEtale.exists_compactlySupportedSections_openInclusion_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpen.lean, line 906. The attribute's comment: “cosheaf, image of the canonical injection”.

Stacks 0F74. A compactly supported section of F is the extension by zero of a compactly supported section on an open subscheme exactly when its support lies in that open subscheme: this identifies the image of the canonical injection.

public theorem exists_compactlySupportedSections_openInclusion_eq {X' X : B.Scheme}
    (j : X' ⟶ X) (f : X.obj ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f]
    [IsOpenImmersion (B.inclusion.map j)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (t : compactlySupportedSections k X.obj f B X.property F) :
    letI : LocallyOfFiniteType (B.inclusion.map j ≫ f) := inferInstance
    let F' := ((smallEtaleBaseChange B j).sheafPullback AddCommGrpCat.{v}
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X'.obj X'.property)).obj F
    (∃ s : compactlySupportedSections k X'.obj (B.inclusion.map j ≫ f) B X'.property F',
        (compactlySupportedSections_openInclusion k B j f F).1 s = t) ↔
      supportSection B X.obj X.property F (SmallEtale.final B X.obj X.property) t.1 ⊆
        Set.range (B.inclusion.map j).base

AlgebraicGeometry.SmallEtale.exists_compactlySupportedSections_openInclusion_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpen.lean, line 987. The attribute's comment: “cosheaf, Mayer–Vietoris”.

Stacks 0F74. Mayer–Vietoris for compactly supported sections: two compactly supported sections on open subschemes with the same extension by zero both come from a compactly supported section on the intersection of the two open subschemes, an open subscheme X₀ whose image is the intersection of the two images — for instance their fibre product, by AlgebraicGeometry.SmallEtale.range_pullback_fst_comp.

public theorem exists_compactlySupportedSections_openInclusion_inter {X₀ X₁ X₂ X : B.Scheme}
    (j₀ : X₀ ⟶ X) (j₁ : X₁ ⟶ X) (j₂ : X₂ ⟶ X) (f : X.obj ⟶ Spec (.of k))
    [IsSeparated f] [LocallyOfFiniteType f] [IsOpenImmersion (B.inclusion.map j₀)]
    [IsOpenImmersion (B.inclusion.map j₁)] [IsOpenImmersion (B.inclusion.map j₂)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (h₀ : Set.range (B.inclusion.map j₀).base =
      Set.range (B.inclusion.map j₁).base ∩ Set.range (B.inclusion.map j₂).base) :
    ∀ (s₁ : compactlySupportedSections k X₁.obj (B.inclusion.map j₁ ≫ f) B X₁.property
        (((smallEtaleBaseChange B j₁).sheafPullback AddCommGrpCat.{v}
          (SmallEtale.topology B X.obj X.property)
          (SmallEtale.topology B X₁.obj X₁.property)).obj F))
      (s₂ : compactlySupportedSections k X₂.obj (B.inclusion.map j₂ ≫ f) B X₂.property
        (((smallEtaleBaseChange B j₂).sheafPullback AddCommGrpCat.{v}
          (SmallEtale.topology B X.obj X.property)
          (SmallEtale.topology B X₂.obj X₂.property)).obj F)),
      (compactlySupportedSections_openInclusion k B j₁ f F).1 s₁ =
          (compactlySupportedSections_openInclusion k B j₂ f F).1 s₂ →
        ∃ s₀ : compactlySupportedSections k X₀.obj (B.inclusion.map j₀ ≫ f) B X₀.property
            (((smallEtaleBaseChange B j₀).sheafPullback AddCommGrpCat.{v}
              (SmallEtale.topology B X.obj X.property)
              (SmallEtale.topology B X₀.obj X₀.property)).obj F),
          (compactlySupportedSections_openInclusion k B j₀ f F).1 s₀ =
            (compactlySupportedSections_openInclusion k B j₁ f F).1 s₁

AlgebraicGeometry.SmallEtale.exists_compactlySupportedSections_openInclusion_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpen.lean, line 1116. The attribute's comment: “cosheaf, gluing”.

Stacks 0F74. Gluing for compactly supported sections: a compactly supported section whose support is the union of two disjoint closed subsets, one inside each of two open subschemes, is the sum of the extensions by zero of compactly supported sections on those two open subschemes.

public theorem exists_compactlySupportedSections_openInclusion_add {X₁ X₂ X : B.Scheme}
    (j₁ : X₁ ⟶ X) (j₂ : X₂ ⟶ X) (f : X.obj ⟶ Spec (.of k))
    [IsSeparated f] [LocallyOfFiniteType f]
    [IsOpenImmersion (B.inclusion.map j₁)] [IsOpenImmersion (B.inclusion.map j₂)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (t : compactlySupportedSections k X.obj f B X.property F)
    (Z₁ Z₂ : Set ((SmallEtale.toScheme B X.obj X.property).obj
      (SmallEtale.final B X.obj X.property)))
    (hZ₁ : IsClosed Z₁) (hZ₂ : IsClosed Z₂) (hdisj : Disjoint Z₁ Z₂)
    (hsupp : supportSection B X.obj X.property F (SmallEtale.final B X.obj X.property) t.1 =
      Z₁ ∪ Z₂)
    (h₁ : Z₁ ⊆ Set.range (B.inclusion.map j₁).base)
    (h₂ : Z₂ ⊆ Set.range (B.inclusion.map j₂).base) :
    ∃ (s₁ : compactlySupportedSections k X₁.obj (B.inclusion.map j₁ ≫ f) B X₁.property
        (((smallEtaleBaseChange B j₁).sheafPullback AddCommGrpCat.{v}
          (SmallEtale.topology B X.obj X.property)
          (SmallEtale.topology B X₁.obj X₁.property)).obj F))
      (s₂ : compactlySupportedSections k X₂.obj (B.inclusion.map j₂ ≫ f) B X₂.property
        (((smallEtaleBaseChange B j₂).sheafPullback AddCommGrpCat.{v}
          (SmallEtale.topology B X.obj X.property)
          (SmallEtale.topology B X₂.obj X₂.property)).obj F)),
      (compactlySupportedSections_openInclusion k B j₁ f F).1 s₁ +
        (compactlySupportedSections_openInclusion k B j₂ f F).1 s₂ = t

AlgebraicGeometry.SmallEtale.exists_zariskiCovering_not_surjective_compactlySupportedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportOpenNotCosheaf.lean, line 178. The attribute's comment: “the cosheaf condition is false in the literal sense: a Zariski covering of ℙ¹_k by two opens on which the sum map H^0_c(U₁) ⊕ H^0_c(U₂) → H^0_c(ℙ¹_k, 𝔾_a) is not surjective”.

Stacks 0F74, the cosheaf condition fails for an actual Zariski covering. For every field k and every big étale site containing the projective line ℙ¹_k, the scheme ℙ¹_k, separated and of finite type (indeed proper) over k, has a Zariski covering by two open subschemes — the complements of the zero and of the infinity section — and an abelian sheaf on its small étale site — the additive group 𝔾_a — such that the sum of the extension-by-zero maps H^0_c(U₁) ⊕ H^0_c(U₂) → H^0_c(ℙ¹_k) is not surjective. So H^0_c is not a cosheaf on the Zariski site in the literal sense; it is a precosheaf with injective transition maps, see AlgebraicGeometry.SmallEtale.compactlySupportedSections_openInclusion.

public theorem exists_zariskiCovering_not_surjective_compactlySupportedSections
    (hP : B.Contains (Stacks.Chow.relativeProjectiveLine (Spec (.of k)))) :
    ∃ (X X₁ X₂ : B.Scheme) (j₁ : X₁ ⟶ X) (j₂ : X₂ ⟶ X) (f : X.obj ⟶ Spec (.of k))
      (_ : IsProper f) (_ : IsOpenImmersion (B.inclusion.map j₁))
      (_ : IsOpenImmersion (B.inclusion.map j₂)),
      Set.range (B.inclusion.map j₁).base ∪ Set.range (B.inclusion.map j₂).base = Set.univ ∧
      ∃ F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u},
        ¬ Function.Surjective
          ((compactlySupportedSections_openInclusion k B j₁ f F).1.coprod
            (compactlySupportedSections_openInclusion k B j₂ f F).1)
Tag 0F75, a lemma

Tag 0F75 in the Stacks Project.

AlgebraicGeometry.SmallEtale.compactlySupportedSections_extensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportCompactification.lean, line 373. The attribute's comment: “canonical isomorphism”.

Stacks 0F75. For an open immersion j : X ⟶ X̄ with X̄ proper over a field k, the compactly supported global sections of an abelian sheaf F on the small étale site of X are canonically the compactly supported global sections of its extension by zero j_! F on X̄.

public noncomputable def compactlySupportedSections_extensionByZero :
    compactlySupportedSections k U.obj.left.obj (B.inclusion.map U.obj.hom ≫ fbar) B
        U.obj.left.property F ≃+
      compactlySupportedSections k Xbar.obj fbar B Xbar.property
        ((abelianExtensionByZero B Xbar.obj Xbar.property U).obj F)

AlgebraicGeometry.SmallEtale.compactlySupportedSections_extensionByZero_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompactSupportCompactification.lean, line 386. The attribute's comment: “restriction characterization”.

Stacks 0F75. The canonical equivalence is determined by the fact that restriction of the extended section to the open subscheme is the original section, identified through the extension-by-zero adjunction unit.

public theorem compactlySupportedSections_extensionByZero_restrict
    (s : compactlySupportedSections k U.obj.left.obj (B.inclusion.map U.obj.hom ≫ fbar) B
      U.obj.left.property F) :
    ((abelianExtensionByZeroAdjunction B Xbar.obj Xbar.property U).unit.app F).hom.app
        (op (SmallEtale.final B U.obj.left.obj U.obj.left.property)) s.1 =
      ((abelianExtensionByZero B Xbar.obj Xbar.property U).obj F).obj.map
        ((SmallEtale.finalIsTerminal B Xbar.obj Xbar.property).from U).op
        (compactlySupportedSections_extensionByZero k B Xbar fbar U F s).1
Tag 0F76, a lemma

Tag 0F76 in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekStalkEquivCompactSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekGeometricStalkIso.lean, line 83.

Stacks 0F76. Let f : X ⟶ Y be separated and locally of finite type, F an abelian sheaf on X_étale and ȳ : Spec k ⟶ Y a geometric point. There is a canonical isomorphism (f_!F)_ȳ ≅ H⁰_c(X_ȳ, F|_{X_ȳ}) between the stalk at ȳ of the direct image with compact support (Stacks 0F4X) and the compactly supported sections (Stacks 0F72) of the inverse image of F on the geometric fibre X_ȳ = X ×_Y Spec k over k. It sends the germ of a section over an étale neighbourhood (V, v̄) to its pullback along X_ȳ ⟶ X_V (AlgebraicGeometry.SmallEtale.fShriekStalkEquivCompactSections_apply_germ).

def fShriekStalkEquivCompactSections :
    ↥(etaleStalk B Y.obj Y.property y (fShriekSubsheaf B f F).val.obj.left.obj) ≃+
      geometricFibreCompactSections B f y hy F

AlgebraicGeometry.SmallEtale.fShriekStalkEquivCompactSections_apply_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekGeometricStalkIso.lean, line 104. The attribute's comment: “the isomorphism pulls a section on an étale neighbourhood back to the fibre”.

Stacks 0F76, the isomorphism on germs. Let (V, v̄) be an étale neighbourhood of ȳ and s a section of f_!F over V, that is a section of F over X_V with support proper over V. Let h : X_ȳ ⟶ X_ȳ ×_X X_V be a morphism over X_ȳ whose composite to V is X_ȳ ⟶ Spec k ⟶ V. Then the isomorphism sends the germ of s at ȳ to the pullback of s along h. Such an h exists and is unique, AlgebraicGeometry.SmallEtale.geometricFibreLift; this is the canonical map c_ȳ of the source.

theorem fShriekStalkEquivCompactSections_apply_germ
    (N : (geometricPointFiber B Y.obj Y.property y).Elements)
    (s : (fShriekSubsheaf B f F).val.obj.left.obj.obj (op N.1))
    (h : final B (geometricFibreObj B f y hy).obj (geometricFibreObj B f y hy).property ⟶
      (smallEtaleBaseChange B (geometricFibreProj B f y hy)).obj
        ((smallEtaleBaseChange B f).obj N.1))
    (hh : (h.hom.left ≫ baseChangeObjProjection B (geometricFibreProj B f y hy)
        ((smallEtaleBaseChange B f).obj N.1)) ≫ pullback.fst N.1.obj.hom f =
      geometricFibreStruct B f y hy ≫ neighborhoodPointHom B y hy N) :
    (fShriekStalkEquivCompactSections B f F y hy
        (etaleGerm B Y.obj Y.property y _ N.1 N.2 s) : geometricFibreSections B f y hy F) =
      pullbackSectionAlongHom B (geometricFibreProj B f y hy) AddCommGrpCat.{max (u + 1) v} F
        ((smallEtaleBaseChange B f).obj N.1) _ h
        ((fShriekSubsheaf B f F).val.arrow.hom.app (op N.1) s)
Tag 0F55, a lemma

Tag 0F55 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekProperBaseChange.lean, line 80.

Stacks 0F55. For a cartesian square of a big étale site with horizontal morphisms p : X' ⟶ X, g : Y' ⟶ Y and vertical morphisms f : X ⟶ Y separated and locally of finite type and f' : X' ⟶ Y', there is an isomorphism g⁻¹f_!F ≅ f'_!(p⁻¹F), natural in the abelian sheaf F on the small étale site of X. Its component at F is the base-change map AlgebraicGeometry.SmallEtale.properSupportBaseChange, the restriction of the pullback map g⁻¹f_*F ⟶ f'_*(p⁻¹F) (AlgebraicGeometry.SmallEtale.properSupportBaseChange_comp_arrow), so the isomorphism is the identification f'_!(p⁻¹F) = g⁻¹f_!F of the source inside f'_*(p⁻¹F). The hypotheses on f' are read off the square.

public def properSupportBaseChangeIso :
    letI := locallyOfFiniteType_of_isPullback B p f' f g sq
    properSupportFunctor B f ⋙ abPullback.{u, v} B g ≅
      abPullback.{u, v} B p ⋙ properSupportFunctor B f'
Tag 0F50, a lemma

Tag 0F50 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportFunctor_compIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekComposition.lean, line 1044.

The canonical comparison is natural in the abelian étale sheaf.

public noncomputable def properSupportFunctor_compIso
    [IsSeparated (B.inclusion.map f)] [IsSeparated (B.inclusion.map g)] :
    letI : LocallyOfFiniteType (B.inclusion.map (f ≫ g)) :=
      by rw [Functor.map_comp]; infer_instance
    { e : properSupportFunctor B f ⋙ properSupportFunctor B g ≅
          properSupportFunctor B (f ≫ g) //
      ∀ F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v},
        e.app F = (properSupportSheaf_compIso B f g F).val }
Tag 0F77, a remark

Tag 0F77 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportFunctor_compIso_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekAssociativity.lean, line 262. The attribute's comment: “composition_coherence”.

Canonical proper-support direct-image comparisons are associative.

public theorem properSupportFunctor_compIso_assoc
    (B : BigEtaleSite.{u}) {X Y Z T : B.Scheme}
    (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T)
    [LocallyOfFiniteType (B.inclusion.map f)]
    [LocallyOfFiniteType (B.inclusion.map g)]
    [LocallyOfFiniteType (B.inclusion.map h)]
    [IsSeparated (B.inclusion.map f)]
    [IsSeparated (B.inclusion.map g)]
    [IsSeparated (B.inclusion.map h)] :
    letI := locallyOfFiniteType_map_comp B f g
    letI := locallyOfFiniteType_map_comp B g h
    letI := locallyOfFiniteType_map_comp B (f ≫ g) h
    letI := locallyOfFiniteType_map_comp B f (g ≫ h)
    letI := isSeparated_map_comp B f g
    letI := isSeparated_map_comp B g h
    let fBang := SmallEtale.properSupportFunctor.{u, v} B f
    let gBang := SmallEtale.properSupportFunctor.{u, v} B g
    let hBang := SmallEtale.properSupportFunctor.{u, v} B h
    (Functor.isoWhiskerRight
        (SmallEtale.properSupportFunctor_compIso.{u, v} B f g).val hBang ≪≫
      (SmallEtale.properSupportFunctor_compIso.{u, v} B (f ≫ g) h).val) =
    (Functor.associator fBang gBang hBang ≪≫
      Functor.isoWhiskerLeft fBang
        (SmallEtale.properSupportFunctor_compIso.{u, v} B g h).val ≪≫
      (SmallEtale.properSupportFunctor_compIso.{u, v} B f (g ≫ h)).val ≪≫
      eqToIso (by
        have heq : f ≫ (g ≫ h) = (f ≫ g) ≫ h := (Category.assoc f g h).symm
        cases heq
        rfl))

AlgebraicGeometry.SmallEtale.properSupportBaseChange_compIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ProperSupportBaseChangeComposition.lean, line 302. The attribute's comment: “part (2): compatibility of the base change maps of 0F55 with the composition isomorphisms of 0F50”.

Stacks, Remark 0F77, part (2). Let 

X' --c--> X
|f'       |f
v         v
Y' --b--> Y
|g'       |g
v         v
Z' --a--> Z
be two cartesian squares of a big étale site, with f and g separated and locally of finite type. Then the square 
a⁻¹ (g ∘ f)_! ------------------------------> (g' ∘ f')_! c⁻¹
     |                                               |
a⁻¹ g_! f_! ------> g'_! b⁻¹ f_! ------> g'_! f'_! c⁻¹
of abelian sheaves on the small étale site of Z' commutes, where the horizontal arrows are the base change maps of Stacks 0F55 (AlgebraicGeometry.SmallEtale.properSupportBaseChange) for the rectangle, for the lower square at f_! F, and g'_! of that for the upper square, and the vertical arrows are the composition isomorphisms of Stacks 0F50 (AlgebraicGeometry.SmallEtale.properSupportFunctor_compIso).

theorem properSupportBaseChange_compIso (sq₁ : IsPullback c f' f b)
    (sq₂ : IsPullback b g' g a)
    [LocallyOfFiniteType (B.inclusion.map f)] [LocallyOfFiniteType (B.inclusion.map g)]
    [IsSeparated (B.inclusion.map f)] [IsSeparated (B.inclusion.map g)]
    (F : AbelianSheaf.{u, v} B X) :
    letI : LocallyOfFiniteType (B.inclusion.map f') :=
      MorphismProperty.of_isPullback (sq₁.map B.inclusion) inferInstance
    letI : LocallyOfFiniteType (B.inclusion.map g') :=
      MorphismProperty.of_isPullback (sq₂.map B.inclusion) inferInstance
    letI : IsSeparated (B.inclusion.map f') :=
      MorphismProperty.of_isPullback (sq₁.map B.inclusion) inferInstance
    letI : IsSeparated (B.inclusion.map g') :=
      MorphismProperty.of_isPullback (sq₂.map B.inclusion) inferInstance
    letI := locallyOfFiniteType_map_comp B f g
    letI := locallyOfFiniteType_map_comp B f' g'
    properSupportBaseChange.{u, v} B c (f' ≫ g') (f ≫ g) a (sq₁.paste_vert sq₂) F ≫
        (properSupportFunctor_compIso B f' g').val.inv.app ((abPullback.{u, v} B c).obj F) =
      (abPullback.{u, v} B a).map ((properSupportFunctor_compIso B f g).val.inv.app F) ≫
        properSupportBaseChange.{u, v} B b g' g a sq₂ ((properSupportFunctor B f).obj F) ≫
        (properSupportFunctor B g').map (properSupportBaseChange.{u, v} B c f' f b sq₁ F)
Tag 0F54, a lemma

Tag 0F54 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportFunctor_isColimit_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCover.lean, line 1117.

Stacks 0F54. Let f : X ⟶ Y be separated and locally of finite type, and let the X_i = U i form an open covering of X that is directed: any two members lie in a third. Writing f_i for the restriction of f to X_i, the proper-support direct image is the colimit f_! F = colim_i f_{i,!}(F|_{X_i}) functorially in the abelian sheaf F, along the canonical extension-by-zero maps: there is a directed diagram of functors whose value at i is F ↦ f_{i,!}(F|_{X_i}) and a colimit cocone on it, in the category of functors from abelian sheaves on X to abelian sheaves on Y, whose vertex is the functor f_! and whose legs are, at every sheaf F, the canonical maps f_{i,!}(F|_{X_i}) ⟶ f_! F.

public theorem properSupportFunctor_isColimit_openCover [IsDirected ι (· ≤ ·)]
    (hcover : ∀ x : X.obj, ∃ i, x ∈ Set.range (B.inclusion.map (j.app i)).base) :
    ∃ (D : ι ⥤ (Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v} ⥤
        Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{v}))
      (c : Cocone D) (hpt : c.pt = properSupportFunctor B f),
      (∀ i,
        let ji : U.obj i ⟶ X := j.app i
        letI : IsOpenImmersion (B.inclusion.map ji) := hopen i
        letI : LocallyOfFiniteType (B.inclusion.map (ji ≫ f)) := by
          change LocallyOfFiniteType (B.inclusion.map ji ≫ B.inclusion.map f)
          infer_instance
        let res := (smallEtaleBaseChange B ji).sheafPullback AddCommGrpCat.{v}
          (SmallEtale.topology B X.obj X.property)
          (SmallEtale.topology B (U.obj i).obj (U.obj i).property)
        ∃ (hi : D.obj i = res ⋙ properSupportFunctor B (ji ≫ f)),
          ∀ F, (c.ι.app i ≫ eqToHom hpt).app F =
            (eqToHom hi).app F ≫ (openInclusionShriekMap B ji f F).val) ∧
        Nonempty (IsColimit c)
Tag 0F56, a lemma

Tag 0F56 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportFunctor_preservesColimitsOfShape_discrete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekDirectSums.lean, line 445.

Stacks 0F56. Let f : X ⟶ Y be a morphism of schemes which is separated and locally of finite type. Then the proper-support direct image f_! of abelian sheaves on the small étale sites commutes with direct sums: it preserves colimits indexed by any discrete category, so it carries a direct sum of an arbitrarily indexed family of abelian sheaves on the small étale site of X to the direct sum of their proper-support direct images.

public theorem properSupportFunctor_preservesColimitsOfShape_discrete
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [IsSeparated (B.inclusion.map f)] [LocallyOfFiniteType (B.inclusion.map f)]
    (ι : Type w) :
    PreservesColimitsOfShape (Discrete ι) (properSupportFunctor.{u, v} B f)
Tag 0F57, a lemma

Tag 0F57 in the Stacks Project.

AlgebraicGeometry.SmallEtale.properSupportStalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ProperSupportStalk.lean, line 64. The attribute's comment: “part (1)”.

Stacks 0F57, part (1). For a separated locally quasi-finite morphism f : X ⟶ Y and a geometric point ȳ of Y, the stalk at ȳ of the proper-support direct image f_!F is the direct sum of the stalks of F at the geometric points x̄ of X with f(x̄) = ȳ, functorially in the abelian étale sheaf F.

public def properSupportStalkFunctorIso (s : GeometricPoint Y.obj) :
    properSupportFunctor.{u, max (u + 1) v} B f ⋙
        (geometricPointSitePoint B Y.obj Y.property s).sheafFiber
          (A := AddCommGrpCat.{max (u + 1) v}) ≅
      Adjunction.sigmaFamily (fun x : GeometricFiberPoint B f s =>
        (geometricPointSitePoint B X.obj X.property (x.toGeometricPoint B f s)).sheafFiber
          (A := AddCommGrpCat.{max (u + 1) v}))

AlgebraicGeometry.SmallEtale.properSupportFunctor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ProperSupportStalk.lean, line 77. The attribute's comment: “part (2)”. References: SGA 4 XVII (6.1.4), “more general”.

Stacks 0F57, part (2). For a separated locally quasi-finite morphism the proper-support direct image f_! on abelian étale sheaves is an exact functor.

public theorem properSupportFunctor_exact :
    exactFunctor _ _ (properSupportFunctor.{u, max (u + 1) v} B f)
Sources
LeanAlgebraicGeometry.SmallEtale.properSupportSections · AlgebraicGeometry.SmallEtale.properSupportSections_restrict · AlgebraicGeometry.SmallEtale.properSupportSections_descend · AlgebraicGeometry.SmallEtale.fShriekSubsheaf · AlgebraicGeometry.SmallEtale.mem_range_fShriekSubsheaf_arrow_iff · AlgebraicGeometry.SmallEtale.abelianExtensionByZeroToPushforward_range_eq_fShriekSubsheaf · AlgebraicGeometry.SmallEtale.properSupportIsoPushforward · AlgebraicGeometry.SmallEtale.fShriekSubsheaf_arrow_isIso

Section63.4 Sections with finite support#

Section 63.4 of the Stacks Project, Tag 0F6E. 15 tags here are carried by 87 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0F6E, the section

Tag 0F6E in the Stacks Project.

AlgebraicGeometry.SmallEtale.isFiniteSupport_iff_exists_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportProper.lean, line 123. The attribute's comment: “the footnote: a support is finite over the base exactly when it is proper”.

Stacks 0F6E, the footnote. For a locally quasi-finite f, a subset of X_V is an eligible support of the finite-support direct image — the range of an immersion finite over V — exactly when it is the range of an immersion proper over V. The source states this as "since f is locally quasi-finite, Z → V is finite if and only if it is proper".

public theorem isFiniteSupport_iff_exists_isProper
    [LocallyQuasiFinite (B.inclusion.map f)] (V : SmallEtale B Y.obj Y.property)
    (E : Set ((SmallEtale.toScheme B X.obj X.property).obj (baseChange B f V))) :
    IsFiniteSupport B f V E ↔
      ∃ (Z : Scheme.{u})
        (i : Z ⟶ (SmallEtale.toScheme B X.obj X.property).obj (baseChange B f V)),
        IsImmersion i ∧
          IsProper (i ≫ B.inclusion.map (pullback.fst V.obj.hom f)) ∧
          Set.range i.base = E

Declarations registered for the tag:

Tag 0F6J, an equation

Tag 0F6J in the Stacks Project.

AlgebraicGeometry.SmallEtale.exists_finiteSupport_sum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 336. The attribute's comment: “the formal sum presentation”.

Stacks 0F6J. Every section with finite support over V is a finite formal sum s = ∑ (Z_i, s_i), where each Z_i is a support finite over V and s_i ∈ H_{Z_i}(F), the pair (Z_i, s_i) standing for the image of s_i under the colimit inclusion at Z_i.

public theorem exists_finiteSupport_sum
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (V : SmallEtale B Y.obj Y.property) [Small.{v} (FiniteSupport B f V)]
    (s : ↥(finiteSupportSections B f F V)) :
    ∃ (n : ℕ) (Z : Fin n → FiniteSupport B f V)
      (t : ∀ i, supportedSections B X.obj X.property F (baseChange B f V) (Z i).1
        (finiteSupport_isLocallyClosed B f V (Z i))),
      s = ∑ i, colimit.ι (finiteSupportDiagram B f F V) (Z i) (t i)
Tag 0F6M, an equation

Tag 0F6M in the Stacks Project.

AlgebraicGeometry.SmallEtale.FiniteSupport, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 233. The attribute's comment: “the index of the colimit”.

Stacks 0F6M. The partially ordered set of supports of X_V which are finite over V.

public abbrev FiniteSupport (V : SmallEtale B Y.obj Y.property)

AlgebraicGeometry.SmallEtale.finiteSupport_isLocallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 240. The attribute's comment: “local closedness of the supports”.

The support of a subscheme finite over V is locally closed, so the group H_Z(F) of Stacks 0F6F is defined for it.

public theorem finiteSupport_isLocallyClosed (V : SmallEtale B Y.obj Y.property)
    (E : FiniteSupport B f V) : IsLocallyClosed E.1

AlgebraicGeometry.SmallEtale.finiteSupport_closedWithin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 251. The attribute's comment: “closedness of the transition inclusions”.

One support finite over V contained in another is closed in it. This is the relation making the transition maps of Stacks 0F6F available on the index, and in the source it is the observation that Z → Z' is a closed immersion because Z → V is finite and Z' → V is separated.

public theorem finiteSupport_closedWithin (V : SmallEtale B Y.obj Y.property)
    (E E' : FiniteSupport B f V) (h : E ≤ E') :
    IsClosed ((Subtype.val : E'.1 → _) ⁻¹' E.1)

AlgebraicGeometry.SmallEtale.finiteSupportDiagram, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 297. The attribute's comment: “the diagram of supported sections”.

Stacks 0F6M. The diagram Z ↦ H_Z(F) of supported sections over the supports finite over V, with the transition maps of Stacks 0F6F along the inclusions.

public def finiteSupportDiagram
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (V : SmallEtale B Y.obj Y.property) :
    FiniteSupport B f V ⥤ AddCommGrpCat.{v}

AlgebraicGeometry.SmallEtale.finiteSupportSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 326. The attribute's comment: “the colimit formula”.

Stacks 0F6M. The abelian group of sections with finite support over V, namely the colimit of H_Z(F) over the supports finite over V.

public abbrev finiteSupportSections
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (V : SmallEtale B Y.obj Y.property)
    [Small.{v} (FiniteSupport B f V)] : AddCommGrpCat.{v}

AlgebraicGeometry.SmallEtale.isFiniteSupport_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 349. The attribute's comment: “base change of the supports”.

Stacks 0F6M. The inverse image of a support finite over V along a morphism V' ⟶ V of the small étale site of Y is a support finite over V'.

public theorem isFiniteSupport_preimage {V V' : SmallEtale B Y.obj Y.property} (g : V' ⟶ V)
    (E : FiniteSupport B f V) :
    IsFiniteSupport B f V' (((SmallEtale.toScheme B X.obj X.property).map
      ((smallEtaleBaseChange B f).map g)).base ⁻¹' E.1)

AlgebraicGeometry.SmallEtale.finiteSupportBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 460. The attribute's comment: “base change of supported sections”.

Stacks 0F6M. Base change of a support finite over V and of its supported sections along a morphism V' ⟶ V of the small étale site of Y. The support is the set-theoretic inverse image and the map on sections is restriction.

public def finiteSupportBaseChange
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    {V V' : SmallEtale B Y.obj Y.property} (g : V' ⟶ V)
    (E : FiniteSupport B f V) : FiniteSupportBaseChange B f F g E

AlgebraicGeometry.SmallEtale.finiteSupportPresheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 853. The attribute's comment: “the finite-support presheaf”.

Stacks 0F6M. The abelian presheaf V ↦ colim_Z H_Z(F) on the small étale site of Y, with base change of supports as its restriction maps.

public abbrev finiteSupportPresheaf
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v})
    (hsmall : ∀ V : SmallEtale B Y.obj Y.property, Small.{v} (FiniteSupport B f V)) :
    (SmallEtale B Y.obj Y.property)ᵒᵖ ⥤ AddCommGrpCat.{v}

AlgebraicGeometry.SmallEtale.finiteSupportPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupport.lean, line 966. The attribute's comment: “the finite-support direct image functor”.

Stacks 0F6M. The direct image with finite support, as a functor from abelian sheaves on the small étale site of X to abelian presheaves on the small étale site of Y. Its values are the colimits colim_Z H_Z(F) and both of its functorial actions are pinned down on the colimit generators.

public def finiteSupportPushforward
    [LocallyOfFiniteType (B.inclusion.map f)] [LocallyQuasiFinite (B.inclusion.map f)]
    (hsmall : ∀ V : SmallEtale B Y.obj Y.property, Small.{v} (FiniteSupport B f V)) :
    {P : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{v} ⥤
        ((SmallEtale B Y.obj Y.property)ᵒᵖ ⥤ AddCommGrpCat.{v}) //
      FiniteSupportPushforwardSpec B f hsmall P}
Tag 0F6N, a lemma

Tag 0F6N in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekFunctorIsoProperSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 196. The attribute's comment: “functor comparison of the two models of f_!”.

The two models of the direct image with compact support agree: the sheafification of the finite-support direct image presheaf is the proper-support subsheaf of the ordinary direct image.

public def fShriekFunctorIsoProperSupport [IsSeparated (B.inclusion.map g)]
    [LocallyQuasiFinite (B.inclusion.map g)] :
    fShriekFunctor.{u, v} B g ≅ properSupportFunctor.{u, max (u + 1) v} B g

AlgebraicGeometry.SmallEtale.finiteSupportPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportPushforward.lean, line 211. References: SGA 4 XVII (6.3.16), “colimit formula”.

For a separated, locally finite type and locally quasi-finite morphism f of a big étale site, the finite-support direct image presheaf f_{p!} of [Stacks, Tag 0F6M] is isomorphic to the proper-support direct image f_! of [Stacks, Tag 0F4X], as functors from abelian sheaves on the small étale site of X to abelian presheaves on the small étale site of Y. The isomorphism is pinned down on the colimit generators: the generator of an eligible support carrying a supported section goes to the section of f_!F which restricts to that section on the canonical open of the support.

public def finiteSupportPushforwardIso (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [IsSeparated (B.inclusion.map f)] [LocallyOfFiniteType (B.inclusion.map f)]
    [LocallyQuasiFinite (B.inclusion.map f)] :
    let hsmall : ∀ V : SmallEtale B Y.obj Y.property,
      Small.{max u v} (FiniteSupport B f V) := fun _ => inferInstance
    let P := finiteSupportPushforward.{u, max u v} B f hsmall
    {e : P.val ≅ properSupportFunctor B f ⋙
        sheafToPresheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{max u v} //
      ∀ (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max u v})
        (V : SmallEtale B Y.obj Y.property) (E : FiniteSupport B f V)
        (s : supportedSections B X.obj X.property F (baseChange B f V) E.1
          (finiteSupport_isLocallyClosed B f V E)),
        letI := hsmall V
        (F.obj.map (openObjectι B X.obj X.property (baseChange B f V)
            (finiteSupportOpen B f V E)).op).hom
          ((colimit.ι (finiteSupportDiagram B f F V) E ≫
            eqToHom (P.property.obj_eq F V).symm ≫
            (e.hom.app F).app (op V) ≫
            (fShriekSubsheaf B f F).val.arrow.hom.app (op V)).hom s) = s.val}
Tag 0F6P, a lemma

Tag 0F6P in the Stacks Project.

AlgebraicGeometry.SmallEtale.surjective_finiteSupportStalkToFiberStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportStalkGeometric.lean, line 598. The attribute's comment: “surjectivity of the germ decomposition”.

The surjectivity half of Stacks 0F6P. The germ decomposition map (f_{p!}F)_ȳ ⟶ ⊕_{f(x̄) = ȳ} F_x̄ is surjective.

public theorem surjective_finiteSupportStalkToFiberStalks
    (hsmall : ∀ V : SmallEtale B Y.obj Y.property, Small.{max u v} (FiniteSupport B f V)) :
    Function.Surjective (finiteSupportStalkToFiberStalks B f s F hsmall)

AlgebraicGeometry.SmallEtale.injective_finiteSupportStalkToFiberStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportStalkIso.lean, line 962. The attribute's comment: “injectivity of the germ decomposition”.

The injectivity half of Stacks 0F6P. The germ decomposition map (f_{p!}F)_ȳ ⟶ ⊕_{f(x̄) = ȳ} F_x̄ is injective.

An element of the stalk is a finite sum of germs of supported sections over one étale neighbourhood of ȳ, and such a sum of germs vanishes as soon as the family of germ decompositions does.

public theorem injective_finiteSupportStalkToFiberStalks :
    Function.Injective (finiteSupportStalkToFiberStalks B f s F hsmall)

AlgebraicGeometry.SmallEtale.finiteSupportStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportStalkIso.lean, line 995. The attribute's comment: “the germ decomposition is an isomorphism”.

Stacks 0F6P. For a locally quasi-finite morphism f : X ⟶ Y, the stalk of the finite-support direct image f_{p!}F at a geometric point ȳ of Y is the direct sum of the stalks of F over the geometric points of X lying over ȳ: (f_{p!}F)_ȳ ≅ ⊕_{f(x̄) = ȳ} F_x̄.

public def finiteSupportStalkIso :
    etaleStalk B Y.obj Y.property s ((finiteSupportPushforward B f hsmall).1.obj F) ≅
      AddCommGrpCat.of (fiberStalks B f s F)
Tag 0F6Q, a lemma

Tag 0F6Q in the Stacks Project.

AlgebraicGeometry.SmallEtale.etaleExtensionToFiniteSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportExtensionByZero/Comparison.lean, line 412. The attribute's comment: “canonical natural presheaf map”.

Stacks 0F6Q. The canonical map j_{p!} ⟶ f_{p!} from the presheaf extension by zero along the étale morphism U ⟶ X to the finite-support direct image presheaf, natural in the abelian sheaf on the small étale site of U. It is the map the universal property of the left Kan extension produces from the graph generators.

public def etaleExtensionToFiniteSupport :
    abelianPresheafExtensionByZero B X hX U ⟶ etaleFiniteSupportPresheaf B X hX U

AlgebraicGeometry.SmallEtale.etaleExtensionToFiniteSupport_on_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportExtensionByZero/Comparison.lean, line 456. The attribute's comment: “graph-support formula on generators”.

Stacks 0F6Q. The value of the canonical map on a generator of the presheaf extension by zero: the section of F over an étale object W → U, viewed in the summand of j_{p!}F over W indexed by W ⟶ U, goes to the colimit generator of colim_Z H_Z(F) at the graph of W → U, carrying the section supported on that graph. Naturality of the comparison then extends the formula to every lift V ⟶ U of an arbitrary étale test object V ⟶ X.

public theorem etaleExtensionToFiniteSupport_on_graph
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      AddCommGrpCat.{u + 1})
    (W : SmallEtale B U.obj.left.1 U.obj.left.property) (s : F.obj.obj (op W)) :
    ((etaleExtensionToFiniteSupport B X hX U).app F).app
        (op ((smallEtalePostcompose B X hX U).obj W))
        (((smallEtalePostcompose B X hX U).op.lanUnit.app F.obj).app (op W) s) =
      colimit.ι (finiteSupportDiagram B U.obj.hom F ((smallEtalePostcompose B X hX U).obj W))
        (etaleGraphFiniteSupport B X hX U W) (etaleGraphSection B X hX U F W s)

AlgebraicGeometry.SmallEtale.graphSupportedSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportExtensionByZero/Comparison.lean, line 530. The attribute's comment: “graph supports”.

Stacks 0F6Q, the graph supports. For an étale object W → U the graph of W → U is an open immersion W ⟶ U ×_X W whose image is a support finite over W, and a section of an abelian sheaf over W is a section supported on that graph.

public def graphSupportedSection (W : SmallEtale B U.obj.left.1 U.obj.left.property) :
    GraphSupportedSectionData B X hX U W

AlgebraicGeometry.SmallEtale.etaleExtensionToFiniteSupport_sheafify_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportExtensionByZero/Stalk.lean, line 511. The attribute's comment: “isomorphism after sheafification”.

Stacks 0F6Q. The canonical map j_{p!}F ⟶ f_{p!}F becomes an isomorphism after sheafification: it is an isomorphism on every geometric stalk, both sides becoming the direct sum of the stalks of F over the geometric fibre, and a map of abelian étale sheaves which is an isomorphism on every geometric stalk is an isomorphism. So the sheaf j_!F = (j_{p!}F)^# of Stacks 03S3 is identified with (f_{p!}F)^#.

public theorem etaleExtensionToFiniteSupport_sheafify_isIso
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      AddCommGrpCat.{u + 1}) :
    IsIso ((presheafToSheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}).map
      ((etaleExtensionToFiniteSupport B X hX U).app F))
Tag 0F6R, a definition

Tag 0F6R in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalk.lean, line 141.

Stacks 0F6R. The direct image with compact support f_! of a locally quasi-finite morphism, on abelian sheaves on the small étale sites: the sheafification of the finite-support direct image presheaf f_{p!} of Stacks 0F6M.

public def fShriekFunctor :
    Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{max (u + 1) v}
Tag 0F5F, a lemma

Tag 0F5F in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalkDecomposition.lean, line 78. The attribute's comment: “part (1), stalk decomposition”.

Stacks 0F5F, part (1). The stalk of the direct image with compact support f_!F of a locally quasi-finite morphism at a geometric point ȳ of Y is the direct sum of the stalks of F over the geometric points of X lying over ȳ: (f_!F)_ȳ ≅ ⊕_{f(x̄) = ȳ} F_x̄.

public def fShriekStalkIso (s : GeometricPoint Y.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    etaleStalk B Y.obj Y.property s ((fShriekFunctor.{u, v} B f).obj F).obj ≅
      AddCommGrpCat.of (fiberStalks.{u, max (u + 1) v} B f s F)

AlgebraicGeometry.SmallEtale.fShriekStalkIso_comp_sheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalkDecomposition.lean, line 90. The attribute's comment: “part (1), canonical comparison”.

Stacks 0F5F, part (1). The stalk decomposition of f_!F is the canonical one: the comparison of the stalk of f_!F with the stalk of the finite-support direct image presheaf f_{p!}F, which is induced by the sheafification unit, carries it to the germ decomposition of Stacks 0F6P.

public theorem fShriekStalkIso_comp_sheafification (s : GeometricPoint Y.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    colim.map (Functor.whiskerLeft
        (CategoryOfElements.π (geometricPointFiber B Y.obj Y.property s)).op
        (toSheafify (SmallEtale.topology B Y.obj Y.property)
          ((finiteSupportPushforward.{u, max (u + 1) v} B f
            (fun _ => inferInstance)).1.obj F))) ≫
      (fShriekStalkIso.{u, v} B f s F).hom =
      (finiteSupportStalkIso.{u, max (u + 1) v} B f s F fun _ => inferInstance).hom

AlgebraicGeometry.SmallEtale.fShriekStalkIso_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalkDecomposition.lean, line 105. The attribute's comment: “part (1), functoriality”.

Stacks 0F5F, part (1). The stalk decomposition of the direct image with compact support is natural in the abelian sheaf: a morphism of sheaves on X acts on the direct sum of stalks over the geometric fibre by its maps on those stalks.

public theorem fShriekStalkIso_natural (s : GeometricPoint Y.obj)
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}}
    (φ : F ⟶ G) :
    colim.map (Functor.whiskerLeft
        (CategoryOfElements.π (geometricPointFiber B Y.obj Y.property s)).op
        ((fShriekFunctor.{u, v} B f).map φ).1) ≫ (fShriekStalkIso.{u, v} B f s G).hom =
      (fShriekStalkIso.{u, v} B f s F).hom ≫
        AddCommGrpCat.ofHom (fiberStalksMap.{u, max (u + 1) v} B f s φ)

AlgebraicGeometry.SmallEtale.fShriekFunctor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalkDecomposition.lean, line 370. The attribute's comment: “part (2), exactness”.

Stacks 0F5F, part (2). The direct image with compact support of a locally quasi-finite morphism is an exact functor on abelian étale sheaves.

Preservation of finite colimits is the colimit preservation of the stalk decomposition; preservation of finite limits follows from it together with preservation of monomorphisms.

public theorem fShriekFunctor_exact :
    exactFunctor _ _ (fShriekFunctor.{u, v} B f)

AlgebraicGeometry.SmallEtale.fShriekFunctor_preservesCoproductsOfShape, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalkDecomposition.lean, line 392. The attribute's comment: “part (2), direct sums”.

Stacks 0F5F, part (2). The direct image with compact support of a locally quasi-finite morphism commutes with arbitrary direct sums of abelian étale sheaves.

public theorem fShriekFunctor_preservesCoproductsOfShape (I : Type (max (u + 1) v)) :
    PreservesColimitsOfShape (Discrete I) (fShriekFunctor.{u, v} B f)

AlgebraicGeometry.SmallEtale.fShriekStalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekStalkFunctorDecomposition.lean, line 51. The attribute's comment: “part (1), stalk decomposition as an isomorphism of functors”.

Stacks 0F5F, part (1), as an isomorphism of functors. The composite of the direct image with compact support f_! with the stalk functor at a geometric point ȳ of Y is the coproduct of the stalk functors of X at the geometric points lying over ȳ.

public def fShriekStalkFunctorIso (s : GeometricPoint Y.obj) :
    fShriekFunctor.{u, v} B f ⋙ (geometricPointSitePoint B Y.obj Y.property s).sheafFiber
        (A := AddCommGrpCat.{max (u + 1) v}) ≅
      Adjunction.sigmaFamily (fun x : GeometricFiberPoint B f s =>
        (geometricPointSitePoint B X.obj X.property (x.toGeometricPoint B f s)).sheafFiber
          (A := AddCommGrpCat.{max (u + 1) v}))
Tag 0F6S, a remark

Tag 0F6S in the Stacks Project.

AlgebraicGeometry.SmallEtale.OpenCoverShriek.shriekLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverComplex.lean, line 137. The attribute's comment: “covariance along an inclusion of opens of the source”.

The Čech face map. For an inclusion V ≤ W of open subschemes of X, the covariance map (j_V ≫ f)_!((-)|_V) ⟶ (j_W ≫ f)_!((-)|_W) of Stacks 0F6S for the open immersion V ⟶ W.

public def shriekLE {V W : (B.inclusion.obj X).Opens} (h : V ≤ W) :
    openShriekPushforward.{u, v} B (openSchemeι B V) f ⟶
      openShriekPushforward.{u, v} B (openSchemeι B W) f

AlgebraicGeometry.SmallEtale.ofHom_of_comp_fShriekStalkIso_openCovariance, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverStalkCovariance.lean, line 164. The attribute's comment: “part (1), stalk compatibility on the stalk decomposition of Stacks 0F5F”.

Stacks 0F6S, part (1), on the stalk decompositions of Stacks 0F5F: on the direct sums of stalks over the geometric fibres the covariance map of the direct images with compact support is extension by zero along the inclusion of geometric fibres, so it carries the summand of a point of the geometric fibre of j ≫ f to the summand of its image in the geometric fibre of f.

public theorem ofHom_of_comp_fShriekStalkIso_openCovariance
    [DecidableEq (GeometricFiberPoint B (j ≫ f) s)]
    [DecidableEq (GeometricFiberPoint B f s)] (y : GeometricFiberPoint B (j ≫ f) s) :
    AddCommGrpCat.ofHom (DirectSum.of (fun y' : GeometricFiberPoint B (j ≫ f) s =>
          ↑(etaleStalk B X'.obj X'.property (y'.toGeometricPoint B (j ≫ f) s)
            ((openRestriction.{u, v} B j).obj F).obj)) y) ≫
        (fShriekStalkIso.{u, v} B (j ≫ f) s ((openRestriction.{u, v} B j).obj F)).inv ≫
        ((geometricPointSitePoint B Y.obj Y.property s).sheafFiber
            (A := AddCommGrpCat.{max (u + 1) v})).map
          ((openCovarianceShriekMap.{u, v} B j f).app F) ≫
        (fShriekStalkIso.{u, v} B f s F).hom =
      (openFiberStalkIso.{u, v} B j f F s y).hom ≫
        AddCommGrpCat.ofHom (DirectSum.of (fun x : GeometricFiberPoint B f s =>
          ↑(etaleStalk B X.obj X.property (x.toGeometricPoint B f s) F.obj))
            (openFiberPoint B j f s y))

AlgebraicGeometry.SmallEtale.openCovariancePresheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovariance/PresheafMap.lean, line 466. The attribute's comment: “covariance, presheaf map”.

The canonical covariance map of finite-support direct-image presheaves for an open subscheme of the source. Its generator formula and the canonical extension of supported sections are part of the construction; naturality in the test object and in the abelian sheaf is part of its being a natural transformation of functors.

public def openCovariancePresheafMap :
    {α : openFiniteSupportPushforward.{u, v} B j f ⟶
      wholeFiniteSupportPushforward.{u, v} B f //
      OpenCovariancePresheafMapSpec B j f α}

AlgebraicGeometry.SmallEtale.openCovarianceShriekMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovariance/PresheafMap.lean, line 506. The attribute's comment: “covariance”.

Sheafifying the canonical presheaf map gives covariance of the direct image with compact support under an open immersion of the source.

public def openCovarianceShriekMap :
    openShriekPushforward.{u, v} B j f ⟶ fShriekFunctor.{u, v} B f

AlgebraicGeometry.SmallEtale.mono_openCovarianceShriekMap_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceInjectivity.lean, line 199. The attribute's comment: “part (4), injectivity for a separated morphism”.

Stacks 0F6S, part (4), for a separated morphism. The covariance map of the direct images with compact support attached to an open subscheme of the source is a monomorphism: it is the sheafification of the presheaf covariance map, and sheafification of abelian sheaves is left exact.

public theorem mono_openCovarianceShriekMap_app :
    Mono ((openCovarianceShriekMap.{u, v} B j f).app F)

AlgebraicGeometry.SmallEtale.openCovariancePresheafMap_comp_finiteSupportPushforwardIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceSeparated.lean, line 261. The attribute's comment: “part (2), agreement with the map of Stacks 0F53 through Stacks 0F6N”.

Stacks 0F6S, part (2). For a separated morphism the covariance map of finite-support direct-image presheaves attached to an open subscheme of the source is the extension by zero of Stacks 0F53, transported along the isomorphism of Stacks 0F6N.

public theorem openCovariancePresheafMap_comp_finiteSupportPushforwardIso :
    (openCovariancePresheafMap.{u, v} B j f).val.app F ≫
        (finiteSupportPushforwardIso.{u, max (u + 1) v} B f).val.hom.app F =
      (finiteSupportPushforwardIso.{u, max (u + 1) v} B (j ≫ f)).val.hom.app
          ((openRestriction.{u, v} B j).obj F) ≫
        (openInclusionShriekMap.{u, max (u + 1) v} B j f F).val.hom

AlgebraicGeometry.SmallEtale.fiberStalkComponent_covarianceSectionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalk.lean, line 293. The attribute's comment: “part (1), stalk compatibility on a generator, summand in the open”.

Stacks Project, Tag 0F6S part (1) on a colimit generator, in a summand indexed by a point of the geometric fibre of j ≫ f: the germ of the extended section at the image point is the germ of the original section, read through the identification of the two stalks.

public theorem fiberStalkComponent_covarianceSectionMap
    [LocallyOfFiniteType (B.inclusion.map f)] [LocallyQuasiFinite (B.inclusion.map f)]
    (V : SmallEtale B Y.obj Y.property)
    (u : (geometricPointFiber B Y.obj Y.property s).obj V)
    (E : FiniteSupport B (j ≫ f) V)
    (a : supportedSections B X'.obj X'.property ((openRestriction.{u, v} B j).obj F)
      (baseChange B (j ≫ f) V) E.1 (finiteSupport_isLocallyClosed B (j ≫ f) V E))
    (x : GeometricFiberPoint B (j ≫ f) s) :
    fiberStalkComponent.{u, max (u + 1) v} B f s F V u (imageFiniteSupport B j f V E)
        (covarianceSectionMap B j f F V E _ (imageFiniteSupport_coe B j f V E) a)
        (openFiberPoint B j f s x) =
      (openFiberStalkIso.{u, v} B j f F s x).hom
        (fiberStalkComponent.{u, max (u + 1) v} B (j ≫ f) s
          ((openRestriction.{u, v} B j).obj F) V u E a x)

AlgebraicGeometry.SmallEtale.fiberStalkComponent_covarianceSectionMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalk.lean, line 402. The attribute's comment: “part (1), stalk compatibility on a generator, summand outside the open”.

Stacks Project, Tag 0F6S part (1) on a colimit generator, in a summand outside the image of the geometric fibre of j ≫ f: the germ of the extended section vanishes there, the extended section being supported on the image of the original support.

public theorem fiberStalkComponent_covarianceSectionMap_eq_zero
    (V : SmallEtale B Y.obj Y.property)
    (u : (geometricPointFiber B Y.obj Y.property s).obj V)
    (E : FiniteSupport B (j ≫ f) V) (D : FiniteSupport B f V)
    (hD : D.1 = (openBaseChangeHom B j f V).base '' E.1)
    (a : supportedSections B X'.obj X'.property ((openRestriction.{u, v} B j).obj F)
      (baseChange B (j ≫ f) V) E.1 (finiteSupport_isLocallyClosed B (j ≫ f) V E))
    (y : GeometricFiberPoint B f s)
    (hy : ∀ x : GeometricFiberPoint B (j ≫ f) s, openFiberPoint B j f s x ≠ y) :
    fiberStalkComponent.{u, max (u + 1) v} B f s F V u D
      (covarianceSectionMap B j f F V E D hD a) y = 0

AlgebraicGeometry.SmallEtale.fiberStalks_openCovarianceStalkMap_openFiberPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalk.lean, line 552. The attribute's comment: “part (1), stalk compatibility, presheaf form, summands in the open”.

Stacks Project, Tag 0F6S part (1) for the finite-support direct-image presheaves, in a summand indexed by a point of the geometric fibre of j ≫ f: on the stalk decompositions of Stacks 0F6P the covariance map of Stacks 0F6S carries the summand at a point of the geometric fibre of j ≫ f to the summand at its image, through the identification of the two stalks.

public theorem fiberStalks_openCovarianceStalkMap_openFiberPoint
    (V : SmallEtale B Y.obj Y.property)
    (w : (geometricPointFiber B Y.obj Y.property s).obj V) (E : FiniteSupport B (j ≫ f) V)
    (a : (finiteSupportDiagram B (j ≫ f) ((openRestriction.{u, v} B j).obj F) V).obj E)
    (x : GeometricFiberPoint B (j ≫ f) s) :
    ((finiteSupportStalkIso.{u, max (u + 1) v} B f s F (fun _ => inferInstance)).hom
          ((openCovarianceStalkMap.{u, v} B j f F s)
            (finiteSupportStalkGenerator.{u, v} B (j ≫ f)
              ((openRestriction.{u, v} B j).obj F) s
              (Functor.elementsMk (geometricPointFiber B Y.obj Y.property s) V w) E a)) :
        fiberStalks.{u, max (u + 1) v} B f s F) (openFiberPoint B j f s x) =
      (openFiberStalkIso.{u, v} B j f F s x).hom
        (((finiteSupportStalkIso.{u, max (u + 1) v} B (j ≫ f) s
              ((openRestriction.{u, v} B j).obj F) (fun _ => inferInstance)).hom
            (finiteSupportStalkGenerator.{u, v} B (j ≫ f)
              ((openRestriction.{u, v} B j).obj F) s
              (Functor.elementsMk (geometricPointFiber B Y.obj Y.property s) V w) E a) :
          fiberStalks.{u, max (u + 1) v} B (j ≫ f) s
            ((openRestriction.{u, v} B j).obj F)) x)

AlgebraicGeometry.SmallEtale.fiberStalks_openCovarianceStalkMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalk.lean, line 590. The attribute's comment: “part (1), stalk compatibility, presheaf form, summands outside the open”.

Stacks Project, Tag 0F6S part (1) for the finite-support direct-image presheaves, in a summand outside the image of the geometric fibre of j ≫ f: on the stalk decompositions of Stacks 0F6P the covariance map of Stacks 0F6S has vanishing component there. Together with the previous theorem this says that on the stalk at s the covariance map is the extension by zero along the inclusion of geometric fibres.

public theorem fiberStalks_openCovarianceStalkMap_eq_zero
    (V : SmallEtale B Y.obj Y.property)
    (w : (geometricPointFiber B Y.obj Y.property s).obj V) (E : FiniteSupport B (j ≫ f) V)
    (a : (finiteSupportDiagram B (j ≫ f) ((openRestriction.{u, v} B j).obj F) V).obj E)
    (y : GeometricFiberPoint B f s)
    (hy : ∀ x : GeometricFiberPoint B (j ≫ f) s, openFiberPoint B j f s x ≠ y) :
    ((finiteSupportStalkIso.{u, max (u + 1) v} B f s F (fun _ => inferInstance)).hom
        ((openCovarianceStalkMap.{u, v} B j f F s)
          (finiteSupportStalkGenerator.{u, v} B (j ≫ f)
            ((openRestriction.{u, v} B j).obj F) s
            (Functor.elementsMk (geometricPointFiber B Y.obj Y.property s) V w) E a)) :
      fiberStalks.{u, max (u + 1) v} B f s F) y = 0

AlgebraicGeometry.SmallEtale.fiberStalks_openCovarianceStalkMap_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalkInjectivity.lean, line 152. The attribute's comment: “part (1), stalk compatibility, presheaf form, summands in the open, any element”.

Stacks 0F6S, part (1) on an arbitrary element of the stalk: on the stalk decompositions of Stacks 0F6P the covariance map carries the component at a point of the geometric fibre of j ≫ f to the component at its image, through the identification of the two stalks.

public theorem fiberStalks_openCovarianceStalkMap_apply
    (z : ↑(etaleStalk B Y.obj Y.property s
      ((finiteSupportPushforward.{u, max (u + 1) v} B (j ≫ f)
        (fun _ => inferInstance)).val.obj ((openRestriction.{u, v} B j).obj F))))
    (x : GeometricFiberPoint B (j ≫ f) s) :
    ((finiteSupportStalkIso.{u, max (u + 1) v} B f s F (fun _ => inferInstance)).hom
          ((openCovarianceStalkMap.{u, v} B j f F s) z) :
        fiberStalks.{u, max (u + 1) v} B f s F) (openFiberPoint B j f s x) =
      (openFiberStalkIso.{u, v} B j f F s x).hom
        (((finiteSupportStalkIso.{u, max (u + 1) v} B (j ≫ f) s
              ((openRestriction.{u, v} B j).obj F) (fun _ => inferInstance)).hom z :
          fiberStalks.{u, max (u + 1) v} B (j ≫ f) s
            ((openRestriction.{u, v} B j).obj F)) x)

AlgebraicGeometry.SmallEtale.fiberStalks_openCovarianceStalkMap_apply_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalkInjectivity.lean, line 173. The attribute's comment: “part (1), stalk compatibility, presheaf form, summands outside, any element”.

Stacks 0F6S, part (1) on an arbitrary element of the stalk, in a summand outside the image of the geometric fibre of j ≫ f: the component of the image vanishes there.

public theorem fiberStalks_openCovarianceStalkMap_apply_eq_zero
    (z : ↑(etaleStalk B Y.obj Y.property s
      ((finiteSupportPushforward.{u, max (u + 1) v} B (j ≫ f)
        (fun _ => inferInstance)).val.obj ((openRestriction.{u, v} B j).obj F))))
    (y : GeometricFiberPoint B f s)
    (hy : ∀ x : GeometricFiberPoint B (j ≫ f) s, openFiberPoint B j f s x ≠ y) :
    ((finiteSupportStalkIso.{u, max (u + 1) v} B f s F (fun _ => inferInstance)).hom
        ((openCovarianceStalkMap.{u, v} B j f F s) z) :
      fiberStalks.{u, max (u + 1) v} B f s F) y = 0

AlgebraicGeometry.SmallEtale.mono_openCovarianceShriekMap_app_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceStalkInjectivity.lean, line 275. The attribute's comment: “part (4), injectivity”.

Stacks Project, Tag 0F6S, part (4), in its unrestricted form: for an open immersion j : X' ⟶ X and a morphism f : X ⟶ Y locally of finite type and locally quasi-finite, with no separatedness assumed, the covariance map (j ≫ f)_!(F|_{X'}) ⟶ f_!F of the direct images with compact support is a monomorphism.

On the stalk at a geometric point the map is extension by zero along the inclusion of geometric fibres of Stacks 0F6P, hence injective; the stalks at the geometric points jointly detect monomorphisms of abelian sheaves on the small étale site.

public theorem mono_openCovarianceShriekMap_app_general :
    Mono ((openCovarianceShriekMap.{u, v} B j f).app F)

AlgebraicGeometry.SmallEtale.openCovariancePresheafMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceTransitivity.lean, line 860. The attribute's comment: “part (3), transitivity, presheaf form”.

Stacks 0F6S, part (3). Transitivity of covariance for the finite-support direct-image presheaves: for nested open subschemes of the source, the covariance map of the composite open immersion is the composite of the two covariance maps, once the two descriptions of restriction to the smallest open subscheme are identified.

public theorem openCovariancePresheafMap_comp :
    (openFiniteSupportCompIso.{u, v} B j k f).hom ≫
        Functor.whiskerLeft (openRestriction.{u, v} B k)
          (openCovariancePresheafMap.{u, v} B j (k ≫ f)).val ≫
        (openCovariancePresheafMap.{u, v} B k f).val =
      (openCovariancePresheafMap.{u, v} B (j ≫ k) f).val

AlgebraicGeometry.SmallEtale.openCovarianceShriekMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/OpenCovarianceTransitivity.lean, line 926. The attribute's comment: “part (3), transitivity”.

Stacks 0F6S, part (3). Transitivity of covariance after sheafification: for nested open subschemes of the source, the covariance map of the direct image with compact support along the composite open immersion is the composite of the two covariance maps.

public theorem openCovarianceShriekMap_comp :
    (openShriekCompIso.{u, v} B j k f).hom ≫
        Functor.whiskerLeft (openRestriction.{u, v} B k)
          (openCovarianceShriekMap.{u, v} B j (k ≫ f)) ≫
        openCovarianceShriekMap.{u, v} B k f =
      openCovarianceShriekMap.{u, v} B (j ≫ k) f
Tag 0F5H, a lemma

Tag 0F5H in the Stacks Project.

AlgebraicGeometry.SmallEtale.OpenCoverShriek.cechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverComplex.lean, line 296. The attribute's comment: “the complex, functorial in the abelian sheaf”.

Stacks 0F5H. The Čech complex of an open covering X = ⋃_{i ∈ I} X_i for the direct image with compact support along a locally quasi-finite morphism f : X ⟶ Y: a complex

… → ⊕_{i₀,i₁} f_{i₀i₁,!}((-)|_{X_{i₀i₁}}) → ⊕_{i₀} f_{i₀,!}((-)|_{X_{i₀}}) → f_!(-) → 0

of functors on abelian sheaves on the small étale site of X, hence functorial in the sheaf.

public def cechComplex : ChainComplex (ShriekCat.{u, v} B X Y) ℕ

AlgebraicGeometry.SmallEtale.OpenCoverShriek.cechComplexObj_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverExactness.lean, line 427. The attribute's comment: “exactness of the complex”.

Stacks 0F5H, exactness. For a family of open subschemes covering X, the Čech complex ⋯ ⟶ ⊕_{i₀} f_{i₀,!}(F|_{X_{i₀}}) ⟶ f_!F ⟶ 0 of an abelian sheaf F on the small étale site of X is acyclic.

public theorem cechComplexObj_acyclic (hU : (⨆ i, U i) = ⊤)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    (cechComplexObj.{u, v} B f U F).Acyclic
Tag 0F5I, a remark

Tag 0F5I in the Stacks Project.

AlgebraicGeometry.SmallEtale.OpenCoverShriek.exists_isSeparated_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverCokernel.lean, line 97. The attribute's comment: “the covering with every restriction separated, by affine opens”.

Stacks 0F5I. A locally quasi-finite morphism f : X ⟶ Y admits an open covering X = ⋃_{i ∈ I} X_i such that every restriction f_{i₀…i_p} : X_{i₀…i_p} ⟶ Y is separated: the covering of X by its affine opens is one.

public theorem exists_isSeparated_openCover :
    ∃ (J : Type (max (u + 1) v)) (V : J → (B.inclusion.obj X).Opens),
      (⨆ j, V j) = ⊤ ∧ (∀ j, IsAffineOpen (V j)) ∧
        ∀ {n : ℕ} (t : Fin (n + 1) → J),
          IsSeparated (B.inclusion.map (openSchemeι B (coverOpen B V t) ≫ f))

AlgebraicGeometry.SmallEtale.OpenCoverShriek.cechFamilyIsoProperSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverCokernel.lean, line 121. The attribute's comment: “each term is the construction of Section 0F4W, the restrictions being separated”.

Stacks 0F5I. Along a covering by affine opens the term of the Čech complex at a tuple of indices is the proper-support direct image of Section 0F4W: the restriction f_{i₀…i_p} is separated, so the two models of the direct image with compact support agree on it by Stacks 0F6N.

public def cechFamilyIsoProperSupport (hU : ∀ i, IsAffineOpen (U i)) {n : ℕ}
    (t : Fin (n + 1) → I) :
    cechFamily.{u, v} B f U (n + 1) t ≅
      openRestriction.{u, v} B (openSchemeι B (coverOpen B U t)) ⋙
        properSupportFunctor.{u, max (u + 1) v} B (openSchemeι B (coverOpen B U t) ≫ f)

AlgebraicGeometry.SmallEtale.OpenCoverShriek.cechComplexObj_isColimit_cokernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverCokernel.lean, line 150. The attribute's comment: “f_! F is the cokernel of the penultimate map of the complex of Stacks 0F5H”.

Stacks 0F5I. For an open covering of X and an abelian sheaf F on the small étale site of X, the sheaf f_! F is the cokernel of the penultimate differential of the Čech complex of Stacks 0F5H:

f_! F = Coker(⊕_{i₀,i₁} f_{i₀i₁,!} F|_{X_{i₀i₁}} ⟶ ⊕_{i₀} f_{i₀,!} F|_{X_{i₀}}).

public def cechComplexObj_isColimit_cokernel (hU : (⨆ i, U i) = ⊤)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    IsColimit (CokernelCofork.ofπ ((cechAugMap.{u, v} B f U 1).app F)
      ((cechComplexObj.{u, v} B f U F).d_comp_d 2 1 0))

AlgebraicGeometry.SmallEtale.OpenCoverShriek.cechComplex_isColimit_cokernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekOpenCoverCokernel.lean, line 185. The attribute's comment: “the functor f_! is that cokernel, the alternative construction”.

Stacks 0F5I. The alternative construction of the functor f_! for a locally quasi-finite morphism: for an open covering of X the functor f_! is the cokernel, in the category of functors on abelian sheaves of the small étale site of X, of the penultimate differential of the Čech complex of Stacks 0F5H. Taking this cokernel as the definition of f_! therefore recovers f_! together with its functoriality.

public def cechComplex_isColimit_cokernel (hU : (⨆ i, U i) = ⊤) :
    IsColimit (CokernelCofork.ofπ (cechAugMap.{u, v} B f U 1)
      ((cechComplex.{u, v} B f U).d_comp_d 2 1 0))
Tag 0F78, a remark

Tag 0F78 in the Stacks Project.

AlgebraicGeometry.sheafifiedPushforwardMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SheafifiedPushforward.lean, line 66. The attribute's comment: “canonical map”.

Stacks 0F78. The map from the sheafification of G to the small-étale direct image of the sheafification of G' induced by a map α : G ⟶ g_* G' of abelian presheaves.

public def sheafifiedPushforwardMap
    (G : (SmallEtale B S.obj S.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (G' : (SmallEtale B T.obj T.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (α : G ⟶ (smallEtaleBaseChange B g).op ⋙ G') :
    (SmallEtale.topology B S.obj S.property).sheafify G ⟶
      (smallEtaleBaseChange B g).op ⋙
        (SmallEtale.topology B T.obj T.property).sheafify G'

AlgebraicGeometry.sheafifiedPushforwardMap_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SheafifiedPushforward.lean, line 84. The attribute's comment: “commutative square”.

Stacks 0F78. The induced map commutes with the two sheafification maps.

public theorem sheafifiedPushforwardMap_comm
    (G : (SmallEtale B S.obj S.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (G' : (SmallEtale B T.obj T.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (α : G ⟶ (smallEtaleBaseChange B g).op ⋙ G') :
    (SmallEtale.topology B S.obj S.property).toSheafify G ≫
        sheafifiedPushforwardMap B g G G' α =
      α ≫ Functor.whiskerLeft (smallEtaleBaseChange B g).op
        ((SmallEtale.topology B T.obj T.property).toSheafify G')

AlgebraicGeometry.sheafifiedPushforwardMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SheafifiedPushforward.lean, line 97. The attribute's comment: “uniqueness”.

Stacks 0F78. The commutative square of the previous result determines the induced map uniquely.

public theorem sheafifiedPushforwardMap_unique
    (G : (SmallEtale B S.obj S.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (G' : (SmallEtale B T.obj T.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (α : G ⟶ (smallEtaleBaseChange B g).op ⋙ G')
    (β : (SmallEtale.topology B S.obj S.property).sheafify G ⟶
      (smallEtaleBaseChange B g).op ⋙
        (SmallEtale.topology B T.obj T.property).sheafify G')
    (hβ : (SmallEtale.topology B S.obj S.property).toSheafify G ≫ β =
      α ≫ Functor.whiskerLeft (smallEtaleBaseChange B g).op
        ((SmallEtale.topology B T.obj T.property).toSheafify G')) :
    β = sheafifiedPushforwardMap B g G G' α

AlgebraicGeometry.sheafifiedPushforwardAdjoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SheafifiedPushforward.lean, line 113. The attribute's comment: “adjoint map”.

Stacks 0F78. The induced map transported through the adjunction between the small-étale inverse image and direct image along g.

public def sheafifiedPushforwardAdjoint
    (G : (SmallEtale B S.obj S.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (G' : (SmallEtale B T.obj T.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (α : G ⟶ (smallEtaleBaseChange B g).op ⋙ G') :
    ((smallEtaleBaseChange B g).sheafPullback AddCommGrpCat.{u + 1}
      (SmallEtale.topology B S.obj S.property)
      (SmallEtale.topology B T.obj T.property)).obj
        ⟨(SmallEtale.topology B S.obj S.property).sheafify G,
          (SmallEtale.topology B S.obj S.property).sheafify_isSheaf G⟩ ⟶
      ⟨(SmallEtale.topology B T.obj T.property).sheafify G',
        (SmallEtale.topology B T.obj T.property).sheafify_isSheaf G'⟩

AlgebraicGeometry.sheafifiedPushforwardMap_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SheafifiedPushforward.lean, line 137. The attribute's comment: “geometric stalk formula”.

Stacks 0F78. The germ, at a lift p' of a geometric point of T, of a section of G over an étale neighborhood U of the image point is carried by the adjoint map to the germ over the base-changed neighborhood of the image of the section under α.

public theorem sheafifiedPushforwardMap_stalk
    (G : (SmallEtale B S.obj S.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (G' : (SmallEtale B T.obj T.property)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
    (α : G ⟶ (smallEtaleBaseChange B g).op ⋙ G')
    (s' : GeometricPoint T.obj)
    [HasColimit ((CategoryOfElements.π
      (geometricPointFiber B T.obj T.property s')).op ⋙
        (((smallEtaleBaseChange B g).sheafPullback AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S.obj S.property)
          (SmallEtale.topology B T.obj T.property)).obj
            ⟨(SmallEtale.topology B S.obj S.property).sheafify G,
              (SmallEtale.topology B S.obj S.property).sheafify_isSheaf G⟩).obj)]
    [HasColimit ((CategoryOfElements.π
      (geometricPointFiber B T.obj T.property s')).op ⋙
        (SmallEtale.topology B T.obj T.property).sheafify G')] :
    let F : Sheaf (SmallEtale.topology B S.obj S.property) AddCommGrpCat.{u + 1} :=
      ⟨(SmallEtale.topology B S.obj S.property).sheafify G,
        (SmallEtale.topology B S.obj S.property).sheafify_isSheaf G⟩
    let D := (CategoryOfElements.π
      (geometricPointFiber B T.obj T.property s')).op ⋙
        (((smallEtaleBaseChange B g).sheafPullback AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S.obj S.property)
          (SmallEtale.topology B T.obj T.property)).obj F).obj
    let D' := (CategoryOfElements.π
      (geometricPointFiber B T.obj T.property s')).op ⋙
        (SmallEtale.topology B T.obj T.property).sheafify G'
    ∀ (U : SmallEtale B S.obj S.property)
        (p' : (geometricPointFiber B T.obj T.property s').obj
          ((smallEtaleBaseChange B g).obj U)),
        (((SmallEtale.topology B S.obj S.property).toSheafify G).app (op U) ≫
            (((smallEtaleBaseChange B g).sheafAdjunctionContinuous
              AddCommGrpCat.{u + 1}
              (SmallEtale.topology B S.obj S.property)
              (SmallEtale.topology B T.obj T.property)).unit.app F).hom.app (op U) ≫
            colimit.ι D (op (Functor.elementsMk _ ((smallEtaleBaseChange B g).obj U) p')) ≫
            colim.map (Functor.whiskerLeft
              ((CategoryOfElements.π
                (geometricPointFiber B T.obj T.property s')).op)
              (sheafifiedPushforwardAdjoint B g G G' α).hom)) =
          α.app (op U) ≫
            ((SmallEtale.topology B T.obj T.property).toSheafify G').app
              (op ((smallEtaleBaseChange B g).obj U)) ≫
              colimit.ι D' (op (Functor.elementsMk _ ((smallEtaleBaseChange B g).obj U) p'))
Tag 0F5J, a lemma

Tag 0F5J in the Stacks Project.

AlgebraicGeometry.SmallEtale.fiberPointBaseChange_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChange.lean, line 102. The attribute's comment: “the bijection of geometric fibres induced by the horizontal morphism”.

Stacks 0F5J. For a cartesian square, p induces a bijection from the geometric fibre of f' over a geometric point t of Y' onto the geometric fibre of f over the image of t: transitivity of fibre products identifies X'_t with X_{g ∘ t}.

public theorem fiberPointBaseChange_bijective (sq : IsPullback p f' f g)
    (t : GeometricPoint Y'.obj) :
    Function.Bijective (fiberPointBaseChange B p f' f g sq t)

AlgebraicGeometry.SmallEtale.fiberStalkBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChange.lean, line 149. The attribute's comment: “the identification of the stalks over corresponding points of the fibres”.

Stacks 0F5J. The stalk of the inverse image p⁻¹F at a point x of the geometric fibre of f' is the stalk of F at the corresponding point of the geometric fibre of f. This is the right vertical arrow of the comparison square of Stacks 0F5J.

public def fiberStalkBaseChangeIso (sq : IsPullback p f' f g) (t : GeometricPoint Y'.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v})
    (x : GeometricFiberPoint B f' t) :
    etaleStalk B X.obj X.property
        ((fiberPointBaseChange B p f' f g sq t x).toGeometricPoint B f
          (t.map (B.inclusion.map g))) F.obj ≅
      etaleStalk B X'.obj X'.property (x.toGeometricPoint B f' t)
        ((abPullback.{u, v} B p).obj F).obj

AlgebraicGeometry.SmallEtale.fiberStalksBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChange.lean, line 164. The attribute's comment: “the comparison of the two direct sums of stalks over the geometric fibres”.

Stacks 0F5J. The direct sums of stalks over the two geometric fibres agree: the fibres are in bijection through p, and over corresponding points the stalks of F and of p⁻¹F agree.

public def fiberStalksBaseChangeEquiv (sq : IsPullback p f' f g) (t : GeometricPoint Y'.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    fiberStalks.{u, max (u + 1) v} B f (t.map (B.inclusion.map g)) F ≃+
      fiberStalks.{u, max (u + 1) v} B f' t ((abPullback.{u, v} B p).obj F)

AlgebraicGeometry.SmallEtale.fiberStalksBaseChangeEquiv_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChange.lean, line 190. The attribute's comment: “functoriality in the sheaf of the comparison of the direct sums of stalks”.

Stacks 0F5J. The comparison of the two direct sums of stalks is functorial in the abelian sheaf: it intertwines the map induced on the direct sum of stalks over the geometric fibre of f by a morphism of sheaves with the map induced over the geometric fibre of f' by its inverse image.

public theorem fiberStalksBaseChangeEquiv_natural (sq : IsPullback p f' f g)
    (t : GeometricPoint Y'.obj)
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}}
    (φ : F ⟶ G) (w : fiberStalks.{u, max (u + 1) v} B f (t.map (B.inclusion.map g)) F) :
    fiberStalksBaseChangeEquiv B p f' f g sq t G
        (fiberStalksMap.{u, max (u + 1) v} B f (t.map (B.inclusion.map g)) φ w) =
      fiberStalksMap.{u, max (u + 1) v} B f' t ((abPullback.{u, v} B p).map φ)
        (fiberStalksBaseChangeEquiv B p f' f g sq t F w)

AlgebraicGeometry.SmallEtale.fShriekStalkBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChange.lean, line 232. The attribute's comment: “the base-change isomorphism on the stalk at a geometric point of the base”.

Stacks 0F5J. The base-change comparison on stalks: for a geometric point t of Y' the stalk of g⁻¹f_!F at t is the stalk of f'_!p⁻¹F at t. It is obtained from the stalk decompositions of Stacks 0F5F on both sides, the bijection of geometric fibres and the identification of the stalks over corresponding points of the fibres, so it is compatible with those decompositions by construction.

public def fShriekStalkBaseChangeIso (sq : IsPullback p f' f g) (t : GeometricPoint Y'.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    etaleStalk B Y'.obj Y'.property t
        ((abPullback.{u, v} B g).obj ((fShriekFunctor.{u, v} B f).obj F)).obj ≅
      etaleStalk B Y'.obj Y'.property t
        ((fShriekFunctor.{u, v} B f').obj ((abPullback.{u, v} B p).obj F)).obj

AlgebraicGeometry.SmallEtale.fShriekStalkBaseChangeIso_comp_fShriekStalkIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChange.lean, line 250. The attribute's comment: “compatibility of the stalkwise comparison with the decompositions of 0F5F”.

Stacks 0F5J. The precise compatibility of the stalkwise base-change comparison with the stalk decompositions of Stacks 0F5F: the square whose horizontal arrows are those decompositions, whose left vertical arrow is the comparison preceded by the identification of the stalk of an inverse image, and whose right vertical arrow is the summandwise comparison of the two direct sums, commutes.

public theorem fShriekStalkBaseChangeIso_comp_fShriekStalkIso (sq : IsPullback p f' f g)
    (t : GeometricPoint Y'.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    (etaleStalkSmallEtalePullObjIso B g t AddCommGrpCat.{max (u + 1) v}
          ((fShriekFunctor.{u, v} B f).obj F)).inv ≫
        (fShriekStalkBaseChangeIso B p f' f g sq t F).hom ≫
        (fShriekStalkIso.{u, v} B f' t ((abPullback.{u, v} B p).obj F)).hom =
      (fShriekStalkIso.{u, v} B f (t.map (B.inclusion.map g)) F).hom ≫
        AddCommGrpCat.ofHom
          (fiberStalksBaseChangeEquiv B p f' f g sq t F).toAddMonoidHom

AlgebraicGeometry.SmallEtale.fiberStalkComponent_fiberBaseChangeSectionsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 215. The attribute's comment: “the germ of a base-changed supported section at a point of the geometric fibre”.

Stacks 0F5J. The germ at a point of the geometric fibre of f' of the base change of a supported section is the germ of the section at the corresponding point of the geometric fibre of f, read through the identification of the two stalks. This is the commutative square of the source, on a single summand of the stalk decompositions of Stacks 0F5F.

public theorem fiberStalkComponent_fiberBaseChangeSectionsMap
    (s : supportedSections B X.obj X.property F (baseChange B f V) E.1
      (finiteSupport_isLocallyClosed B f V E))
    (x : GeometricFiberPoint B f' t) :
    fiberStalkComponent.{u, u + 1} B f' t ((abPullback.{u, u + 1} B p).obj F)
        (baseChange B g V) (geometricPointFiberBaseChangeEquiv B g t V u)
        (fiberBaseChangeSupport B p f' f g sq V E)
        (fiberBaseChangeSectionsMap.{u, u + 1} B p f' f g sq V E F s) x =
      (fiberStalkBaseChangeIso.{u, u + 1} B p f' f g sq t F x).hom
        (fiberStalkComponent.{u, u + 1} B f (t.map (B.inclusion.map g)) F V u E s
          (fiberPointBaseChange B p f' f g sq t x))

AlgebraicGeometry.SmallEtale.fiberBaseChangeDiagramMap_comp_fiberStalkHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 338. The attribute's comment: “the germ decompositions exchanged by the base-change map on supported sections”.

Stacks 0F5J. The germ decompositions of Stacks 0F5F on the two sides of the square are exchanged by the base-change map on supported sections and the comparison of the direct sums of stalks over the two geometric fibres.

public theorem fiberBaseChangeDiagramMap_comp_fiberStalkHom
    [LocallyOfFiniteType (B.inclusion.map f)] [LocallyOfFiniteType (B.inclusion.map f')] :
    fiberBaseChangeDiagramMap.{u, u + 1} B p f' f g sq V F E ≫
        fiberStalkHom.{u, u + 1} B f' t ((abPullback.{u, u + 1} B p).obj F)
          (baseChange B g V) (geometricPointFiberBaseChangeEquiv B g t V u)
          (fiberBaseChangeSupport B p f' f g sq V E) =
      fiberStalkHom.{u, u + 1} B f (t.map (B.inclusion.map g)) F V u E ≫
        (AddEquiv.toAddCommGrpIso
          (fiberStalksBaseChangeEquiv.{u, u + 1} B p f' f g sq t F)).hom

AlgebraicGeometry.SmallEtale.fShriekBaseChangeMap_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 593. The attribute's comment: “the base-change map on the stalk at a geometric point, through the 0F5F decompositions”.

Stacks 0F5J. On the stalk at a geometric point t of Y' the base-change map is the base-change comparison of stalks: the identification of the stalk of an inverse image, the stalk decomposition of Stacks 0F5F for f, and the comparison of the direct sums of stalks over the two geometric fibres.

public theorem fShriekBaseChangeMap_stalk :
    (etaleStalkPresheafFunctor B Y'.obj Y'.property t AddCommGrpCat.{u + 1}).map
          (fShriekBaseChangeMap.{u} B p f' f g sq F).hom ≫
        (fShriekStalkIso.{u, u + 1} B f' t ((abPullback.{u, u + 1} B p).obj F)).hom =
      (etaleStalkSmallEtalePullObjIso B g t AddCommGrpCat.{u + 1}
          ((fShriekFunctor.{u, u + 1} B f).obj F)).hom ≫
        (fShriekStalkIso.{u, u + 1} B f (t.map (B.inclusion.map g)) F).hom ≫
        (AddEquiv.toAddCommGrpIso
          (fiberStalksBaseChangeEquiv.{u, u + 1} B p f' f g sq t F)).hom

AlgebraicGeometry.SmallEtale.fShriekBaseChangeMap_stalk_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 662. The attribute's comment: “the stalk of the base-change map is the stalkwise base-change isomorphism”.

Stacks 0F5J. The base-change map is, on the stalk at a geometric point of Y', the base-change isomorphism of stalks of StacksFrontier.AlgebraicGeometry.Etale.FShriekBaseChange.

public theorem fShriekBaseChangeMap_stalk_eq :
    (etaleStalkPresheafFunctor B Y'.obj Y'.property t AddCommGrpCat.{u + 1}).map
        (fShriekBaseChangeMap.{u} B p f' f g sq F).hom =
      (fShriekStalkBaseChangeIso.{u, u + 1} B p f' f g sq t F).hom

AlgebraicGeometry.SmallEtale.isIso_fShriekBaseChangeMap, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 684. The attribute's comment: “the base-change map is an isomorphism”.

Stacks 0F5J. The base-change map g⁻¹f_!F ⟶ f'_!(p⁻¹F) is an isomorphism: it is an isomorphism on the stalk at every geometric point of Y', both sides becoming the direct sum of the stalks of F over the geometric fibre, and a map of abelian étale sheaves which is an isomorphism on every geometric stalk is an isomorphism, which is Stacks 03PU.

public instance isIso_fShriekBaseChangeMap :
    IsIso (fShriekBaseChangeMap.{u} B p f' f g sq F)

AlgebraicGeometry.SmallEtale.fShriekBaseChangeNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 703. The attribute's comment: “the isomorphism g⁻¹f_!F ≅ f'_!(p⁻¹F), functorial in F”.

Stacks 0F5J. For a cartesian square with f locally quasi-finite there is an isomorphism g⁻¹f_!F ≅ f'_!(p⁻¹F), functorial in the abelian sheaf F on the small étale site of X: the map c of the source, sheafified and transposed, which is an isomorphism because it is one on every geometric stalk.

public def fShriekBaseChangeNatIso :
    fShriekFunctor.{u, u + 1} B f ⋙ abPullback.{u, u + 1} B g ≅
      abPullback.{u, u + 1} B p ⋙ fShriekFunctor.{u, u + 1} B f'

AlgebraicGeometry.SmallEtale.fShriekBaseChangeNatIso_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 722. The attribute's comment: “the isomorphism agrees with the stalk descriptions of 0F5F”.

Stacks 0F5J. The base-change isomorphism agrees with the stalk descriptions of Stacks 0F5F: on the stalk at a geometric point t of Y' it is the identification of the stalk of an inverse image followed by the stalk decomposition of f_!F at the image point, the comparison of the direct sums of stalks over the two geometric fibres, and the inverse of the stalk decomposition of f'_!(p⁻¹F).

public theorem fShriekBaseChangeNatIso_stalk (t : GeometricPoint Y'.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
    (etaleStalkPresheafFunctor B Y'.obj Y'.property t AddCommGrpCat.{u + 1}).map
          ((fShriekBaseChangeNatIso.{u} B p f' f g sq).hom.app F).hom ≫
        (fShriekStalkIso.{u, u + 1} B f' t ((abPullback.{u, u + 1} B p).obj F)).hom =
      (etaleStalkSmallEtalePullObjIso B g t AddCommGrpCat.{u + 1}
          ((fShriekFunctor.{u, u + 1} B f).obj F)).hom ≫
        (fShriekStalkIso.{u, u + 1} B f (t.map (B.inclusion.map g)) F).hom ≫
        (AddEquiv.toAddCommGrpIso
          (fiberStalksBaseChangeEquiv.{u, u + 1} B p f' f g sq t F)).hom

AlgebraicGeometry.SmallEtale.exists_fShriekBaseChangeIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeIso.lean, line 751. The attribute's comment: “the isomorphism, functorial in the sheaf and compatible with the 0F5F stalk descriptions”.

Stacks 0F5J. For a cartesian square of a big étale site with f locally quasi-finite there is an isomorphism g⁻¹f_!F ≅ f'_!(p⁻¹F), functorial in F in the abelian sheaves on the small étale site of X, which agrees with the stalk descriptions of Stacks 0F5F: on the stalk at a geometric point t of Y' it is the identification of the stalk of an inverse image, the stalk decomposition of f_!F at the image point, and the comparison of the direct sums of the stalks over the two geometric fibres.

Only the hypotheses of the source are assumed: the finite-type and quasi-finiteness conditions on the base change f' are supplied from the cartesian square.

public theorem exists_fShriekBaseChangeIso :
    letI := locallyOfFiniteType_of_isPullback B p f' f g sq
    letI := locallyQuasiFinite_of_isPullback B p f' f g sq
    ∃ e : fShriekFunctor.{u, u + 1} B f ⋙ abPullback.{u, u + 1} B g ≅
        abPullback.{u, u + 1} B p ⋙ fShriekFunctor.{u, u + 1} B f',
      ∀ (t : GeometricPoint Y'.obj)
        (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}),
        (etaleStalkPresheafFunctor B Y'.obj Y'.property t AddCommGrpCat.{u + 1}).map
              (e.hom.app F).hom ≫
            (fShriekStalkIso.{u, u + 1} B f' t ((abPullback.{u, u + 1} B p).obj F)).hom =
          (etaleStalkSmallEtalePullObjIso B g t AddCommGrpCat.{u + 1}
              ((fShriekFunctor.{u, u + 1} B f).obj F)).hom ≫
            (fShriekStalkIso.{u, u + 1} B f (t.map (B.inclusion.map g)) F).hom ≫
            (AddEquiv.toAddCommGrpIso
              (fiberStalksBaseChangeEquiv.{u, u + 1} B p f' f g sq t F)).hom

AlgebraicGeometry.SmallEtale.fiberBaseChangePresheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeMap.lean, line 232. The attribute's comment: “the map c of abelian presheaves”.

Stacks 0F5J. The map c of the proof: the map of abelian presheaves on the small étale site of Y from the finite-support direct image f_{p!}F to the direct image along g of f'_!(p⁻¹F).

public def fiberBaseChangePresheafMap
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
    (finiteSupportPushforward.{u, u + 1} B f (fun _ => inferInstance)).1.obj F ⟶
      (smallEtaleBaseChange B g).op ⋙
        ((fShriekFunctor.{u, u + 1} B f').obj ((abPullback.{u, u + 1} B p).obj F)).obj

AlgebraicGeometry.SmallEtale.fShriekBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeMap.lean, line 281. The attribute's comment: “the base-change map of sheaves, before it is shown to be an isomorphism”.

Stacks 0F5J. The base-change map g⁻¹f_!F ⟶ f'_!(p⁻¹F) of abelian sheaves on the small étale site of Y': the map c of the source, sheafified and transposed through the inverse-image adjunction along g.

public def fShriekBaseChangeMap
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
    (abPullback.{u, u + 1} B g).obj ((fShriekFunctor.{u, u + 1} B f).obj F) ⟶
      (fShriekFunctor.{u, u + 1} B f').obj ((abPullback.{u, u + 1} B p).obj F)

AlgebraicGeometry.SmallEtale.fShriekBaseChangeNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeMap.lean, line 380. The attribute's comment: “functoriality in the sheaf of the base-change map of sheaves”.

Stacks 0F5J. The base-change map g⁻¹f_!F ⟶ f'_!(p⁻¹F) is functorial in F: it is a morphism of functors on abelian sheaves on the small étale site of X.

public def fShriekBaseChangeNatTrans :
    fShriekFunctor.{u, u + 1} B f ⋙ abPullback.{u, u + 1} B g ⟶
      abPullback.{u, u + 1} B p ⋙ fShriekFunctor.{u, u + 1} B f'

AlgebraicGeometry.SmallEtale.fiberBaseChangeColimitMap_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeRestriction.lean, line 362. The attribute's comment: “naturality in the test object of the map c”.

Stacks 0F5J. The base-change map on finite-support sections is compatible with the restriction maps of the finite-support direct image presheaves: restricting a section to a smaller test object V₁ of Y and then base changing it along the square is base changing it and then restricting along V'₁ ⟶ V'. This is the naturality in V of the map c of the source.

public theorem fiberBaseChangeColimitMap_restriction :
    finiteSupportBaseChangeHom B f F i ≫ fiberBaseChangeColimitMap B p f' f g sq V₁ F =
      fiberBaseChangeColimitMap B p f' f g sq V F ≫
        finiteSupportBaseChangeHom B f' ((abPullback.{u, v} B p).obj F)
          ((smallEtaleBaseChange B g).map i)

AlgebraicGeometry.SmallEtale.fiberBaseChangeSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeSupport.lean, line 461. The attribute's comment: “the base change of a support finite over the test object”.

Stacks 0F5J. The base change of a support finite over V along the cartesian square: the inverse image of the support under the comparison of the two étale base changes. It is again a support finite over V'.

public def fiberBaseChangeSupport (sq : IsPullback p f' f g)
    (V : SmallEtale B Y.obj Y.property) (E : FiniteSupport B f V) :
    FiniteSupport B f' (baseChange B g V)

AlgebraicGeometry.SmallEtale.fiberBaseChangeSectionsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeSupport.lean, line 614. The attribute's comment: “the pullback map H_Z(F) ⟶ H_{Z'}(p⁻¹F) on supported sections”.

Stacks 0F5J. The pullback map on supported sections: a section of F supported on a support E finite over V is carried by the unit of the inverse-image adjunction to a section of p⁻¹F supported on the base change of E.

public def fiberBaseChangeSectionsMap (sq : IsPullback p f' f g)
    (V : SmallEtale B Y.obj Y.property) (E : FiniteSupport B f V)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    supportedSections B X.obj X.property F (baseChange B f V) E.1
        (finiteSupport_isLocallyClosed B f V E) →+
      supportedSections B X'.obj X'.property ((abPullback.{u, v} B p).obj F)
        (baseChange B f' (baseChange B g V)) (fiberBaseChangeSupport B p f' f g sq V E).1
        (finiteSupport_isLocallyClosed B f' (baseChange B g V)
          (fiberBaseChangeSupport B p f' f g sq V E))

AlgebraicGeometry.SmallEtale.fiberBaseChangeSectionsMap_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeSupport.lean, line 796. The attribute's comment: “compatibility of the pullback map with the transitions of the colimit”.

Stacks 0F5J. The pullback map on supported sections is compatible with the transition maps of Stacks 0F6H: enlarging the support commutes with base change. This is what makes the pullback maps a map out of the colimit defining f_{p!}F.

public theorem fiberBaseChangeSectionsMap_transition (sq : IsPullback p f' f g)
    (V : SmallEtale B Y.obj Y.property) {E E₁ : FiniteSupport B f V} (hle : E ≤ E₁)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    (fiberBaseChangeSectionsMap B p f' f g sq V E₁ F).comp
        (supportedSectionsMap B X.obj X.property F (baseChange B f V) E.1 E₁.1
          (finiteSupport_isLocallyClosed B f V E) (finiteSupport_isLocallyClosed B f V E₁) hle
          (finiteSupport_closedWithin B f V E E₁ hle)) =
      (supportedSectionsMap B X'.obj X'.property ((abPullback.{u, v} B p).obj F)
          (baseChange B f' (baseChange B g V))
          (fiberBaseChangeSupport B p f' f g sq V E).1
          (fiberBaseChangeSupport B p f' f g sq V E₁).1
          (finiteSupport_isLocallyClosed B f' (baseChange B g V)
            (fiberBaseChangeSupport B p f' f g sq V E))
          (finiteSupport_isLocallyClosed B f' (baseChange B g V)
            (fiberBaseChangeSupport B p f' f g sq V E₁))
          (fiberBaseChangeSupport_mono B p f' f g sq V hle)
          (finiteSupport_closedWithin B f' (baseChange B g V)
            (fiberBaseChangeSupport B p f' f g sq V E)
            (fiberBaseChangeSupport B p f' f g sq V E₁)
            (fiberBaseChangeSupport_mono B p f' f g sq V hle))).comp
        (fiberBaseChangeSectionsMap B p f' f g sq V E F)

AlgebraicGeometry.SmallEtale.fiberBaseChangeSectionsMap_sheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeSupport.lean, line 851. The attribute's comment: “functoriality in the sheaf of the pullback map on supported sections”.

Stacks 0F5J. The pullback map on supported sections is functorial in the abelian sheaf: a morphism of sheaves on X acts on the pullbacks through its inverse image.

public theorem fiberBaseChangeSectionsMap_sheafMap (sq : IsPullback p f' f g)
    (V : SmallEtale B Y.obj Y.property) (E : FiniteSupport B f V)
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}}
    (φ : F ⟶ G) :
    (fiberBaseChangeSectionsMap B p f' f g sq V E G).comp
        (supportedSectionsSheafMap B X.obj X.property φ (baseChange B f V) E.1
          (finiteSupport_isLocallyClosed B f V E)) =
      (supportedSectionsSheafMap B X'.obj X'.property ((abPullback.{u, v} B p).map φ)
          (baseChange B f' (baseChange B g V))
          (fiberBaseChangeSupport B p f' f g sq V E).1
          (finiteSupport_isLocallyClosed B f' (baseChange B g V)
            (fiberBaseChangeSupport B p f' f g sq V E))).comp
        (fiberBaseChangeSectionsMap B p f' f g sq V E F)

AlgebraicGeometry.SmallEtale.fiberBaseChangeColimitMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeSupport.lean, line 917. The attribute's comment: “the map c on finite-support sections over a test object”.

Stacks 0F5J. The base-change map on finite-support sections over an étale test object V of Y: the generator of a support Z carrying a section s goes to the generator of the base change of Z carrying the pullback of s. This is the map c of the source, over V.

public def fiberBaseChangeColimitMap (sq : IsPullback p f' f g)
    (V : SmallEtale B Y.obj Y.property)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    finiteSupportSections B f F V ⟶
      finiteSupportSections B f' ((abPullback.{u, v} B p).obj F) (baseChange B g V)

AlgebraicGeometry.SmallEtale.fiberBaseChangeColimitMap_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekBaseChangeSupport.lean, line 940. The attribute's comment: “functoriality in the sheaf of the map c over a test object”.

Stacks 0F5J. The base-change map on finite-support sections over an étale test object is functorial in the abelian sheaf.

public theorem fiberBaseChangeColimitMap_natural (sq : IsPullback p f' f g)
    (V : SmallEtale B Y.obj Y.property)
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}}
    (φ : F ⟶ G) :
    colim.map (finiteSupportDiagramMap B f φ V) ≫
        fiberBaseChangeColimitMap B p f' f g sq V G =
      fiberBaseChangeColimitMap B p f' f g sq V F ≫
        colim.map (finiteSupportDiagramMap B f' ((abPullback.{u, v} B p).map φ)
          (baseChange B g V))
Tag 0F79, a lemma

Tag 0F79 in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekCompProperIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompProperSupportCompat.lean, line 70. The attribute's comment: “part (b), compatibility with the base change isomorphisms of 0F5J and 0F55”.

Stacks 0F79, part (b). For a base change b : Z₁ ⟶ Z, with cartesian squares X₁ = X ×_Y Y₁ and Y₁ = Y ×_Z Z₁, the isomorphism (g ∘ f)_! ≅ g_! ∘ f_! of Stacks 0F79 is compatible with the base-change isomorphisms of Stacks 0F5J and 0F55: the base-change isomorphism b⁻¹ (g ∘ f)_! F ≅ (g₁ ∘ f₁)_! a⁻¹ F of Stacks 0F5J followed by the isomorphism for f₁ and g₁ equals b⁻¹ of the isomorphism for f and g, followed by the base change b⁻¹ g_! ⟶ g₁_! b'⁻¹ of Stacks 0F55 and g₁_! of the base-change isomorphism b'⁻¹ f_! F ≅ f₁_! a⁻¹ F of Stacks 0F5J.

public theorem fShriekCompProperIso_baseChange :
    letI := locallyOfFiniteType_of_isPullback B a f₁ f b' sq₁
    letI := locallyQuasiFinite_of_isPullback B a f₁ f b' sq₁
    letI := locallyOfFiniteType_of_isPullback B b' g₁ g b sq₂
    letI : IsSeparated (B.inclusion.map g₁) :=
      MorphismProperty.of_isPullback (sq₂.map B.inclusion) inferInstance
    letI : LocallyQuasiFinite (B.inclusion.map (f₁ ≫ g₁)) :=
      MorphismProperty.of_isPullback ((sq₁.paste_vert sq₂).map B.inclusion) inferInstance
    (fShriekBaseChangeNatIso.{u} B a (f₁ ≫ g₁) (f ≫ g) b (sq₁.paste_vert sq₂)).hom.app F ≫
        (fShriekCompProperIso.{u, u + 1} B f₁ g₁).hom.app ((abPullback.{u, u + 1} B a).obj F) =
      (abPullback.{u, u + 1} B b).map ((fShriekCompProperIso.{u, u + 1} B f g).hom.app F) ≫
        properSupportBaseChange.{u, u + 1} B b' g₁ g b sq₂
          ((fShriekFunctor.{u, u + 1} B f).obj F) ≫
        (properSupportFunctor.{u, u + 1} B g₁).map
          ((fShriekBaseChangeNatIso.{u} B a f₁ f b' sq₁).hom.app F)

AlgebraicGeometry.SmallEtale.fShriekCompProperIso_eq_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompProperSupportCompat.lean, line 108. The attribute's comment: “part (c), the isomorphism of 0F50 via the identifications of 0F6N for f' separated”.

Stacks 0F79, part (c). If f is separated as well, the isomorphism (g ∘ f)_! ≅ g_! ∘ f_! of Stacks 0F79 is the isomorphism (g ∘ f)_! = g_! ∘ f_! of proper-support direct images of Stacks 0F50, read through the identifications of Stacks 0F6N of (g ∘ f)_! and f_! with their proper-support models.

public theorem fShriekCompProperIso_eq_of_isSeparated [IsSeparated (B.inclusion.map f)] :
    letI := isSeparated_map_comp B f g
    fShriekCompProperIso.{u, v} B f g =
      fShriekFunctorIsoProperSupport.{u, v} B (f ≫ g) ≪≫
        (properSupportFunctor_compIso B f g).val.symm ≪≫
        Functor.isoWhiskerRight (fShriekFunctorIsoProperSupport.{u, v} B f).symm
          (properSupportFunctor.{u, max (u + 1) v} B g)

AlgebraicGeometry.SmallEtale.fShriekCompProperIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompProperSupportIso.lean, line 592. The attribute's comment: “the canonical isomorphism g_! ∘ f'_! ≅ f_!”.

Stacks 0F79. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of a big étale site with f and f ≫ g locally quasi-finite (locally of finite type and locally quasi-finite) and g separated and locally of finite type. Then there is a canonical isomorphism of functors on abelian étale sheaves (g ∘ f)_! ≅ g_! ∘ f_!, where f_! and (g ∘ f)_! are the direct images with compact support of locally quasi-finite morphisms (Stacks 0F6R) and g_! is the proper-support direct image of Stacks 0F4X. Its component at F is the map c' of the source, AlgebraicGeometry.SmallEtale.sepCompShriekMap: the sheafification of the map sending a local generator (T, s) of (g ∘ f)_{p!} F over W to the generator (T, s) of f_{p!} F over W ×_Z Y, through X_{W ×_Z Y} = X_W.

public def fShriekCompProperIso :
    fShriekFunctor.{u, v} B (f ≫ g) ≅
      fShriekFunctor.{u, v} B f ⋙ properSupportFunctor.{u, max (u + 1) v} B g

AlgebraicGeometry.SmallEtale.sepCompShriekMap_openCovariance, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompProperSupportOpen.lean, line 400. The attribute's comment: “part (a), compatibility with covariance for open embeddings, Remarks 0F53, 0F6S”.

Stacks 0F79, part (a). Let f : X ⟶ Y and g : Y ⟶ Z be as in Stacks 0F79, let jY : Y₁ ⟶ Y be an open immersion, and let X₁ = X ×_Y Y₁ with projections jX : X₁ ⟶ X and f₁ : X₁ ⟶ Y₁. Then the isomorphism c' of Stacks 0F79 is compatible with covariance with respect to open embeddings: the composite of the covariance map (jX ≫ f ≫ g)_!(F|_{X₁}) ⟶ (f ≫ g)_! F of Stacks 0F6S with c' : (f ≫ g)_! F ⟶ g_!(f_! F) equals the composite of c' for f₁ and jY ≫ g, (f₁ ≫ jY ≫ g)_!(F|_{X₁}) ⟶ (jY ≫ g)_!(f₁_!(F|_{X₁})), the identification f₁_!(F|_{X₁}) ≅ (f_! F)|_{Y₁} of Stacks 0F5J ("the construction of f_! is local on the base") and the extension by zero (jY ≫ g)_!((f_! F)|_{Y₁}) ⟶ g_!(f_! F) of Stacks 0F53.

public theorem sepCompShriekMap_openCovariance :
    letI : IsOpenImmersion (B.inclusion.map jX) :=
      MorphismProperty.of_isPullback (sq.flip.map B.inclusion) inferInstance
    letI := locallyOfFiniteType_of_isPullback B jX f₁ f jY sq
    letI := locallyQuasiFinite_of_isPullback B jX f₁ f jY sq
    letI : IsSeparated (B.inclusion.map (jY ≫ g)) := by
      rw [Functor.map_comp]
      infer_instance
    letI : LocallyQuasiFinite (B.inclusion.map (f₁ ≫ jY ≫ g)) := by
      rw [show f₁ ≫ jY ≫ g = jX ≫ f ≫ g by rw [← Category.assoc, ← sq.w, Category.assoc]]
      infer_instance
    (openCovarianceShriekMap.{u, u + 1} B jX (f ≫ g)).app F ≫ sepCompShriekMap.{u, u + 1} B f g F =
      eqToHom (congrArg (fun G => G.obj ((openRestriction.{u, u + 1} B jX).obj F))
        (fShriekFunctor_congr.{u, u + 1} B
          (show jX ≫ f ≫ g = f₁ ≫ jY ≫ g by rw [← Category.assoc, sq.w, Category.assoc]))) ≫
      sepCompShriekMap.{u, u + 1} B f₁ (jY ≫ g) ((openRestriction.{u, u + 1} B jX).obj F) ≫
      (properSupportFunctor.{u, u + 1} B (jY ≫ g)).map
        ((fShriekBaseChangeNatIso.{u} B jX f₁ f jY sq).inv.app F) ≫
      (openInclusionShriekMap.{u, u + 1} B jY g ((fShriekFunctor.{u, u + 1} B f).obj F)).val
Tag 0F6T, a lemma

Tag 0F6T in the Stacks Project.

AlgebraicGeometry.SmallEtale.fShriekCompIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompBaseChange.lean, line 164. The attribute's comment: “part (5)”.

Stacks 0F6T, part (5). For a diagram with both squares cartesian 

X' --c--> X
|f'       |f
Y' --b--> Y
|g'       |g
Z' --a--> Z
and f, g locally quasi-finite, the composition isomorphisms and the base-change isomorphisms of Stacks 0F5J make the diagram 
a⁻¹(g ∘ f)_! ----------------> (g' ∘ f')_! c⁻¹
     |                                |
a⁻¹ g_! f_! --> g'_! b⁻¹ f_! --> g'_! f'_! c⁻¹
commute. The base changes f' and g' are locally quasi-finite because f and g are.

public theorem fShriekCompIso_baseChange :
    letI := locallyOfFiniteType_of_isPullback B c f' f b sq₁
    letI := locallyQuasiFinite_of_isPullback B c f' f b sq₁
    letI := locallyOfFiniteType_of_isPullback B b g' g a sq₂
    letI := locallyQuasiFinite_of_isPullback B b g' g a sq₂
    (fShriekBaseChangeNatIso.{u} B c (f' ≫ g') (f ≫ g) a (sq₁.paste_vert sq₂)).hom ≫
        Functor.whiskerLeft (abPullback.{u, u + 1} B c) (fShriekCompIso.{u, u + 1} B f' g').hom =
      Functor.whiskerRight (fShriekCompIso.{u, u + 1} B f g).hom (abPullback.{u, u + 1} B a) ≫
        Functor.whiskerLeft (fShriekFunctor.{u, u + 1} B f)
          (fShriekBaseChangeNatIso.{u} B b g' g a sq₂).hom ≫
        Functor.whiskerRight (fShriekBaseChangeNatIso.{u} B c f' f b sq₁).hom
          (fShriekFunctor.{u, u + 1} B g')

AlgebraicGeometry.SmallEtale.fShriekCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompIso.lean, line 136. The attribute's comment: “the canonical isomorphism (g ∘ f)_! ≅ g_! ∘ f_!”.

Stacks 0F6T. For composable locally quasi-finite morphisms f : X ⟶ Y and g : Y ⟶ Z there is a canonical isomorphism of functors (g ∘ f)_! ≅ g_! ∘ f_! on abelian étale sheaves: the comparison of AlgebraicGeometry.SmallEtale.compShriekMap, glued from the comparisons on the inverse images of the affine opens of Y, natural in the sheaf and an isomorphism on every geometric stalk.

public def fShriekCompIso :
    fShriekFunctor.{u, v} B (f ≫ g) ≅ fShriekFunctor.{u, v} B f ⋙ fShriekFunctor.{u, v} B g

AlgebraicGeometry.SmallEtale.fShriekCompIso_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompIso.lean, line 153. The attribute's comment: “part (3)”.

Stacks 0F6T, part (3). At a geometric point z̄ of Z, the isomorphism ((g ∘ f)_!F)_z̄ ≅ (g_!f_!F)_z̄ followed by the stalk decomposition (g_!f_!F)_z̄ = ⊕_{g(ȳ) = z̄} (f_!F)_ȳ of Stacks 0F5F is the stalk decomposition ((g ∘ f)_!F)_z̄ = ⊕_{g(f(x̄)) = z̄} F_x̄ followed by the regrouping of the geometric fibre of g ∘ f over the one of g, each F_x̄ being placed in (f_!F)_{f(x̄)} = ⊕_{f(x̄') = f(x̄)} F_x̄' through the decomposition of Stacks 0F5F for f.

public theorem fShriekCompIso_stalk (s : GeometricPoint Z.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) v}) :
    ((geometricPointSitePoint B Z.obj Z.property s).sheafFiber
        (A := AddCommGrpCat.{max (u + 1) v})).map ((fShriekCompIso B f g).hom.app F) ≫
      (fShriekStalkIso.{u, v} B g s ((fShriekFunctor.{u, v} B f).obj F)).hom =
    (fShriekStalkIso.{u, v} B (f ≫ g) s F).hom ≫
      AddCommGrpCat.ofHom (compFiberStalksMap B f g s F)

AlgebraicGeometry.SmallEtale.fShriekCompIso_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompIso.lean, line 275. The attribute's comment: “part (4)”.

Stacks 0F6T, part (4). For a third locally quasi-finite morphism h : Z ⟶ T the two isomorphisms (h ∘ g ∘ f)_! ≅ h_! ∘ g_! ∘ f_! obtained from the composition isomorphisms agree: through (h ∘ g)_! ∘ f_! and through h_! ∘ (g ∘ f)_!. The identification (h ∘ (g ∘ f))_! = ((h ∘ g) ∘ f)_! along the associativity of composition is written out.

public theorem fShriekCompIso_assoc :
    eqToHom (fShriekFunctor_congr.{u, v} B (Category.assoc f g h)) ≫
        (fShriekCompIso B f (g ≫ h)).hom ≫
        Functor.whiskerLeft (fShriekFunctor.{u, v} B f) (fShriekCompIso B g h).hom =
      (fShriekCompIso B (f ≫ g) h).hom ≫
        Functor.whiskerRight (fShriekCompIso B f g).hom (fShriekFunctor.{u, v} B h)

AlgebraicGeometry.SmallEtale.fShriekCompIso_eq_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompSeparated.lean, line 463. The attribute's comment: “part (1)”.

Stacks 0F6T, part (1). If f and g are separated, the isomorphism (g ∘ f)_! ≅ g_! ∘ f_! agrees with the identification g_! f_! = (g ∘ f)_! of proper-support direct images of Stacks 0F50, read through the identifications of Stacks 0F6N of the finite-support model of f_!, g_! and (g ∘ f)_! with the proper-support model.

public theorem fShriekCompIso_eq_of_isSeparated :
    fShriekCompIso B f g =
      fShriekFunctorIsoProperSupport.{u, v} B (f ≫ g) ≪≫
        (properSupportFunctor_compIso B f g).val.symm ≪≫
        Functor.isoWhiskerRight (fShriekFunctorIsoProperSupport.{u, v} B f).symm
          (properSupportFunctor.{u, max (u + 1) v} B g) ≪≫
        Functor.isoWhiskerLeft (fShriekFunctor.{u, v} B f)
          (fShriekFunctorIsoProperSupport.{u, v} B g).symm

AlgebraicGeometry.SmallEtale.fShriekCompIso_generator_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekCompSeparated.lean, line 787. The attribute's comment: “part (2)”.

Stacks 0F6T, part (2). If g is separated, the isomorphism (g ∘ f)_! ≅ g_! ∘ f_! agrees with the isomorphism of Stacks 0F79: read in the proper-support model of g_! through Stacks 0F6N, it is the sheafification of the map c of the proof of Stacks 0F79, which sends a local generator (Z, s) of (g ∘ f)_{p!}F over W — a section s of F over X_W supported on Z ⊆ X_W finite over W — to the generator (Z, s) of f_{p!}F over W ×_Z Y, through X_{W ×_Z Y} = X_W. The generators generate (g ∘ f)_{p!}F, so this determines the isomorphism.

public theorem fShriekCompIso_generator_of_isSeparated (W : SmallEtale B Z.obj Z.property)
    (E : FiniteSupport B (f ≫ g) W) (a : (finiteSupportDiagram B (f ≫ g) F W).obj E) :
    properSupportSection B g ((fShriekFunctor.{u, v} B f).obj F) W
        (((fShriekFunctorIsoProperSupport.{u, v} B g).hom.app
          ((fShriekFunctor.{u, v} B f).obj F)).hom.app (op W)
          (((fShriekCompIso B f g).hom.app F).hom.app (op W)
            ((finiteSupportPushforwardGenerator B (f ≫ g) F W E ≫
              (toSheafify (SmallEtale.topology B Z.obj Z.property)
                ((finiteSupportPushforward.{u, max (u + 1) v} B (f ≫ g)
                  (fun _ => inferInstance)).val.obj F)).app (op W)) a))) =
      (finiteSupportPushforwardGenerator B f F (baseChange B g W) (sepCompSupport B f g W E) ≫
        (toSheafify (SmallEtale.topology B Y.obj Y.property)
          ((finiteSupportPushforward.{u, max (u + 1) v} B f
            (fun _ => inferInstance)).val.obj F)).app (op (baseChange B g W)))
        (sepCompSection B f g F W E a)
Sources
LeanAlgebraicGeometry.SmallEtale.isFiniteSupport_iff_exists_isProper · AlgebraicGeometry.SmallEtale.FiniteSupport · AlgebraicGeometry.SmallEtale.finiteSupport_closedWithin · AlgebraicGeometry.SmallEtale.finiteSupportSections · AlgebraicGeometry.SmallEtale.exists_finiteSupport_sum · AlgebraicGeometry.SmallEtale.finiteSupportPresheaf · AlgebraicGeometry.SmallEtale.finiteSupportPushforward · AlgebraicGeometry.SmallEtale.finiteSupport_isLocallyClosed

Section63.5 Weightings and trace maps for locally quasi-finite morphisms#

Section 63.5 of the Stacks Project, Tag 0GKE. 7 tags here are carried by 28 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GKF, a lemma

Tag 0GKF in the Stacks Project.

AlgebraicGeometry.SmallEtale.modFShriekProjectionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FShriekModuleProjectionIso.lean, line 206. The attribute's comment: “the projection formula isomorphism”.

Stacks 0GKF, the canonical isomorphism of the projection formula f_!F ⊗_Λ G ≅ f_!(F ⊗_Λ f^{-1}G) for a locally quasi-finite morphism f : X ⟶ Y.

public def modFShriekProjectionIso
    (F : ModuleSheaf.{u, v, max (u + 1) v} B X Λ)
    (G : ModuleSheaf.{u, v, max (u + 1) v} B Y Λ) :
    (fShriekMod.{u, v, max (u + 1) v} B Λ f).obj F ⊗ G ≅
      (fShriekMod.{u, v, max (u + 1) v} B Λ f).obj
        (F ⊗ ((modPullback.{u, v, max (u + 1) v} B Λ f).obj G))
Tag 0GKG, a lemma

Tag 0GKG in the Stacks Project.

AlgebraicGeometry.separableDegreeWeightedFiberSum_flatQuasiFiniteWeight_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleCanonicalWeighting.lean, line 150. The attribute's comment: “The fibre integral ∫_{U → V} w out of which the trace map Tr_{f, w} is built, computed for an étale morphism with its canonical weighting: it is the plain separable-degree fibre count. For an étale morphism with its canonical weighting the trace map itself is the counit of j_! ⊣ j^{-1}, by AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit of StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.EtaleTraceIsCounit; for a general locally quasi-finite morphism and a general weighting its construction is a separate matter. Its uniqueness and its characterisation on stalks are, for an arbitrary locally quasi-finite morphism and an arbitrary integer-valued weight, in StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.WeightedTraceConstruction; and the fibre integral of a section supported on a part finite over the base, for an arbitrary locally quasi-finite morphism and an arbitrary weighting, in StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.FibreIntegral.”.

The fibre integral defining the trace map of Stacks 0GKG, for an étale morphism with its canonical weighting. The construction of Tr_{f, w} sends a section supported on a locally closed Z ⊂ X_V finite over V to the fibre integral ∫_{Z → V} w|_Z, which is AlgebraicGeometry.separableDegreeWeightedFiberSum. For an étale morphism carrying its canonical weighting that integral is the plain separable-degree fibre count: the weights contribute nothing.

theorem separableDegreeWeightedFiberSum_flatQuasiFiniteWeight_of_etale
    {V : Scheme.{u}} (π : U ⟶ V) :
    separableDegreeWeightedFiberSum π (flatQuasiFiniteWeight j) =
      separableDegreeWeightedFiberSum π 1

AlgebraicGeometry.etaleCanonicalTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceCounit.lean, line 91. The attribute's comment: “The trace map Tr_{f, w} : f_! f^{-1}ℱ ⟶ ℱ in the single case of an étale morphism carrying its canonical weighting, where by Remark 0GL4 it is the counit of j_! ⊣ j^{-1}; it is defined here to be that counit. The general construction, for a locally quasi-finite morphism and an arbitrary weighting, is a separate matter. That the counit does satisfy the stalk characterisation AlgebraicGeometry.SmallEtale.HasWeightedTraceStalks of Lemma 0GKG for the canonical weighting, so that by AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_unique it is the trace map of Lemma 0GKG in the étale case, is AlgebraicGeometry.hasWeightedTraceStalks_counit in StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.EtaleTraceIsCounit. The substantive fact licensing this case is the companion AlgebraicGeometry.flatQuasiFiniteWeight_eq_one_of_etale.”.

The trace map of Stacks 0GKG for an étale morphism with its canonical weighting. The canonical weighting of an étale j : U ⟶ X is the constant function 1 (AlgebraicGeometry.flatQuasiFiniteWeight_eq_one_of_etale), for which the prescribed stalk behaviour of the trace is the sum map ⨁_{j(ū) = x̄} ℱ_x̄ ⟶ ℱ_x̄; that map is the counit of j_! ⊣ j^{-1}, and the counit is what is taken here.

def etaleCanonicalTrace :
    abelianRestriction B X hX U ⋙ abelianExtensionByZero B X hX U ⟶
      𝟭 (Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1})

AlgebraicGeometry.moduleEtaleCanonicalTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceCounit.lean, line 158. The attribute's comment: “The trace map on étale sheaves of Λ-modules, in the single case of an étale morphism carrying its canonical weighting, where by Remark 0GL4 it is the counit of j_! ⊣ j^{-1}; it is defined here to be that counit. Same scope as AlgebraicGeometry.etaleCanonicalTrace: the general weighted construction of Lemma 0GKG, for a locally quasi-finite morphism and an arbitrary weighting, is a separate matter, and the stalk characterisation AlgebraicGeometry.SmallEtale.HasWeightedTraceStalks under which it is unique is verified for the counit with abelian coefficients in AlgebraicGeometry.hasWeightedTraceStalks_counit.”.

The trace map of Stacks 0GKG for an étale morphism with its canonical weighting, on sheaves of Λ-modules. As in the abelian case, this is the counit of j_! ⊣ j^{-1}.

def moduleEtaleCanonicalTrace :
    moduleRestriction B X hX U Λ ⋙ moduleExtensionByZero B X hX U Λ ⟶
      𝟭 (Sheaf (SmallEtale.topology B X hX) (ModuleCat.{max (u + 1) v} Λ))

AlgebraicGeometry.SmallEtale.existsUnique_hasWeightedTraceStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceExistence.lean, line 88.

Stacks 0GKG. Let f : X ⟶ Y be a locally quasi-finite morphism of schemes and let w : X → ℤ be a weighting of f. For every abelian sheaf F on the small étale site of Y there exists a unique trace map Tr_{f, w, F} : f_! f^{-1}F ⟶ F with the prescribed behaviour on stalks: at every geometric point s̄ of Y the map it induces on stalks, read through the decomposition of (f_! f^{-1}F)_{s̄} into the direct sum of the stalks of f^{-1}F over the geometric fibre above s̄, is the weighted sum (a_{x̄})_{x̄} ↦ ∑_{x̄} w(x̄) · a_{x̄} over that fibre.

public theorem existsUnique_hasWeightedTraceStalks {w : X.obj → ℤ}
    (hw : IsWeighting (B.inclusion.map f) w)
    (F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{max (u + 1) v}) :
    ∃! τ : (fShriekFunctor.{u, v} B f).obj ((abPullback.{u, v} B f).obj F) ⟶ F,
      HasWeightedTraceStalks.{u, v} B f w F τ
Tag 0GKH, a lemma

Tag 0GKH in the Stacks Project.

AlgebraicGeometry.etaleCanonicalTrace_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceCounit.lean, line 114. The attribute's comment: “Part (1) only — functoriality of the trace map in the sheaf — for an étale morphism with its canonical weighting, the case of Remark 0GL4, where the trace is the counit of j_! ⊣ j^{-1}. Part (1) for an ARBITRARY locally quasi-finite morphism and an arbitrary weight is AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_naturality, stated for the morphisms with the characterising stalk behaviour of Lemma 0GKG. Part (2), compatibility with arbitrary base change, and part (3), the version for K in the unbounded derived category D(Y_étale, Λ), are NOT carried by this declaration. The general weighted trace of Lemma 0GKG that parts (1)-(3) are about is AlgebraicGeometry.SmallEtale.weightedTrace of StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.WeightedTraceExistence; see the clause on AlgebraicGeometry.etaleCanonicalTrace.”.

The trace map is functorial in the abelian sheaf: for φ : ℱ ⟶ 𝒢 the square formed by Tr_ℱ, Tr_𝒢 and j_! j^{-1}φ commutes.

theorem etaleCanonicalTrace_naturality
    {F G : Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}} (φ : F ⟶ G) :
    (abelianRestriction B X hX U ⋙ abelianExtensionByZero B X hX U).map φ ≫
        (etaleCanonicalTrace B X hX U).app G =
      (etaleCanonicalTrace B X hX U).app F ≫ φ

AlgebraicGeometry.moduleEtaleCanonicalTrace_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceCounit.lean, line 179. The attribute's comment: “Part (1) with Λ-module coefficients — functoriality of the trace map in the sheaf of Λ-modules — for an étale morphism with its canonical weighting. This is the coefficient half of part (3); the DERIVED half of part (3), for K in D(Y_étale, Λ), is NOT carried, and neither is part (2), compatibility with arbitrary base change. For part (1) with abelian coefficients but an arbitrary locally quasi-finite morphism and arbitrary weight, see AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_naturality. The general weighted trace of Lemma 0GKG is AlgebraicGeometry.SmallEtale.weightedTrace; see the clause on AlgebraicGeometry.moduleEtaleCanonicalTrace.”.

The trace map is functorial in the sheaf of Λ-modules.

theorem moduleEtaleCanonicalTrace_naturality
    {F G : Sheaf (SmallEtale.topology B X hX) (ModuleCat.{max (u + 1) v} Λ)} (φ : F ⟶ G) :
    (moduleRestriction B X hX U Λ ⋙ moduleExtensionByZero B X hX U Λ).map φ ≫
        (moduleEtaleCanonicalTrace B X hX U Λ).app G =
      (moduleEtaleCanonicalTrace B X hX U Λ).app F ≫ φ

AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceBaseChange.lean, line 504. The attribute's comment: “part (2), compatibility of the trace map with arbitrary base change, for an arbitrary cartesian square with locally quasi-finite vertical morphism and an arbitrary integer-valued weight: the base change of a trace map for (f, w) is a trace map for (f', w ∘ p), and the square formed by the base-change isomorphism of 0F5J, the comparison of the two iterated inverse images, and the two trace maps commutes. The trace maps enter through the behaviour on geometric stalks by which 0GKG characterises them, which determines at most one morphism per sheaf by AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_unique. The finite-type and quasi-finiteness conditions on the base change are supplied from the square.”. References: SGA 4 XVII (6.2.5), “more general”.

Stacks 0GKH, part (2): the trace map is compatible with arbitrary base change. Let f : X ⟶ Y be locally quasi-finite, let w be an integer-valued function on X, let F be an abelian sheaf on the small étale site of Y, and let

X' --p--> X
|f'       |f
Y' --g--> Y

be a cartesian square. Then the base change along g of a trace map τ for (f, w) at F, transported along the base-change isomorphism g^{-1}f_!G ≅ f'_!p^{-1}G of Stacks 0F5J and the comparison p^{-1}f^{-1}F ≅ f'^{-1}g^{-1}F of the two iterated inverse images, is a trace map for (f', w ∘ p) at g^{-1}F; equivalently, the square formed by those two comparisons and the two trace maps commutes.

The finite-type and quasi-finiteness hypotheses on the base change f' are supplied from the square, so only the hypotheses of the source are assumed. The weighting hypothesis of the source is not needed: the statement holds for an arbitrary integer-valued w, the pulled-back function w ∘ p being a weighting of f' whenever w is a weighting of f by Stacks 0F3B (AlgebraicGeometry.IsWeighting.comp_of_isPullback). The trace maps enter through the behaviour on geometric stalks by which Stacks 0GKG characterises them, which by AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_unique determines at most one morphism for each sheaf.

public theorem hasWeightedTraceStalks_baseChange (w : X.obj → ℤ)
    (F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1})
    {τ : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F}
    (hτ : HasWeightedTraceStalks.{u, u + 1} B f w F τ) :
    letI := locallyOfFiniteType_of_isPullback B p f' f g sq
    letI := locallyQuasiFinite_of_isPullback B p f' f g sq
    HasWeightedTraceStalks.{u, u + 1} B f' (w ∘ B.inclusion.map p)
        ((abPullback.{u, u + 1} B g).obj F)
        ((fShriekFunctor.{u, u + 1} B f').map
            ((inverseImageSquareIso.{u} B p f' f g sq).inv.app F) ≫
          (fShriekBaseChangeNatIso.{u} B p f' f g sq).inv.app
            ((abPullback.{u, u + 1} B f).obj F) ≫
          (abPullback.{u, u + 1} B g).map τ) ∧
      ∀ τ' : (fShriekFunctor.{u, u + 1} B f').obj
          ((abPullback.{u, u + 1} B f').obj ((abPullback.{u, u + 1} B g).obj F)) ⟶
            (abPullback.{u, u + 1} B g).obj F,
        HasWeightedTraceStalks.{u, u + 1} B f' (w ∘ B.inclusion.map p)
            ((abPullback.{u, u + 1} B g).obj F) τ' →
          (fShriekBaseChangeNatIso.{u} B p f' f g sq).hom.app
              ((abPullback.{u, u + 1} B f).obj F) ≫
            (fShriekFunctor.{u, u + 1} B f').map
              ((inverseImageSquareIso.{u} B p f' f g sq).hom.app F) ≫ τ' =
            (abPullback.{u, u + 1} B g).map τ

AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceDerivedConstruction.lean, line 455. The attribute's comment: “part (3), the weighted trace with coefficients in a ring Λ on unbounded derived categories, for an arbitrary cartesian square with locally quasi-finite vertical morphism and a weighting w of it: for every K in D(Y_étale, Λ) a morphism Tr_{f,w,K} : f_!f^{-1}K ⟶ K, functorial in K, restricting to the sheaf-level trace of 0GKG, and compatible with arbitrary base change. The Λ-linear inverse images along f, f', g and p are AlgebraicGeometry.SmallEtale.pullbackMod, the lift of the abelian inverse image of 03Q1; the two comparisons attached to the square are the lifts AlgebraicGeometry.SmallEtale.fShriekBaseChangeMod and AlgebraicGeometry.SmallEtale.inverseImageSquareMod of the isomorphism of 0F5J and of the comparison of the two iterated inverse images; the trace maps at Λ-coefficients are AlgebraicGeometry.SmallEtale.weightedTraceMod, the trace of 0GKG read as a morphism of sheaves of Λ-modules, which the first two clauses show to have the characterising behaviour on geometric stalks of 0GKG and to be the unique morphism with it. The base-change square at Λ-coefficients is deduced from part (2) at abelian coefficients, and the derived square is its image under the deriving operation. The finite-type and quasi-finiteness conditions on the base change are supplied from the square, so the hypotheses are those of the source. The coefficient universes are those at which 0F5J is available: ModuleSheaf.{u, u+1, u} with Λ : Type u.”. References: SGA 4 XVII (6.2.5), “more general”.

The weighted trace with coefficients in a ring, on unbounded derived categories. Let f : X ⟶ Y be locally quasi-finite, let w be a weighting of f, let Λ be a ring, and let

X' --p--> X
|f'       |f
Y' --g--> Y

be a cartesian square. Then:

  • for every sheaf of Λ-modules M on the small étale site of Y the morphism Tr_{f, w, M} : f_! f^{-1}M ⟶ M of AlgebraicGeometry.SmallEtale.weightedTraceMod has the behaviour on geometric stalks by which Stacks 0GKG characterises the trace of (f, w), and it is the only morphism of sheaves of Λ-modules with that behaviour;
  • f^{-1} and f_! are exact on sheaves of Λ-modules, so each induces a functor on unbounded derived categories, and the trace maps induce a natural transformation Tr_{f, w} : f_! f^{-1} ⟶ id of D(Y_étale, Λ), whose component at K is Tr_{f, w, K} : f_! f^{-1}K ⟶ K;
  • that transformation is functorial in K: every naturality square commutes;
  • it restricts to the sheaf-level trace: it is the derived form of the natural transformation whose component at a sheaf of Λ-modules M is Tr_{f, w, M}, read through the canonical identification of the derived functor of f^{-1} ⋙ f_! with the composite of the derived functors and of the derived functor of the identity with the identity;
  • it is compatible with arbitrary base change: the two comparisons attached to the square at Λ-coefficients — the base-change isomorphism g^{-1}f_!N ≅ f'_!p^{-1}N of Stacks 0F5J and the comparison p^{-1}f^{-1}M ≅ f'^{-1}g^{-1}M of the two iterated inverse images — carry the derived trace of (f, w) to the derived trace of (f', w ∘ p), both whiskered by the derived g^{-1};
  • and the weight attached to the base change is the right one: w ∘ p is a weighting of f', which is Stacks 0F3B.

Every object of the statement is constructed: the Λ-linear inverse images along the four morphisms of the square are AlgebraicGeometry.SmallEtale.pullbackMod, the two comparisons are AlgebraicGeometry.SmallEtale.fShriekBaseChangeMod and AlgebraicGeometry.SmallEtale.inverseImageSquareMod, and the trace maps at Λ-coefficients are AlgebraicGeometry.SmallEtale.weightedTraceMod for (f, w) and for (f', w ∘ p).

The finite-type and quasi-finiteness hypotheses on the base change f' are supplied from the square, so the hypotheses are those of the source: f locally quasi-finite, w a weighting of f, and the square cartesian.

The coefficient universes are the ones at which the base-change isomorphism of Stacks 0F5J is available: the abelian étale sheaves have coefficients in AddCommGrpCat.{u + 1}, so the sheaves of Λ-modules are taken at ModuleSheaf.{u, u + 1, u} with Λ : Type u.

public theorem derivedWeightedTraceMod_spec {w : X.obj → ℤ}
    (hw : IsWeighting (B.inclusion.map f) w) :
    letI := locallyOfFiniteType_of_isPullback B p f' f g sq
    letI := locallyQuasiFinite_of_isPullback B p f' f g sq
    (∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
        HasWeightedTraceStalksMod.{u, u + 1, u} B Λ f (pullbackMod.{u, u + 1, u} B Λ f)
          (pullbackModForgetIso.{u, u + 1, u} B Λ f) w M
          (weightedTraceMod.{u, u + 1, u} B Λ f hw M)) ∧
      (∀ (M : ModuleSheaf.{u, u + 1, u} B Y Λ)
          (σ : (fShriekMod.{u, u + 1, u} B Λ f).obj
            ((pullbackMod.{u, u + 1, u} B Λ f).obj M) ⟶ M),
          HasWeightedTraceStalksMod.{u, u + 1, u} B Λ f (pullbackMod.{u, u + 1, u} B Λ f)
            (pullbackModForgetIso.{u, u + 1, u} B Λ f) w M σ →
            σ = weightedTraceMod.{u, u + 1, u} B Λ f hw M) ∧
      (∀ (K K' : DerivedCategory (ModuleSheaf.{u, u + 1, u} B Y Λ)) (ψ : K ⟶ K'),
          ((pullbackMod.{u, u + 1, u} B Λ f).mapDerivedCategory ⋙
              (fShriekMod.{u, u + 1, u} B Λ f).mapDerivedCategory).map ψ ≫
              (derivedWeightedTraceMod.{u, u + 1, t, u} B Λ f hw).app K' =
            (derivedWeightedTraceMod.{u, u + 1, t, u} B Λ f hw).app K ≫ ψ) ∧
      (derivedWeightedTraceMod.{u, u + 1, t, u} B Λ f hw =
          (Stacks.Cohomology.PerfectComplexTriangles.mapDerivedCategoryCompIso
              (pullbackMod.{u, u + 1, u} B Λ f) (fShriekMod.{u, u + 1, u} B Λ f)).inv ≫
            NatTrans.mapDerivedCategory
              (weightedTraceModTrans.{u, u + 1, u} B Λ f hw) ≫
            (Functor.mapDerivedCategoryIdIso _).hom) ∧
      (∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
          (weightedTraceModTrans.{u, u + 1, u} B Λ f hw).app M =
            weightedTraceMod.{u, u + 1, u} B Λ f hw M) ∧
      (NatTrans.mapDerivedCategory
            (traceBaseChangeComparison.{u, u + 1, u} B Λ f' f (pullbackMod.{u, u + 1, u} B Λ f)
              (pullbackMod.{u, u + 1, u} B Λ f') (pullbackMod.{u, u + 1, u} B Λ g)
              (pullbackMod.{u, u + 1, u} B Λ p) (fShriekBaseChangeMod.{u} B Λ p f' f g sq)
              (inverseImageSquareMod.{u} B Λ p f' f g sq)).hom ≫
          (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
            (pullbackMod.{u, u + 1, u} B Λ g)
            (pullbackMod.{u, u + 1, u} B Λ f' ⋙ fShriekMod.{u, u + 1, u} B Λ f')).hom ≫
          Functor.whiskerLeft (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory
            (NatTrans.mapDerivedCategory
              (weightedTraceModTrans.{u, u + 1, u} B Λ f'
                (AlgebraicGeometry.IsWeighting.comp_of_isPullback hw (sq.map B.inclusion)))) ≫
          (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
            (pullbackMod.{u, u + 1, u} B Λ g)
            (𝟭 (ModuleSheaf.{u, u + 1, u} B Y' Λ))).inv =
        (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
            (pullbackMod.{u, u + 1, u} B Λ f ⋙ fShriekMod.{u, u + 1, u} B Λ f)
            (pullbackMod.{u, u + 1, u} B Λ g)).hom ≫
          Functor.whiskerRight
            (NatTrans.mapDerivedCategory (weightedTraceModTrans.{u, u + 1, u} B Λ f hw))
            (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory ≫
          (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
            (𝟭 (ModuleSheaf.{u, u + 1, u} B Y Λ))
            (pullbackMod.{u, u + 1, u} B Λ g)).inv) ∧
      AlgebraicGeometry.IsWeighting (B.inclusion.map f') (w ∘ B.inclusion.map p)

AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceProperties.lean, line 160. The attribute's comment: “part (1), functoriality of the trace map in the sheaf, for an arbitrary locally quasi-finite morphism and an arbitrary integer-valued weight. Stated for morphisms with the behaviour on geometric stalks by which Lemma 0GKG characterises the trace map, which by AlgebraicGeometry.SmallEtale.existsUnique_hasWeightedTraceStalks is exactly the trace map of that lemma: it exists for every weighting and every sheaf, and is unique. Part (2) is AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_baseChange.”. References: SGA 4 XVII (6.2.5).

Stacks 0GKH, part (1): the trace map is functorial in the abelian sheaf. If τ_F and τ_G are trace maps for (f, w) at F and at G — morphisms with the weighted behaviour on geometric stalks which characterises the trace of Stacks 0GKG — then for every φ : F ⟶ G the square f_! f^{-1}F ⟶ f_! f^{-1}G ⟶ G versus f_! f^{-1}F ⟶ F ⟶ G commutes.

The source deduces this from the characterisation on stalks, and so does the proof here: the geometric stalk functors are jointly faithful, the stalk of a trace map is the weighted sum over the geometric fibre read through the decomposition of Stacks 0F5F, that decomposition is natural in the sheaf, and the weighted sum is natural by AlgebraicGeometry.SmallEtale.weightedTraceStalkMap_natural. No hypothesis on w is needed.

public theorem hasWeightedTraceStalks_naturality (w : X.obj → ℤ)
    {F G : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{max (u + 1) v}}
    (φ : F ⟶ G)
    {τF : (fShriekFunctor.{u, v} B f).obj ((abPullback.{u, v} B f).obj F) ⟶ F}
    {τG : (fShriekFunctor.{u, v} B f).obj ((abPullback.{u, v} B f).obj G) ⟶ G}
    (hF : HasWeightedTraceStalks.{u, v} B f w F τF)
    (hG : HasWeightedTraceStalks.{u, v} B f w G τG) :
    (fShriekFunctor.{u, v} B f).map ((abPullback.{u, v} B f).map φ) ≫ τG = τF ≫ φ
Tag 0GL3, a lemma

Tag 0GL3 in the Stacks Project.

AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceCompositionDerived.lean, line 425. The attribute's comment: “the derived trace maps compose: g_! Tr_{f,w_f,g^{-1}K} followed by Tr_{g,w_g,K} is Tr_{g∘f,w_{g∘f},K} for every K in D(Z_étale, Λ)”.

Stacks 0GL3. Let f : X ⟶ Y and g : Y ⟶ Z be locally quasi-finite morphisms, w_f a weighting of f and w_g a weighting of g, and Λ a ring. For K in D(Z_étale, Λ) the composite (g ∘ f)_!(g ∘ f)^{-1}K = g_! f_! f^{-1} g^{-1}K ⟶ g_! g^{-1}K ⟶ K of g_! Tr_{f, w_f, g^{-1}K} and Tr_{g, w_g, K} is Tr_{g ∘ f, w_{g ∘ f}, K}, where w_{g ∘ f}(x) = w_f(x) w_g(f(x)) (a weighting of g ∘ f by Stacks 0GK9).

The identification (g ∘ f)_!(g ∘ f)^{-1}K = g_! f_! f^{-1} g^{-1}K is the derived form of the composition laws (g ∘ f)^{-1} ≅ f^{-1} ∘ g^{-1} of Stacks 021J and (g ∘ f)_! ≅ g_! ∘ f_! of Stacks 0F6T at Λ-coefficients, followed by the identification of the derived functor of a composite with the composite of the derived functors. The trace maps are those of Stacks 0GKH, part (3).

public theorem derivedWeightedTraceMod_comp (K : DerivedCategory (ModuleSheaf.{u, v, r} B Z Λ)) :
    (fShriekMod.{u, v, r} B Λ (f ≫ g)).mapDerivedCategory.map
        ((CategoryTheory.mapDerivedCategoryIsoComp (pullbackMod.{u, v, r} B Λ g)
          (pullbackMod.{u, v, r} B Λ f) (pullbackMod.{u, v, r} B Λ (f ≫ g))
          (pullbackModCompIso B Λ f g)).hom.app K) ≫
      (CategoryTheory.mapDerivedCategoryIsoComp (fShriekMod.{u, v, r} B Λ f)
          (fShriekMod.{u, v, r} B Λ g) (fShriekMod.{u, v, r} B Λ (f ≫ g))
          (fShriekModCompIso B Λ f g)).hom.app
        ((pullbackMod.{u, v, r} B Λ f).mapDerivedCategory.obj
          ((pullbackMod.{u, v, r} B Λ g).mapDerivedCategory.obj K)) ≫
      (fShriekMod.{u, v, r} B Λ g).mapDerivedCategory.map
        ((derivedWeightedTraceMod.{u, v, t, r} B Λ f hw_f).app
          ((pullbackMod.{u, v, r} B Λ g).mapDerivedCategory.obj K)) ≫
      (derivedWeightedTraceMod.{u, v, t, r} B Λ g hw_g).app K =
    (derivedWeightedTraceMod.{u, v, t, r} B Λ (f ≫ g) (isWeighting_comp B f g hw_f hw_g)).app K
Tag 0GKI, an example

Tag 0GKI in the Stacks Project.

AlgebraicGeometry.SmallEtale.flatQuasiFiniteTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/FlatQuasiFiniteTrace.lean, line 156. The attribute's comment: “the trace maps Tr_{f, K} : f_! f^{-1} K ⟶ K for K in D(Y_étale, Λ), obtained -- as the example says -- by applying Lemmas 0GKG and 0GKH to f and the canonical weighting of 0F3D, which is AlgebraicGeometry.flatQuasiFiniteWeight. The example asserts no property of these maps beyond the two in the next two declarations, functoriality in K and compatibility with arbitrary base change.”. References: SGA 4½ Cycle (2.3.1), “special case”.

Stacks Project, Example 0GKI: the trace maps of a flat quasi-finite morphism. For f : X ⟶ Y flat, locally quasi-finite and locally of finite presentation, and a ring Λ, the family of trace maps

Tr_{f, K} : f_! f^{-1} K ⟶ K, K ∈ D(Y_étale, Λ),

obtained by applying Stacks 0GKG and 0GKH to f and the canonical weighting of Stacks 0F3D. It is a natural transformation of endofunctors of D(Y_étale, Λ), so the example's "functorial for K" is built into the datum; it is stated separately as AlgebraicGeometry.SmallEtale.flatQuasiFiniteTrace_naturality.

def flatQuasiFiniteTrace :
    (pullbackMod.{u, u + 1, u} B Λ f).mapDerivedCategory ⋙
        (fShriekMod.{u, u + 1, u} B Λ f).mapDerivedCategory ⟶
      𝟭 (DerivedCategory (ModuleSheaf.{u, u + 1, u} B Y Λ))

AlgebraicGeometry.SmallEtale.flatQuasiFiniteTrace_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/FlatQuasiFiniteTrace.lean, line 166. The attribute's comment: “the example's functorial for K in D(Y_étale, Λ), for the trace maps attached to the canonical weighting”.

Stacks Project, Example 0GKI: the trace maps are functorial in K.

theorem flatQuasiFiniteTrace_naturality
    {K K' : DerivedCategory (ModuleSheaf.{u, u + 1, u} B Y Λ)} (ψ : K ⟶ K') :
    ((pullbackMod.{u, u + 1, u} B Λ f).mapDerivedCategory ⋙
          (fShriekMod.{u, u + 1, u} B Λ f).mapDerivedCategory).map ψ ≫
        (flatQuasiFiniteTrace.{u, t} B Λ f).app K' =
      (flatQuasiFiniteTrace.{u, t} B Λ f).app K ≫ ψ

AlgebraicGeometry.SmallEtale.flatQuasiFiniteTrace_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/FlatQuasiFiniteTrace.lean, line 218. The attribute's comment: “the example's compatible with arbitrary base change, for the trace maps attached to the canonical weighting. Both sides are traces of the example: the f' side is the trace attached to the canonical weighting of f' itself, not to the restricted weight that 0GKH part (2) delivers, the two being identified by AlgebraicGeometry.flatQuasiFiniteWeight_of_isPullback -- the example's closing claim that w restricts to the canonical weighting of f'”. References: SGA 4 XVII (6.2.3), “more general”; SGA 4 XVII (6.2.5), “special case”.

Stacks Project, Example 0GKI: the trace maps are compatible with arbitrary base change. Let

X' --p--> X
|f'       |f
Y' --g--> Y

be cartesian. Then f' is again flat, locally quasi-finite and locally of finite presentation, so it has its own canonical weighting, and the square formed by the base-change comparison g^{-1} f_! ≅ f'_! p^{-1} of Stacks 0F5J, the comparison of the two iterated inverse images, and the two trace maps of the example commutes.

The statement is the base-change clause of AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod_spec with the weighting on the f' side replaced by the canonical weighting of f'. That replacement is exactly the example's closing remark that w restricts to the canonical weighting of f', which is AlgebraicGeometry.flatQuasiFiniteWeight_of_isPullback.

theorem flatQuasiFiniteTrace_baseChange :
    letI := locallyOfFiniteType_of_isPullback B p f' f g sq
    letI := locallyQuasiFinite_of_isPullback B p f' f g sq
    letI : Flat (B.inclusion.map f') :=
      MorphismProperty.of_isPullback (sq.map B.inclusion) inferInstance
    letI : LocallyOfFinitePresentation (B.inclusion.map f') :=
      MorphismProperty.of_isPullback (sq.map B.inclusion) inferInstance
    NatTrans.mapDerivedCategory
          (traceBaseChangeComparison.{u, u + 1, u} B Λ f' f (pullbackMod.{u, u + 1, u} B Λ f)
            (pullbackMod.{u, u + 1, u} B Λ f') (pullbackMod.{u, u + 1, u} B Λ g)
            (pullbackMod.{u, u + 1, u} B Λ p) (fShriekBaseChangeMod.{u} B Λ p f' f g sq)
            (inverseImageSquareMod.{u} B Λ p f' f g sq)).hom ≫
        (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
          (pullbackMod.{u, u + 1, u} B Λ g)
          (pullbackMod.{u, u + 1, u} B Λ f' ⋙ fShriekMod.{u, u + 1, u} B Λ f')).hom ≫
        Functor.whiskerLeft (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory
          (NatTrans.mapDerivedCategory
            (weightedTraceModTrans.{u, u + 1, u} B Λ f'
              (flatQuasiFiniteWeight_isWeighting (B.inclusion.map f')))) ≫
        (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
          (pullbackMod.{u, u + 1, u} B Λ g)
          (𝟭 (ModuleSheaf.{u, u + 1, u} B Y' Λ))).inv =
      (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
          (pullbackMod.{u, u + 1, u} B Λ f ⋙ fShriekMod.{u, u + 1, u} B Λ f)
          (pullbackMod.{u, u + 1, u} B Λ g)).hom ≫
        Functor.whiskerRight
          (NatTrans.mapDerivedCategory (weightedTraceModTrans.{u, u + 1, u} B Λ f
            (flatQuasiFiniteWeight_isWeighting (B.inclusion.map f))))
          (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory ≫
        (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
          (𝟭 (ModuleSheaf.{u, u + 1, u} B Y Λ))
          (pullbackMod.{u, u + 1, u} B Λ g)).inv

AlgebraicGeometry.SmallEtale.flatQuasiFiniteWeight_and_flatQuasiFiniteTrace_allClauses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/FlatQuasiFiniteTrace.lean, line 303. The attribute's comment: “the example in full, as one conjunction in its own order: (1) positivity and (2) the weighting property of the function w of the displayed formula, which is the example's canonical positive weighting; (3) functoriality in K and (4) compatibility with the arbitrary base change, for the family Tr_{f, K} : f_! f^{-1} K ⟶ K of AlgebraicGeometry.SmallEtale.flatQuasiFiniteTrace; (5) that the base change f' is again flat, locally quasi-finite and locally of finite presentation; and (6) that w restricts along p to the canonical weighting of f'. The trace maps themselves are data, so they enter by name: the conjunction asserts every property the example asserts of them.”. References: SGA 4 XVII (6.2.3), “more general”; SGA 4 XVII (6.2.5), “special case”.

Stacks Project, Example 0GKI, in full. For f : X ⟶ Y flat, locally quasi-finite and locally of finite presentation, a ring Λ, and an arbitrary cartesian square

X' --p--> X
|f'       |f
Y' --g--> Y

the six conjuncts are, in the example's own order:

  1. the function w = flatQuasiFiniteWeight f of the displayed formula is strictly positive, and
  2. is a weighting of f — together, the example's "canonical positive weighting";
  3. the family flatQuasiFiniteTrace of trace maps Tr_{f, K} : f_! f^{-1} K ⟶ K is functorial for K in D(Y_étale, Λ), and
  4. compatible with the base change, which being arbitrary gives "compatible with arbitrary base change";
  5. f' is again flat, locally quasi-finite and locally of finite presentation; and
  6. w restricts along p to the canonical weighting of f'.

The trace maps themselves are data, so they enter the conjunction by name rather than as an existential: every property the example asserts of them is asserted here of AlgebraicGeometry.SmallEtale.flatQuasiFiniteTrace.

Neither side of conjunct 4 can be written down without the four instances of f', so the statement binds them in a letI block; each is the proof conjunct 5 asserts, so nothing beyond the example's hypotheses is assumed, and the elaborated statement carries no binder for them.

theorem flatQuasiFiniteWeight_and_flatQuasiFiniteTrace_allClauses :
    -- the canonical positive weighting `w` of the example
    (∀ x, 0 < flatQuasiFiniteWeight (B.inclusion.map f) x) ∧
    IsWeighting (B.inclusion.map f) (flatQuasiFiniteWeight (B.inclusion.map f)) ∧
    -- the trace maps are functorial for `K` in `D(Y_étale, Λ)`
    (∀ (K K' : DerivedCategory (ModuleSheaf.{u, u + 1, u} B Y Λ)) (ψ : K ⟶ K'),
        ((pullbackMod.{u, u + 1, u} B Λ f).mapDerivedCategory ⋙
              (fShriekMod.{u, u + 1, u} B Λ f).mapDerivedCategory).map ψ ≫
            (flatQuasiFiniteTrace.{u, t} B Λ f).app K' =
          (flatQuasiFiniteTrace.{u, t} B Λ f).app K ≫ ψ) ∧
    -- and compatible with the arbitrary base change
    (letI := locallyOfFiniteType_of_isPullback B p f' f g sq
     letI := locallyQuasiFinite_of_isPullback B p f' f g sq
     letI : Flat (B.inclusion.map f') :=
       MorphismProperty.of_isPullback (sq.map B.inclusion) inferInstance
     letI : LocallyOfFinitePresentation (B.inclusion.map f') :=
       MorphismProperty.of_isPullback (sq.map B.inclusion) inferInstance
     NatTrans.mapDerivedCategory
           (traceBaseChangeComparison.{u, u + 1, u} B Λ f' f (pullbackMod.{u, u + 1, u} B Λ f)
             (pullbackMod.{u, u + 1, u} B Λ f') (pullbackMod.{u, u + 1, u} B Λ g)
             (pullbackMod.{u, u + 1, u} B Λ p) (fShriekBaseChangeMod.{u} B Λ p f' f g sq)
             (inverseImageSquareMod.{u} B Λ p f' f g sq)).hom ≫
         (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
           (pullbackMod.{u, u + 1, u} B Λ g)
           (pullbackMod.{u, u + 1, u} B Λ f' ⋙ fShriekMod.{u, u + 1, u} B Λ f')).hom ≫
         Functor.whiskerLeft (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory
           (NatTrans.mapDerivedCategory
             (weightedTraceModTrans.{u, u + 1, u} B Λ f'
               (flatQuasiFiniteWeight_isWeighting (B.inclusion.map f')))) ≫
         (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
           (pullbackMod.{u, u + 1, u} B Λ g)
           (𝟭 (ModuleSheaf.{u, u + 1, u} B Y' Λ))).inv =
       (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
           (pullbackMod.{u, u + 1, u} B Λ f ⋙ fShriekMod.{u, u + 1, u} B Λ f)
           (pullbackMod.{u, u + 1, u} B Λ g)).hom ≫
         Functor.whiskerRight
           (NatTrans.mapDerivedCategory (weightedTraceModTrans.{u, u + 1, u} B Λ f
             (flatQuasiFiniteWeight_isWeighting (B.inclusion.map f))))
           (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory ≫
         (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
           (𝟭 (ModuleSheaf.{u, u + 1, u} B Y Λ))
           (pullbackMod.{u, u + 1, u} B Λ g)).inv) ∧
    -- any base change of `f` satisfies the same three properties
    (Flat (B.inclusion.map f') ∧ LocallyQuasiFinite (B.inclusion.map f') ∧
      LocallyOfFinitePresentation (B.inclusion.map f')) ∧
    -- and `w` restricts to the canonical weighting of `f'`
    flatQuasiFiniteWeight (B.inclusion.map f') =
      flatQuasiFiniteWeight (B.inclusion.map f) ∘ (B.inclusion.map p)

AlgebraicGeometry.flatQuasiFiniteWeight_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FlatLengthBaseChange.lean, line 203. The attribute's comment: “the final claim: any base change f' of f satisfies the same three hypotheses -- which is AlgebraicGeometry.Flat.isStableUnderBaseChange, AlgebraicGeometry.locallyQuasiFinite_isStableUnderBaseChange and AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange, recorded on the tag in StacksFrontier.AlgebraicGeometry.Spaces.Groupoids.WeightingBaseChange -- and that the canonical weighting w of the example restricts along the projection to the canonical weighting of f'”.

Stacks Project, Example 0GKI, final claim. Let f : X ⟶ Y be flat, locally quasi-finite and locally of finite presentation and let f' : X' ⟶ Y' be a base change of f along g : Y' ⟶ Y, with p : X' ⟶ X the projection. Then the canonical weighting of f' is the restriction along p of the canonical weighting of f.

The weight at a point is the length of the local ring of the scheme-theoretic fibre through it times the inseparable degree of the residue field extension. The comparison morphism of fibres N is flat, so Tag 02M1 splits the length upstairs as the length downstairs times the length of the local ring of the fibre of N, and Stacks.Chow.length_fiberStalk_mul_finInsepDegree_of_isPullback trades that last length against the two inseparable degrees.

theorem flatQuasiFiniteWeight_of_isPullback {X Y X' Y' : Scheme.{u}} (f : X ⟶ Y)
    {p : X' ⟶ X} {f' : X' ⟶ Y'} {g : Y' ⟶ Y} (sq : IsPullback p f' f g)
    [LocallyQuasiFinite f] [LocallyOfFinitePresentation f] [Flat f] :
    flatQuasiFiniteWeight f' = flatQuasiFiniteWeight f ∘ p

Declarations registered for the tag:

Tag 0GL4, a remark

Tag 0GL4 in the Stacks Project.

AlgebraicGeometry.flatQuasiFiniteWeight_eq_one_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleCanonicalWeighting.lean, line 101. The attribute's comment: “The canonical weighting of Example 0GKI is identically 1 for an étale morphism — the computation that makes its trace map the counit of j_! ⊣ j^{-1}. The remark's own equality of the two morphisms is AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit in StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.EtaleTraceIsCounit, which uses this computation together with the stalk characterisation of Lemma 0GKG.”.

Stacks 0GL4. The canonical weighting of Stacks 0F3D, for an étale morphism of schemes, takes the value 1 at every point of the source.

This is the reason the trace map of Example 0GKI for an étale j : U ⟶ X is the counit of the adjunction j_! ⊣ j^{-1}: the trace for a weighting w acts on the stalk (j_! j^{-1}ℱ)_ȳ = ⨁_{j(x̄) = ȳ} ℱ_ȳ by multiplication by w(x̄) on the summand indexed by x̄, so for w = 1 it is the sum map, which is the counit.

theorem flatQuasiFiniteWeight_eq_one_of_etale (u : U) :
    flatQuasiFiniteWeight j u = 1

AlgebraicGeometry.flatQuasiFiniteWeight_etale_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleCanonicalWeighting.lean, line 128. The attribute's comment: “The canonical weighting of Example 0GKI is identically 1 for an étale morphism, as an equality of functions. Same scope as AlgebraicGeometry.flatQuasiFiniteWeight_eq_one_of_etale; the remark's equality of the trace with the counit is AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit.”.

Stacks 0GL4. The canonical weighting of an étale morphism is the constant function 1, as an equality of functions U → ℤ.

theorem flatQuasiFiniteWeight_etale_eq_one : flatQuasiFiniteWeight j = 1

AlgebraicGeometry.etaleCanonicalTrace_eq_comparison_comp_abelianTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceCounit.lean, line 136. The attribute's comment: “The Étale Cohomology, Section 03SH half of the remark: the counit of j_! ⊣ j^{-1} is the morphism already called the trace there, namely the trace map of Stacks 03SE read through the comparison j_! ⟶ j_*. Stated for a FINITE étale j, because that is where the 03SE trace is defined in this library. The remark's own equality — counit versus the trace map of Example 0GKI — is AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit in StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.EtaleTraceIsCounit.”.

For a finite étale j the trace map of Stacks 03SE is defined on j_* j^{-1} rather than on j_! j^{-1}, through the comparison isomorphism j_! ≅ j_*. Composing the comparison with it returns the counit: the morphism for which the terminology "trace" was already used in Étale Cohomology, Section 03SH is the counit of j_! ⊣ j^{-1}.

theorem etaleCanonicalTrace_eq_comparison_comp_abelianTrace :
    etaleCanonicalTrace B X hX U =
      Functor.whiskerLeft (abelianRestriction B X hX U)
        (abelianExtensionByZeroToPushforward B X hX U) ≫ abelianTrace B X hX U

AlgebraicGeometry.moduleEtaleCanonicalTrace_eq_comparison_comp_moduleTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceCounit.lean, line 198. The attribute's comment: “The Étale Cohomology, Section 03SH half of the remark on sheaves of Λ-modules: the counit of j_! ⊣ j^{-1} is the morphism already called the trace there, namely the trace map of Stacks 03SE read through the comparison j_! ⟶ j_*. Stated for a FINITE étale j, where the 03SE trace is defined. The remark's own equality against the trace map of Example 0GKI, with abelian coefficients, is AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit.”.

On sheaves of Λ-modules: for a finite étale j, composing the comparison j_! ⟶ j_* with the trace map of Stacks 03SE returns the counit of j_! ⊣ j^{-1}.

theorem moduleEtaleCanonicalTrace_eq_comparison_comp_moduleTrace :
    moduleEtaleCanonicalTrace B X hX U Λ =
      Functor.whiskerLeft (moduleRestriction B X hX U Λ)
        (moduleExtensionByZeroToPushforward B X hX U Λ) ≫ moduleTrace B X hX U Λ

AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceIsCounit.lean, line 290. The attribute's comment: “For an abelian étale sheaf ℱ: a morphism j_! j^{-1}ℱ ⟶ ℱ has the behaviour on geometric stalks by which Lemma 0GKG characterises the trace map of Example 0GKI, for the canonical weighting of Stacks 0F3D, exactly when it is the counit of the adjunction j_! ⊣ j^{-1}. The forward implication is the remark's equality; the backward implication produces the trace map, so nothing about it is assumed.”. References: SGA 4 XVII (6.2.11), “more general”; SGA 4 XVIII (3.1.8), “(iii), special case”; SGA 4½ Dualite (2.3), “special case”.

For an étale morphism j : U ⟶ X the trace map Tr : j_! j^{-1}ℱ ⟶ ℱ of Example 0GKI is the counit of the adjunction between j_! and j^{-1}.

The trace map of Example 0GKI is the morphism Stacks 0GKG attaches to the canonical weighting of Stacks 0F3D, characterised by its behaviour on geometric stalks; so the identification is stated as an equivalence: a morphism j_! j^{-1}ℱ ⟶ ℱ has that behaviour exactly when it is the counit. The forward direction is the remark's equality and the backward direction produces the trace map.

public theorem hasWeightedTraceStalks_iff_eq_counit
    (τ : (SmallEtale.fShriekFunctor.{u, u + 1} B U.obj.hom).obj
      ((SmallEtale.abPullback.{u, u + 1} B U.obj.hom).obj F) ⟶ F) :
    SmallEtale.HasWeightedTraceStalks.{u, u + 1} B U.obj.hom
        (flatQuasiFiniteWeight (B.inclusion.map U.obj.hom)) F τ ↔
      τ = (etaleFShriekAbPullbackAdjunction B X hX U).counit.app F

AlgebraicGeometry.derivedWeightedTraceFamily_eq_derivedCounit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceIsCounitDerived.lean, line 316. The attribute's comment: “At derived coefficients, on the unbounded derived category of abelian étale sheaves: for an étale j the derived form of the family of trace maps of Example 0GKI -- each of them characterised on geometric stalks by Lemma 0GKG for the canonical weighting of 0F3D -- is the counit of the adjunction between the derived functors of j_! and j^{-1}, which is the derived form of the adjunction of Stacks 03S3. Both descents are constructed here: the trace by CategoryTheory.NatTrans.mapDerivedCategoryCompToId as in 0GKH part (3), the adjunction by CategoryTheory.Adjunction.mapDerivedCategory, and they are compared by the coherence lemma CategoryTheory.Adjunction.mapDerivedCategory_counit. The sheaf-level input is AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit. Coefficients in AddCommGrpCat.{u + 1}, the universe at which 03S3 is available here; the universe of the derived category is arbitrary.”.

Stacks 0GL4 on the unbounded derived category of abelian étale sheaves. Let j : U ⟶ X be étale and let τ be the family of trace maps of Example 0GKI, that is a morphism j_! j^{-1}ℱ ⟶ ℱ for each abelian étale sheaf ℱ on X with the behaviour on geometric stalks by which Lemma 0GKG characterises the trace for the canonical weighting of Stacks 0F3D. Both j_! and j^{-1} are exact, so the family descends to a natural transformation j_! j^{-1} ⟶ id of the unbounded derived category, and the adjunction of Stacks 03S3 descends to an adjunction of the descended functors. Then the descended trace is the counit of the descended adjunction.

The weighting hypothesis of Stacks 0GKG is not needed and the trace maps are not assumed to exist: the counit itself is such a family, by AlgebraicGeometry.hasWeightedTraceStalks_counit.

public theorem derivedWeightedTraceFamily_eq_derivedCounit :
    NatTrans.mapDerivedCategoryCompToId (abPullback.{u, u + 1} B U.obj.hom)
        (fShriekFunctor.{u, u + 1} B U.obj.hom)
        (weightedTraceFamilyNatTrans.{u, u + 1} B U.obj.hom
          (flatQuasiFiniteWeight (B.inclusion.map U.obj.hom)) τ hτ) =
      (Adjunction.mapDerivedCategory (etaleFShriekAbPullbackAdjunction B X hX U)).counit

AlgebraicGeometry.hasWeightedTraceStalksMod_iff_eq_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceIsCounitDerived.lean, line 464. The attribute's comment: “At Lambda-coefficients on a single sheaf of Lambda-modules, for an arbitrary ring Lambda: a morphism j_!j^{-1}M ⟶ M of sheaves of Lambda-modules is the trace map of 0GKH part (3) for the canonical weighting of 0F3D -- its underlying morphism of abelian sheaves having the behaviour on geometric stalks prescribed by 0GKG -- if and only if it is the counit of the Lambda-linear adjunction AlgebraicGeometry.SmallEtale.etaleFShriekModPullbackAdjunction at M. The backward direction is the existence of the trace map at Lambda-coefficients, the forward direction is the remark. The Lambda-linear form of AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit.”. References: SGA 4 IX (5.1), “more general”; SGA 4 XVII (6.2.11), “more general”; SGA 4 XVIII (3.1.8), “(iii), special case”; SGA 4½ Dualite (2.3), “special case”.

Stacks 0GL4 at Λ-coefficients, on a single sheaf of Λ-modules. For an étale j, a ring Λ and a sheaf of Λ-modules M on the small étale site of X, a morphism τ : j_! j^{-1}M ⟶ M is the trace map of Stacks 0GKH part (3) for the canonical weighting of j — that is, the morphism of abelian sheaves underlying it has the behaviour on geometric stalks prescribed by Lemma 0GKG — if and only if it is the counit of the Λ-linear adjunction j_! ⊣ j^{-1} at M. The backward direction produces the trace map, so the equivalence also says that the trace map exists.

public theorem hasWeightedTraceStalksMod_iff_eq_counit
    (M : ModuleSheaf.{u, u + 1, u} B (B.obj X hX) Λ)
    (τ : (fShriekMod.{u, u + 1, u} B Λ U.obj.hom).obj
      ((pullbackMod.{u, u + 1, u} B Λ U.obj.hom).obj M) ⟶ M) :
    HasWeightedTraceStalksMod.{u, u + 1, u} B Λ U.obj.hom
        (pullbackMod.{u, u + 1, u} B Λ U.obj.hom)
        (pullbackModForgetIso.{u, u + 1, u} B Λ U.obj.hom)
        (flatQuasiFiniteWeight (B.inclusion.map U.obj.hom)) M τ ↔
      τ = (etaleFShriekModPullbackAdjunction B X hX U Λ).counit.app M

AlgebraicGeometry.derivedWeightedTraceMod_eq_derivedCounit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceIsCounitDerived.lean, line 661. The attribute's comment: “At the derived coefficients of the remark, D(X_etale, Lambda) for an arbitrary ring Lambda: for an étale j the derived trace Tr_{j,w} of 0GKH part (3) -- AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod for the canonical weighting of 0F3D -- is the counit of the adjunction between the derived functors of the Lambda-linear j_! and j^{-1}, so for each K in D(X_etale, Lambda) the morphism Tr_{j,w,K} : j_!j^{-1}K ⟶ K is the counit at K. Every object the statement names is constructed and nothing is quantified over: the derived trace is AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod, the derived form of the sheaf-level AlgebraicGeometry.SmallEtale.weightedTraceMod, which is the trace of 0GKG by AlgebraicGeometry.SmallEtale.weightedTraceMod_hasWeightedTraceStalksMod and the unique such morphism by AlgebraicGeometry.SmallEtale.hasWeightedTraceStalksMod_unique; the Lambda-linear inverse image is AlgebraicGeometry.SmallEtale.pullbackMod, the lift of the abelian j^{-1} of 03Q1; the Lambda-linear adjunction is AlgebraicGeometry.SmallEtale.etaleFShriekModPullbackAdjunction, the lift of the abelian adjunction of 03S3, whose counit is the abelian counit on underlying abelian sheaves by AlgebraicGeometry.SmallEtale.forgetModuleSheaf_map_etaleFShriekModPullbackAdjunction_counit; and the weighting is the canonical one of 0F3D, a weighting by AlgebraicGeometry.flatQuasiFiniteWeight_isWeighting. The identification of the derived trace with the derived counit comes from the abelian case AlgebraicGeometry.hasWeightedTraceStalks_iff_eq_counit through the coherence lemma CategoryTheory.Adjunction.mapDerivedCategory_counit, which says that the counit of a derived adjunction is the derived counit, and the sheaf-level trace is the counit by AlgebraicGeometry.hasWeightedTraceStalksMod_counit_etale with the uniqueness of 0GKG at Lambda-coefficients. Coefficient universes ModuleSheaf.{u, u+1, u} with Lambda : Type u, those of 0GKH part (3); the universe of the derived category is arbitrary.”. References: SGA 4 XVII (6.2.11), “more general”; SGA 4 XVIII (3.1.8), “(iii), special case”; SGA 4½ Dualite (2.3), “special case”.

Stacks 0GL4 on D(X_étale, Λ). Let j : U ⟶ X be étale and let Λ be a ring. The derived trace Tr_{j, w} : j_! j^{-1} ⟶ id of D(X_étale, Λ) of Stacks 0GKH part (3), for the canonical weighting w of j of Stacks 0F3D, is the counit of the adjunction between the derived functors of the Λ-linear j_! and j^{-1}.

Every object in the statement is constructed. The trace is AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod, the derived form of the sheaf-level trace AlgebraicGeometry.SmallEtale.weightedTraceMod, which has at each sheaf of Λ-modules the behaviour on geometric stalks by which Lemma 0GKG characterises the trace — that is AlgebraicGeometry.SmallEtale.weightedTraceMod_hasWeightedTraceStalksMod — and is by AlgebraicGeometry.SmallEtale.hasWeightedTraceStalksMod_unique the only such morphism, so it is the trace map and Tr_{j, w} is the derived trace rather than one of a family of candidates. The Λ-linear inverse image is AlgebraicGeometry.SmallEtale.pullbackMod and the Λ-linear adjunction AlgebraicGeometry.SmallEtale.etaleFShriekModPullbackAdjunction, the lift of the adjunction of Stacks 03S3, whose counit is the abelian counit on underlying abelian sheaves by AlgebraicGeometry.SmallEtale.forgetModuleSheaf_map_etaleFShriekModPullbackAdjunction_counit; the weighting is the canonical one, a weighting by AlgebraicGeometry.flatQuasiFiniteWeight_isWeighting.

This is AlgebraicGeometry.derivedWeightedTrace_pullbackMod_eq_derivedCounit, which leaves the trace family general, instantiated at that constructed trace.

public theorem derivedWeightedTraceMod_eq_derivedCounit :
    SmallEtale.derivedWeightedTraceMod.{u, u + 1, t, u} B Λ U.obj.hom
        (flatQuasiFiniteWeight_isWeighting (B.inclusion.map U.obj.hom)) =
      (Adjunction.mapDerivedCategory
        (etaleFShriekModPullbackAdjunction B X hX U Λ)).counit

AlgebraicGeometry.derivedWeightedTraceMod_app_eq_derivedCounit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/EtaleTraceIsCounitDerived.lean, line 686. The attribute's comment: “At a fixed object K of D(X_etale, Lambda) for an arbitrary ring Lambda, which is how the remark reads: for an étale j the trace map Tr_{j,w,K} : j_!j^{-1}K ⟶ K of 0GKH part (3) -- the component at K of AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod for the canonical weighting of 0F3D -- is the counit at K of the adjunction between the derived functors of the Lambda-linear j_! and j^{-1}. The trace, the two functors and the adjunction are all constructed and nothing is quantified over; this is the component form of AlgebraicGeometry.derivedWeightedTraceMod_eq_derivedCounit.”. References: SGA 4 XVIII (3.1.8), “(iii), special case”.

Stacks 0GL4 on D(X_étale, Λ), at a fixed object. For an étale j, a ring Λ and an object K of D(X_étale, Λ), the trace map Tr_{j, w, K} : j_! j^{-1}K ⟶ K of Stacks 0GKH part (3), for the canonical weighting w of j, is the counit at K of the adjunction between the derived functors of the Λ-linear j_! and j^{-1}. This is the form in which the remark reads, and it is the component at K of AlgebraicGeometry.derivedWeightedTraceMod_eq_derivedCounit.

public theorem derivedWeightedTraceMod_app_eq_derivedCounit_app
    (K : DerivedCategory (ModuleSheaf.{u, u + 1, u} B (B.obj X hX) Λ)) :
    (SmallEtale.derivedWeightedTraceMod.{u, u + 1, t, u} B Λ U.obj.hom
          (flatQuasiFiniteWeight_isWeighting (B.inclusion.map U.obj.hom))).app K =
      (Adjunction.mapDerivedCategory
        (etaleFShriekModPullbackAdjunction B X hX U Λ)).counit.app K
Tag 0GKJ, an example

Tag 0GKJ in the Stacks Project.

AlgebraicGeometry.exists_weighting_genericSeparableDegree_of_isGeometricallyUnibranch, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceLocallyQuasiFinite.lean, line 144. The attribute's comment: “the weighting of the example, with the sign the cited lemma gives: a locally quasi-finite morphism locally of finite type onto a geometrically unibranch locally Noetherian base carries a weighting w, nonnegative, equal at each point to the generic separable degree of the strict henselizations, and restricting along every base change of f to a weighting there. Nonnegative and not positive is what the source's own citation 0F3E gives, and 0F3C forbids more for an f that is not universally open. The trace maps Tr_{f, w, K} that the example then reads off 0GKG and 0GKH for this f and w are not asserted here; they come from AlgebraicGeometry.SmallEtale.weightedTrace and 0GKH, both of which are about an arbitrary weighting and not about this example's hypotheses. The whole example, this weighting together with its trace maps on abelian sheaves and on D(Y_étale, Λ), is the theorem exists_weighting_derivedWeightedTraceMod_of_isGeometricallyUnibranch of the namespace AlgebraicGeometry.SmallEtale”.

A locally quasi-finite morphism locally of finite type onto a geometrically unibranch locally Noetherian scheme carries an integer-valued weighting w which is nonnegative, whose restriction along an arbitrary base change of f is a weighting of that base change, and whose value at a point x is the generic separable degree of the strict henselization of the local ring at x over the strict henselization of the local ring at f x — the number of geometric points of the generic fibre of Spec O_{X, x}^{sh} ⟶ Spec O_{Y, f(x)}^{sh}, which is how Stacks 0GKJ describes it.

The last conjunct is the description quantified over all compatible choices of strict henselizations, of the minimal prime of the one downstairs and of an algebraic closure of its residue field, exactly as in AlgebraicGeometry.exists_weighting_genericSeparableDegree, so no choice of henselization is built into the statement.

0 ≤ w x is all the sign information there is, and the source's word positive cannot be taken literally: see the implementation notes and AlgebraicGeometry.not_exists_positive_weighting_of_not_universallyOpen.

public theorem exists_weighting_genericSeparableDegree_of_isGeometricallyUnibranch
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    [IsLocallyNoetherian Y] (hY : IsGeometricallyUnibranch Y) :
    ∃ w : X → ℤ,
      IsWeighting f w ∧
      (∀ x : X, 0 ≤ w x) ∧
      (∀ (X' Y' : Scheme.{u}) (q : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y),
        IsPullback q f' f g → IsWeighting f' (w ∘ q)) ∧
      ∀ (x : X)
        (κY : Type u) [Field κY]
        [Algebra (maximalIdeal (Y.presheaf.stalk (f x))).ResidueField κY]
        [IsSepClosure (maximalIdeal (Y.presheaf.stalk (f x))).ResidueField κY]
        (Rsh : Type u) [CommRing Rsh] [IsLocalRing Rsh]
        [Algebra (Y.presheaf.stalk (f x)) Rsh]
        (_hRsh : Stacks.StrictHenselization.IsStrictHenselization
          (Y.presheaf.stalk (f x)) κY Rsh)
        (κX : Type u) [Field κX]
        [Algebra (maximalIdeal (X.presheaf.stalk x)).ResidueField κX]
        [IsSepClosure (maximalIdeal (X.presheaf.stalk x)).ResidueField κX]
        (Ssh : Type u) [CommRing Ssh] [IsLocalRing Ssh]
        [Algebra (X.presheaf.stalk x) Ssh] [Algebra Rsh Ssh]
        [Algebra (Y.presheaf.stalk (f x)) Ssh]
        [IsScalarTower (Y.presheaf.stalk (f x)) Rsh Ssh]
        (_hSsh : Stacks.StrictHenselization.IsStrictHenselization
          (X.presheaf.stalk x) κX Ssh)
        (_hcomp : (algebraMap (Y.presheaf.stalk (f x)) Ssh) =
          (algebraMap (X.presheaf.stalk x) Ssh).comp (f.stalkMap x).hom)
        (p : Ideal Rsh) [p.IsPrime] (_hp : p ∈ minimalPrimes Rsh)
        (Kbar : Type u) [Field Kbar]
        [Algebra p.ResidueField Kbar] [IsAlgClosure p.ResidueField Kbar],
        w x = (Nat.card (AlgHom p.ResidueField
          (TensorProduct Rsh p.ResidueField Ssh) Kbar) : ℤ)

AlgebraicGeometry.SmallEtale.exists_weighting_weightedTrace_of_isGeometricallyUnibranch, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceQuasiFiniteUnibranch.lean, line 111. The attribute's comment: “the example in the generality of arbitrary Λ-linear lifts, of which the form with every lift, comparison and trace family constructed, the faithful registration of 0GKJ, is exists_weighting_derivedWeightedTraceMod_of_isGeometricallyUnibranch in the namespace AlgebraicGeometry.SmallEtale: for the nonnegative generic-separable-degree weighting w of 0F3E, 0GKG and all three parts of 0GKH hold, the derived clause for every choice of Λ-linear inverse images, comparisons and trace families compatible with the abelian ones. The source's word positive is a slip for nonnegative: 0F3E, the lemma 0GKJ cites, gives Z_{≥0}, and AlgebraicGeometry.exists_locallyQuasiFinite_isNormal_not_exists_positive_weighting exhibits a morphism at these hypotheses with no positive weighting; 0GKG and 0GKH impose no sign condition on w, so this costs the trace maps nothing. The trace maps enter through the behaviour on geometric stalks by which 0GKG characterises them, whose uniqueness half is one of the clauses, and the Λ-linear inverse images and the comparisons attached to the cartesian square are quantified over as lifts of the abelian ones exactly as in AlgebraicGeometry.SmallEtale.derivedWeightedTrace_spec_of_lifts. The coefficient universe is AddCommGrpCat.{u+1} with ModuleSheaf.{u, u+1, u} and Λ : Type u, which is where 0F5J and hence parts (2) and (3) live. The first assertion on its own is AlgebraicGeometry.exists_weighting_genericSeparableDegree_of_isGeometricallyUnibranch.”. References: SGA 4 XVII (6.2.5), “special case”.

The trace maps of a locally quasi-finite morphism over a geometrically unibranch locally Noetherian base. Let f : X ⟶ Y be a locally quasi-finite morphism of a big étale site, locally of finite type, with Y geometrically unibranch and locally Noetherian. Then there is an integer-valued function w on X such that:

  • w is a weighting of f, it is nonnegative, and its value at x is the generic separable degree of the strict henselization of the local ring at x over the strict henselization of the local ring at f x;
  • Stacks 0GKG for (f, w): for every abelian sheaf F on the small étale site of Y there is exactly one trace map Tr_{f, w, F} : f_! f^{-1}F ⟶ F with the behaviour on geometric stalks that lemma prescribes, namely the weighted sum (a_x̄)_x̄ ↦ ∑_x̄ w(x̄) · a_x̄ over the geometric fibre;
  • Stacks 0GKH part (1): those trace maps are functorial in F;
  • Stacks 0GKH part (2): they are compatible with arbitrary base change — for a cartesian square with horizontal morphisms p : X' ⟶ X, g : Y' ⟶ Y, the restriction w ∘ p is a weighting of f' (with nothing assumed about Y'), the base change along g of a trace map for (f, w) is a trace map for (f', w ∘ p), and the square formed by the base-change isomorphism g^{-1}f_!G ≅ f'_!p^{-1}G of Stacks 0F5J, the comparison p^{-1}f^{-1}F ≅ f'^{-1}g^{-1}F of the two iterated inverse images, and the two trace maps commutes;
  • Stacks 0GKH part (3): given a ring Λ, the trace maps induce on unbounded derived categories a natural transformation f_! f^{-1} ⟶ id of D(Y_étale, Λ), whose component at K is Tr_{f, w, K} : f_! f^{-1}K ⟶ K; it is functorial in K, it restricts to the sheaf-level trace, and it is compatible with arbitrary base change.

The last clause quantifies over the Λ-linear inverse images along the four morphisms of the square and the two comparisons attached to it, each presented as a lift of its abelian counterpart, and over the families of Λ-linear trace maps characterised on geometric stalks.

public theorem exists_weighting_weightedTrace_of_isGeometricallyUnibranch
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [LocallyOfFiniteType (B.inclusion.map f)] [LocallyQuasiFinite (B.inclusion.map f)]
    [IsLocallyNoetherian Y.obj] (hY : IsGeometricallyUnibranch Y.obj) :
    ∃ w : X.obj → ℤ,
      -- the weighting of the first assertion, which the trace maps below belong to
      IsWeighting (B.inclusion.map f) w ∧
      (∀ x : X.obj, 0 ≤ w x) ∧
      (∀ (x : X.obj)
          (κY : Type u) [Field κY]
          [Algebra (maximalIdeal (Y.obj.presheaf.stalk (B.inclusion.map f x))).ResidueField κY]
          [IsSepClosure
            (maximalIdeal (Y.obj.presheaf.stalk (B.inclusion.map f x))).ResidueField κY]
          (Rsh : Type u) [CommRing Rsh] [IsLocalRing Rsh]
          [Algebra (Y.obj.presheaf.stalk (B.inclusion.map f x)) Rsh]
          (_hRsh : Stacks.StrictHenselization.IsStrictHenselization
            (Y.obj.presheaf.stalk (B.inclusion.map f x)) κY Rsh)
          (κX : Type u) [Field κX]
          [Algebra (maximalIdeal (X.obj.presheaf.stalk x)).ResidueField κX]
          [IsSepClosure (maximalIdeal (X.obj.presheaf.stalk x)).ResidueField κX]
          (Ssh : Type u) [CommRing Ssh] [IsLocalRing Ssh]
          [Algebra (X.obj.presheaf.stalk x) Ssh] [Algebra Rsh Ssh]
          [Algebra (Y.obj.presheaf.stalk (B.inclusion.map f x)) Ssh]
          [IsScalarTower (Y.obj.presheaf.stalk (B.inclusion.map f x)) Rsh Ssh]
          (_hSsh : Stacks.StrictHenselization.IsStrictHenselization
            (X.obj.presheaf.stalk x) κX Ssh)
          (_hcomp : algebraMap (Y.obj.presheaf.stalk (B.inclusion.map f x)) Ssh =
            (algebraMap (X.obj.presheaf.stalk x) Ssh).comp
              ((B.inclusion.map f).stalkMap x).hom)
          (q : Ideal Rsh) [q.IsPrime] (_hq : q ∈ minimalPrimes Rsh)
          (Kbar : Type u) [Field Kbar]
          [Algebra q.ResidueField Kbar] [IsAlgClosure q.ResidueField Kbar],
          w x = (Nat.card (AlgHom q.ResidueField
            (TensorProduct Rsh q.ResidueField Ssh) Kbar) : ℤ)) ∧
      -- Stacks 0GKG for `(f, w)`: the trace map exists and is unique
      (∀ F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1},
        ∃! τ : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F,
          HasWeightedTraceStalks.{u, u + 1} B f w F τ) ∧
      -- Stacks 0GKH part (1): functoriality in the abelian sheaf
      (∀ (F G : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1})
          (φ : F ⟶ G)
          (τF : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F)
          (τG : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj G) ⟶ G),
          HasWeightedTraceStalks.{u, u + 1} B f w F τF →
          HasWeightedTraceStalks.{u, u + 1} B f w G τG →
            (fShriekFunctor.{u, u + 1} B f).map ((abPullback.{u, u + 1} B f).map φ) ≫ τG =
              τF ≫ φ) ∧
      -- Stacks 0GKH part (2): compatibility with arbitrary base change
      (∀ (X' Y' : B.Scheme) (p : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y)
          (sq : IsPullback p f' f g)
          (F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1})
          (τ : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F),
          HasWeightedTraceStalks.{u, u + 1} B f w F τ →
          letI := locallyOfFiniteType_of_isPullback B p f' f g sq
          letI := locallyQuasiFinite_of_isPullback B p f' f g sq
          IsWeighting (B.inclusion.map f') (w ∘ B.inclusion.map p) ∧
          HasWeightedTraceStalks.{u, u + 1} B f' (w ∘ B.inclusion.map p)
              ((abPullback.{u, u + 1} B g).obj F)
              ((fShriekFunctor.{u, u + 1} B f').map
                  ((inverseImageSquareIso.{u} B p f' f g sq).inv.app F) ≫
                (fShriekBaseChangeNatIso.{u} B p f' f g sq).inv.app
                  ((abPullback.{u, u + 1} B f).obj F) ≫
                (abPullback.{u, u + 1} B g).map τ) ∧
            ∀ τ' : (fShriekFunctor.{u, u + 1} B f').obj
                ((abPullback.{u, u + 1} B f').obj ((abPullback.{u, u + 1} B g).obj F)) ⟶
                  (abPullback.{u, u + 1} B g).obj F,
              HasWeightedTraceStalks.{u, u + 1} B f' (w ∘ B.inclusion.map p)
                  ((abPullback.{u, u + 1} B g).obj F) τ' →
                (fShriekBaseChangeNatIso.{u} B p f' f g sq).hom.app
                    ((abPullback.{u, u + 1} B f).obj F) ≫
                  (fShriekFunctor.{u, u + 1} B f').map
                    ((inverseImageSquareIso.{u} B p f' f g sq).hom.app F) ≫ τ' =
                  (abPullback.{u, u + 1} B g).map τ) ∧
      -- Stacks 0GKH part (3): the trace on `D(Y_étale, Λ)`
      (∀ (Λ : Type u) [Ring Λ] (X' Y' : B.Scheme) (p : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y)
          (sq : IsPullback p f' f g),
        letI := locallyOfFiniteType_of_isPullback B p f' f g sq
        letI := locallyQuasiFinite_of_isPullback B p f' f g sq
        ∀ (modPullF : ModuleSheaf.{u, u + 1, u} B Y Λ ⥤ ModuleSheaf.{u, u + 1, u} B X Λ)
          (hpullF : modPullF ⋙ forgetModuleSheaf.{u, u + 1, u} B X Λ ≅
            forgetModuleSheaf.{u, u + 1, u} B Y Λ ⋙ abPullback.{u, u + 1} B f)
          (modPullF' : ModuleSheaf.{u, u + 1, u} B Y' Λ ⥤ ModuleSheaf.{u, u + 1, u} B X' Λ)
          (hpullF' : modPullF' ⋙ forgetModuleSheaf.{u, u + 1, u} B X' Λ ≅
            forgetModuleSheaf.{u, u + 1, u} B Y' Λ ⋙ abPullback.{u, u + 1} B f')
          (modPullG : ModuleSheaf.{u, u + 1, u} B Y Λ ⥤ ModuleSheaf.{u, u + 1, u} B Y' Λ)
          (hpullG : modPullG ⋙ forgetModuleSheaf.{u, u + 1, u} B Y' Λ ≅
            forgetModuleSheaf.{u, u + 1, u} B Y Λ ⋙ abPullback.{u, u + 1} B g)
          (modPullP : ModuleSheaf.{u, u + 1, u} B X Λ ⥤ ModuleSheaf.{u, u + 1, u} B X' Λ)
          (hpullP : modPullP ⋙ forgetModuleSheaf.{u, u + 1, u} B X' Λ ≅
            forgetModuleSheaf.{u, u + 1, u} B X Λ ⋙ abPullback.{u, u + 1} B p)
          (bcMod : fShriekMod.{u, u + 1, u} B Λ f ⋙ modPullG ≅
            modPullP ⋙ fShriekMod.{u, u + 1, u} B Λ f')
          (epsMod : modPullF ⋙ modPullP ≅ modPullG ⋙ modPullF')
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B X Λ)]
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B Y Λ)]
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B X' Λ)]
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B Y' Λ)],
          (∀ n : ModuleSheaf.{u, u + 1, u} B X Λ,
            (forgetModuleSheaf.{u, u + 1, u} B Y' Λ).map (bcMod.hom.app n) ≫
                (fShriekModForgetIso.{u, u + 1, u} B Λ f').hom.app (modPullP.obj n) ≫
                (fShriekFunctor.{u, u + 1} B f').map (hpullP.hom.app n) =
              hpullG.hom.app ((fShriekMod.{u, u + 1, u} B Λ f).obj n) ≫
                (abPullback.{u, u + 1} B g).map
                  ((fShriekModForgetIso.{u, u + 1, u} B Λ f).hom.app n) ≫
                (fShriekBaseChangeNatIso.{u} B p f' f g sq).hom.app
                  ((forgetModuleSheaf.{u, u + 1, u} B X Λ).obj n)) →
          (∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
            (forgetModuleSheaf.{u, u + 1, u} B X' Λ).map (epsMod.hom.app M) ≫
                hpullF'.hom.app (modPullG.obj M) ≫
                (abPullback.{u, u + 1} B f').map (hpullG.hom.app M) =
              hpullP.hom.app (modPullF.obj M) ≫
                (abPullback.{u, u + 1} B p).map (hpullF.hom.app M) ≫
                (inverseImageSquareIso.{u} B p f' f g sq).hom.app
                  ((forgetModuleSheaf.{u, u + 1, u} B Y Λ).obj M)) →
          ∀ (τ : ∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
              (fShriekMod.{u, u + 1, u} B Λ f).obj (modPullF.obj M) ⟶ M)
            (hτ : ∀ M, HasWeightedTraceStalksMod.{u, u + 1, u} B Λ f modPullF hpullF w M (τ M))
            (τ' : ∀ N : ModuleSheaf.{u, u + 1, u} B Y' Λ,
              (fShriekMod.{u, u + 1, u} B Λ f').obj (modPullF'.obj N) ⟶ N)
            (hτ' : ∀ N, HasWeightedTraceStalksMod.{u, u + 1, u} B Λ f' modPullF' hpullF'
              (w ∘ B.inclusion.map p) N (τ' N)),
            letI := additive_of_forgetModPullIso.{u, u + 1, u} B Λ f modPullF hpullF
            letI := preservesFiniteLimits_of_forgetModPullIso.{u, u + 1, u} B Λ f modPullF hpullF
            letI :=
              preservesFiniteColimits_of_forgetModPullIso.{u, u + 1, u} B Λ f modPullF hpullF
            letI := additive_of_forgetModPullIso.{u, u + 1, u} B Λ f' modPullF' hpullF'
            letI :=
              preservesFiniteLimits_of_forgetModPullIso.{u, u + 1, u} B Λ f' modPullF' hpullF'
            letI :=
              preservesFiniteColimits_of_forgetModPullIso.{u, u + 1, u} B Λ f' modPullF' hpullF'
            letI := additive_of_forgetModPullIso.{u, u + 1, u} B Λ g modPullG hpullG
            letI := preservesFiniteLimits_of_forgetModPullIso.{u, u + 1, u} B Λ g modPullG hpullG
            letI :=
              preservesFiniteColimits_of_forgetModPullIso.{u, u + 1, u} B Λ g modPullG hpullG
            letI := additive_of_forgetModPullIso.{u, u + 1, u} B Λ p modPullP hpullP
            letI := preservesFiniteLimits_of_forgetModPullIso.{u, u + 1, u} B Λ p modPullP hpullP
            letI :=
              preservesFiniteColimits_of_forgetModPullIso.{u, u + 1, u} B Λ p modPullP hpullP
            -- functoriality in `K`
            (∀ (K K' : DerivedCategory (ModuleSheaf.{u, u + 1, u} B Y Λ)) (ψ : K ⟶ K'),
                (modPullF.mapDerivedCategory ⋙
                    (fShriekMod.{u, u + 1, u} B Λ f).mapDerivedCategory).map ψ ≫
                    (derivedWeightedTrace.{u, u + 1, t, u} B Λ f modPullF hpullF w τ hτ).app K' =
                  (derivedWeightedTrace.{u, u + 1, t, u} B Λ f modPullF hpullF w τ hτ).app K ≫
                    ψ) ∧
              -- the derived trace is the sheaf-level trace, derived
              (derivedWeightedTrace.{u, u + 1, t, u} B Λ f modPullF hpullF w τ hτ =
                  (Stacks.Cohomology.PerfectComplexTriangles.mapDerivedCategoryCompIso
                      modPullF (fShriekMod.{u, u + 1, u} B Λ f)).inv ≫
                    NatTrans.mapDerivedCategory
                      (weightedTraceModNatTrans.{u, u + 1, u} B Λ f modPullF hpullF w τ hτ) ≫
                    (Functor.mapDerivedCategoryIdIso _).hom) ∧
              (∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
                  (weightedTraceModNatTrans.{u, u + 1, u} B Λ f modPullF hpullF w τ hτ).app M =
                    τ M) ∧
              -- compatibility with arbitrary base change
              (NatTrans.mapDerivedCategory
                    (traceBaseChangeComparison.{u, u + 1, u} B Λ f' f modPullF modPullF' modPullG
                      modPullP bcMod epsMod).hom ≫
                  (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso modPullG
                    (modPullF' ⋙ fShriekMod.{u, u + 1, u} B Λ f')).hom ≫
                  Functor.whiskerLeft modPullG.mapDerivedCategory
                    (NatTrans.mapDerivedCategory
                      (weightedTraceModNatTrans.{u, u + 1, u} B Λ f' modPullF' hpullF'
                        (w ∘ B.inclusion.map p) τ' hτ')) ≫
                  (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso modPullG
                    (𝟭 (ModuleSheaf.{u, u + 1, u} B Y' Λ))).inv =
                (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
                    (modPullF ⋙ fShriekMod.{u, u + 1, u} B Λ f) modPullG).hom ≫
                  Functor.whiskerRight
                    (NatTrans.mapDerivedCategory
                      (weightedTraceModNatTrans.{u, u + 1, u} B Λ f modPullF hpullF w τ hτ))
                    modPullG.mapDerivedCategory ≫
                  (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
                    (𝟭 (ModuleSheaf.{u, u + 1, u} B Y Λ)) modPullG).inv))

AlgebraicGeometry.SmallEtale.exists_weighting_derivedWeightedTraceMod_of_isGeometricallyUnibranch, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/WeightedTrace/WeightedTraceQuasiFiniteUnibranchDerived.lean, line 116. The attribute's comment: “the full example: a locally quasi-finite f (LocallyOfFiniteType together with Mathlib's LocallyQuasiFinite) onto a geometrically unibranch locally Noetherian Y carries a weighting w, the generic separable degree of the strict henselizations (0F3E), and for this w the trace maps of 0GKG exist and are unique on abelian sheaves, are functorial and compatible with arbitrary base change (0GKH (1), (2)), and for every ring Λ the constructed trace AlgebraicGeometry.SmallEtale.derivedWeightedTraceMod : f_!f^{-1}K ⟶ K on D(Y_étale, Λ) (any model of the derived categories) is functorial in K, restricts to the sheaf-level trace AlgebraicGeometry.SmallEtale.weightedTraceMod, and is compatible with arbitrary base change through the constructed comparisons fShriekBaseChangeMod and inverseImageSquareMod, w ∘ p being a weighting of every base change f'. Nothing is quantified over beyond Λ, K, the square and the derived-category model. The source's word positive is false as written: 0F3E gives Z_{≥0}, and AlgebraicGeometry.exists_locallyQuasiFinite_isNormal_not_exists_positive_weighting is a counterexample (the closed point (2) of Spec ℤ), so w is stated nonnegative; 0GKG and 0GKH need no sign. Coefficients: ModuleSheaf.{u, u+1, u} with Λ : Type u, where 0F5J is available.”. References: SGA 4 XVII (6.2.5), “special case”.

The trace for a locally quasi-finite morphism over a geometrically unibranch base. Let f : X ⟶ Y be a locally quasi-finite morphism (locally of finite type with quasi-finite fibres) of a big étale site, with Y geometrically unibranch and locally Noetherian. Then there is a weighting w : X → ℤ of f such that:

  • w is nonnegative and its value at x is the generic separable degree of the strict henselization of the local ring at x over that of the local ring at f x (Stacks 0F3E);
  • Stacks 0GKG for (f, w): every abelian sheaf F on Y_étale has exactly one trace map Tr_{f, w, F} : f_! f^{-1}F ⟶ F with the prescribed behaviour on geometric stalks;
  • Stacks 0GKH (1), (2): these trace maps are functorial in F and compatible with arbitrary base change, the restriction w ∘ p along a base change being a weighting of f';
  • the trace on D(Y_étale, Λ): for every ring Λ and every cartesian square X' --p--> X, f' : X' ⟶ Y', g : Y' ⟶ Y, the trace map Tr_{f, w, M} = weightedTraceMod on sheaves of Λ-modules has the stalk behaviour of 0GKG and is the only morphism with it, and the derived trace Tr_{f, w} = derivedWeightedTraceMod : f_! f^{-1} ⟶ id of D(Y_étale, Λ) is functorial in K, restricts to the sheaf-level trace, and is compatible with the base change: the comparisons g^{-1}f_! ≅ f'_!p^{-1} (Stacks 0F5J) and p^{-1}f^{-1} ≅ f'^{-1}g^{-1} at Λ-coefficients carry the derived trace of (f, w), whiskered by the derived g^{-1}, to the derived trace of (f', w ∘ p).

All the Λ-linear functors, comparison isomorphisms and trace maps are the constructed ones of StacksFrontier.AlgebraicGeometry.EtaleCohomology.WeightedTrace.WeightedTraceDerivedConstruction; the derived categories are arbitrary models.

public theorem exists_weighting_derivedWeightedTraceMod_of_isGeometricallyUnibranch
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [LocallyOfFiniteType (B.inclusion.map f)] [LocallyQuasiFinite (B.inclusion.map f)]
    [IsLocallyNoetherian Y.obj] (hY : IsGeometricallyUnibranch Y.obj) :
    ∃ (w : X.obj → ℤ) (hw : IsWeighting (B.inclusion.map f) w),
      (∀ x : X.obj, 0 ≤ w x) ∧
      (∀ (x : X.obj)
          (κY : Type u) [Field κY]
          [Algebra (maximalIdeal (Y.obj.presheaf.stalk (B.inclusion.map f x))).ResidueField κY]
          [IsSepClosure
            (maximalIdeal (Y.obj.presheaf.stalk (B.inclusion.map f x))).ResidueField κY]
          (Rsh : Type u) [CommRing Rsh] [IsLocalRing Rsh]
          [Algebra (Y.obj.presheaf.stalk (B.inclusion.map f x)) Rsh]
          (_hRsh : Stacks.StrictHenselization.IsStrictHenselization
            (Y.obj.presheaf.stalk (B.inclusion.map f x)) κY Rsh)
          (κX : Type u) [Field κX]
          [Algebra (maximalIdeal (X.obj.presheaf.stalk x)).ResidueField κX]
          [IsSepClosure (maximalIdeal (X.obj.presheaf.stalk x)).ResidueField κX]
          (Ssh : Type u) [CommRing Ssh] [IsLocalRing Ssh]
          [Algebra (X.obj.presheaf.stalk x) Ssh] [Algebra Rsh Ssh]
          [Algebra (Y.obj.presheaf.stalk (B.inclusion.map f x)) Ssh]
          [IsScalarTower (Y.obj.presheaf.stalk (B.inclusion.map f x)) Rsh Ssh]
          (_hSsh : Stacks.StrictHenselization.IsStrictHenselization
            (X.obj.presheaf.stalk x) κX Ssh)
          (_hcomp : algebraMap (Y.obj.presheaf.stalk (B.inclusion.map f x)) Ssh =
            (algebraMap (X.obj.presheaf.stalk x) Ssh).comp
              ((B.inclusion.map f).stalkMap x).hom)
          (q : Ideal Rsh) [q.IsPrime] (_hq : q ∈ minimalPrimes Rsh)
          (Kbar : Type u) [Field Kbar]
          [Algebra q.ResidueField Kbar] [IsAlgClosure q.ResidueField Kbar],
          w x = (Nat.card (AlgHom q.ResidueField
            (TensorProduct Rsh q.ResidueField Ssh) Kbar) : ℤ)) ∧
      -- Stacks 0GKG for `(f, w)`: the trace map on abelian sheaves exists and is unique
      (∀ F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1},
        ∃! τ : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F,
          HasWeightedTraceStalks.{u, u + 1} B f w F τ) ∧
      -- Stacks 0GKH part (1): functoriality in the abelian sheaf
      (∀ (F G : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1})
          (φ : F ⟶ G)
          (τF : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F)
          (τG : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj G) ⟶ G),
          HasWeightedTraceStalks.{u, u + 1} B f w F τF →
          HasWeightedTraceStalks.{u, u + 1} B f w G τG →
            (fShriekFunctor.{u, u + 1} B f).map ((abPullback.{u, u + 1} B f).map φ) ≫ τG =
              τF ≫ φ) ∧
      -- Stacks 0GKH part (2): compatibility with arbitrary base change on abelian sheaves
      (∀ (X' Y' : B.Scheme) (p : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y)
          (sq : IsPullback p f' f g)
          (F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1})
          (τ : (fShriekFunctor.{u, u + 1} B f).obj ((abPullback.{u, u + 1} B f).obj F) ⟶ F),
          HasWeightedTraceStalks.{u, u + 1} B f w F τ →
          letI := locallyOfFiniteType_of_isPullback B p f' f g sq
          letI := locallyQuasiFinite_of_isPullback B p f' f g sq
          IsWeighting (B.inclusion.map f') (w ∘ B.inclusion.map p) ∧
          HasWeightedTraceStalks.{u, u + 1} B f' (w ∘ B.inclusion.map p)
              ((abPullback.{u, u + 1} B g).obj F)
              ((fShriekFunctor.{u, u + 1} B f').map
                  ((inverseImageSquareIso.{u} B p f' f g sq).inv.app F) ≫
                (fShriekBaseChangeNatIso.{u} B p f' f g sq).inv.app
                  ((abPullback.{u, u + 1} B f).obj F) ≫
                (abPullback.{u, u + 1} B g).map τ) ∧
            ∀ τ' : (fShriekFunctor.{u, u + 1} B f').obj
                ((abPullback.{u, u + 1} B f').obj ((abPullback.{u, u + 1} B g).obj F)) ⟶
                  (abPullback.{u, u + 1} B g).obj F,
              HasWeightedTraceStalks.{u, u + 1} B f' (w ∘ B.inclusion.map p)
                  ((abPullback.{u, u + 1} B g).obj F) τ' →
                (fShriekBaseChangeNatIso.{u} B p f' f g sq).hom.app
                    ((abPullback.{u, u + 1} B f).obj F) ≫
                  (fShriekFunctor.{u, u + 1} B f').map
                    ((inverseImageSquareIso.{u} B p f' f g sq).hom.app F) ≫ τ' =
                  (abPullback.{u, u + 1} B g).map τ) ∧
      -- the trace `Tr_{f, w, K}` on `D(Y_étale, Λ)`, every piece constructed
      (∀ (Λ : Type u) [Ring Λ] (X' Y' : B.Scheme) (p : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y)
          (sq : IsPullback p f' f g)
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B X Λ)]
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B Y Λ)]
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B X' Λ)]
          [HasDerivedCategory.{t} (ModuleSheaf.{u, u + 1, u} B Y' Λ)],
        letI := locallyOfFiniteType_of_isPullback B p f' f g sq
        letI := locallyQuasiFinite_of_isPullback B p f' f g sq
        -- the trace map at `Λ`-coefficients has the stalk behaviour of 0GKG ...
        (∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
            HasWeightedTraceStalksMod.{u, u + 1, u} B Λ f (pullbackMod.{u, u + 1, u} B Λ f)
              (pullbackModForgetIso.{u, u + 1, u} B Λ f) w M
              (weightedTraceMod.{u, u + 1, u} B Λ f hw M)) ∧
          -- ... and is the only morphism with it
          (∀ (M : ModuleSheaf.{u, u + 1, u} B Y Λ)
              (σ : (fShriekMod.{u, u + 1, u} B Λ f).obj
                ((pullbackMod.{u, u + 1, u} B Λ f).obj M) ⟶ M),
              HasWeightedTraceStalksMod.{u, u + 1, u} B Λ f (pullbackMod.{u, u + 1, u} B Λ f)
                (pullbackModForgetIso.{u, u + 1, u} B Λ f) w M σ →
                σ = weightedTraceMod.{u, u + 1, u} B Λ f hw M) ∧
          -- functoriality of `Tr_{f, w, K}` in `K`
          (∀ (K K' : DerivedCategory (ModuleSheaf.{u, u + 1, u} B Y Λ)) (ψ : K ⟶ K'),
              ((pullbackMod.{u, u + 1, u} B Λ f).mapDerivedCategory ⋙
                  (fShriekMod.{u, u + 1, u} B Λ f).mapDerivedCategory).map ψ ≫
                  (derivedWeightedTraceMod.{u, u + 1, t, u} B Λ f hw).app K' =
                (derivedWeightedTraceMod.{u, u + 1, t, u} B Λ f hw).app K ≫ ψ) ∧
          -- the derived trace is the sheaf-level trace, derived
          (derivedWeightedTraceMod.{u, u + 1, t, u} B Λ f hw =
              (Stacks.Cohomology.PerfectComplexTriangles.mapDerivedCategoryCompIso
                  (pullbackMod.{u, u + 1, u} B Λ f) (fShriekMod.{u, u + 1, u} B Λ f)).inv ≫
                NatTrans.mapDerivedCategory
                  (weightedTraceModTrans.{u, u + 1, u} B Λ f hw) ≫
                (Functor.mapDerivedCategoryIdIso _).hom) ∧
          (∀ M : ModuleSheaf.{u, u + 1, u} B Y Λ,
              (weightedTraceModTrans.{u, u + 1, u} B Λ f hw).app M =
                weightedTraceMod.{u, u + 1, u} B Λ f hw M) ∧
          -- compatibility with arbitrary base change
          (NatTrans.mapDerivedCategory
                (traceBaseChangeComparison.{u, u + 1, u} B Λ f' f
                  (pullbackMod.{u, u + 1, u} B Λ f) (pullbackMod.{u, u + 1, u} B Λ f')
                  (pullbackMod.{u, u + 1, u} B Λ g) (pullbackMod.{u, u + 1, u} B Λ p)
                  (fShriekBaseChangeMod.{u} B Λ p f' f g sq)
                  (inverseImageSquareMod.{u} B Λ p f' f g sq)).hom ≫
              (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
                (pullbackMod.{u, u + 1, u} B Λ g)
                (pullbackMod.{u, u + 1, u} B Λ f' ⋙ fShriekMod.{u, u + 1, u} B Λ f')).hom ≫
              Functor.whiskerLeft (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory
                (NatTrans.mapDerivedCategory
                  (weightedTraceModTrans.{u, u + 1, u} B Λ f'
                    (AlgebraicGeometry.IsWeighting.comp_of_isPullback hw
                      (sq.map B.inclusion)))) ≫
              (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
                (pullbackMod.{u, u + 1, u} B Λ g)
                (𝟭 (ModuleSheaf.{u, u + 1, u} B Y' Λ))).inv =
            (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
                (pullbackMod.{u, u + 1, u} B Λ f ⋙ fShriekMod.{u, u + 1, u} B Λ f)
                (pullbackMod.{u, u + 1, u} B Λ g)).hom ≫
              Functor.whiskerRight
                (NatTrans.mapDerivedCategory (weightedTraceModTrans.{u, u + 1, u} B Λ f hw))
                (pullbackMod.{u, u + 1, u} B Λ g).mapDerivedCategory ≫
              (Stacks.DerivedCategoryComparisons.mapDerivedCategoryCompIso
                (𝟭 (ModuleSheaf.{u, u + 1, u} B Y Λ))
                (pullbackMod.{u, u + 1, u} B Λ g)).inv) ∧
          AlgebraicGeometry.IsWeighting (B.inclusion.map f') (w ∘ B.inclusion.map p))
Sources
LeanAlgebraicGeometry.SmallEtale.modFShriekProjectionIso · AlgebraicGeometry.separableDegreeWeightedFiberSum_flatQuasiFiniteWeight_of_etale · AlgebraicGeometry.etaleCanonicalTrace · AlgebraicGeometry.moduleEtaleCanonicalTrace · AlgebraicGeometry.SmallEtale.existsUnique_hasWeightedTraceStalks · AlgebraicGeometry.etaleCanonicalTrace_naturality · AlgebraicGeometry.moduleEtaleCanonicalTrace_naturality · AlgebraicGeometry.SmallEtale.hasWeightedTraceStalks_baseChange

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.