59.28 Kummer theory to 59.45 Topological invariance of…

Section59.28 Kummer theory#

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

Tag 03PL, a lemma

Tag 03PL in the Stacks Project.

AlgebraicGeometry.kummerSequence_shortExact_bigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Etale.lean, line 526. The attribute's comment: “big étale site”. References: SGA 1 XI (6.1), “exact sequence (big)”; SGA 4 XVIII (1.6.1), “m = O_X (Y empty)”; SGA 4 IX (3.2), “big étale site”; SGA 4½ Arcata (2.2.5), “more general”; SGA 4½ Sommes trig (4.7), “special case”; SGA 7 IX (14.3), “special case”.

The Kummer sequence of abelian sheaves on the big étale site is short exact when the exponent is invertible on the base.

public theorem kummerSequence_shortExact_bigEtale
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (n : ℕ) (hn : IsUnit (n : Scheme.Γ.obj (Opposite.op S))) :
    (kummerSequence (BigEtaleOver.topology B S hS)
      (BigEtaleOver.toScheme B S hS)
      (unitsPresheaf_isSheaf_bigEtale B S hS) n).ShortExact

AlgebraicGeometry.kummerSequence_shortExact_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Etale.lean, line 547. The attribute's comment: “small étale site”. References: SGA 4 IX (3.2); SGA 1 XI (6.1), “exact sequence (small)”; SGA 4½ Arcata (2.2.5); SGA 4½ Sommes trig (4.7), “special case”; SGA 7 IX (14.3), “special case”.

The Kummer sequence of abelian sheaves on the small étale site is short exact when the exponent is invertible on the base.

public theorem kummerSequence_shortExact_smallEtale
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (n : ℕ) (hn : IsUnit (n : Scheme.Γ.obj (Opposite.op S))) :
    (kummerSequence (SmallEtale.topology B S hS)
      (SmallEtale.toScheme B S hS)
      (unitsPresheaf_isSheaf_smallEtale B S hS) n).ShortExact

Tag 040N, a lemma

Tag 040N in the Stacks Project.

AlgebraicGeometry.kummerSequence_shortExact_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FppfAndSyntomic.lean, line 504. The attribute's comment: “fppf Kummer sequence”. References: SGA 7 IX (14.3), “special case”; SGA 7 IX (9.4.3).

Stacks Project, Tag 040N (fppf). The canonical Kummer complex of abelian sheaves on the big fppf site is short exact.

public theorem kummerSequence_shortExact_fppf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (n : ℕ) (hn : 0 < n) :
    (kummerSequence (BigFppfOver.topology B S hS)
      (BigFppfOver.toScheme B S hS)
      (unitsPresheaf_isSheaf_fppf B S hS) n).ShortExact

AlgebraicGeometry.kummerSequence_shortExact_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FppfAndSyntomic.lean, line 527. The attribute's comment: “syntomic Kummer sequence”. References: SGA 7 IX (14.3), “special case”.

Stacks Project, Tag 040N (syntomic). The canonical Kummer complex of abelian sheaves on the big syntomic site is short exact.

public theorem kummerSequence_shortExact_syntomic
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (n : ℕ) (hn : 0 < n) :
    (kummerSequence (BigSyntomicOver.topology B S hS)
      (BigSyntomicOver.toScheme B S hS)
      (unitsPresheaf_isSheaf_syntomic B S hS) n).ShortExact

Tag 040P, an equation

Tag 040P in the Stacks Project.

AlgebraicGeometry.pairIso_torsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Basic.lean, line 688. The attribute's comment: “every pair isomorphism is uniquely a scalar translate”.

Once an isomorphism of pairs has been chosen, every other isomorphism is uniquely its scalar translate by a global nth root of unity.

public theorem pairIso_torsor (S : Scheme.{u}) (n : ℕ)
    (P Q : TrivializedPower S n) (φ : PairIso P Q) :
    ∀ ψ : PairIso P Q, ∃! a :
      (AlgebraicGeometry.rootsOfUnitySections n).obj (Opposite.op S),
      IsScalarTranslate a φ ψ

AlgebraicGeometry.scalarTranslate_pairIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Basic.lean, line 725. The attribute's comment: “every global root gives a unique pair isomorphism”.

Every global nth root of unity acts on a chosen isomorphism of pairs, giving a unique isomorphism whose sheaf map is its specified scalar translate.

public theorem scalarTranslate_pairIso (S : Scheme.{u}) (n : ℕ)
    (P Q : TrivializedPower S n) (φ : PairIso P Q) :
    ∀ a : (AlgebraicGeometry.rootsOfUnitySections n).obj (Opposite.op S),
      ∃! ψ : PairIso P Q, IsScalarTranslate a φ ψ

Tag 040Q, a lemma

Tag 040Q in the Stacks Project.

AlgebraicGeometry.pairIso_unitPair_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Basic.lean, line 841. The attribute's comment: “the pair side of the identification for pairs whose invertible sheaf is the structure sheaf: two such pairs are isomorphic exactly when their trivializing units agree modulo nth powers of global units, so the isomorphism classes of such pairs are the global units modulo nth powers; the cohomological side is AlgebraicGeometry.pairIso_iff_kummerBoundary_eq”.

Two pairs whose invertible sheaf is the structure sheaf are isomorphic exactly when their trivializing units differ by the nth power of a global unit; so the isomorphism classes of such pairs are the global units modulo nth powers.

public theorem pairIso_unitPair_iff (S : Scheme.{u}) (n : ℕ)
    (f g : (Scheme.Γ.obj (Opposite.op S))ˣ) :
    Nonempty (PairIso (unitPair S n f) (unitPair S n g)) ↔
      ∃ u : (Scheme.Γ.obj (Opposite.op S))ˣ, f = u ^ n * g

AlgebraicGeometry.exists_trivializedPower_sheaf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Basic.lean, line 877. The attribute's comment: “the invertible sheaves occurring in a pair are exactly those whose nth tensor power is trivial, with no restriction to the structure sheaf”.

An invertible sheaf carries a trivialization of its nth tensor power exactly when that power is trivial; so the invertible sheaves of pairs are exactly those whose class in the Picard group is n-torsion.

public theorem exists_trivializedPower_sheaf_iff (S : Scheme.{u}) (n : ℕ)
    (L : SheafOfModules.{u} (ringSheaf S))
    (hL : IsInvertible S.presheaf (ringSheafCond S) L) :
    (∃ P : TrivializedPower S n, P.sheaf = L) ↔
      Nonempty (tensorPower S.presheaf (ringSheafCond S) L (n : ℤ) ≅
        SheafOfModules.unit (ringSheaf S))

AlgebraicGeometry.pairIso_iff_trivializationRatio_eq_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Basic.lean, line 1049. The attribute's comment: “the pair side for an arbitrary, possibly nontrivial, invertible sheaf: two pairs with the same invertible sheaf are isomorphic exactly when their trivializations differ by the nth power of a global unit, so the pairs with a given invertible sheaf form one coset of the nth powers in the global units”.

Two pairs with the same, possibly nontrivial, invertible sheaf are isomorphic exactly when their trivializations differ by the nth power of a global unit.

public theorem pairIso_iff_trivializationRatio_eq_pow (S : Scheme.{u}) (n : ℕ)
    (L : SheafOfModules.{u} (ringSheaf S))
    [hL : IsInvertible S.presheaf (ringSheafCond S) L]
    (α β : tensorPower S.presheaf (ringSheafCond S) L (n : ℤ) ≅
      SheafOfModules.unit (ringSheaf S)) :
    Nonempty (PairIso ⟨L, hL, α⟩ ⟨L, hL, β⟩) ↔
      ∃ u : (Scheme.Γ.obj (Opposite.op S))ˣ, trivializationRatio S n α β = u ^ n

AlgebraicGeometry.exists_pairIso_unitPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Basic.lean, line 1087. The attribute's comment: “every pair whose invertible sheaf is isomorphic to the structure sheaf is isomorphic to a unit pair, so the trivial-invertible-sheaf case is not a restriction to the literal structure sheaf”.

A pair whose invertible sheaf is isomorphic to the structure sheaf — not only equal to it — is isomorphic to the pair given by the structure sheaf and a global unit.

public theorem exists_pairIso_unitPair (S : Scheme.{u}) (n : ℕ) (P : TrivializedPower S n)
    (e : P.sheaf ≅ SheafOfModules.unit (ringSheaf S)) :
    ∃ f : (Scheme.Γ.obj (Opposite.op S))ˣ, Nonempty (PairIso P (unitPair S n f))

AlgebraicGeometry.basePairCohomologyClassHom_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Comparison040Q.lean, line 84. The attribute's comment: “the comparison homomorphism from the isomorphism classes of pairs to H^1 of the roots of unity is bijective. The group isomorphism the tag asserts is read off from this in AlgebraicGeometry.basePairClassesAddEquivH1, and the three statements of the tag -- etale for n invertible on the base, fppf and syntomic for n positive -- in the three declarations after it”.

The comparison homomorphism of Tag 040Q is bijective.

All six hypotheses of Stacks.Kummer.bijective_of_comparison are discharged from the library; see the head of this file.

public theorem basePairCohomologyClassHom_bijective
    (hroot : LocalRoots (BigFppfOver.baseRingedSite B S hS τ) n)
    (hSE : (kummerSequence (BigFppfOver.baseOverTopology B S hS τ)
      (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS τ) n).ShortExact)
    (hT : IsTerminal (C := BigFppfOver B S hS) (Over.mk (𝟙 (B.obj hS)))) :
    Function.Bijective (basePairCohomologyClassHom B S hS τ n hroot)

AlgebraicGeometry.pairClassesAddEquivH1Etale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Comparison040Q.lean, line 158. The attribute's comment: “the etale statement: for n invertible on S, H^1_etale(S, mu_n) is the group of pairs (L, alpha) up to isomorphism, as an isomorphism of abelian groups”.

Stacks Project, Tag 040Q, the étale statement. For n invertible on S, H¹_étale(S, μ_n) is the group of pairs (ℒ, α) — an invertible 𝒪_S-module with a trivialization of its n-th tensor power — up to isomorphism.

public noncomputable def pairClassesAddEquivH1Etale
    (hn : IsUnit (n : Scheme.Γ.obj (op S))) :
    PairClasses S n ≃+
      Sheaf.H (rootsOfUnitySheaf (BigFppfOver.baseOverTopology B S hS .etale)
        (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS .etale) n) 1

AlgebraicGeometry.pairClassesAddEquivH1Fppf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Comparison040Q.lean, line 172. The attribute's comment: “the fppf statement: for every positive n, with no invertibility hypothesis, H^1_fppf(S, mu_n) is the group of pairs (L, alpha) up to isomorphism, as an isomorphism of abelian groups”.

Stacks Project, Tag 040Q, the fppf statement. For every positive n, with no invertibility hypothesis, H¹_fppf(S, μ_n) is the group of pairs (ℒ, α) up to isomorphism.

public noncomputable def pairClassesAddEquivH1Fppf (hn : 0 < n) :
    PairClasses S n ≃+
      Sheaf.H (rootsOfUnitySheaf (BigFppfOver.baseOverTopology B S hS .fppf)
        (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS .fppf) n) 1

AlgebraicGeometry.pairClassesAddEquivH1Syntomic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/Comparison040Q.lean, line 184. The attribute's comment: “the syntomic statement: for every positive n, with no invertibility hypothesis, H^1_syntomic(S, mu_n) is the group of pairs (L, alpha) up to isomorphism, as an isomorphism of abelian groups”.

Stacks Project, Tag 040Q, the syntomic statement. The same with fppf replaced by syntomic.

public noncomputable def pairClassesAddEquivH1Syntomic (hn : 0 < n) :
    PairClasses S n ≃+
      Sheaf.H (rootsOfUnitySheaf (BigFppfOver.baseOverTopology B S hS .syntomic)
        (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS .syntomic) n) 1

AlgebraicGeometry.basePairCohomologyClass_picard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/ComparisonCompatibilities.lean, line 277. The attribute's comment: “the comparison map from the isomorphism classes of pairs to H^1 of the roots of unity is compatible with the right-hand end of the two extensions: composed with the map to H^1 of the multiplicative group and the identification of that with the Picard group (Tag 03P8) it is the Picard class of the invertible sheaf of the pair. Injectivity and surjectivity of the comparison are not proved here, nor is the compatibility with the left-hand end”.

The comparison map of Tag 040Q is compatible with the Picard group, read on the class of a pair: the image of the class of a pair (ℒ, α) in H¹((Sch/S)_τ, μ_n) is carried by H¹(μ_n) ⟶ H¹(𝐆_m) = Pic(S) to the Picard class of ℒ.

This is AlgebraicGeometry.trivializationTorsor_firstCohomologyMap followed by Stacks.Picard.AllTopologies.baseH1UnitsAddEquivSchemePicardGroup_symm_classOf.

public theorem basePairCohomologyClass_picard
    (hroot : LocalRoots (BigFppfOver.baseRingedSite B S hS τ) n) (P : TrivializedPower S n) :
    Stacks.Picard.AllTopologies.baseH1UnitsAddEquivSchemePicardGroup B S hS τ
        (Sheaf.H.map (kernel.ι (powerSheaf (BigFppfOver.baseOverTopology B S hS τ)
            (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS τ) n)) 1
          (basePairCohomologyClassHom B S hS τ n hroot (pairClass P))) =
      pairSheafClassHom S n (pairClass P)

AlgebraicGeometry.baseAssociatedModule_map_scalarEnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/ComparisonCompatibilities.lean, line 329. The attribute's comment: “the associated-module functor of Descent, Proposition 03DX carries multiplication by a global function of the base to multiplication by that same function over the terminal object of the big tau-site; this is one ingredient of the compatibility of the comparison map with the left-hand end of the two extensions, and neither that compatibility nor any other part of the tag is proved here”.

The associated-module functor carries multiplication by a global function of S to multiplication by that same global function, read over the terminal object S / S of the big τ-site.

The functor is the pullback along the morphism of ringed sites ((Sch/S)_τ, 𝒪) → (S_Zar, 𝒪_S), for which there is no formula on morphisms; the identity is obtained from the corresponding one for the pushforward, Stacks.SheafOfModules.map_globalSectionToEnd, through CategoryTheory.Adjunction.map_endOfId. Its hypothesis is the square saying that the structure map of the morphism of sites carries the restrictions of s from the top open of S to the restrictions of s from S / S, and over the top open that map is the identification Γ(S, ⊤) = Γ(⊤, ⊤).

public theorem baseAssociatedModule_map_scalarEnd
    (hT : IsTerminal (C := BigFppfOver B S hS) (Over.mk (𝟙 (B.obj hS))))
    (s : Scheme.Γ.obj (op S)) (M : SheafOfModules.{u} (ringSheaf S)) :
    (BigFppfOver.baseAssociatedModule B S hS τ).map (scalarEnd S s M) =
      Stacks.Cohomology.Torsors.Generators.scalarEndOfTerminal
        (BigFppfOver.baseRingedSite B S hS τ) hT s
        ((BigFppfOver.baseAssociatedModule B S hS τ).obj M)

AlgebraicGeometry.exists_unitPairTrivialization_eq_basePairTriv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/ComparisonCompatibilities.lean, line 574. The attribute's comment: “the transported trivialization of the unit pair of a global unit f is the site-level trivialization of the unit pair at c * f, for one global unit c independent of f; this is the identification the compatibility of the comparison map with the left-hand end of the two extensions needs, and that compatibility is proved below, not here”.

The transported trivialization of the unit pair is the site-level trivialization of the unit pair, after one fixed twist. There is a global unit c of S, independent of f, with AlgebraicGeometry.basePairTriv at the unit pair of f the comparison of the two structure sheaves followed by Stacks.Cohomology.Torsors.Generators.unitPairTrivialization at c * f.

This is the identification the compatibility of the comparison map of Tag 040Q with the left-hand end of the two extensions was missing.

public theorem exists_unitPairTrivialization_eq_basePairTriv
    (hT : IsTerminal (C := BigFppfOver B S hS) (Over.mk (𝟙 (B.obj hS)))) :
    ∃ c : (Scheme.Γ.obj (op S))ˣ, ∀ f : (Scheme.Γ.obj (op S))ˣ,
      powerMap (BigFppfOver.baseRingedSite B S hS τ)
            (BigFppfOver.baseAssociatedModulePicardUnitIso B S hS τ) n ≪≫
          unitPairTrivialization (BigFppfOver.baseRingedSite B S hS τ) hT n (c * f) =
        basePairTriv B S hS τ n (unitPair S n f)

AlgebraicGeometry.exists_kummerBoundary_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/ExactSequence.lean, line 162. The attribute's comment: “the image of the pairs with trivial invertible sheaf in H^1 of the roots of unity is exactly the kernel of the map to H^1 of the multiplicative group; so the injection of pairIso_iff_kummerBoundary_eq misses exactly the classes with nonzero image there”.

Stacks Project, Tag 040Q, the image of the pairs whose invertible sheaf is trivial. A class in H¹(S, μ_n) is the class of such a pair — equivalently, a Kummer boundary — exactly when its image in H¹(S, 𝐆_m) vanishes. So the injection of AlgebraicGeometry.pairIso_iff_kummerBoundary_eq has for its image precisely the kernel of H¹(S, μ_n) ⟶ H¹(S, 𝐆_m).

theorem exists_kummerBoundary_iff (x : Sheaf.H (kummerSequence J F hF n).X₁ 1) :
    (∃ a : (Scheme.Γ.obj (op (F.obj T)))ˣ, kummerBoundary J F hF n hS hT a = x) ↔
      Sheaf.H.map (kummerSequence J F hF n).f 1 x = 0

AlgebraicGeometry.exists_kummerFirstCohomologyMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/ExactSequence.lean, line 184. The attribute's comment: “the image of H^1 of the roots of unity in H^1 of the multiplicative group is exactly the n-torsion; with the kernel computed by exists_kummerBoundary_iff this presents H^1(S, mu_n) as an extension of that n-torsion by the global units modulo nth powers. What remains between this and the full statement of 040Q is the abelian-group structure on AlgebraicGeometry.PairClasses, for which no AddCommGroup instance exists, together with the comparison homomorphism to H^1; Tag 03P8 is NOT the gap, being proved at Picard/MultiplicativeGroupFirstCohomology.lean:206”.

Stacks Project, Tag 040Q, the image of H¹(S, μ_n) in H¹(S, 𝐆_m). It is exactly the n-torsion subgroup, since the second map of the Kummer sequence induces multiplication by n on first cohomology.

theorem exists_kummerFirstCohomologyMap_iff (y : Sheaf.H (kummerSequence J F hF n).X₂ 1) :
    (∃ x : Sheaf.H (kummerSequence J F hF n).X₁ 1,
        Sheaf.H.map (kummerSequence J F hF n).f 1 x = y) ↔ n • y = 0

AlgebraicGeometry.forall_exists_kummerBoundary_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/ExactSequence.lean, line 201. The attribute's comment: “the obstruction to surjectivity: the pairs with trivial invertible sheaf exhaust H^1 of the roots of unity exactly when H^1 of the multiplicative group has no n-torsion, so the missing classes are measured by that torsion group”.

Stacks Project, Tag 040Q, the obstruction to surjectivity. The pairs whose invertible sheaf is trivial exhaust H¹(S, μ_n) exactly when H¹(S, 𝐆_m) has no n-torsion. So the classes of Tag 040Q that the trivial-invertible-sheaf part misses are measured by that torsion group, and by Tag 03P8 it is the n-torsion of the Picard group.

theorem forall_exists_kummerBoundary_iff :
    (∀ x : Sheaf.H (kummerSequence J F hF n).X₁ 1,
        ∃ a : (Scheme.Γ.obj (op (F.obj T)))ˣ, kummerBoundary J F hF n hS hT a = x) ↔
      ∀ y : Sheaf.H (kummerSequence J F hF n).X₂ 1, n • y = 0 → y = 0

AlgebraicGeometry.pairIso_iff_kummerBoundary_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FirstCohomologyOfRootsOfUnity.lean, line 359. The attribute's comment: “the pairs whose invertible sheaf is trivial: the canonical injective homomorphism from the global units modulo nth powers into H^1 of the roots of unity, carrying a pair to the class of its torsor of trivializations, on any site over the base having a terminal object and a short exact Kummer sequence (by 040N and 03PL: fppf, syntomic, and etale for n invertible on the base); pairs with a nontrivial invertible sheaf, and surjectivity onto H^1, are not covered”. References: SGA 7 IX (9.4.3), “special case”.

Stacks Project, Tag 040Q, for the pairs with trivial invertible sheaf. Two pairs whose invertible sheaf is the structure sheaf of the base are isomorphic as pairs exactly when they have the same class in the first cohomology of the sheaf of nth roots of unity. Together with AlgebraicGeometry.kummerBoundary_mul this is an injective homomorphism from the group of isomorphism classes of such pairs — the global units modulo nth powers — into H¹(S, μ_n), and by AlgebraicGeometry.terminalBoundary_eq_fiberTorsorClass it carries a pair to the class of its torsor of trivializations.

theorem pairIso_iff_kummerBoundary_eq (f g : (Scheme.Γ.obj (op (F.obj T)))ˣ) :
    Nonempty (PairIso (unitPair (F.obj T) n f) (unitPair (F.obj T) n g)) ↔
      kummerBoundary J F hF n hS hT f = kummerBoundary J F hF n hS hT g

AlgebraicGeometry.pairIso_iff_kummerBoundary_eq_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FirstCohomologyOfRootsOfUnity.lean, line 374. The attribute's comment: “the fppf case of the trivial-invertible-sheaf part, with the terminal object and the short exactness of the Kummer sequence discharged”. References: SGA 7 IX (9.4.3), “special case”.

Stacks Project, Tag 040Q on the big fppf site. The hypotheses of AlgebraicGeometry.pairIso_iff_kummerBoundary_eq hold on the big fppf site over S, with no assumption on n beyond positivity: the Kummer sequence is short exact there by Tag 040N, and S / S is the terminal object.

theorem pairIso_iff_kummerBoundary_eq_fppf (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (n : ℕ) (hn : 0 < n)
    [HasSheafify (BigFppfOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (BigFppfOver.topology B S hS) AddCommGrpCat.{u})]
    (f g : (Scheme.Γ.obj (op S))ˣ) :
    Nonempty (PairIso (unitPair S n f) (unitPair S n g)) ↔
      kummerBoundary (BigFppfOver.topology B S hS) (BigFppfOver.toScheme B S hS)
          (unitsPresheaf_isSheaf_fppf B S hS) n
          (kummerSequence_shortExact_fppf B S hS n hn)
          (Over.mkIdTerminal : IsTerminal (Over.mk (𝟙 (B.obj hS)))) f =
        kummerBoundary (BigFppfOver.topology B S hS) (BigFppfOver.toScheme B S hS)
          (unitsPresheaf_isSheaf_fppf B S hS) n
          (kummerSequence_shortExact_fppf B S hS n hn)
          (Over.mkIdTerminal : IsTerminal (Over.mk (𝟙 (B.obj hS)))) g

AlgebraicGeometry.pairIso_iff_kummerBoundary_eq_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FirstCohomologyOfRootsOfUnity.lean, line 395. The attribute's comment: “the syntomic case of the trivial-invertible-sheaf part, with the terminal object and the short exactness of the Kummer sequence discharged”.

Stacks Project, Tag 040Q on the big syntomic site.

theorem pairIso_iff_kummerBoundary_eq_syntomic (B : BigSyntomicSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (n : ℕ) (hn : 0 < n)
    [HasSheafify (BigSyntomicOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (BigSyntomicOver.topology B S hS) AddCommGrpCat.{u})]
    (f g : (Scheme.Γ.obj (op S))ˣ) :
    Nonempty (PairIso (unitPair S n f) (unitPair S n g)) ↔
      kummerBoundary (BigSyntomicOver.topology B S hS) (BigSyntomicOver.toScheme B S hS)
          (unitsPresheaf_isSheaf_syntomic B S hS) n
          (kummerSequence_shortExact_syntomic B S hS n hn)
          (Over.mkIdTerminal : IsTerminal (Over.mk (𝟙 (B.obj S hS)))) f =
        kummerBoundary (BigSyntomicOver.topology B S hS) (BigSyntomicOver.toScheme B S hS)
          (unitsPresheaf_isSheaf_syntomic B S hS) n
          (kummerSequence_shortExact_syntomic B S hS n hn)
          (Over.mkIdTerminal : IsTerminal (Over.mk (𝟙 (B.obj S hS)))) g

AlgebraicGeometry.pairIso_iff_kummerBoundary_eq_bigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FirstCohomologyOfRootsOfUnity.lean, line 417. The attribute's comment: “the big etale case of the trivial-invertible-sheaf part, for n invertible on the base, with the terminal object and the short exactness of the Kummer sequence discharged”.

Stacks Project, Tag 040Q on the big étale site, for n invertible on S.

theorem pairIso_iff_kummerBoundary_eq_bigEtale (B : BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (n : ℕ) (hn : IsUnit (n : Scheme.Γ.obj (op S)))
    [HasSheafify (BigEtaleOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (BigEtaleOver.topology B S hS) AddCommGrpCat.{u})]
    (f g : (Scheme.Γ.obj (op S))ˣ) :
    Nonempty (PairIso (unitPair S n f) (unitPair S n g)) ↔
      kummerBoundary (BigEtaleOver.topology B S hS) (BigEtaleOver.toScheme B S hS)
          (unitsPresheaf_isSheaf_bigEtale B S hS) n
          (kummerSequence_shortExact_bigEtale B S hS n hn)
          (Over.mkIdTerminal : IsTerminal (Over.mk (𝟙 (B.obj S hS)))) f =
        kummerBoundary (BigEtaleOver.topology B S hS) (BigEtaleOver.toScheme B S hS)
          (unitsPresheaf_isSheaf_bigEtale B S hS) n
          (kummerSequence_shortExact_bigEtale B S hS n hn)
          (Over.mkIdTerminal : IsTerminal (Over.mk (𝟙 (B.obj S hS)))) g

AlgebraicGeometry.pairIso_iff_kummerBoundary_eq_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/FirstCohomologyOfRootsOfUnity.lean, line 438. The attribute's comment: “the small etale case of the trivial-invertible-sheaf part, for n invertible on the base, with the terminal object and the short exactness of the Kummer sequence discharged”.

Stacks Project, Tag 040Q on the small étale site, for n invertible on S.

theorem pairIso_iff_kummerBoundary_eq_smallEtale (B : BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (n : ℕ) (hn : IsUnit (n : Scheme.Γ.obj (op S)))
    [HasSheafify (SmallEtale.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{u})]
    (f g : (Scheme.Γ.obj (op S))ˣ) :
    Nonempty (PairIso (unitPair S n f) (unitPair S n g)) ↔
      kummerBoundary (SmallEtale.topology B S hS) (SmallEtale.toScheme B S hS)
          (unitsPresheaf_isSheaf_smallEtale B S hS) n
          (kummerSequence_shortExact_smallEtale B S hS n hn)
          (SmallEtale.finalIsTerminal B S hS) f =
        kummerBoundary (SmallEtale.topology B S hS) (SmallEtale.toScheme B S hS)
          (unitsPresheaf_isSheaf_smallEtale B S hS) n
          (kummerSequence_shortExact_smallEtale B S hS n hn)
          (SmallEtale.finalIsTerminal B S hS) g

AlgebraicGeometry.instAddCommGroupPairClasses, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairAddCommGroup.lean, line 74. The attribute's comment: “the abelian-group structure on the isomorphism classes of pairs (L, alpha), with addition the tensor product of pairs, zero the structure sheaf with its canonical trivialization, and negation the inverse pair; this is the group the tag identifies with H^1 of the roots of unity, but the identification itself is not stated here”.

The isomorphism classes of pairs form an abelian group. The addition is the tensor product of pairs, the zero is the structure sheaf with its canonical trivialization, and the negation is the inverse pair.

instance instAddCommGroupPairClasses (S : Scheme.{u}) (n : ℕ) :
    AddCommGroup (PairClasses S n)

AlgebraicGeometry.basePairTriv_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairComparisonHom.lean, line 112. The attribute's comment: “the transport to the big tau-site carries the tensor product of pairs to the tensor product of pairs”.

The transported trivialization of a tensor product of pairs is the tensor product of the two transported trivializations, on the big τ-site of S.

This is part (4) of the second construction of Tag 040Q: it is Stacks.SheafOfModules.TensorPowerTransport.transportTriv_tensor at the associated-module functor of Descent, Proposition 03DX, whose four coherences are AlgebraicGeometry.BigFppfOver.baseAssociatedModuleTensorIso'_natural, _associator, _braiding and _rightUnitor.

public theorem basePairTriv_tensor (P Q : TrivializedPower S n) :
    letI := basePairSheaf_isInvertible B S hS τ n P
    letI := basePairSheaf_isInvertible B S hS τ n Q
    letI : IsInvertible (BigFppfOver.baseRingedSite B S hS τ).O.obj
        (Stacks.SheafOfModules.Tensor.ringSheaf (BigFppfOver.baseRingedSite B S hS τ).O).2
        ((BigFppfOver.baseAssociatedModule B S hS τ).obj
          ((((Stacks.SheafOfModules.Tensor.sheafTensor
            ⟨S.presheaf, Presheaf.isSheaf_of_isSheaf_comp _ S.presheaf
              (forget₂ CommRingCat RingCat) (ringSheafCond S)⟩).obj P.sheaf).obj Q.sheaf))) :=
      basePairSheaf_isInvertible B S hS τ n (tensorPair S n P Q)
    letI : IsInvertible (BigFppfOver.baseRingedSite B S hS τ).O.obj
        (Stacks.SheafOfModules.Tensor.ringSheaf (BigFppfOver.baseRingedSite B S hS τ).O).2
        (tensorSheafOfModules (BigFppfOver.baseRingedSite B S hS τ)
          ((BigFppfOver.baseAssociatedModule B S hS τ).obj P.sheaf)
          ((BigFppfOver.baseAssociatedModule B S hS τ).obj Q.sheaf)) :=
      Stacks.SheafOfModules.isInvertible_tensorSheaf
        (BigFppfOver.baseRingedSite B S hS τ).O.obj
        (Stacks.SheafOfModules.Tensor.ringSheaf (BigFppfOver.baseRingedSite B S hS τ).O).2
        (basePairSheaf B S hS τ n P) (basePairSheaf B S hS τ n Q)
    powerMap (BigFppfOver.baseRingedSite B S hS τ)
          (BigFppfOver.baseAssociatedModuleTensorIso' B S hS τ P.sheaf Q.sheaf) n ≪≫
        tensorTriv (BigFppfOver.baseRingedSite B S hS τ) (basePairSheaf B S hS τ n P)
          (basePairSheaf B S hS τ n Q) n (basePairTriv B S hS τ n P)
          (basePairTriv B S hS τ n Q) =
      basePairTriv B S hS τ n (tensorPair S n P Q)

AlgebraicGeometry.basePairClass_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairComparisonHom.lean, line 159. The attribute's comment: “the torsor of trivializations of a tensor product of pairs”.

A tensor product of pairs has the torsor of trivializations of the tensor product of the two transported pairs. This is AlgebraicGeometry.trivializationTorsor_class_eq_of_iso' fed the object-level tensor comparison of the associated-module functor and AlgebraicGeometry.basePairTriv_tensor.

public theorem basePairClass_tensor (hroot : LocalRoots (BigFppfOver.baseRingedSite B S hS τ) n)
    (P Q : TrivializedPower S n) :
    Quotient.mk
          (torsorSetoid (rootsOfUnitySheaf (BigFppfOver.baseOverTopology B S hS τ)
            (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS τ) n))
          (trivializationTorsor (BigFppfOver.baseOverTopology B S hS τ)
            (BigFppfOver.toScheme B S hS) (BigFppfOver.baseRingedSite B S hS τ).O.property
            (unitsPresheaf_isSheaf_base B S hS τ) n
            (baseRingedSite_isLocallyRinged B S hS τ) hroot
            (basePairSheaf B S hS τ n (tensorPair S n P Q))
            (basePairSheaf_isInvertible B S hS τ n (tensorPair S n P Q))
            (basePairTriv B S hS τ n (tensorPair S n P Q))) =
      Quotient.mk
        (torsorSetoid (rootsOfUnitySheaf (BigFppfOver.baseOverTopology B S hS τ)
          (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS τ) n))
        (trivializationTorsor (BigFppfOver.baseOverTopology B S hS τ)
          (BigFppfOver.toScheme B S hS) (BigFppfOver.baseRingedSite B S hS τ).O.property
          (unitsPresheaf_isSheaf_base B S hS τ) n
          (baseRingedSite_isLocallyRinged B S hS τ) hroot
          (tensorSheafOfModules (BigFppfOver.baseRingedSite B S hS τ)
            (basePairSheaf B S hS τ n P) (basePairSheaf B S hS τ n Q))
          (Stacks.SheafOfModules.isInvertible_tensorSheaf
            (BigFppfOver.baseRingedSite B S hS τ).O.obj
            (Stacks.SheafOfModules.Tensor.ringSheaf (BigFppfOver.baseRingedSite B S hS τ).O).2
            (basePairSheaf B S hS τ n P) (basePairSheaf B S hS τ n Q))
          (tensorTriv (BigFppfOver.baseRingedSite B S hS τ) (basePairSheaf B S hS τ n P)
            (basePairSheaf B S hS τ n Q) n (basePairTriv B S hS τ n P)
            (basePairTriv B S hS τ n Q)))

AlgebraicGeometry.basePairCohomologyClass_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairComparisonHom.lean, line 207. The attribute's comment: “the comparison map is additive on classes of pairs”.

The comparison map of Tag 040Q is additive, read on classes of pairs: the class of a tensor product of pairs is the sum of the two classes.

public theorem basePairCohomologyClass_add
    (hroot : LocalRoots (BigFppfOver.baseRingedSite B S hS τ) n) (P Q : TrivializedPower S n) :
    basePairCohomologyClass B S hS τ n hroot (pairClass P + pairClass Q) =
      basePairCohomologyClass B S hS τ n hroot (pairClass P) +
        basePairCohomologyClass B S hS τ n hroot (pairClass Q)

AlgebraicGeometry.basePairCohomologyClassHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairComparisonHom.lean, line 229. The attribute's comment: “the comparison map from the isomorphism classes of pairs to H^1 of the roots of unity as a homomorphism of abelian groups; injectivity and surjectivity are not proved here”.

The comparison map of Tag 040Q as a homomorphism of abelian groups, PairClasses S n →+ H¹((Sch/S)_τ, μ_n). The addition of the source is the tensor product of pairs and that of the target is the addition of Ext¹; additivity is AlgebraicGeometry.basePairCohomologyClass_add, and the vanishing at the zero class follows from it, the two groups being groups.

This is the map Stacks.Kummer.bijective_of_comparison consumes.

public def basePairCohomologyClassHom
    (hroot : LocalRoots (BigFppfOver.baseRingedSite B S hS τ) n) :
    PairClasses S n →+
      Sheaf.H (rootsOfUnitySheaf (BigFppfOver.baseOverTopology B S hS τ)
        (BigFppfOver.toScheme B S hS) (unitsPresheaf_isSheaf_base B S hS τ) n) 1

AlgebraicGeometry.pairSheafClassHom_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairExactSequence.lean, line 141. The attribute's comment: “exactness in the middle of the pair side of the extension, as abelian groups: the kernel of the homomorphism from the isomorphism classes of pairs to the Picard group is the image of the homomorphism from the global units; neither the cohomology group nor the comparison with it occurs”.

Stacks Project, Tag 040Q, exactness in the middle of the pair side. A class of pairs has trivial Picard class — that is, its invertible sheaf is isomorphic to the structure sheaf — exactly when it is the class of a pair coming from a global unit. The forward direction is AlgebraicGeometry.exists_pairIso_unitPair, that a pair whose invertible sheaf is merely isomorphic to the structure sheaf is isomorphic to a unit pair.

theorem pairSheafClassHom_eq_zero_iff (S : Scheme.{u}) (n : ℕ) (x : PairClasses S n) :
    pairSheafClassHom S n x = 0 ↔
      ∃ f : Additive (Scheme.Γ.obj (op S))ˣ, unitPairHom S n f = x

AlgebraicGeometry.exists_pairSheafClassHom_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/KummerTheory/PairExactSequence.lean, line 161. The attribute's comment: “the image of the homomorphism from the isomorphism classes of pairs to the Picard group is exactly the n-torsion, as abelian groups; this is the surjectivity half of the pair side of the extension, and the cohomology group does not occur”.

Stacks Project, Tag 040Q, surjectivity of the pair side onto the torsion. A Picard class is the Picard class of a class of pairs exactly when it is n-torsion. This is AlgebraicGeometry.exists_trivializedPower_classOf_iff read through the group of isomorphism classes of pairs.

theorem exists_pairSheafClassHom_eq_iff (S : Scheme.{u}) (n : ℕ)
    (c : PicardGroup S.presheaf (ringSheafCond S)) :
    (∃ x : PairClasses S n, pairSheafClassHom S n x = c) ↔ n • c = 0

Sources

• Section 59.28, Tag 03PK
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.kummerSequence_shortExact_bigEtale · AlgebraicGeometry.kummerSequence_shortExact_smallEtale · AlgebraicGeometry.kummerSequence_shortExact_fppf · AlgebraicGeometry.kummerSequence_shortExact_syntomic · AlgebraicGeometry.pairIso_torsor · AlgebraicGeometry.scalarTranslate_pairIso · AlgebraicGeometry.pairIso_unitPair_iff · AlgebraicGeometry.exists_trivializedPower_sheaf_iff

Section59.29 Neighborhoods, stalks and points#

Section 59.29 of the Stacks Project, Tag 03PN. 11 tags here are carried by 43 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03PO, a definition

Tag 03PO in the Stacks Project.

AlgebraicGeometry.GeometricPoint, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/Basic.lean, line 47. The attribute's comment: “part (1)”. References: SGA 4½ Arcata (2.3.1), “special case”; SGA 7 XIX (1.4).

A geometric point of a scheme is a morphism from the spectrum of an algebraically closed field.

structure GeometricPoint (S : Scheme.{u})

AlgebraicGeometry.GeometricPoint.LiesOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/Basic.lean, line 66. The attribute's comment: “part (2)”.

A geometric point lies over the point which is its image in the underlying topological space.

abbrev LiesOver {S : Scheme.{u}} (s : GeometricPoint S) (x : S) : Prop

AlgebraicGeometry.GeometricPoint.EtaleNeighborhood, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/Basic.lean, line 77. The attribute's comment: “part (3)”. References: SGA 4 VIII (3.9), “objects of C_ξ”.

An étale neighborhood of a geometric point consists of an étale scheme over the base together with a lift of the geometric point.

structure EtaleNeighborhood {S : Scheme.{u}} (s : GeometricPoint S)

AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/Basic.lean, line 95. The attribute's comment: “part (4)”.

A morphism of étale neighborhoods is a morphism over the base which carries the chosen lift to the chosen lift.

structure Hom {S : Scheme.{u}} {s : GeometricPoint S} (U V : EtaleNeighborhood s)

Tag 03PP, a remark

Tag 03PP in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch59.lean, line 163 (StacksFrontier): “an S-morphism between étale S-schemes is étale”. References: EGA IV (17.1.5), “special case”; EGA IV (17.3.5), “étale clause”; SGA 1 V (3.3), “special case”; SGA 4 VII (1.2), “more general”; SGA 4½ Arcata (2.1.3); SGA 4½ Arcata (2.1.4), “more general”.

Tag 04HT, a remark

Tag 04HT in the Stacks Project.

AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.toEtaleNeighborhood, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/PointNeighborhood.lean, line 59. The attribute's comment: “first direction”.

An étale neighbourhood (U, ū) of a geometric point σ lying over s gives the étale neighbourhood (U, u) of (S, s), where u is the image of ū.

def toEtaleNeighborhood (U : σ.EtaleNeighborhood) (h : σ.LiesOver s) :
    AlgebraicGeometry.EtaleNeighborhood S s

AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.geometricPoint_liesOver_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/PointNeighborhood.lean, line 88. The attribute's comment: “first direction: u is the unique point under ū”.

The distinguished point u of the étale neighbourhood (U, u) attached to (U, ū) is the unique point of U over which the geometric point ū lies.

theorem geometricPoint_liesOver_iff (U : σ.EtaleNeighborhood) (h : σ.LiesOver s)
    (x : U.scheme) : U.geometricPoint.LiesOver x ↔ x = (U.toEtaleNeighborhood h).point

AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.toEtaleNeighborhood_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/PointNeighborhood.lean, line 96. The attribute's comment: “converse direction”.

Conversely, every étale neighbourhood (U, u) of (S, s) comes from an étale neighbourhood of a geometric point σ lying over s: there is a geometric point ū of U lying over u such that (U, ū) is an étale neighbourhood of (S, σ).

theorem toEtaleNeighborhood_surjective (h : σ.LiesOver s) :
    Function.Surjective fun U : σ.EtaleNeighborhood ↦ U.toEtaleNeighborhood h

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch59.lean, line 318 (StacksFrontier): “converse: a geometric point ū of U over u with (U, ū) → (S, s̄)”. References: EGA IV (18.8.1), “(a)⇒(c), special case”; SGA 4 VIII (3.2), “partial”.

Tag 03PQ, a lemma

Tag 03PQ in the Stacks Project.

Declarations registered for the tag:

• instIsCofilteredElementsEtaleCompOverForgetObjOppositeFunctorTypeCoyonedaOpMk registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch59.lean, line 166 (StacksFrontier): “the étale neighborhoods of a geometric point s : Spec Ω → S (Ω separably closed) form a cofiltered category”.

Tag 03PR, a lemma

Tag 03PR in the Stacks Project.

AlgebraicGeometry.Scheme.Cover.exists_etaleNeighborhood_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/CoverLift.lean, line 44.

Let s : Spec Ω ⟶ S be a geometric point of S, with Ω separably closed, and let (U, u) be an étale neighborhood of s, that is f : U ⟶ S is étale and u ≫ f = s. Then for every étale covering 𝒰 of U there are an index i and a lift uᵢ of u to 𝒰.X i, so that (𝒰.X i, uᵢ) is an étale neighborhood of s and 𝒰.f i is a morphism of étale neighborhoods (𝒰.X i, uᵢ) ⟶ (U, u).

theorem exists_etaleNeighborhood_lift {S U : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (s : Spec (.of Ω) ⟶ S) (f : U ⟶ S) [Etale f] (u : Spec (.of Ω) ⟶ U) (hu : u ≫ f = s)
    (𝒰 : U.Cover.{v} etalePrecoverage) :
    ∃ (i : 𝒰.I₀) (uᵢ : Spec (.of Ω) ⟶ 𝒰.X i),
      Etale (𝒰.f i ≫ f) ∧ uᵢ ≫ 𝒰.f i ≫ f = s ∧ uᵢ ≫ 𝒰.f i = u

Tag 040R, a definition

Tag 040R in the Stacks Project.

AlgebraicGeometry.geometricPointFiber_initiallySmall, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointFiber.lean, line 156. The attribute's comment: “small neighborhood basis”.

The neighborhoods of a geometric point in the chosen small étale site admit a universe-u cofinal subcategory.

public instance geometricPointFiber_initiallySmall :
    InitiallySmall.{u} (geometricPointFiber B S hS s).Elements

AlgebraicGeometry.etaleStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointFiber.lean, line 178.

The stalk of a presheaf on the small étale site at a geometric point, as the colimit over its étale neighborhoods.

public def etaleStalk {A : Type v} [Category.{w} A] (F : (SmallEtale B S hS)ᵒᵖ ⥤ A)
    [HasColimit ((CategoryOfElements.π (geometricPointFiber B S hS s)).op ⋙ F)] : A

Tag 04FM, a lemma

Tag 04FM in the Stacks Project.

AlgebraicGeometry.etaleStalkSkyscraperAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/GeometricSkyscraper.lean, line 73. The attribute's comment: “the stalk at a geometric point is left adjoint to the skyscraper there”.

Stacks 04FM. The stalk functor at a geometric point s̄ of S is left adjoint to the skyscraper functor at s̄: a map F_s̄ ⟶ M is the same as a map F ⟶ s̄_* M.

public def etaleStalkSkyscraperAdjunction [HasColimitsOfSize.{u, u} A] :
    (geometricPointSitePoint B S hS s).sheafFiber (A := A) ⊣
      etaleSkyscraperFunctor B S hS s A

AlgebraicGeometry.geometricPointFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointFiber.lean, line 81. The attribute's comment: “the functor u : U ↦ |U_s̄|”.

The lifts of a geometric point to objects of the small étale site, i.e. the functor

u : S_étale ⟶ Sets, U ↦ {ū such that (U, ū) is an étale neighbourhood of s̄}

sending U to the morphisms s̄ ⟶ U over S.

public def geometricPointFiber : SmallEtale B S hS ⥤ Type u

AlgebraicGeometry.geometricPointFiberObjEquivGeometricFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/GeometricFibre.lean, line 128. The attribute's comment: “the two descriptions of u(U): the geometric fibre and the étale neighbourhoods”.

Stacks Project, Tag 04FM, the identification of the two descriptions of the value of the fibre functor. For an object U of the small étale site of S, the set (geometricPointFiber B S hS s).obj U of lifts of the geometric point s to U — the set {ū : (U, ū) is an étale neighbourhood of s̄} of the source — is in bijection with the underlying set |U_s̄| of the geometric fibre of U at s.

def geometricPointFiberObjEquivGeometricFibre (U : SmallEtale B S hS) :
    (geometricPointFiber B S hS s).obj U ≃
      ↥(pullback (B.inclusion.map U.obj.hom) s.hom)

AlgebraicGeometry.geometricPointSitePoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SitePoint.lean, line 157. The attribute's comment: “the functor u defines a point of the small étale site”.

Stacks Project, Tag 04FM. The functor u of AlgebraicGeometry.geometricPointFiber defines a point p of the site S_étale: a geometric point of S, viewed as a point of the small étale site of S, with fiber functor u.

The source obtains this from the criterion of Sites, Proposition 00YC, checking that u(S) is a singleton, that u preserves fibre products, and that ∐ u(U_i) ⟶ u(U) is surjective for a covering. Mathlib's CategoryTheory.GrothendieckTopology.Point asks instead for cofilteredness of the category of elements of u, which for this u is the cofilteredness of the category of étale neighbourhoods of the geometric point (AlgebraicGeometry.isCofiltered_geometricPointFiber_elements), together with the joint surjectivity, which is AlgebraicGeometry.geometricPointFiber_jointly_surjective. The two descriptions of a point agree on a site with finite limits by CategoryTheory.GrothendieckTopology.Point.equivFiber, the formalization of Tag 00YC.

public def geometricPointSitePoint :
    (SmallEtale.topology B S hS).Point

AlgebraicGeometry.etaleStalk_eq_presheafFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SitePoint.lean, line 178. The attribute's comment: “the stalk functor of p is the stalk at the geometric point”.

Stacks Project, Tag 04FM, the final assertion: the stalk functor F ↦ F_p attached to the point p = AlgebraicGeometry.geometricPointSitePoint by Sites, Equation 04EH — which is CategoryTheory.GrothendieckTopology.Point.presheafFiber — is the stalk functor F ↦ F_s̄ at the geometric point of Tag 040R, which is AlgebraicGeometry.etaleStalk. Both are given by the same colimit over the category of étale neighbourhoods, so the general theory of points of a site — exactness, invariance under sheafification, commutation with colimits — applies to the stalk at a geometric point.

public theorem etaleStalk_eq_presheafFiber {A : Type v} [Category.{w} A]
    [HasColimitsOfSize.{u, u} A] (F : (SmallEtale B S hS)ᵒᵖ ⥤ A) :
    etaleStalk B S hS s F = (geometricPointSitePoint B S hS s).presheafFiber.obj F

Tag 04FN, a remark

Tag 04FN in the Stacks Project.

AlgebraicGeometry.GeometricPoint.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 432. The attribute's comment: “morphism of geometric points”.

A morphism of geometric points over the same scheme.

public structure Hom {S : Scheme.{u}}
    (s t : GeometricPoint S)

AlgebraicGeometry.geometricPointFiberMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 444. The attribute's comment: “map of geometric fibers”.

A lift of t to an étale scheme yields a lift of s by precomposition.

public def geometricPointFiberMap (a : GeometricPoint.Hom s t) :
    geometricPointFiber B S hS t ⟶
      geometricPointFiber B S hS s

AlgebraicGeometry.geometricPointFiberMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 494. The attribute's comment: “isomorphism of site points”.

For a morphism a : s ⟶ t of geometric points of S, the map of geometric fibres geometricPointFiberMap B S hS a, given by precomposition with a, is an isomorphism.

public theorem geometricPointFiberMap_isIso :
    IsIso (geometricPointFiberMap B S hS a)

AlgebraicGeometry.neighborhoodFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 509. The attribute's comment: “functor on neighborhoods”.

Restriction of an étale neighborhood of t along a.

public def neighborhoodFunctor (a : GeometricPoint.Hom s t) :
    (geometricPointFiber B S hS t).Elements ⥤
      (geometricPointFiber B S hS s).Elements

AlgebraicGeometry.neighborhoodFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 516. The attribute's comment: “equivalence of neighborhoods”.

Restriction along a is an equivalence of étale-neighborhood categories.

public theorem neighborhoodFunctor_isEquivalence :
    (neighborhoodFunctor B S hS a).IsEquivalence

AlgebraicGeometry.geometricPointStalkMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 529. The attribute's comment: “canonical map of stalk functors”.

The canonical map from the stalk at t to the stalk at s, natural in the presheaf.

public def geometricPointStalkMap (A : Type v) [Category.{w} A]
    [HasColimitsOfShape (geometricPointFiber B S hS t).Elementsᵒᵖ A]
    [HasColimitsOfShape (geometricPointFiber B S hS s).Elementsᵒᵖ A] :
    etaleStalkPresheafFunctor B S hS t A ⟶
      etaleStalkPresheafFunctor B S hS s A

AlgebraicGeometry.geometricPointStalkMap_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 548. The attribute's comment: “action on represented sections”.

The canonical map takes the germ of (U, u', σ) to the germ of (U, u' ∘ a, σ).

public theorem geometricPointStalkMap_germ
    (F : (SmallEtale B S hS)ᵒᵖ ⥤ Type u)
    (U : (geometricPointFiber B S hS t).Elementsᵒᵖ)
    (σ : F.obj (Opposite.op U.unop.1)) :
    (geometricPointStalkMap B S hS a (Type u)).app F
        ((colimit.ι
          ((CategoryOfElements.π (geometricPointFiber B S hS t)).op ⋙ F) U) σ) =
      (colimit.ι
        ((CategoryOfElements.π (geometricPointFiber B S hS s)).op ⋙ F)
        ((neighborhoodFunctor B S hS a).op.obj U)) σ

AlgebraicGeometry.geometricPointStalkMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 566. The attribute's comment: “isomorphism of stalk functors”.

A morphism of geometric points induces a canonical natural isomorphism of étale stalk functors.

public theorem geometricPointStalkMap_isIso (A : Type v) [Category.{w} A]
    [HasColimitsOfShape (geometricPointFiber B S hS t).Elementsᵒᵖ A]
    [HasColimitsOfShape (geometricPointFiber B S hS s).Elementsᵒᵖ A] :
    IsIso (geometricPointStalkMap B S hS a A)

AlgebraicGeometry.smallEtalePointHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 587. The attribute's comment: “morphism of associated site points”.

The morphism of points of the unrestricted small étale site induced by a. Its fiber component sends a lift u' to u' ∘ a.

public def smallEtalePointHom :
    Scheme.pointSmallEtale s.hom ⟶ Scheme.pointSmallEtale t.hom

AlgebraicGeometry.smallEtalePointHom_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 605. The attribute's comment: “isomorphism of associated site points”.

A morphism of geometric points induces an isomorphism of their associated points of the small étale site.

public theorem smallEtalePointHom_isIso : IsIso (smallEtalePointHom S a)

Tag 03PT, a lemma

Tag 03PT in the Stacks Project.

AlgebraicGeometry.Scheme.pointSmallEtale_presheafFiber_ab_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointSmallEtaleStalkExact.lean, line 65. The attribute's comment: “(1) the stalk functor on abelian presheaves is exact”.

The stalk functor on abelian presheaves is exact. For a geometric point s of S, the stalk functor PAb(S_et) ⥤ Ab, 𝓕 ↦ 𝓕_s̄, commutes with finite limits and finite colimits.

theorem pointSmallEtale_presheafFiber_ab_exact :
    PreservesFiniteLimits ((pointSmallEtale s).presheafFiber (A := AddCommGrpCat.{max u v})) ∧
      PreservesFiniteColimits
        ((pointSmallEtale s).presheafFiber (A := AddCommGrpCat.{max u v}))

AlgebraicGeometry.Scheme.isIso_pointSmallEtale_presheafFiber_map_toSheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointSmallEtaleStalkExact.lean, line 77. The attribute's comment: “(2) the stalk of a presheaf of sets equals the stalk of its sheafification”.

Stalks of a presheaf of sets and of its sheafification agree. For a geometric point s of S and a presheaf of sets 𝓕 on S_et, the map 𝓕_s̄ ⟶ (𝓕^#)_s̄ induced by 𝓕 ⟶ 𝓕^# is an isomorphism.

theorem isIso_pointSmallEtale_presheafFiber_map_toSheafify
    (F : S.Etaleᵒᵖ ⥤ Type u) :
    IsIso ((pointSmallEtale s).presheafFiber.map (toSheafify (smallEtaleTopology S) F))

AlgebraicGeometry.Scheme.isIso_pointSmallEtale_presheafFiber_map_toSheafify', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointSmallEtaleStalkExact.lean, line 86. The attribute's comment: “(2) the stalk of a presheaf of sets equals the stalk of its sheafification”.

Stalks of a presheaf of sets and of its sheafification agree, for presheaves of sets in Type (max (u + 1) v). For a geometric point s of S and a presheaf of sets 𝓕 on S_et, the map 𝓕_s̄ ⟶ (𝓕^#)_s̄ induced by 𝓕 ⟶ 𝓕^# is an isomorphism.

theorem isIso_pointSmallEtale_presheafFiber_map_toSheafify'
    (F : S.Etaleᵒᵖ ⥤ Type (max (u + 1) v)) :
    IsIso ((pointSmallEtale s).presheafFiber.map (toSheafify (smallEtaleTopology S) F))

AlgebraicGeometry.Scheme.pointSmallEtale_sheafFiber_ab_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointSmallEtaleStalkExact.lean, line 94. The attribute's comment: “(3) the stalk functor on abelian sheaves is exact”.

The stalk functor on abelian sheaves is exact. For a geometric point s of S, the stalk functor Ab(S_et) ⥤ Ab, 𝓕 ↦ 𝓕_s̄, commutes with finite limits and finite colimits.

theorem pointSmallEtale_sheafFiber_ab_exact :
    PreservesFiniteLimits ((pointSmallEtale s).sheafFiber (A := AddCommGrpCat.{max u v})) ∧
      PreservesFiniteColimits ((pointSmallEtale s).sheafFiber (A := AddCommGrpCat.{max u v}))

AlgebraicGeometry.Scheme.pointSmallEtale_presheafFiber_type_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointSmallEtaleStalkExact.lean, line 105. The attribute's comment: “(4) the stalk functor on presheaves of sets is exact and commutes with colimits”.

The stalk functor on presheaves of sets is exact and commutes with colimits. For a geometric point s of S, the stalk functor PSh(S_et) ⥤ Sets, 𝓕 ↦ 𝓕_s̄, commutes with finite limits, with finite colimits, and with colimits of any size.

theorem pointSmallEtale_presheafFiber_type_exact :
    PreservesFiniteLimits ((pointSmallEtale s).presheafFiber (A := Type (max u v))) ∧
      PreservesFiniteColimits ((pointSmallEtale s).presheafFiber (A := Type (max u v))) ∧
      PreservesColimitsOfSize.{w₁, w₂}
        ((pointSmallEtale s).presheafFiber (A := Type (max u v)))

AlgebraicGeometry.Scheme.pointSmallEtale_sheafFiber_type_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointSmallEtaleStalkExact.lean, line 119. The attribute's comment: “(4) the stalk functor on sheaves of sets is exact and commutes with colimits”.

The stalk functor on sheaves of sets is exact and commutes with colimits. For a geometric point s of S, the stalk functor Sh(S_et) ⥤ Sets, 𝓕 ↦ 𝓕_s̄, commutes with finite limits, with finite colimits, and with colimits of any size.

theorem pointSmallEtale_sheafFiber_type_exact :
    PreservesFiniteLimits ((pointSmallEtale s).sheafFiber (A := Type (max u v))) ∧
      PreservesFiniteColimits ((pointSmallEtale s).sheafFiber (A := Type (max u v))) ∧
      PreservesColimitsOfSize.{w₁, w₂}
        ((pointSmallEtale s).sheafFiber (A := Type (max u v)))

Tag 03PU, a theorem

Tag 03PU in the Stacks Project.

AlgebraicGeometry.isZero_of_forall_isZero_etaleStalk_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageFaithfulnessModules.lean, line 131. The attribute's comment: “module coefficients, the vanishing case of the isomorphism criterion: a sheaf of modules whose geometric stalks all vanish is zero”.

Stacks 03PU for sheaves of modules, the vanishing case. A sheaf of Λ-modules on the small étale site of S whose stalk at every geometric point of S vanishes is zero.

The zero map from the zero sheaf is surjective on every geometric stalk, the target of each of those maps being a zero module, so it is locally surjective by Tag 03PU and therefore an epimorphism; an epimorphism out of a zero object forces the identity of its target to vanish.

public theorem isZero_of_forall_isZero_etaleStalk_module (S : Scheme.{u}) (hS : B.Contains S)
    (F : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{u + 1} Λ))
    (h : ∀ t : GeometricPoint S, IsZero (etaleStalk B S hS t F.obj)) :
    IsZero F

AlgebraicGeometry.isIso_of_bijective_etaleStalkMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardBaseChange.lean, line 202. The attribute's comment: “sheaves of sets, the isomorphism case”.

A morphism of sheaves of sets on the small étale site of X which is bijective on the stalk at every geometric point of X is an isomorphism.

public theorem isIso_of_bijective_etaleStalkMap (α : F ⟶ G)
    (h : ∀ s : GeometricPoint X, Function.Bijective
      ((etaleStalkFunctor.{u, u + 1} B X hX s).map α)) :
    IsIso α

AlgebraicGeometry.GeometricPoint.mono_iff_forall_injective_stalkFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/StalksTestMaps.lean, line 147. The attribute's comment: “injectivity on stalks at geometric points”. References: SGA 4 VIII (3.6), “mono ⟺ inj on stalks”.

Stacks Project, Tag 03PU. A map of sheaves of sets on the small étale site of a scheme is injective if and only if it is injective on the stalk at every geometric point.

theorem mono_iff_forall_injective_stalkFunctor (φ : F ⟶ G) :
    Mono φ ↔ ∀ s : GeometricPoint S, Function.Injective (s.stalkFunctor.map φ)

AlgebraicGeometry.GeometricPoint.epi_iff_forall_surjective_stalkFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/StalksTestMaps.lean, line 160. The attribute's comment: “surjectivity on stalks at geometric points”. References: SGA 4 VIII (3.6), “epi ⟺ surj on stalks”.

Stacks Project, Tag 03PU. A map of sheaves of sets on the small étale site of a scheme is surjective if and only if it is surjective on the stalk at every geometric point.

theorem epi_iff_forall_surjective_stalkFunctor (φ : F ⟶ G) :
    Epi φ ↔ ∀ s : GeometricPoint S, Function.Surjective (s.stalkFunctor.map φ)

AlgebraicGeometry.isLocallySurjective_of_surjective_etaleStalkMapOfCoefficients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/ModuleCoefficients.lean, line 106. The attribute's comment: “local surjectivity from surjectivity on geometric stalks, arbitrary coefficients”.

Stacks 03PU for an arbitrary concrete coefficient category. A map of sheaves on the small étale site of S which is surjective on the stalk at every geometric point of S is locally surjective.

A section over V is, near every point of V, the image of a section: its germ at the geometric point attached to that point is the image of a germ, germs are computed on étale neighbourhoods, and two sections with the same germ agree on an étale neighbourhood of the point.

public theorem isLocallySurjective_of_surjective_etaleStalkMapOfCoefficients
    {F G : Sheaf (SmallEtale.topology B S hS) A} (α : F ⟶ G)
    (h : ∀ s : GeometricPoint S, Function.Surjective
      ((etaleStalkPresheafFunctor B S hS s A).map α.hom)) :
    Presheaf.IsLocallySurjective (SmallEtale.topology B S hS) α.hom

AlgebraicGeometry.surjective_etaleStalkMap_of_isLocallySurjective_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/ModuleCoefficients.lean, line 225. The attribute's comment: “surjectivity on geometric stalks, module coefficients”.

Stacks 03PU for sheaves of modules. A locally surjective map of sheaves of Λ-modules on a small étale site is surjective on the stalk at every geometric point: the stalk is the fiber of the point of the site attached to the geometric point, and a point of a site turns local surjectivity into surjectivity.

public theorem surjective_etaleStalkMap_of_isLocallySurjective_module
    (S : Scheme.{u}) (hS : B.Contains S)
    {F G : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{u + 1} Λ)} (α : F ⟶ G)
    [Presheaf.IsLocallySurjective (SmallEtale.topology B S hS) α.hom]
    (s : GeometricPoint S) :
    Function.Surjective
      ((etaleStalkPresheafFunctor B S hS s (ModuleCat.{u + 1} Λ)).map α.hom)

AlgebraicGeometry.isLocallySurjective_of_surjective_etaleStalkMap_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/ModuleCoefficients.lean, line 238. The attribute's comment: “local surjectivity from surjectivity on geometric stalks, module coefficients”.

Stacks 03PU for sheaves of modules. A map of sheaves of Λ-modules on the small étale site of S which is surjective on the stalk at every geometric point of S is locally surjective.

public theorem isLocallySurjective_of_surjective_etaleStalkMap_module
    (S : Scheme.{u}) (hS : B.Contains S)
    {F G : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{u + 1} Λ)} (α : F ⟶ G)
    (h : ∀ s : GeometricPoint S, Function.Surjective
      ((etaleStalkPresheafFunctor B S hS s (ModuleCat.{u + 1} Λ)).map α.hom)) :
    Presheaf.IsLocallySurjective (SmallEtale.topology B S hS) α.hom

AlgebraicGeometry.jointlyFaithful_etaleStalkSheafFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkExactnessCriterion.lean, line 100. The attribute's comment: “the geometric stalks are jointly faithful on abelian étale sheaves”. References: SGA 4 VIII (3.7), “special case”.

Stacks 03PU. The stalk functors at the geometric points of S are jointly faithful on abelian sheaves on the small étale site of S: two morphisms of sheaves inducing the same map on every stalk are equal.

Two morphisms with the same germ at every geometric point agree, over each object of the site, on the sieve of arrows along which the two sections become equal; that sieve is covering because every point of the object carries a geometric point lifting to it, and a sheaf is separated for a covering sieve.

public theorem jointlyFaithful_etaleStalkSheafFiber :
    JointlyFaithful (fun s : GeometricPoint S =>
      (geometricPointSitePoint B S hS s).sheafFiber (A := AddCommGrpCat.{max (u + 1) v}))

AlgebraicGeometry.exact_iff_etaleStalk_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkExactnessCriterion.lean, line 138. The attribute's comment: “exactness of abelian étale sheaves is checked on geometric stalks”.

Stacks 03PU. A short complex of abelian sheaves on the small étale site of S is exact exactly when its short complex of stalks at every geometric point of S is exact.

A stalk is a filtered colimit, so the stalk functors are exact and the condition is necessary; it is sufficient because the stalk functors are jointly faithful, so a sheaf whose stalks all vanish vanishes, applied to the homology of the complex.

public theorem exact_iff_etaleStalk_exact
    (T : ShortComplex (Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{max (u + 1) v})) :
    T.Exact ↔ ∀ s : GeometricPoint S,
      let Φ := sheafToPresheaf (SmallEtale.topology B S hS) AddCommGrpCat.{max (u + 1) v} ⋙
        etaleStalkPresheafFunctor B S hS s AddCommGrpCat.{max (u + 1) v}
      ∀ b : Φ.obj T.X₂,
        ((Φ.map T.g).hom b = 0 ↔ ∃ a : Φ.obj T.X₁, (Φ.map T.f).hom a = b)

AlgebraicGeometry.surjective_etaleStalkMap_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedDerivedEquivalence.lean, line 268. The attribute's comment: “surjectivity on stalks at geometric points, abelian sheaves”. References: SGA 4 VIII (3.6), “epi ⇒ surj on stalks”.

Stacks 03PU. A locally surjective morphism of abelian sheaves on a small étale site is surjective on the stalk at every geometric point: the stalk is the fiber of the point of the site attached to the geometric point, and a point of a site turns local surjectivity into surjectivity.

public theorem surjective_etaleStalkMap_of_isLocallySurjective
    (Y : Scheme.{u}) (hY : B.Contains Y)
    {F G : Sheaf (SmallEtale.topology B Y hY) AddCommGrpCat.{u + 1}} (α : F ⟶ G)
    [Presheaf.IsLocallySurjective (SmallEtale.topology B Y hY) α.hom]
    (s : GeometricPoint Y) :
    Function.Surjective
      ((etaleStalkPresheafFunctor B Y hY s AddCommGrpCat.{u + 1}).map α.hom)

Tag 04HU, a lemma

Tag 04HU in the Stacks Project.

AlgebraicGeometry.exists_geometricPoint_fiber_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/SitePoints.lean, line 582. The attribute's comment: “part (1)”. References: SGA 4 VIII (7.9), “essential surjectivity”.

Stacks 04HU, part (1). Every point of the small étale site of S is given by a geometric point of S: its fibre functor is naturally isomorphic to the functor of lifts of that geometric point, which is the fibre functor of AlgebraicGeometry.geometricPointSitePoint.

public theorem exists_geometricPoint_fiber_iso
    (p : (SmallEtale.topology B S hS).Point.{u}) :
    ∃ s : GeometricPoint S, Nonempty (p.fiber ≅ geometricPointFiber B S hS s)

AlgebraicGeometry.exists_geometricPoint_inverseImage_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NeighborhoodsStalksPoints/SitePoints.lean, line 703. The attribute's comment: “part (2)”. References: SGA 4 VIII (7.9), “essential surjectivity”.

Stacks 04HU, part (2). Every point of the small étale topos of S has the geometric stalk functor of a geometric point of S as its inverse image: the stalk of a sheaf F at the point is the colimit of F over the category of étale neighbourhoods of that geometric point.

The point of the topos is first reconstructed as a point of the site (PointOfTopos.exists_sitePoint_fiber_eq, Stacks 00YA (2)); that point of the site is then a geometric point by AlgebraicGeometry.exists_geometricPoint_fiber_iso, part (1), and the canonical comparison identifies the two inverse images (PointOfTopos.isIso_sheafFiberComparison).

public theorem exists_geometricPoint_inverseImage_iso
    (p : PointOfTopos.{u + 1} (SmallEtale.topology B S hS)) :
    ∃ s : GeometricPoint S,
      Nonempty (p.inverseImage ≅
        sheafToPresheaf (SmallEtale.topology B S hS) (Type (u + 1)) ⋙
          (Functor.whiskeringLeft _ _ _).obj
            (Functor.Elements.π (geometricPointFiber B S hS s)).op ⋙
          colim)

Sources

• Section 59.29, Tag 03PN
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GeometricPoint · AlgebraicGeometry.GeometricPoint.LiesOver · AlgebraicGeometry.GeometricPoint.EtaleNeighborhood · AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.Hom · AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme · AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.toEtaleNeighborhood · AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.geometricPoint_liesOver_iff · AlgebraicGeometry.GeometricPoint.EtaleNeighborhood.toEtaleNeighborhood_surjective

Section59.30 Points in other topologies#

Section 59.30 of the Stacks Project, Tag 06VW. 1 tag here is carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06VX, a lemma

Tag 06VX in the Stacks Project.

AlgebraicGeometry.bigAffineEtale_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigAffineEtale.lean, line 46. The attribute's comment: “big_affine_etale”.

Stacks 06VX, big affine étale case. The big affine étale site over a scheme has enough points.

public theorem bigAffineEtale_hasConservativeFamily
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    GrothendieckTopology.HasConservativeFamily.{u + 1}
      (AlgebraicGeometry.BigAffineEtale.topology B S hS)

AlgebraicGeometry.bigAffineFppf_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigAffineFppf.lean, line 42. The attribute's comment: “big_affine_fppf”.

Stacks 06VX, big affine fppf case. The big affine fppf site over a scheme has enough points.

public theorem bigAffineFppf_hasConservativeFamily
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (AlgebraicGeometry.BigAffineFppf.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigAffineSmooth_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigAffineSmooth.lean, line 96. The attribute's comment: “big_affine_smooth”.

Stacks 06VX, big affine smooth case. The big affine smooth site over S has enough points.

public theorem bigAffineSmooth_hasConservativeFamily
    (B : AlgebraicGeometry.BigSmoothSite.{u}) (S : Scheme.{u})
    (hS : S.size < B.cutoff) :
    (AlgebraicGeometry.BigAffineSmooth.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigEtale_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigEtale.lean, line 42. The attribute's comment: “big_etale”.

Stacks 06VX, big étale case. The big étale site over a scheme has enough points.

public theorem bigEtale_hasConservativeFamily
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    GrothendieckTopology.HasConservativeFamily.{u + 1}
      (AlgebraicGeometry.BigEtaleOver.topology B S hS)

AlgebraicGeometry.bigFppf_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigFppf.lean, line 41. The attribute's comment: “big_fppf”.

Stacks 06VX, big fppf case. The big fppf site over a scheme has enough points.

public theorem bigFppf_hasConservativeFamily
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (AlgebraicGeometry.BigFppfOver.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigSmooth_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigSmooth.lean, line 42. The attribute's comment: “big_smooth”.

Stacks 06VX, big smooth case. The big smooth site over S has enough points.

public theorem bigSmooth_hasConservativeFamily
    (B : AlgebraicGeometry.BigSmoothSite.{u}) (S : Scheme.{u})
    (hS : S.size < B.cutoff) :
    (AlgebraicGeometry.BigSmoothOver.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigAffineSyntomic_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigSyntomic.lean, line 46. The attribute's comment: “big_affine_syntomic”.

Stacks 06VX, big affine syntomic case. The big affine syntomic site over a scheme has enough points.

public theorem bigAffineSyntomic_hasConservativeFamily
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (BigAffineSyntomic.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigSyntomic_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigSyntomic.lean, line 57. The attribute's comment: “big_syntomic”.

Stacks 06VX, big syntomic case. The big syntomic site over a scheme has enough points.

public theorem bigSyntomic_hasConservativeFamily
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (BigSyntomicOver.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigAffineZariski_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigZariski.lean, line 46. The attribute's comment: “big_affine_zariski”.

Stacks 06VX, big affine Zariski case. The big affine Zariski site over a scheme has enough points.

public theorem bigAffineZariski_hasConservativeFamily
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (BigAffineZariski.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.bigZariski_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/BigZariski.lean, line 57. The attribute's comment: “big_zariski”.

Stacks 06VX, big Zariski case. The big Zariski site over a scheme has enough points.

public theorem bigZariski_hasConservativeFamily
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (BigZariskiOver.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.smallAffineEtale_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/SmallAffineEtale.lean, line 193. The attribute's comment: “small_affine_etale”.

Stacks 06VX, small affine étale case. The small affine étale site of a scheme has enough points.

public theorem smallAffineEtale_hasConservativeFamily
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    GrothendieckTopology.HasConservativeFamily.{u}
      (AlgebraicGeometry.SmallAffineEtale.topology B S hS)

AlgebraicGeometry.SmallEtale.hasConservativeFamily, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/SmallEtale.lean, line 414. The attribute's comment: “small_etale”.

The small étale site of a scheme has enough points.

public lemma hasConservativeFamily (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    (AlgebraicGeometry.SmallEtale.topology B S hS).HasConservativeFamily.{u}

AlgebraicGeometry.smallAffineZariski_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/SmallZariski.lean, line 51. The attribute's comment: “small_affine_zariski”.

Stacks 06VX, small affine Zariski case. The small affine Zariski site of a scheme has enough points.

public theorem smallAffineZariski_hasConservativeFamily
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (SmallAffineZariski.topology B S hS).HasConservativeFamily.{u + 1}

AlgebraicGeometry.smallZariski_hasConservativeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/SmallZariski.lean, line 62. The attribute's comment: “small_zariski”.

Stacks 06VX, small Zariski case. The small Zariski site of a scheme has enough points.

public theorem smallZariski_hasConservativeFamily
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (SmallZariski.topology B S hS).HasConservativeFamily.{u + 1}

Sources

• Section 59.30, Tag 06VW
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.bigAffineEtale_hasConservativeFamily · AlgebraicGeometry.bigAffineFppf_hasConservativeFamily · AlgebraicGeometry.bigAffineSmooth_hasConservativeFamily · AlgebraicGeometry.bigEtale_hasConservativeFamily · AlgebraicGeometry.bigFppf_hasConservativeFamily · AlgebraicGeometry.bigSmooth_hasConservativeFamily · AlgebraicGeometry.bigAffineSyntomic_hasConservativeFamily · AlgebraicGeometry.bigSyntomic_hasConservativeFamily

Section59.31 Supports of abelian sheaves#

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

Tag 04HV, a lemma

Tag 04HV in the Stacks Project.

AlgebraicGeometry.existsUnique_open_of_isSubterminal_topos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/ExistenceClause.lean, line 465. The attribute's comment: “the case of a subterminal object of the topos of AlgebraicGeometry.smallEtaleRingedSite, whose sections are of Type u; this is AlgebraicGeometry.existsUnique_open_of_isSubterminal, which carries the tag in its own generality Type (max u v), instantiated at v := u with no transport in between”.

Stacks 04HV for a subterminal object of the topos of the small étale ringed site. A subsheaf of the final object of (Sh(S_étale), 𝒪_S) is represented by exactly one open subscheme of S.

This is AlgebraicGeometry.existsUnique_open_of_isSubterminal with its free sections universe instantiated at the universe u of the sections of AlgebraicGeometry.smallEtaleRingedSite, a RingedSite.{u + 1, u, u}. Nothing is transported: CategoryTheory.IsSubterminal is a condition in the sheaf category and the representability conclusion is about the same sheaf, and the two sides are the same category, because AlgebraicGeometry.RingedTopos.Topos of that ringed site is CategoryTheory.Sheaf (SmallEtale.topology B S hS) (Type u).

theorem existsUnique_open_of_isSubterminal_topos (X : B.Scheme)
    (F : (RingedSite.toRingedTopos (smallEtaleRingedSite B X.obj X.property)).Topos)
    (hF : IsSubterminal F) :
    ∃! W : X.obj.Opens,
      Nonempty (F ≅
        (presheafToSheaf (SmallEtale.topology B X.obj X.property) (Type u)).obj
          ((SmallEtale.inclusion B X.obj X.property ⋙
            Over.post (X := B.obj X.obj X.property) B.inclusion).op ⋙
            uliftYoneda.{u}.obj (Over.mk W.ι)))

AlgebraicGeometry.existsUnique_open_of_isSubterminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SubterminalSheaves.lean, line 722.

A subterminal sheaf on the small étale site is represented by a unique open subscheme of the base.

public theorem existsUnique_open_of_isSubterminal
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : smallEtaleTopos.{u, max (u + 1) v} B S hS)
    (hF : IsSubterminal F) :
    ∃! W : S.Opens,
      Nonempty (F ≅
        (presheafToSheaf (SmallEtale.topology B S hS)
          (Type (max (u + 1) v))).obj
          ((SmallEtale.inclusion B S hS ⋙
            Over.post (X := B.obj S hS) B.inclusion).op ⋙
            uliftYoneda.{max (u + 1) v}.obj (Over.mk W.ι)))

Tag 04FR, a lemma

Tag 04FR in the Stacks Project.

AlgebraicGeometry.SmallEtale.etaleGerm_eq_zero_iff_mem_zeroOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteSupportStalkVanishing.lean, line 89. The attribute's comment: “part (3): a germ vanishes exactly when the lift lands in the zero locus”.

Stacks 04FR, part (3). A germ vanishes exactly when the lift lands in the maximal open zero locus of the section.

A geometric point ū of the object W of the small étale site is a lift q to W of a geometric point t of S, the relation t = (W → S) ∘ ū of the source being the defining condition on a lift; so quantifying over t and over q is quantifying over the geometric points of W. The germ etaleGerm … t F.obj W q a is the source's class of (U, ū, σ) in F_s̄, and zeroOpen … W a is the source's W, so this is the asserted equivalence (U, ū, σ) = 0 in F_s̄ ↔ ū ∈ W.

The coefficient universe v is free, which is more general than the source; UnivLE.{u, v} and the existence of the colimit are what that extra generality costs, and both are automatic instances at v = u, so at the source's generality the statement carries no hypothesis. They are size conditions for the stalk to be formed at all, not mathematical hypotheses: etaleGerm is a colimit injection and does not typecheck without the colimit.

public theorem etaleGerm_eq_zero_iff_mem_zeroOpen (W : SmallEtale B S hS)
    (q : (geometricPointFiber B S hS t).obj W) (a : F.obj.obj (op W)) :
    etaleGerm B S hS t F.obj W q a = 0 ↔
      q.1.base default ∈
        (zeroOpen B S hS F W a : Set ((SmallEtale.toScheme B S hS).obj W))

AlgebraicGeometry.SmallEtale.map_eq_zero_iff_range_subset_zeroOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 552. The attribute's comment: “part (2): vanishing over the image”. References: SGA 2 XIV (1.8.2.1), “abelian, image criterion”.

A section pulls back to zero along an arbitrary arrow of the small étale site precisely when the image of that arrow is contained in its maximal Zariski open zero locus.

public theorem map_eq_zero_iff_range_subset_zeroOpen
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (σ : F.obj.obj (op U))
    (V : SmallEtale B S hS) (f : V ⟶ U) :
    F.obj.map f.op σ = 0 ↔
      Set.range ((SmallEtale.toScheme B S hS).map f).base ⊆
        (zeroOpen B S hS F U σ : Set ((SmallEtale.toScheme B S hS).obj U))

Declarations registered for the tag:

• AlgebraicGeometry.SmallEtale.zeroOpen, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 395 (StacksFrontier): “part (1): maximal open zero locus”.
• AlgebraicGeometry.SmallEtale.map_eq_zero_iff_le_zeroOpen, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 397 (StacksFrontier): “part (1): vanishing and maximality on Zariski opens”.

Tag 04FS, a definition

Tag 04FS in the Stacks Project.

AlgebraicGeometry.SmallEtale.supportSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 196. The attribute's comment: “support of a section”. References: SGA 4 VIII (6.6), “support of a section”.

The support of a section of an abelian sheaf on the small étale site is the complement of its maximal Zariski open zero locus.

public def supportSection (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (s : F.obj.obj (op U)) :
    Set ((SmallEtale.toScheme B S hS).obj U)

AlgebraicGeometry.SmallEtale.map_eq_zero_iff_le_zeroOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 272. The attribute's comment: “support of a section”. References: SGA 2 XIV (1.8.2.1), “abelian, s'=0”.

Along an open immersion of the small étale site, a section restricts to zero precisely when the image is contained in the maximal zero open.

public theorem map_eq_zero_iff_le_zeroOpen
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (s : F.obj.obj (op U))
    (V : SmallEtale B S hS) (f : V ⟶ U)
    [IsOpenImmersion ((SmallEtale.toScheme B S hS).map f)] :
    F.obj.map f.op s = 0 ↔
      ((SmallEtale.toScheme B S hS).map f).opensRange ≤ zeroOpen B S hS F U s

AlgebraicGeometry.supportSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportSection.lean, line 136. The attribute's comment: “support_section”.

The support of a section is the complement of its maximal Zariski open zero locus.

public def supportSection (B : BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (s : F.obj.obj (op U)) :
    Set ((SmallEtale.toScheme B S hS).obj U)

AlgebraicGeometry.zero_restrict_iff_image_le_zeroOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportSection.lean, line 146. The attribute's comment: “support_section”.

On an open immersion, the section vanishes precisely when the image is contained in the maximal zero open.

public theorem zero_restrict_iff_image_le_zeroOpen (B : BigEtaleSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S)
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (s : F.obj.obj (op U))
    (V : SmallEtale B S hS) (f : V ⟶ U)
    [IsOpenImmersion ((SmallEtale.toScheme B S hS).map f)] :
    F.obj.map f.op s = 0 ↔
  ((SmallEtale.toScheme B S hS).map f).opensRange ≤ zeroOpen B S hS F U s

AlgebraicGeometry.supportSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportSheaf.lean, line 76. The attribute's comment: “support_sheaf”.

The points of a scheme at which a geometric stalk of an abelian étale sheaf is nonzero.

public def supportSheaf : Set S

AlgebraicGeometry.mem_supportSheaf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportSheaf.lean, line 133. The attribute's comment: “support_sheaf”. References: SGA 4 VIII (6.6), “support of a sheaf”.

Nonvanishing of a stalk is independent of the geometric point above x.

public theorem mem_supportSheaf_iff (p : GeometricPoint S) (x : S)
    (hp : GeometricPoint.LiesOver p x) :
    x ∈ supportSheaf B S hS F ↔
      ¬ IsZero (etaleStalk B S hS p
        (F.obj ⋙ AddCommGrpCat.uliftFunctor.{u, v}))

Tag 04FT, a lemma

Tag 04FT in the Stacks Project.

AlgebraicGeometry.SmallEtale.isClosed_supportSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 621. The attribute's comment: “the support of a section is closed”.

The support of a section of an abelian étale sheaf is closed.

public theorem isClosed_supportSection
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (s : F.obj.obj (op U)) :
    IsClosed (supportSection B S hS F U s)

AlgebraicGeometry.SmallEtale.supportSection_add_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 629. The attribute's comment: “the support of a sum of sections”.

The support of a sum of sections is contained in the union of their supports.

public theorem supportSection_add_subset
    (F : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (U : SmallEtale B S hS) (s s' : F.obj.obj (op U)) :
    supportSection B S hS F U (s + s') ⊆
      supportSection B S hS F U s ∪ supportSection B S hS F U s'

AlgebraicGeometry.SmallEtale.supportSection_map_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSections.lean, line 659. The attribute's comment: “the support under a morphism of sheaves”.

A morphism of abelian sheaves cannot enlarge the support of a section.

public theorem supportSection_map_subset
    (F G : Sheaf (SmallEtale.topology B S hS) AddCommGrpCat.{v})
    (φ : F ⟶ G) (U : SmallEtale B S hS) (s : F.obj.obj (op U)) :
    supportSection B S hS G U (φ.hom.app (op U) s) ⊆ supportSection B S hS F U s

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

Stacks 04FT, part (4). The support of an abelian sheaf on the small étale site is the union, over all objects of the site and all sections of the sheaf over them, of the images in the base scheme of the supports of those sections.

public theorem supportSheaf_eq_iUnion_image_supportSection :
    AlgebraicGeometry.supportSheaf B S hS F =
      ⋃ (U : SmallEtale B S hS), ⋃ (a : F.obj.obj (op U)),
        (B.inclusion.map U.obj.hom).base '' supportSection B S hS F U a

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

Stacks 04FT, part (5). If a map of abelian sheaves on the small étale site is surjective, that is locally surjective, then the support of its target is contained in the support of its source.

public theorem supportSheaf_subset_of_isLocallySurjective (φ : F ⟶ G)
    [Sheaf.IsLocallySurjective φ] :
    AlgebraicGeometry.supportSheaf B S hS G ⊆ AlgebraicGeometry.supportSheaf B S hS F

AlgebraicGeometry.supportSheaf_subset_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSheafSections.lean, line 192. The attribute's comment: “part (6)”.

Stacks 04FT, part (6). If a map of abelian sheaves on the small étale site is injective, then the support of its source is contained in the support of its target.

public theorem supportSheaf_subset_of_injective (φ : F ⟶ G)
    (hφ : ∀ U, Function.Injective (φ.hom.app U)) :
    AlgebraicGeometry.supportSheaf B S hS F ⊆ AlgebraicGeometry.supportSheaf B S hS G

AlgebraicGeometry.isClosed_supportSection_and_supportSheaf_eq_iUnion_image_supportSection_and_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSheafSections.lean, line 247.

Stacks Project, Tag 04FT. Let S be a scheme, let F be an abelian sheaf on the small étale site of S, let U be an object of that site and let σ ∈ F(U). Then

1. the support of σ is closed in U;
2. the support of σ + σ' is contained in the union of the supports of σ and σ', for every σ' ∈ F(U);
3. for every map φ : F ⟶ G of abelian sheaves on the site, the support of φ(σ) is contained in the support of σ;
4. the support of F is the union of the images in S of the supports of all local sections of F;
5. if φ : F ⟶ G is surjective then the support of G is contained in the support of F;
6. if φ : F ⟶ G is injective then the support of F is contained in the support of G,

the support of a section being AlgebraicGeometry.SmallEtale.supportSection of Stacks 04FS and the support of a sheaf being AlgebraicGeometry.supportSheaf.

This is the whole tag in one statement, under exactly the source's hypotheses: nothing beyond the site, the sheaf, the object and the section is assumed, and the further sheaf G and map φ of parts (3), (5) and (6) are quantified where the source introduces them. Surjectivity in part (5) is local surjectivity, CategoryTheory.Sheaf.IsLocallySurjective, which is what makes a map of abelian sheaves an epimorphism; injectivity in part (6) is injectivity on every group of sections. Each part is proved by the theorem of this chapter that states it alone: AlgebraicGeometry.SmallEtale.isClosed_supportSection, AlgebraicGeometry.SmallEtale.supportSection_add_subset and AlgebraicGeometry.SmallEtale.supportSection_map_subset, in StacksFrontier.AlgebraicGeometry.Etale.SupportSections, for parts (1), (2) and (3); and AlgebraicGeometry.supportSheaf_eq_iUnion_image_supportSection, AlgebraicGeometry.supportSheaf_subset_of_isLocallySurjective and AlgebraicGeometry.supportSheaf_subset_of_injective, above, for parts (4), (5) and (6). Those six registrations are retained, each stating its own part of the tag.

public theorem isClosed_supportSection_and_supportSheaf_eq_iUnion_image_supportSection_and_subset
    (U : SmallEtale B S hS) (σ : F.obj.obj (op U)) :
    IsClosed (supportSection B S hS F U σ) ∧
      (∀ σ' : F.obj.obj (op U), supportSection B S hS F U (σ + σ') ⊆
        supportSection B S hS F U σ ∪ supportSection B S hS F U σ') ∧
      (∀ φ : F ⟶ G, supportSection B S hS G U (φ.hom.app (op U) σ) ⊆
        supportSection B S hS F U σ) ∧
      (AlgebraicGeometry.supportSheaf B S hS F =
        ⋃ (V : SmallEtale B S hS), ⋃ (a : F.obj.obj (op V)),
          (B.inclusion.map V.obj.hom).base '' supportSection B S hS F V a) ∧
      (∀ φ : F ⟶ G, Sheaf.IsLocallySurjective φ →
        AlgebraicGeometry.supportSheaf B S hS G ⊆ AlgebraicGeometry.supportSheaf B S hS F) ∧
      (∀ φ : F ⟶ G, (∀ V, Function.Injective (φ.hom.app V)) →
        AlgebraicGeometry.supportSheaf B S hS F ⊆ AlgebraicGeometry.supportSheaf B S hS G)

Tag 04FU, a lemma

Tag 04FU in the Stacks Project.

AlgebraicGeometry.SmallEtale.isClosed_supportSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/SupportSheaf.lean, line 165.

Stacks 04FU. The support of a sheaf of rings on the small étale site is closed: a ring is zero exactly when its unit is zero, so the support of a sheaf of rings is the support of its unit section, which is closed.

public theorem isClosed_supportSheaf :
    IsClosed (supportSheaf B S hS (toAddCommGrp B S hS F))

Sources

• Section 59.31, Tag 04FQ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.existsUnique_open_of_isSubterminal_topos · AlgebraicGeometry.existsUnique_open_of_isSubterminal · AlgebraicGeometry.SmallEtale.etaleGerm_eq_zero_iff_mem_zeroOpen · AlgebraicGeometry.SmallEtale.map_eq_zero_iff_range_subset_zeroOpen · AlgebraicGeometry.SmallEtale.zeroOpen · AlgebraicGeometry.SmallEtale.map_eq_zero_iff_le_zeroOpen · AlgebraicGeometry.SmallEtale.supportSection · AlgebraicGeometry.supportSection

Section59.32 Henselian rings#

Section 59.32 of the Stacks Project, Tag 03QD. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03QE, a theorem

Tag 03QE in the Stacks Project.

Algebra.exists_etale_finite_factors_positiveDim_remainder, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalStructureFibreDimension.lean, line 184. References: EGA IV (18.12.1), “affine case”.

After an étale base change preserving the residue field at p, a finite type algebra splits into finitely many finite factors, each with exactly one prime over p', and a factor whose fibre has no zero-dimensional irreducible component.

theorem exists_etale_finite_factors_positiveDim_remainder
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] (p : Ideal R) [p.IsPrime] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
      (p' : Ideal R') (_ : p'.IsPrime) (_ : p'.LiesOver p)
      (n : ℕ) (e : Fin (n + 1) → R' ⊗[R] S)
      (_ : CompleteOrthogonalIdempotents e)
      (r : Fin n → Ideal (R' ⊗[R] S))
      (_ : ∀ i, (r i).IsPrime) (_ : ∀ i, (r i).LiesOver p'),
      Function.Bijective (Ideal.ResidueField.mapₐ p p' (Algebra.ofId _ _) (p'.over_def p)) ∧
      (∀ i : Fin n, Module.Finite R' (Localization.Away (e i.castSucc))) ∧
      (∀ i : Fin n, e i.castSucc ∉ r i) ∧
      (∀ (i : Fin n) (q : Ideal (R' ⊗[R] S)), q.IsPrime → q.LiesOver p' →
        e i.castSucc ∉ q → q = r i) ∧
      (∀ Z ∈ irreducibleComponents
          (PrimeSpectrum (p'.Fiber (Localization.Away (e (Fin.last n))))),
        1 ≤ topologicalKrullDim Z)

Tag 03QF, a definition

Tag 03QF in the Stacks Project.

Declarations registered for the tag:

• HenselianLocalRing registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch59.lean, line 322 (StacksFrontier). References: EGA IV (18.5.8), “special case”; SGA 4 VIII (4.1); SGA 4 XII (6.13), “special case”.
• HenselianLocalRing.TFAE registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch59.lean, line 323 (StacksFrontier): “Stacks' formulation, with a₀ in the residue field (item 2)”.

Tag 03QG, a theorem

Tag 03QG in the Stacks Project.

Declarations registered for the tag:

• IsAdicComplete.henselianRing registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch59.lean, line 327 (StacksFrontier): “for I = maximalIdeal R, HenselianRing R (maximalIdeal R) is the condition of 03QF”. References: EGA IV (18.5.14), “more general”; EGA IV (18.5.16), “more general”; SGA 3 X (4.0), “Recall 4.0”.

Tag 03QH, a theorem

Tag 03QH in the Stacks Project.

IsLocalRing.henselian_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Characterizations.lean, line 318. References: EGA IV (18.5.13), “a'') existence half”; EGA IV (18.5.9), “(ii)”; EGA IV (18.5.11), “a), a'), b)”; SGA 4 VIII (4.1), “(i), (iii), (iv)”; SGA 3 X (4.5), “special case”; SGA 7 IX (2.2.3), “(4), special case”.

Stacks 03QH. The five standard characterizations of a henselian local ring: henselianness, coprime factorization lifting, decomposition of module-finite algebras, splitting the finite part of finite type algebras, and splitting pointed étale algebras.

theorem henselian_tfae (R : Type u) [CommRing R] [IsLocalRing R] :
    List.TFAE [HenselianLocalRing R,
      HasCoprimeFactorizationLifting R,
      FiniteAlgebrasSplitIntoLocalFactors.{u, v} R,
      FiniteTypeAlgebrasSplitOffFiniteLocalFactors.{u, v} R,
      PointedEtaleAlgebrasSplit.{u, v} R]

Tag 03QJ, a lemma

Tag 03QJ in the Stacks Project.

exists_algEquiv_pi_henselianLocalRing_of_module_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/FiniteAlgebras.lean, line 44. References: EGA IV (18.5.10), “R henselian local”; EGA IV (18.5.9), “(ii) necessity”; EGA IV (18.5.11), “(F), partial”; EGA IV (18.6.7), “special case”; SGA 4 VIII (4.1), “(i), forward direction”.

A finite algebra over a henselian local ring is a finite product of henselian local rings, each finite over the base.

theorem exists_algEquiv_pi_henselianLocalRing_of_module_finite
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    (A : Type v) [CommRing A] [Algebra R A] [Module.Finite R A] :
    ∃ (ι : Type v) (_ : Finite ι) (B : ι → Type v)
      (_ : ∀ i, CommRing (B i)) (_ : ∀ i, Algebra R (B i))
      (_ : ∀ i, HenselianLocalRing (B i)),
      (∀ i, Module.Finite R (B i)) ∧ Nonempty (A ≃ₐ[R] ∀ i, B i)

Tag 03QK, a definition

Tag 03QK in the Stacks Project.

StrictlyHenselianLocalRing, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CompleteLocal/StrictlyHenselian.lean, line 35. References: SGA 7 XIII (0.2), “(0.2.3) ring case”; SGA 4 VIII (4.2), “(i)”; SGA 7 I (0.0.2), “ring case”.

A commutative ring is strictly henselian if it is a henselian local ring and its residue field is separably closed.

class StrictlyHenselianLocalRing (R : Type*) [CommRing R] : Prop extends
  HenselianLocalRing R, IsSepClosed (IsLocalRing.ResidueField R)

Tag 03QI, an example

Tag 03QI in the Stacks Project.

Stacks.EtaleCohomology.exists_algEquiv_pi_puncturedKummerAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComplexPowerSeries.lean, line 390. The attribute's comment: “classification of étale algebras”.

Every étale algebra over ℂ⟦t⟧ is a finite product of trivial factors and punctured Kummer extensions of positive degree.

theorem exists_algEquiv_pi_puncturedKummerAlgebra
    (A : Type*) [CommRing A] [Algebra (PowerSeries ℂ) A]
    [Algebra.Etale (PowerSeries ℂ) A] :
    ∃ (ι κ : Type*) (_ : Finite ι) (_ : Finite κ) (n : κ → ℕ),
      (∀ j, 0 < n j) ∧
      Nonempty (A ≃ₐ[PowerSeries ℂ]
        (ι → PowerSeries ℂ) × (∀ j, puncturedKummerAlgebra (n j)))

Stacks.EtaleCohomology.etale_puncturedKummerAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComplexPowerSeries.lean, line 436. The attribute's comment: “étaleness of the Kummer extensions”.

A punctured Kummer extension of positive degree is étale over ℂ⟦t⟧.

theorem etale_puncturedKummerAlgebra (n : ℕ) (hn : 0 < n) :
    Algebra.Etale (PowerSeries ℂ) (puncturedKummerAlgebra n)

Stacks.EtaleCohomology.isUnit_parameter_puncturedKummerAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComplexPowerSeries.lean, line 468. The attribute's comment: “factorization through the punctured spectrum”.

The parameter is invertible on a punctured Kummer extension, so its spectrum maps into D(t).

theorem isUnit_parameter_puncturedKummerAlgebra (n : ℕ) :
    IsUnit (algebraMap (PowerSeries ℂ) (puncturedKummerAlgebra n) PowerSeries.X)

Stacks.EtaleCohomology.etaleCover_has_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComplexPowerSeries.lean, line 487. The attribute's comment: “refinement by the identity cover”.

An étale covering of Spec ℂ⟦t⟧ has a member whose structure morphism admits a section, so the identity cover refines it.

theorem etaleCover_has_section
    (𝒰 : (Spec (.of (PowerSeries ℂ))).Cover Scheme.etalePrecoverage) :
    ∃ i : 𝒰.I₀, ∃ s : Spec (.of (PowerSeries ℂ)) ⟶ 𝒰.X i,
      s ≫ 𝒰.f i = 𝟙 (Spec (.of (PowerSeries ℂ)))

Tag 03QL, a theorem

Tag 03QL in the Stacks Project.

IsLocalRing.henselizationTower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/HenselizationTower.lean, line 195. The attribute's comment: “existence, flat local maps, and parts (1), (2), and (4)”.

The canonical henselization/strict-henselization tower associated to a local ring and a chosen separable closure of its residue field.

public noncomputable def henselizationTower (R : Type u) [CommRing R] [IsLocalRing R]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep] : HenselizationTower R κsep

HenselianLocalRing.existsUnique_isLocalHom_of_ind_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Canonicity.lean, line 57. The attribute's comment: “canonicity of the map from the henselization”. References: EGA IV (18.6.6), “(ii)”; SGA 4 VIII (4.1), “partial”.

The universal property of the henselization, in existential form (Stacks 04GS). Let (R, 𝔪, κ) be a local ring, let Rh be a local R-algebra with R → Rh local which is a filtered colimit of étale R-algebras and has residue field κ, and let Sh be a henselian local ring with R → Sh local. Then there is exactly one R-algebra map Rh → Sh that is a local ring map. This is what makes the maps R → R^h → R^{sh} of Tag 03QL canonical: applied to Rh = R^h and Sh = R^{sh} it pins the map out of the henselization uniquely.

public theorem HenselianLocalRing.existsUnique_isLocalHom_of_ind_etale
    {R : Type u} {Rh : Type v} {Sh : Type w} [CommRing R] [CommRing Rh] [CommRing Sh]
    [IsLocalRing R]
    [IsLocalRing Rh] [HenselianLocalRing Sh] [Algebra R Rh] [Algebra R Sh]
    [IsLocalHom (algebraMap R Rh)] [IsLocalHom (algebraMap R Sh)]
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rh)))
    (hres : Function.Surjective (ResidueField.map (algebraMap R Rh))) :
    ∃! f : Rh →ₐ[R] Sh, IsLocalHom f

Declarations registered for the tag:

• IsLocalRing.IsHenselization.map_maximalIdeal, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/HenselizationTower.lean, line 282 (StacksFrontier): “part (3): maximal ideals”.

Sources

• Section 59.32, Tag 03QD
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.exists_etale_finite_factors_positiveDim_remainder · HenselianLocalRing · HenselianLocalRing.TFAE · IsAdicComplete.henselianRing · IsLocalRing.henselian_tfae · exists_algEquiv_pi_henselianLocalRing_of_module_finite · StrictlyHenselianLocalRing · Stacks.EtaleCohomology.exists_algEquiv_pi_puncturedKummerAlgebra

Section59.33 Stalks of the structure sheaf#

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

Tag 04HX, a lemma

Tag 04HX in the Stacks Project.

AlgebraicGeometry.structureSheafStalkFromLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/EtaleLocalRing.lean, line 197. The attribute's comment: “the ordinary-to-étale germ map”.

The canonical map from the ordinary local ring to the stalk of the ring-valued étale structure sheaf.

public noncomputable def structureSheafStalkFromLocalRing
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S) :
    S.presheaf.stalk (s.hom (closedPoint s.residueField)) →+*
      ↥(etaleStalk B S hS s
        (SmallEtale.structureSheaf B S hS).obj)

AlgebraicGeometry.structureSheafStalkToGeometricField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/EtaleLocalRing.lean, line 265. The attribute's comment: “the geometric evaluation map”.

Evaluation of a structure-sheaf stalk germ in the geometric residue field.

public noncomputable def structureSheafStalkToGeometricField
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S) :
    ↥(etaleStalk B S hS s
      (SmallEtale.structureSheaf B S hS).obj) →+* s.residueField

AlgebraicGeometry.structureSheafStalkFromLocalRing_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/EtaleLocalRing.lean, line 585. The attribute's comment: “compatibility with ordinary germs”.

The canonical ordinary-to-étale germ map is characterized at every étale neighborhood by ordinary restriction of sections.

public theorem structureSheafStalkFromLocalRing_germ
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S)
    (U : (geometricPointFiber B S hS s).Elementsᵒᵖ)
    (r : S.presheaf.stalk (s.hom (closedPoint s.residueField)))
    (a : Γ((SmallEtale.toScheme B S hS).obj U.unop.1, ⊤)) :
    let f : ((SmallEtale.toScheme B S hS).obj U.unop.1) ⟶ S :=
      B.inclusion.map U.unop.1.obj.hom
    let p := U.unop.2.1
    let x := p (closedPoint s.residueField)
    let h : f x = s.hom (closedPoint s.residueField) :=
      (Scheme.Hom.comp_apply p f (closedPoint s.residueField)).symm.trans
        (congrArg (fun q : s.source ⟶ S => q (closedPoint s.residueField)) U.unop.2.2)
    (f.stalkMap x).hom (h.symm ▸ r) =
        ((SmallEtale.toScheme B S hS).obj U.unop.1).presheaf.germ
          ⊤ x trivial a →
      structureSheafStalkFromLocalRing B S hS s r = (colimit.ι
        ((Functor.Elements.π (geometricPointFiber B S hS s)).op ⋙
          (SmallEtale.structureSheaf B S hS).obj) U).hom a

AlgebraicGeometry.structureSheafStalkToGeometricField_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/EtaleLocalRing.lean, line 654. The attribute's comment: “geometric evaluation of germs”.

Evaluation of a germ of the structure sheaf is its value at the chosen geometric lift on every étale neighborhood.

public theorem structureSheafStalkToGeometricField_ι
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S)
    (U : (geometricPointFiber B S hS s).Elementsᵒᵖ) :
    (structureSheafStalkToGeometricField B S hS s).comp ((colimit.ι
      ((Functor.Elements.π (geometricPointFiber B S hS s)).op ⋙
        (SmallEtale.structureSheaf B S hS).obj) U).hom) =
      ((U.unop.2.1).appTop ≫ (Scheme.ΓSpecIso (.of s.residueField)).hom).hom

AlgebraicGeometry.etaleLocalRing_strictHenselization_canonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/EtaleLocalRing.lean, line 982. The attribute's comment: “the strict-henselization identification”.

The étale stalk is canonically the strict henselization of the ordinary local ring, with its residue field identified with the separable subextension of the geometric point's field.

public noncomputable def etaleLocalRing_strictHenselization_canonical
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S)
    (T : IsLocalRing.HenselizationTower
        (S.presheaf.stalk (s.hom (closedPoint s.residueField)))
        (separableClosure (ResidueField
          (S.presheaf.stalk (s.hom (closedPoint s.residueField))))
          s.residueField)) :
    { e : T.strictHenselization ≃+*
        ↥(etaleStalk B S hS s
          (SmallEtale.structureSheaf B S hS).obj) //
      (∀ r, e (algebraMap
        (S.presheaf.stalk (s.hom (closedPoint s.residueField)))
        T.strictHenselization r) = structureSheafStalkFromLocalRing B S hS s r) ∧
      (∀ a, structureSheafStalkToGeometricField B S hS s (e a) =
        ((T.strictHenselizationResidueEquiv.symm
          (residue T.strictHenselization a) :
            separableClosure (ResidueField
              (S.presheaf.stalk (s.hom (closedPoint s.residueField))))
              s.residueField) : s.residueField)) }

AlgebraicGeometry.etaleLocalRing_strictHenselization_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/EtaleLocalRing.lean, line 1058. The attribute's comment: “uniqueness of the canonical identification”.

The comparison is uniquely determined by the map from the ordinary local ring and by the inclusion of the relative separable closure in the geometric point's field.

public theorem etaleLocalRing_strictHenselization_unique
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S)
    (T : IsLocalRing.HenselizationTower
      (S.presheaf.stalk (s.hom (closedPoint s.residueField)))
      (separableClosure (ResidueField
        (S.presheaf.stalk (s.hom (closedPoint s.residueField)))) s.residueField))
    (e : T.strictHenselization ≃+*
      ↥(etaleStalk B S hS s
        (SmallEtale.structureSheaf B S hS).obj))
    (hbase : ∀ r, e (algebraMap
      (S.presheaf.stalk (s.hom (closedPoint s.residueField)))
      T.strictHenselization r) = structureSheafStalkFromLocalRing B S hS s r)
    (hres : ∀ a, structureSheafStalkToGeometricField B S hS s (e a) =
      ((T.strictHenselizationResidueEquiv.symm
        (residue T.strictHenselization a) :
          separableClosure (ResidueField
            (S.presheaf.stalk (s.hom (closedPoint s.residueField))))
            s.residueField) : s.residueField)) :
    e = (etaleLocalRing_strictHenselization_canonical B S hS s T).val

AlgebraicGeometry.isConstant_smallEtalePullbackAb_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocalAcyclicity/StrictHenselizationLocallyConstant.lean, line 150. The attribute's comment: “a locally constant abelian étale sheaf becomes constant on the strict henselization, because every étale covering of a strictly henselian local scheme splits”.

A locally constant abelian étale sheaf has constant inverse image on the strict henselization. The inverse image is locally constant by Tag 093R, and over the spectrum of the strictly henselian local ring 𝒪^{sh}_{X,x} a locally constant sheaf is constant, because the canonical geometric point there has the final object of the small étale site as an initial étale neighbourhood.

theorem isConstant_smallEtalePullbackAb_strictHenselization
    (G : Sheaf (smallEtaleTopology X) Ab.{u + 1})
    (hG : Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology X) G) :
    Sheaf.IsConstant (smallEtaleTopology (strictHenselization B X hX x))
      ((smallEtalePullbackAb (strictHenselizationToBase B X hX x)).obj G)

AlgebraicGeometry.Space.geometricEval, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricEvaluation.lean, line 98. The attribute's comment: “the geometric evaluation map, for an algebraic space”.

Evaluation of germs at a geometric point. The homomorphism from the étale local ring of F at x̄ to the field of x̄ sending the germ of a regular function on a small étale neighbourhood to its value at the chosen lift of x̄.

def geometricEval (x : GeometricPoint B S hS F) :
    ↥(etaleLocalRing B S hS F x) →+* x.val.carrier

Tag 03PS, a definition

Tag 03PS in the Stacks Project.

AlgebraicGeometry.etaleLocalRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SchemeLocalRings.lean, line 62. The attribute's comment: “part (1)”. References: SGA 7 I (0.0.4), “strict henselization”; SGA 4 VIII (4.3), “strictly local ring”.

The étale local ring of S at a geometric point s: the stalk at s of the structure sheaf of the small étale site of S.

public abbrev etaleLocalRing (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (s : GeometricPoint S) : RingCat.{u}

AlgebraicGeometry.henselizationRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SchemeLocalRings.lean, line 74. The attribute's comment: “part (2)”.

The henselization of the local ring of S at a point x.

public abbrev henselizationRing (S : Scheme.{u}) (x : S) : Type u

AlgebraicGeometry.henselization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SchemeLocalRings.lean, line 95. The attribute's comment: “part (4)”.

The henselization of a scheme at an ordinary point: the spectrum of the henselization of its local ring.

public abbrev henselization (S : Scheme.{u}) (x : S) : Scheme.{u}

AlgebraicGeometry.strictHenselization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/StrictHenselization.lean, line 166. The attribute's comment: “part (3)”. References: SGA 2 XIV (1.1); SGA 4 VIII (4.3); SGA 4 VIII (7.1), “partial”; SGA 4½ Arcata (2.3.3), “Ỹ = Spec(O_{Y”; SGA 4½ Arcata (5.1.1); SGA 4½ Th finitude (2.11); SGA 7 I (0.0.4); SGA 7 XIII (2.1.3), “The scheme X_(x̄)”; SGA 7 XVI (1.6), “S_(s̄) only”.

The strict henselization of a scheme at a geometric point: the spectrum of the étale local ring there.

public abbrev strictHenselization : Scheme.{u}

Tag 04HY, a lemma

Tag 04HY in the Stacks Project.

AlgebraicGeometry.instIsFilteredOppositeElementaryEtaleNeighborhood, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Henselization.lean, line 1253. The attribute's comment: “the henselization is the colimit of O(U) over the étale neighbourhoods with κ(s)”. References: EGA IV (18.6.3), “more general”.

Stacks Project, Tag 05KS. The opposite of the category of elementary étale neighborhoods of a point is filtered.

instance instIsFilteredOppositeElementaryEtaleNeighborhood
    (S : Scheme.{u}) (s : S) :
    IsFiltered (ElementaryEtaleNeighborhood S s)ᵒᵖ

AlgebraicGeometry.isColimit_globalSections, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/Henselization.lean, line 1354. The attribute's comment: “the henselization is the colimit of O(U) over the étale neighbourhoods with κ(s)”.

Stacks Project, Tag 05KS. A henselization of the local ring of a scheme at a point is a colimit of the rings of global sections of its elementary étale neighborhoods.

lemma isColimit_globalSections (S : Scheme.{u}) (s : S)
    (Rh : Type u) [CommRing Rh] [IsLocalRing Rh]
    [Algebra (S.presheaf.stalk s) Rh]
    [IsLocalRing.IsHenselization (S.presheaf.stalk s)
      (IsLocalRing.ResidueField (S.presheaf.stalk s)) Rh] :
    ∃ ι : globalSections S s ⟶
        (Functor.const _).obj (CommRingCat.of Rh),
      (∀ U x, IsLocalRing.residue Rh ((ι.app U).hom x) =
        henselizationResidueFieldMap S s Rh
          (elementaryEtaleAugmentation S s U.unop x)) ∧
      (∀ U : (ElementaryEtaleNeighborhood S s)ᵒᵖ,
        IsOverStalk S s Rh U.unop (ι.app U).hom) ∧
      (∀ ι' : globalSections S s ⟶ (Functor.const _).obj (CommRingCat.of Rh),
        (∀ U x, IsLocalRing.residue Rh ((ι'.app U).hom x) =
          henselizationResidueFieldMap S s Rh
            (elementaryEtaleAugmentation S s U.unop x)) →
        (∀ U : (ElementaryEtaleNeighborhood S s)ᵒᵖ,
          IsOverStalk S s Rh U.unop (ι'.app U).hom) → ι' = ι) ∧
      Nonempty (IsColimit (Cocone.mk _ ι))

Tag 04HZ, a lemma

Tag 04HZ in the Stacks Project.

AlgebraicGeometry.smallEtaleRingedSite_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleRingedSite.lean, line 159.

The small étale site of a scheme, endowed with its structure sheaf, is a locally ringed site.

public theorem smallEtaleRingedSite_isLocallyRinged :
    RingedSite.IsLocallyRinged (smallEtaleRingedSite B S hS)

Sources

• Section 59.33, Tag 04HW
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.structureSheafStalkFromLocalRing · AlgebraicGeometry.structureSheafStalkToGeometricField · AlgebraicGeometry.structureSheafStalkFromLocalRing_germ · AlgebraicGeometry.structureSheafStalkToGeometricField_ι · AlgebraicGeometry.etaleLocalRing_strictHenselization_canonical · AlgebraicGeometry.etaleLocalRing_strictHenselization_unique · AlgebraicGeometry.isConstant_smallEtalePullbackAb_strictHenselization · AlgebraicGeometry.Space.geometricEval

Section59.34 Functoriality of small étale topos#

Section 59.34 of the Stacks Project, Tag 04I0. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04I1, an equation

Tag 04I1 in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GlobalSectionsClosed/InverseImage.lean, line 63.

Base change along f : X ⟶ Y, as a functor from the small étale site of Y to that of X: an étale scheme W over Y is sent to the fibre product W ×_Y X, which is étale over X because étale morphisms are stable under base change. This is the functor u : Y_étale → X_étale, V/Y ↦ X ×_Y V/X of Tag 04I1, with the fibre product written in the other order (see smallEtaleBaseChangeObjIso).

public def smallEtaleBaseChange {X Y : Scheme.{u}} (f : X ⟶ Y) : Y.Etale ⥤ X.Etale

Stacks.EtaleCohomology.smallEtaleBaseChangeObjIso_hom_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GlobalSectionsClosed/InverseImage.lean, line 82. The attribute's comment: “object formula”.

The object formula V/Y ↦ X ×_Y V/X for the base-change functor u : Y_étale → X_étale: under smallEtaleBaseChangeObjIso, the structure morphism of the base change of V to X is the first projection X ×_Y V ⟶ X.

public theorem smallEtaleBaseChangeObjIso_hom_fst {X Y : Scheme.{u}} (f : X ⟶ Y) (V : Y.Etale) :
    (smallEtaleBaseChangeObjIso f V).hom ≫ pullback.fst f V.hom =
      ((smallEtaleBaseChange f).obj V).hom

Sources

• Section 59.34, Tag 04I0
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.smallEtaleBaseChange · Stacks.EtaleCohomology.smallEtaleBaseChangeObjIso_hom_fst

Section59.35 Direct images#

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

Tag 03PW, a definition

Tag 03PW in the Stacks Project.

Stacks.EtaleCohomology.smallEtalePresheafPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/DirectImageSystem.lean, line 199.

The direct image f_*𝓕 of a presheaf of sets 𝓕 on the small étale site of X along f : X ⟶ Y: the presheaf on the small étale site of Y sending V/Y to 𝓕(V ×_Y X / X).

public def smallEtalePresheafPushforward {X Y : Scheme.{u}} (f : X ⟶ Y) :
    ((X.Etale)ᵒᵖ ⥤ Type w) ⥤ ((Y.Etale)ᵒᵖ ⥤ Type w)

Tag 03PX, a remark

Tag 03PX in the Stacks Project.

AlgebraicGeometry.smallEtaleBaseChange_isCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 205. The attribute's comment: “pullback of coverings”.

Pulling an étale covering family of S back along f : T ⟶ S yields an étale covering family of T.

public theorem smallEtaleBaseChange_isCovering {S T : B.Scheme} (f : T ⟶ S)
    (E : Covering (SmallEtale B S.obj S.property))
    (hE : SmallEtale.IsCovering B S.obj S.property E) :
    SmallEtale.IsCovering B T.obj T.property
      ⟨(smallEtaleBaseChange B f).obj E.1, E.2.map (smallEtaleBaseChange B f)⟩

AlgebraicGeometry.isSheafFor_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 218. The attribute's comment: “sheaf condition”.

The sheaf condition for a presheaf on the small étale category of T, tested against the base change of a covering family of S, agrees with the sheaf condition for its direct image tested against the original family.

public theorem isSheafFor_baseChange_iff {S T : B.Scheme} (f : T ⟶ S)
    (P : (SmallEtale B T.obj T.property)ᵒᵖ ⥤ Type v)
    (E : Covering (SmallEtale B S.obj S.property)) :
    Presieve.IsSheafFor ((smallEtaleBaseChange B f).op ⋙ P) E.2.presieve₀ ↔
      Presieve.IsSheafFor P (E.2.map (smallEtaleBaseChange B f)).presieve₀

Declarations registered for the tag:

• CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 227 (StacksFrontier): “direct image of a sheaf”.

Tag 03PY, a definition

Tag 03PY in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleDirectImage, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleDirectImages.lean, line 70. References: SGA 4½ Arcata (2.3), “f_* definition”; SGA 4 VII (1.4).

The direct image, or pushforward, f_* along f : X ⟶ Y on sheaves of sets of the small étale sites: the sheaf f_* F on Y_étale sends an étale Y-scheme V to F(V ×_Y X), that is, f_* is precomposition with base change along f.

abbrev smallEtaleDirectImage :
    Sheaf (smallEtaleTopology X) (Type (max (u + 1) v)) ⥤
      Sheaf (smallEtaleTopology Y) (Type (max (u + 1) v))

Tag 04I2, a definition

Tag 04I2 in the Stacks Project.

Stacks.EtaleCohomology.etaleAbelianHigherDirectImage, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleDirectImages.lean, line 90. References: SGA 4½ Arcata (2.3), “R^p f_* definition”; SGA 4½ Arcata (2.3.3), “higher direct images”.

The higher direct images R^p f_* along f : X ⟶ Y: the right derived functors of the direct image f_* : Ab(X_étale) ⥤ Ab(Y_étale) on abelian sheaves of the small étale sites. The family with p ≥ 1 is what the source calls the higher direct images.

abbrev etaleAbelianHigherDirectImage (p : ℕ) :
    Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}

Sources

• Section 59.35, Tag 03PV
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.smallEtalePresheafPushforward · AlgebraicGeometry.smallEtaleBaseChange_isCovering · AlgebraicGeometry.isSheafFor_baseChange_iff · CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf · Stacks.EtaleCohomology.smallEtaleDirectImage · Stacks.EtaleCohomology.etaleAbelianHigherDirectImage

Section59.36 Inverse image#

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

Tag 03Q0, a definition

Tag 03Q0 in the Stacks Project.

Declarations registered for the tag:

• Stacks.EtaleCohomology.smallEtaleInverseImage, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 52 (StacksFrontier): “the inverse image f⁻¹ on sheaves of sets”.
• Stacks.EtaleCohomology.smallEtaleInverseImageAdjunction, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 55 (StacksFrontier): “f⁻¹ on sheaves of sets is characterised by its adjunction Hom(f⁻¹ G, F) = Hom(G, f_* F)”.
• Stacks.EtaleCohomology.smallEtalePullbackAb, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 59 (StacksFrontier): “the inverse image f⁻¹ on sheaves of abelian groups”.
• Stacks.EtaleCohomology.smallEtaleAdjunctionAb, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 62 (StacksFrontier): “f⁻¹ on sheaves of abelian groups is characterised by its adjunction Hom(f⁻¹ G, F) = Hom(G, f_* F)”.

Tag 04I3, an equation

Tag 04I3 in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleInverseImagePresheafObjIsoColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 77. The attribute's comment: “the displayed presheaf: its sections over U are the colimit of G(V) over the pairs (V, φ : U ⟶ X ×_Y V)”.

The sections over an étale X-scheme U of the presheaf whose sheafification is f⁻¹ G: the colimit of the sets G(V) over the category of pairs (V, φ : U ⟶ X ×_Y V) with V étale over Y, which is the comma category CostructuredArrow (smallEtaleBaseChange f).op (op U). The presheaf is the left Kan extension of G along the opposite of base change, and a left Kan extension along a functor between small categories is computed pointwise by this colimit.

def smallEtaleInverseImagePresheafObjIsoColimit
    (G : Sheaf (smallEtaleTopology Y) (Type (max (u + 1) v))) (U : X.Etale) :
    ((smallEtaleBaseChange f).op.lan.obj G.obj).obj (op U) ≅
      colimit (CostructuredArrow.proj (smallEtaleBaseChange f).op (op U) ⋙ G.obj)

Stacks.EtaleCohomology.smallEtaleInverseImage_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 87. The attribute's comment: “f⁻¹ G is the sheaf associated to the displayed presheaf”.

The inverse image f⁻¹ G of a sheaf of sets on the small étale site of Y is the sheaf associated to the presheaf of smallEtaleInverseImagePresheafObjIsoColimit, that is, to the left Kan extension of G along the opposite of base change.

theorem smallEtaleInverseImage_obj
    (G : Sheaf (smallEtaleTopology Y) (Type (max (u + 1) v))) :
    (smallEtaleInverseImage.{u, v} f).obj G =
      (presheafToSheaf (smallEtaleTopology X) (Type (max (u + 1) v))).obj
        ((smallEtaleBaseChange f).op.lan.obj G.obj)

Tag 03Q1, a lemma

Tag 03Q1 in the Stacks Project.

AlgebraicGeometry.smallEtalePullbackStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/Basic.lean, line 161. The attribute's comment: “pullback_stalk”. References: SGA 4½ Arcata (2.3.3), “(f^*F)_x̄ = F_f(x̄)”.

Stacks 03Q1. Pullback of an étale sheaf commutes naturally with taking stalks at a geometric point.

public def smallEtalePullbackStalkIso (B : BigEtaleSite.{u})
    {S T : B.Scheme} (f : T ⟶ S) (x : GeometricPoint T.1) :
    (smallEtaleBaseChange B f).sheafPullback (Type (u + 1))
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property) ⋙
      etaleStalkFunctor.{u, u + 1} B T.1 T.property x ≅
    etaleStalkFunctor.{u, u + 1} B S.1 S.property (x.map (B.inclusion.map f))

AlgebraicGeometry.smallEtalePullbackStalkIso_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/Basic.lean, line 212. The attribute's comment: “pullback_stalk”.

Stacks 03Q1. The comparison sends the germ of a section pulled back to a pointed étale neighborhood to the germ of the original section.

public theorem smallEtalePullbackStalkIso_germ (B : BigEtaleSite.{u})
    {S T : B.Scheme} (f : T ⟶ S) (x : GeometricPoint T.1)
    (F : Sheaf (SmallEtale.topology B S.1 S.property) (Type (u + 1)))
    (U : (geometricPointFiber B T.1 T.property x).Elements)
    (V : (geometricPointFiber B S.1 S.property
      (x.map (B.inclusion.map f))).Elements)
    (a : U.1 ⟶ (smallEtaleBaseChange B f).obj V.1)
    (ha : U.2.1 ≫ (SmallEtale.toScheme B T.1 T.property).map a ≫
        B.inclusion.map (pullback.fst V.1.obj.hom f) = V.2.1)
    (t : F.obj.obj (Opposite.op V.1)) :
    ((smallEtalePullbackStalkIso B f x).hom.app F)
      ((colimit.ι
        ((CategoryOfElements.π (geometricPointFiber B T.1 T.property x)).op ⋙
          (((smallEtaleBaseChange B f).sheafPullback (Type (u + 1))
            (SmallEtale.topology B S.1 S.property)
            (SmallEtale.topology B T.1 T.property)).obj F).obj)
        (Opposite.op U)) (pullbackSectionAlong B f F V.1 U.1 a t)) =
      (colimit.ι
        ((CategoryOfElements.π (geometricPointFiber B S.1 S.property
          (x.map (B.inclusion.map f)))).op ⋙ F.obj)
        (Opposite.op V)) t

AlgebraicGeometry.smallEtalePullbackSheafFiberIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/Coefficients.lean, line 76. The attribute's comment: “pullback_stalk, arbitrary coefficients”. References: SGA 4½ Arcata (2.3.3), “(f^*F)_x̄ = F_f(x̄)”; SGA 4 VIII (3.4), “(F), special case”.

Stacks 03Q1 for arbitrary coefficients. Inverse image of a sheaf on the small étale site commutes naturally with the stalk at a geometric point.

public def smallEtalePullbackSheafFiberIso (B : BigEtaleSite.{u})
    {S T : B.Scheme} (f : T ⟶ S) (x : GeometricPoint T.obj)
    (A : Type uA) [Category.{vA} A] [HasColimitsOfSize.{u, u} A] [HasProducts.{u} A]
    [((smallEtaleBaseChange B f).sheafPushforwardContinuous A
      (SmallEtale.topology B S.obj S.property)
      (SmallEtale.topology B T.obj T.property)).IsRightAdjoint] :
    (smallEtaleBaseChange B f).sheafPullback A
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property) ⋙
      (geometricPointSitePoint B T.obj T.property x).sheafFiber ≅
    (geometricPointSitePoint B S.obj S.property (x.map (B.inclusion.map f))).sheafFiber

AlgebraicGeometry.smallEtalePullbackSheafFiberIso_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/CoefficientsGerm.lean, line 104. The attribute's comment: “pullback_stalk on germs, arbitrary coefficients”.

Stacks 03Q1 for arbitrary coefficients, on germs: the comparison of the stalk of an inverse image with the stalk at the image point sends the germ of a pulled-back section to the germ of the original section.

public theorem smallEtalePullbackSheafFiberIso_germ
    (F : Sheaf (SmallEtale.topology B S.obj S.property) A)
    (U : (geometricPointFiber B T.obj T.property x).Elements)
    (V : (geometricPointFiber B S.obj S.property
      (x.map (B.inclusion.map f))).Elements)
    (a : U.1 ⟶ (smallEtaleBaseChange B f).obj V.1)
    (ha : U.2.1 ≫ (SmallEtale.toScheme B T.obj T.property).map a ≫
      B.inclusion.map (pullback.fst V.1.obj.hom f) = V.2.1) :
    pullbackSectionAlongHom B f A F V.1 U.1 a ≫
        colimit.ι ((CategoryOfElements.π (geometricPointFiber B T.obj T.property x)).op ⋙
            (((smallEtaleBaseChange B f).sheafPullback A
              (SmallEtale.topology B S.obj S.property)
              (SmallEtale.topology B T.obj T.property)).obj F).obj) (op U) ≫
          (smallEtalePullbackSheafFiberIso B f x A).hom.app F =
      colimit.ι ((CategoryOfElements.π (geometricPointFiber B S.obj S.property
        (x.map (B.inclusion.map f)))).op ⋙ F.obj) (op V)

AlgebraicGeometry.etaleStalkSmallEtalePullObjIso_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/CoefficientsGerm.lean, line 179. The attribute's comment: “pullback_stalk on germs, arbitrary coefficients, single sheaf”.

Stacks 03Q1 for arbitrary coefficients, on germs and on a single sheaf.

public theorem etaleStalkSmallEtalePullObjIso_germ
    (F : Sheaf (SmallEtale.topology B S.obj S.property) A)
    (U : (geometricPointFiber B T.obj T.property x).Elements)
    (V : (geometricPointFiber B S.obj S.property
      (x.map (B.inclusion.map f))).Elements)
    (a : U.1 ⟶ (smallEtaleBaseChange B f).obj V.1)
    (ha : U.2.1 ≫ (SmallEtale.toScheme B T.obj T.property).map a ≫
      B.inclusion.map (pullback.fst V.1.obj.hom f) = V.2.1) :
    pullbackSectionAlongHom B f A F V.1 U.1 a ≫
        colimit.ι ((CategoryOfElements.π (geometricPointFiber B T.obj T.property x)).op ⋙
            (((smallEtaleBaseChange B f).sheafPullback A
              (SmallEtale.topology B S.obj S.property)
              (SmallEtale.topology B T.obj T.property)).obj F).obj) (op U) ≫
          (etaleStalkSmallEtalePullObjIso B f x A F).hom =
      colimit.ι ((CategoryOfElements.π (geometricPointFiber B S.obj S.property
        (x.map (B.inclusion.map f)))).op ⋙ F.obj) (op V)

AlgebraicGeometry.smallEtalePullbackStalkIsoModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/ModuleCoefficients.lean, line 210. The attribute's comment: “module coefficients”.

Stacks 03Q1 for sheaves of modules. Inverse image of sheaves of Λ-modules on small étale sites commutes with taking stalks at a geometric point: the stalk at x of the inverse image along f is the stalk of the original sheaf at the image geometric point, naturally in the sheaf.

public def smallEtalePullbackStalkIsoModule {S T : B.Scheme} (f : T ⟶ S)
    (x : GeometricPoint T.1) :
    (smallEtaleBaseChange B f).sheafPullback (ModuleCat.{u + 1} Λ)
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property) ⋙
      etaleStalkFunctorModule B T.1 T.property Λ x ≅
    etaleStalkFunctorModule B S.1 S.property Λ (x.map (B.inclusion.map f))

AlgebraicGeometry.smallEtaleSheafPullback_preservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 307. The attribute's comment: “exact_sets”.

Inverse image along f : T ⟶ S between the small étale topoi preserves finite limits: being a morphism of sites, base change has an exact left adjoint on sheaves, and that left adjoint is the sheaf pullback.

public instance smallEtaleSheafPullback_preservesFiniteLimits {S T : B.Scheme} (f : T ⟶ S) :
    PreservesFiniteLimits
      ((smallEtaleBaseChange B f).sheafPullback (Type (u + 1))
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property))

Stacks.EtaleCohomology.smallEtaleAbSheafPullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleInverseImageAbelian.lean, line 86. The attribute's comment: “exact_abelian”.

Stacks 03Q1. For a morphism of schemes f : X ⟶ Y, the inverse image functor f⁻¹ : Ab(Y_étale) ⥤ Ab(X_étale) between the categories of abelian sheaves on the small étale sites is exact: it preserves finite limits and finite colimits.

public theorem smallEtaleAbSheafPullback_exact {X Y : Scheme.{u}} (f : X ⟶ Y) :
    exactFunctor
      (Sheaf (smallEtaleTopology Y) Ab.{u + 1})
      (Sheaf (smallEtaleTopology X) Ab.{u + 1})
      ((smallEtaleBaseChange f).sheafPullback Ab.{u + 1}
        (smallEtaleTopology Y) (smallEtaleTopology X))

Stacks.EtaleCohomology.smallEtalePullbackRepresentableNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleInverseImageRepresentable.lean, line 160. The attribute's comment: “pullback_representable”.

For a morphism of schemes f : X ⟶ Y, the inverse image on the small étale sites carries the sheaf represented by an étale Y-scheme V to the sheaf represented by the base change X ×_Y V, naturally in V: f⁻¹ h_V ≅ h_{X ×_Y V} as functors of V.

public def smallEtalePullbackRepresentableNatIso :
    (smallEtaleTopology Y).uliftYoneda.{max (u + 1) v} ⋙
        (smallEtaleBaseChange f).sheafPullback (Type (max (u + 1) v))
          (smallEtaleTopology Y) (smallEtaleTopology X) ≅
      smallEtaleBaseChange f ⋙ (smallEtaleTopology X).uliftYoneda.{max (u + 1) v}

Stacks.EtaleCohomology.smallEtalePullbackRepresentableNatIso_app_hom_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleInverseImageRepresentable.lean, line 184. The attribute's comment: “pullback_representable”.

Under the inverse-image/direct-image adjunction and the Yoneda bijections for sheaves, precomposition with the component of smallEtalePullbackRepresentableNatIso at V is the identity on sections over X ×_Y V.

public lemma smallEtalePullbackRepresentableNatIso_app_hom_comp (V : Y.Etale)
    (F : Sheaf (smallEtaleTopology X) (Type (max (u + 1) v)))
    (g : (smallEtaleTopology X).uliftYoneda.{max (u + 1) v}.obj
      ((smallEtaleBaseChange f).obj V) ⟶ F) :
    (smallEtaleTopology Y).uliftYonedaEquiv
        ((((smallEtaleBaseChange f).sheafAdjunctionContinuous (Type (max (u + 1) v))
          (smallEtaleTopology Y) (smallEtaleTopology X)).homEquiv _ _)
            (((smallEtalePullbackRepresentableNatIso.{u, v} f).app V).hom ≫ g)) =
      (smallEtaleTopology X).uliftYonedaEquiv g

Declarations registered for the tag:

• CategoryTheory.Adjunction.leftAdjoint_preservesColimits registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 317 (StacksFrontier): “exact_sets”. References: SGA 4 I (5.4), “more general”; SGA 4 I (8.7.1.7), “more general”; SGA 4 IV (3.1.3), “partial”; SGA 4 IV (4.5.1), “more general”.

Tag 03Q2, a remark

Tag 03Q2 in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 102 (StacksFrontier): “for a continuous functor u : C₂ ⥤ C₁ the direct image on sheaves is given by f_* F (V) = F (u V)”.
• CategoryTheory.Functor.isMorphismOfSites_of_isTerminal, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleInverseImages.lean, line 106 (StacksFrontier): “a continuous u carrying a final object to a final object and preserving fibre products has an exact left adjoint f⁻¹ of f_*”.

Sources

• Section 59.36, Tag 03PZ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.smallEtaleInverseImage · Stacks.EtaleCohomology.smallEtaleInverseImageAdjunction · Stacks.EtaleCohomology.smallEtalePullbackAb · Stacks.EtaleCohomology.smallEtaleAdjunctionAb · Stacks.EtaleCohomology.smallEtaleInverseImagePresheafObjIsoColimit · Stacks.EtaleCohomology.smallEtaleInverseImage_obj · AlgebraicGeometry.smallEtalePullbackStalkIso · AlgebraicGeometry.smallEtalePullbackStalkIso_germ

Section59.39 Comparing topologies#

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

Tag 09XM, a lemma

Tag 09XM in the Stacks Project.

AlgebraicGeometry.openEqLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/OpenEqualityLocus.lean, line 405. The attribute's comment: “open locus”.

Stacks 09XM, the open locus. The largest open subscheme of S on which two global sections of a sheaf on the small étale site of S agree: the supremum of the opens through which only agreeing morphisms factor.

public def openEqLocus : (B.inclusion.obj S).Opens

AlgebraicGeometry.factorsThrough_openEqLocus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/OpenEqualityLocus.lean, line 435. The attribute's comment: “universal property”.

Stacks 09XM, the universal property. A morphism of the big étale site factors through the open equality locus exactly when the two sections agree after inverse image along the induced morphism of small étale topoi.

public theorem factorsThrough_openEqLocus_iff (f : T ⟶ S) :
    (∃ g : B.inclusion.obj T ⟶ (openEqLocus B S F s t).toScheme,
      g ≫ (openEqLocus B S F s t).ι = B.inclusion.map f) ↔
      (smallEtalePullback B S T f).map s =
        (smallEtalePullback B S T f).map t

Tag 09XN, a lemma

Tag 09XN in the Stacks Project.

AlgebraicGeometry.zariskiInverseImageSectionsComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiPullbackSections.lean, line 288. The attribute's comment: “pullback_formula”.

The section comparisons for all schemes over S, compatible with the canonical small-pullback restriction maps. The family and the compatibility are chosen together.

public noncomputable def zariskiInverseImageSectionsComparison
    (B : BigZariskiSite.{u}) (S : B.Schemes) :
    { e : ∀ X : BigZariskiOver B S.1 S.property,
        (smallZariskiProjection B S).inverseImage ⋙
          (sheafSections (BigZariskiOver.topology B S.1 S.property)
            (Type (u + 1))).obj (Opposite.op X) ≅
        (smallZariskiBaseChange B X.hom).sheafPullback
            (Type (u + 1))
            (SmallZariski.topology B S.1 S.property)
            (SmallZariski.topology B X.left.1 X.left.property) ⋙
          Sheaf.Γ (SmallZariski.topology B X.left.1 X.left.property)
            (Type (u + 1)) //
      ∀ {X Y : BigZariskiOver B S.1 S.property} (g : Y ⟶ X)
        (F : Sheaf (SmallZariski.topology B S.1 S.property) (Type (u + 1))),
        (e X).hom.app F ≫ zariskiPullbackSectionsRestriction B S g F =
          ((smallZariskiProjection B S).inverseImage.obj F).obj.map g.op ≫
            (e Y).hom.app F }

AlgebraicGeometry.zariskiInverseImageSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiPullbackSections.lean, line 366. The attribute's comment: “pullback_formula”.

Stacks 09XN, pullback formula (Zariski case). For a sheaf F on the small Zariski site of S and a scheme f : X ⟶ S over S, the sections of π_S⁻¹F at X are the global sections of the small Zariski pullback f⁻¹F, naturally in F. Restriction in X is recorded by AlgebraicGeometry.zariskiInverseImageSectionsIso_naturality.

public noncomputable def zariskiInverseImageSectionsIso
    (B : BigZariskiSite.{u}) (S : B.Schemes) (X : BigZariskiOver B S.1 S.property) :
    (smallZariskiProjection B S).inverseImage ⋙
      (sheafSections (BigZariskiOver.topology B S.1 S.property)
        (Type (u + 1))).obj (Opposite.op X) ≅
    (smallZariskiBaseChange B X.hom).sheafPullback
        (Type (u + 1))
        (SmallZariski.topology B S.1 S.property)
        (SmallZariski.topology B X.left.1 X.left.property) ⋙
      Sheaf.Γ (SmallZariski.topology B X.left.1 X.left.property)
        (Type (u + 1))

AlgebraicGeometry.etaleInverseImageSectionsComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtalePullbackSections.lean, line 245. The attribute's comment: “pullback_formula”.

The section comparisons for all schemes over S, compatible with the canonical small-pullback restriction maps. The family and the compatibility are chosen together.

public noncomputable def etaleInverseImageSectionsComparison
    (B : BigEtaleSite.{u}) (S : B.Scheme) :
    { e : ∀ X : BigEtaleOver B S.obj S.property,
        (bigEtaleToSmallEtaleMorphism B S.obj S.property).inverseImage ⋙
          (sheafSections (BigEtaleOver.topology B S.obj S.property)
            (Type (u + 1))).obj (Opposite.op X) ≅
        (smallEtaleBaseChange B X.hom).sheafPullback
            (Type (u + 1))
            (SmallEtale.topology B S.obj S.property)
            (SmallEtale.topology B X.left.obj X.left.property) ⋙
          Sheaf.Γ (SmallEtale.topology B X.left.obj X.left.property)
            (Type (u + 1)) //
      ∀ {X Y : BigEtaleOver B S.obj S.property} (g : Y ⟶ X)
        (F : Sheaf (SmallEtale.topology B S.obj S.property) (Type (u + 1))),
        (e X).hom.app F ≫ etalePullbackSectionsRestriction B S g F =
          ((bigEtaleToSmallEtaleMorphism B S.obj S.property).inverseImage.obj F).obj.map g.op ≫
            (e Y).hom.app F }

AlgebraicGeometry.etaleInverseImageSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtalePullbackSections.lean, line 327. The attribute's comment: “pullback_formula”.

Stacks 09XN, pullback formula (étale case). For a sheaf F on the small étale site of S and a scheme f : X ⟶ S over S, the sections of π_S⁻¹F at X are the global sections of the small étale pullback f⁻¹F, naturally in F. Restriction in X is recorded by AlgebraicGeometry.etaleInverseImageSectionsIso_naturality.

public noncomputable def etaleInverseImageSectionsIso
    (B : BigEtaleSite.{u}) (S : B.Scheme) (X : BigEtaleOver B S.obj S.property) :
    (bigEtaleToSmallEtaleMorphism B S.obj S.property).inverseImage ⋙
      (sheafSections (BigEtaleOver.topology B S.obj S.property)
        (Type (u + 1))).obj (Opposite.op X) ≅
    (smallEtaleBaseChange B X.hom).sheafPullback
        (Type (u + 1))
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B X.left.obj X.left.property) ⋙
      Sheaf.Γ (SmallEtale.topology B X.left.obj X.left.property)
        (Type (u + 1))

AlgebraicGeometry.smallSiteInverseImage_sections_and_isSheaf_fpqc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmallSitePullbackSectionsAndFpqcSheaf.lean, line 63.

Stacks 09XN. Let S be a scheme, let τ be the Zariski or the étale topology and let π_S : (Sch/S)_τ ⟶ S_τ be the projection from the big τ-topos over S to the small τ-topos of S. For a sheaf F on the small τ-site of S:

1. the sections of π_S⁻¹F over a scheme f : X ⟶ S over S are the global sections on the small τ-site of X of the small-site pullback f⁻¹F, naturally in F and compatibly with restriction along any morphism of schemes over S;
2. the presheaf underlying π_S⁻¹F is a sheaf for the fpqc topology on the big τ-site over S.

The first component of the conjunction is the Zariski case, the second the étale case; the two are the source's two values of τ, which are unrelated site structures here. Within each case the sections formula is AlgebraicGeometry.zariskiInverseImageSectionsComparison resp. AlgebraicGeometry.etaleInverseImageSectionsComparison — the family of comparison isomorphisms together with its compatibility with restriction — and the fpqc sheaf condition is AlgebraicGeometry.smallZariskiProjection_inverseImage_isSheaf_fpqc resp. AlgebraicGeometry.bigEtaleToSmallEtale_inverseImage_isSheaf_fpqc.

public noncomputable def smallSiteInverseImage_sections_and_isSheaf_fpqc :
    (∀ (B : BigZariskiSite.{u}) (S : B.Schemes),
        { e : ∀ X : BigZariskiOver B S.obj S.property,
            (smallZariskiProjection B S).inverseImage ⋙
              (sheafSections (BigZariskiOver.topology B S.obj S.property)
                (Type (u + 1))).obj (Opposite.op X) ≅
            (smallZariskiBaseChange B X.hom).sheafPullback
                (Type (u + 1))
                (SmallZariski.topology B S.obj S.property)
                (SmallZariski.topology B X.left.obj X.left.property) ⋙
              Sheaf.Γ (SmallZariski.topology B X.left.obj X.left.property)
                (Type (u + 1)) //
          (∀ {X Y : BigZariskiOver B S.obj S.property} (g : Y ⟶ X)
              (F : Sheaf (SmallZariski.topology B S.obj S.property) (Type (u + 1))),
              (e X).hom.app F ≫ zariskiPullbackSectionsRestriction B S g F =
                ((smallZariskiProjection B S).inverseImage.obj F).obj.map g.op ≫
                  (e Y).hom.app F) ∧
            ∀ F : Sheaf (SmallZariski.topology B S.obj S.property) (Type (u + 1)),
              Presheaf.IsSheaf
                ((Scheme.fpqcPrecoverage.comap
                  (BigZariskiOver.toScheme B S.obj S.property)).toGrothendieck)
                ((smallZariskiProjection B S).inverseImage.obj F).obj }) ×'
    ∀ (B : BigEtaleSite.{u}) (S : B.Scheme),
      { e : ∀ X : BigEtaleOver B S.obj S.property,
          (bigEtaleToSmallEtaleMorphism B S.obj S.property).inverseImage ⋙
            (sheafSections (BigEtaleOver.topology B S.obj S.property)
              (Type (u + 1))).obj (Opposite.op X) ≅
          (smallEtaleBaseChange B X.hom).sheafPullback
              (Type (u + 1))
              (SmallEtale.topology B S.obj S.property)
              (SmallEtale.topology B X.left.obj X.left.property) ⋙
            Sheaf.Γ (SmallEtale.topology B X.left.obj X.left.property)
              (Type (u + 1)) //
        (∀ {X Y : BigEtaleOver B S.obj S.property} (g : Y ⟶ X)
            (F : Sheaf (SmallEtale.topology B S.obj S.property) (Type (u + 1))),
            (e X).hom.app F ≫ etalePullbackSectionsRestriction B S g F =
              ((bigEtaleToSmallEtaleMorphism B S.obj S.property).inverseImage.obj F).obj.map
                  g.op ≫
                (e Y).hom.app F) ∧
          ∀ F : Sheaf (SmallEtale.topology B S.obj S.property) (Type (u + 1)),
            Presheaf.IsSheaf
              ((Scheme.fpqcPrecoverage.comap
                (BigEtaleOver.toScheme B S.obj S.property)).toGrothendieck)
              ((bigEtaleToSmallEtaleMorphism B S.obj S.property).inverseImage.obj F).obj }

Tag 0A3H, a lemma

Tag 0A3H in the Stacks Project.

Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIso_of_flat_quasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FlatSections.lean, line 81. The attribute's comment: “Tag 0EZK -- the same conclusion for a universally submersive morphism with geometrically connected fibres -- is a separate cited tag and is carried as the declared hypothesis hEZK, following the 08W5 convention. The content supplied here is that a flat quasi-compact morphism with geometrically connected fibres is universally submersive, proved unconditionally as universally_isQuotientMap_of_flat_quasiCompact.”.

Stacks Project, Tag 0A3H. Pullback along a flat quasi-compact morphism with geometrically connected fibres preserves global sections of every sheaf of sets on the small étale site, naturally in the sheaf.

public def globalSectionsSmallEtaleInverseImageIso_of_flat_quasiCompact
    {T S : Scheme.{u}} (f : T ⟶ S) [Flat f] [QuasiCompact f] [GeometricallyConnected f]
    (hEZK : ∀ {X S' : Scheme.{u}} (g : X ⟶ S'), GeometricallyConnected g →
      (topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally g →
      (Sheaf.Γ (smallEtaleTopology S') (Type (max (u + 1) v)) ≅
        smallEtaleInverseImage.{u, v} g ⋙
          Sheaf.Γ (smallEtaleTopology X) (Type (max (u + 1) v)))) :
    Sheaf.Γ (smallEtaleTopology S) (Type (max (u + 1) v)) ≅
      smallEtaleInverseImage.{u, v} f ⋙
        Sheaf.Γ (smallEtaleTopology T) (Type (max (u + 1) v))

Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImage_of_flat_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FlatSectionsCanonical.lean, line 60. The attribute's comment: “the form the source asserts: the canonical comparison on global sections, rather than a bare isomorphism of global-sections functors”.

Stacks Project, Tag 0A3H. For f : T ⟶ S flat and quasi-compact with geometrically connected fibres, the canonical comparison Γ(S, F) ⟶ Γ(T, f⁻¹F) is an isomorphism for every sheaf of sets F on the small étale site of S, naturally in F. This is the form in which the source asserts the tag — it writes Γ(S, F) = Γ(T, f⁻¹F) for the canonical map, and proves that map injective and surjective — and it is stronger than the bare existence of an isomorphism of global-sections functors, which would not say that the isomorphism is restriction of sections.

public theorem isIso_globalSectionsSmallEtaleInverseImage_of_flat_quasiCompact
    {T S : Scheme.{u}} (f : T ⟶ S) [Flat f] [QuasiCompact f] [GeometricallyConnected f] :
    IsIso (globalSectionsSmallEtaleInverseImage.{u, v} f)

Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIso_of_flat_of_quasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FlatSectionsCanonical.lean, line 73. The attribute's comment: “the natural isomorphism of global-sections functors, with no hypothesis beyond the source's”.

Stacks Project, Tag 0A3H. Pullback along a flat quasi-compact morphism with geometrically connected fibres preserves global sections of every sheaf of sets on the small étale site, naturally in the sheaf. The isomorphism is the canonical comparison, which Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImage_of_flat_quasiCompact inverts.

public def globalSectionsSmallEtaleInverseImageIso_of_flat_of_quasiCompact
    {T S : Scheme.{u}} (f : T ⟶ S) [Flat f] [QuasiCompact f] [GeometricallyConnected f] :
    Sheaf.Γ (smallEtaleTopology S) (Type (max (u + 1) v)) ≅
      smallEtaleInverseImage.{u, v} f ⋙
        Sheaf.Γ (smallEtaleTopology T) (Type (max (u + 1) v))

Tag 0EZK, a lemma

Tag 0EZK in the Stacks Project.

Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SubmersiveSections.lean, line 2480. The attribute's comment: “corrected: Stacks erratum. The tag in the form the source asserts it, about the canonical comparison rather than a bare isomorphism of global-sections functors. The tag is false with only f submersive; see the counterexample in the docstring of globalSectionsSmallEtaleInverseImageIso”.

Stacks Project, Tag 0EZK. For f universally submersive with geometrically connected fibres, the canonical comparison Γ(S, F) ⟶ Γ(X, f⁻¹F) is an isomorphism, naturally in the sheaf F. This is the form in which the source asserts the tag — it says "there is a canonical map Γ(S, F) → Γ(X, f⁻¹F)" and then that it is injective and surjective — and it is strictly stronger than the bare existence of an isomorphism of global-sections functors, which would not say that the isomorphism is restriction of sections.

Stacks erratum. The hypothesis stated here is the corrected one; Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIso carries the characteristic-2 counterexample to the tag as the source writes it.

public theorem isIso_globalSectionsSmallEtaleInverseImage
    {X S : Scheme.{u}} (f : X ⟶ S)
    (hsub : (topologically @Topology.IsQuotientMap :
      MorphismProperty Scheme.{u}).universally f)
    [GeometricallyConnected f] :
    IsIso (globalSectionsSmallEtaleInverseImage.{u, v} f)

Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SubmersiveSections.lean, line 2524. The attribute's comment: “corrected: Stacks erratum. The tag is false with only f submersive, since the proof's reduction is an etale base change and submersivity does not survive one; universal submersivity is assumed instead. Counterexample in characteristic 2: the homeomorphism Spec k[t,1/t] -> Spec {g : g(0) = g(1)} and the double cover T = Spec A[z]/(z^2 + z + a) with a = t^2 + t, for which the sections downstairs are empty while there are two upstairs; see this declaration's docstring”.

Stacks Project, Tag 0EZK. Pullback along a universally submersive morphism with geometrically connected fibres preserves global sections of every sheaf of sets on the small étale site, naturally in the sheaf. The isomorphism is the canonical comparison, which Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImage inverts.

Stacks erratum. The hypothesis stated here is the corrected one. As the source writes the tag it asks only that f be submersive, and in that form the statement is false: the proof reduces along an étale base change, and submersivity does not survive one. The counterexample lives in characteristic 2. Let k be a field of characteristic 2, let A = {g ∈ k[t] ∣ g(0) = g(1)} be the node — the affine line with the two points t = 0 and t = 1 glued — let B = k[t, 1/t] be the affine line with t = 0 removed, and let f : Spec B ⟶ Spec A be the homeomorphism described in the Stacks proof: it is bijective because the node has already glued the removed point t = 0 to the surviving point t = 1. Take F = h_T, the functor of points of T = Spec A[z]/(z² + z + a) with a = t² + t, which is the connected étale double cover of Spec A — étale because the derivative of z² + z + a in z is the unit 1 in characteristic 2. Then Γ(S, F) is EMPTY: a root of z² + z + a in k[t] is t or t + 1, and neither takes the same value at 0 and at 1, so neither lies in A. But Γ(X, f⁻¹F) has TWO elements, t and t + 1, both of which lie in B. So the claimed bijection Γ(S, F) = Γ(X, f⁻¹F) cannot hold, and the submersive hypothesis alone does not suffice. Universal submersivity — equivalently, submersivity after every étale base change — is what the argument uses and what is assumed here; it is part of the corrected statement, not a strengthening of it.

public def globalSectionsSmallEtaleInverseImageIso
    {X S : Scheme.{u}} (f : X ⟶ S)
    (hsub : (topologically @Topology.IsQuotientMap :
      MorphismProperty Scheme.{u}).universally f)
    [GeometricallyConnected f] :
    Sheaf.Γ (smallEtaleTopology S) (Type (max (u + 1) v)) ≅
      smallEtaleInverseImage f ⋙
        Sheaf.Γ (smallEtaleTopology X) (Type (max (u + 1) v))

Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImage_of_etaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SubmersiveSectionsEtaleBaseChange.lean, line 51. The attribute's comment: “corrected: Stacks erratum: f submersive after every etale base change, the exact corrected hypothesis; the source's plain submersivity of f is not enough, see the counterexample in the docstring of globalSectionsSmallEtaleInverseImageIso. The universally submersive special case is isIso_globalSectionsSmallEtaleInverseImage”.

Stacks Project, Tag 0EZK. Let f : X ⟶ S have geometrically connected fibres and be submersive after every étale base change: for every étale g : V ⟶ S the projection V ×_S X ⟶ V is a quotient map. Then the canonical comparison Γ(S, F) ⟶ Γ(X, f⁻¹F) is an isomorphism, naturally in the sheaf F on the small étale site of S.

public theorem isIso_globalSectionsSmallEtaleInverseImage_of_etaleBaseChange
    {X S : Scheme.{u}} (f : X ⟶ S)
    (hsub : ∀ ⦃V : Scheme.{u}⦄ (g : V ⟶ S) [Etale g],
      Topology.IsQuotientMap (pullback.fst g f))
    [GeometricallyConnected f] :
    IsIso (globalSectionsSmallEtaleInverseImage.{u, v} f)

Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIsoOfEtaleBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SubmersiveSectionsEtaleBaseChange.lean, line 77. The attribute's comment: “corrected: Stacks erratum: f submersive after every etale base change, the exact corrected hypothesis; the source's plain submersivity of f is not enough, see the counterexample in the docstring of globalSectionsSmallEtaleInverseImageIso. The universally submersive special case is globalSectionsSmallEtaleInverseImageIso”.

Stacks Project, Tag 0EZK. Pullback along a morphism with geometrically connected fibres that is submersive after every étale base change preserves global sections of every sheaf of sets on the small étale site, naturally in the sheaf; the isomorphism is the canonical comparison Γ(S, F) ⟶ Γ(X, f⁻¹F).

public noncomputable def globalSectionsSmallEtaleInverseImageIsoOfEtaleBaseChange
    {X S : Scheme.{u}} (f : X ⟶ S)
    (hsub : ∀ ⦃V : Scheme.{u}⦄ (g : V ⟶ S) [Etale g],
      Topology.IsQuotientMap (pullback.fst g f))
    [GeometricallyConnected f] :
    Sheaf.Γ (smallEtaleTopology S) (Type (max (u + 1) v)) ≅
      smallEtaleInverseImage f ⋙
        Sheaf.Γ (smallEtaleTopology X) (Type (max (u + 1) v))

Tag 0A3I, a lemma

Tag 0A3I in the Stacks Project.

Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIso_of_isSepClosed, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SeparablyClosedBaseFieldSections.lean, line 41. References: SGA 4 XVI (1.5), “partial”.

For a scheme S over a separably closed field k and any field extension K/k, pullback along the projection S ×_{Spec k} Spec K ⟶ S preserves global sections of every sheaf of sets on the small étale site, naturally in the sheaf.

public def globalSectionsSmallEtaleInverseImageIso_of_isSepClosed
    (k K : Type u) [Field k] [IsSepClosed k] [Field K] [Algebra k K]
    {S : Scheme.{u}} (f : S ⟶ Spec (.of k)) :
    Sheaf.Γ (smallEtaleTopology S) (Type (max (u + 1) v)) ≅
      smallEtaleInverseImage.{u, v}
          (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))) ⋙
        Sheaf.Γ
          (smallEtaleTopology (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))))
          (Type (max (u + 1) v))

Sources

• Section 59.39, Tag 09XL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.openEqLocus · AlgebraicGeometry.factorsThrough_openEqLocus_iff · AlgebraicGeometry.zariskiInverseImageSectionsComparison · AlgebraicGeometry.zariskiInverseImageSectionsIso · AlgebraicGeometry.etaleInverseImageSectionsComparison · AlgebraicGeometry.etaleInverseImageSectionsIso · AlgebraicGeometry.smallSiteInverseImage_sections_and_isSheaf_fpqc · Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageIso_of_flat_quasiCompact

Section59.40 Recovering morphisms#

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

Tag 04I5, a lemma

Tag 04I5 in the Stacks Project.

AlgebraicGeometry.smallEtaleRingedSiteHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/LocallyRinged.lean, line 130.

Stacks 04I5. The morphism of ringed sites (a_small, a_small^♯) associated to a morphism of schemes a : X ⟶ Y is a morphism of locally ringed sites: its square of units subsheaves is cartesian.

The geometric points of X are a conservative family of points of its small étale site, and at each of them the stalk of a⁻¹𝒪_Y ⟶ 𝒪_X is the map of étale local rings (𝒪_Y)_ȳ ⟶ (𝒪_X)_x̄, which is a local ring map.

public theorem smallEtaleRingedSiteHom_isLocallyRinged :
    (smallEtaleRingedSiteHom B a).IsLocallyRinged

Tag 04IJ, a lemma

Tag 04IJ in the Stacks Project.

AlgebraicGeometry.Space.schemeSmallEtaleRingedToposHom_twoMorphism_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeSmallEtaleTwoMorphismRigidity.lean, line 66.

Stacks 04IJ. A 2-morphism from the morphism of small étale ringed topoi induced by a morphism of schemes to itself is the identity.

theorem schemeSmallEtaleRingedToposHom_twoMorphism_eq_id
    (t : AlgebraicGeometry.RingedToposHom.TwoMorphism.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS (schemeSpaceMap g))
      (smallEtaleRingedToposHom B S hS (schemeSpaceMap g))) :
    t = AlgebraicGeometry.RingedToposHom.TwoMorphism.id
      (smallEtaleRingedToposHom B S hS (schemeSpaceMap g))

AlgebraicGeometry.Space.schemeSmallEtaleRingedToposHom_twoMorphismOfRingedTopoi_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeSmallEtaleTwoMorphismRigidity.lean, line 78.

Stacks 04IJ for a 2-morphism over the four-field morphism of ringed topoi: a 2-morphism from the morphism of small étale ringed topoi induced by a morphism of schemes to itself is the identity.

theorem schemeSmallEtaleRingedToposHom_twoMorphismOfRingedTopoi_eq_id
    (t : Stacks.Sheaves.RingedToposModules.TwoMorphismOfRingedTopoi.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS (schemeSpaceMap g)).toRingedToposModulesHom
      (smallEtaleRingedToposHom B S hS (schemeSpaceMap g)).toRingedToposModulesHom) :
    t = Stacks.Sheaves.RingedToposModules.TwoMorphismOfRingedTopoi.id.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS (schemeSpaceMap g)).toRingedToposModulesHom

Tag 04LW, a lemma

Tag 04LW in the Stacks Project.

AlgebraicGeometry.eq_of_smallEtale_twoIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/Faithful.lean, line 441.

Stacks 04LW. Let X and Y be schemes. Two morphisms a, b : X ⟶ Y for which there is a 2-isomorphism (a_small, a_small^♯) ≅ (b_small, b_small^♯) in the 2-category of ringed topoi are equal.

The hypotheses are the data of such a 2-isomorphism: an isomorphism t of the direct images, and the commutation of t with the two structure maps.

public theorem eq_of_smallEtale_twoIso {X Y : B.Scheme} (a b : X ⟶ Y)
    (t : (smallEtaleBaseChange B a).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property) ≅
      (smallEtaleBaseChange B b).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property))
    (hsharp : ∀ (V : SmallEtale B Y.obj Y.property)
        (s : (SmallEtale.commRingStructureSheaf B Y.obj Y.property).obj.obj (op V)),
      (t.hom.app (setStructureSheaf B X.obj X.property)).hom.app (op V)
          ((structureSharp B a).hom.app (op V) s) =
        (structureSharp B b).hom.app (op V) s) :
    a = b

AlgebraicGeometry.eq_of_smallEtale_twoIso_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/Faithful.lean, line 473.

Stacks 04LW, with the compatibility with the structure maps written as the commuting triangle of a 2-morphism of ringed topoi: the composite of a_small^♯ with t, evaluated at the structure sheaf of X, is b_small^♯, after forgetting the ring structure of the two structure sheaves, which is what a 2-morphism of topoi acts on.

public theorem eq_of_smallEtale_twoIso_comm {X Y : B.Scheme} (a b : X ⟶ Y)
    (t : (smallEtaleBaseChange B a).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property) ≅
      (smallEtaleBaseChange B b).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property))
    (hsharp : (sheafCompose (SmallEtale.topology B Y.obj Y.property)
            (forget CommRingCat.{u})).map (structureSharp B a) ≫
          t.hom.app ((sheafCompose (SmallEtale.topology B X.obj X.property)
            (forget CommRingCat.{u})).obj
            (SmallEtale.commRingStructureSheaf B X.obj X.property)) =
        (sheafCompose (SmallEtale.topology B Y.obj Y.property)
          (forget CommRingCat.{u})).map (structureSharp B b)) :
    a = b

AlgebraicGeometry.eq_of_smallEtaleRingedToposHom_twoIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/RingedToposTwoIso.lean, line 86.

Stacks 04LW, in the 2-category of ringed topoi. Two morphisms of schemes a, b : X ⟶ Y for which (a_small, a_small^♯) and (b_small, b_small^♯) are 2-isomorphic are equal.

theorem eq_of_smallEtaleRingedToposHom_twoIso (a b : X ⟶ Y)
    (t : RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} (smallEtaleRingedToposHom B a)
      (smallEtaleRingedToposHom B b)) :
    a = b

AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/RingedToposTwoIso.lean, line 99. The attribute's comment: “the uniqueness clause of 04I6”.

The uniqueness half of Stacks 04I6. A morphism of ringed topoi between the small étale ringed topoi of two schemes is 2-isomorphic to (f_small, f_small^♯) for at most one morphism of schemes f : X ⟶ Y.

theorem eq_of_twoIso_smallEtaleRingedToposHom
    (g : RingedToposHom
      (RingedSite.toRingedTopos (smallEtaleRingedSite B X.obj X.property))
      (RingedSite.toRingedTopos (smallEtaleRingedSite B Y.obj Y.property)))
    (a b : X ⟶ Y)
    (ta : RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g (smallEtaleRingedToposHom B a))
    (tb : RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g (smallEtaleRingedToposHom B b)) :
    a = b

Tag 04I6, a lemma

Tag 04I6 in the Stacks Project.

AlgebraicGeometry.exists_schemeHom_twoIso_of_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/AffineExistence.lean, line 212. The attribute's comment: “the existence clause: 2-isomorphic to some (f_small, f_small^sharp)”.

The existence half of [Stacks Project, Tag 04I6]. Let X and Y be schemes of a big étale site with Y affine, and let

(g, g^♯) : (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y)

be a morphism of locally ringed topoi. Then there is a morphism of schemes f : X ⟶ Y such that (g, g^♯) is 2-isomorphic to (f_{small}, f_{small}^♯) in the sense of [Stacks Project, Tag 04IC].

This is the half of the tag that has content; uniqueness is AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom, i.e. [Stacks Project, Tag 04LW], and needs no hypothesis, so it upgrades this to the ∃! of AlgebraicGeometry.existsUnique_schemeHom_twoIso_of_isLocallyRinged for free. The affineness of X, which the tag assumes, is not needed; see the module documentation.

theorem exists_schemeHom_twoIso_of_isLocallyRinged (hg : g.IsLocallyRinged) :
    ∃ a : X ⟶ Y,
      Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
        (smallEtaleRingedToposHom B a))

AlgebraicGeometry.existsUnique_schemeHom_twoIso_of_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/AffineExistence.lean, line 237.

[Stacks Project, Tag 04I6]. Let X and Y be schemes of a big étale site with Y affine, and let

(g, g^♯) : (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y)

be a morphism of locally ringed topoi. Then there is a unique morphism of schemes f : X ⟶ Y such that (g, g^♯) is 2-isomorphic to (f_{small}, f_{small}^♯) in the sense of [Stacks Project, Tag 04IC].

Existence is AlgebraicGeometry.exists_schemeHom_twoIso_of_isLocallyRinged, whose content is the whole of the source's proof: the ring map on global functions and the morphism f = Spec φ it names, the comparison g⁻¹h_V ≅ h_{X ×_Y V} at the affine étale charts of Y with its stalk computation through [Stacks Project, Tag 04GX], the transport to all charts along [Stacks Project, Tag 04HR], and the agreement of the two structure maps. Uniqueness is [Stacks Project, Tag 04LW], AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom.

The tag assumes X affine as well; that hypothesis is not needed here.

theorem existsUnique_schemeHom_twoIso_of_isLocallyRinged (hg : g.IsLocallyRinged) :
    ∃! a : X ⟶ Y,
      Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
        (smallEtaleRingedToposHom B a))

Declarations registered for the tag:

• AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/RingedToposTwoIso.lean, line 109 (StacksFrontier): “the uniqueness clause: for two affine schemes and a morphism of locally ringed topoi, which this statement covers since it assumes neither”.

Tag 04I7, a theorem

Tag 04I7 in the Stacks Project.

AlgebraicGeometry.existsUnique_schemeHom_twoIso_smallEtaleRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/Existence/Assembly.lean, line 345.

Let X and Y be schemes (of a big étale site) and let (g, g^♯) : (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y) be a morphism of locally ringed topoi. Then there is a unique morphism of schemes f : X ⟶ Y such that (g, g^♯) is 2-isomorphic to (f_small, f_small^♯).

Existence: f is glued from the morphisms f_V : W_V ⟶ V over the affine opens V of Y determined by g on global sections (AlgebraicGeometry.glueHom), and the 2-isomorphism is AlgebraicGeometry.twoIsoGlueHom. Uniqueness is Stacks 04LW (AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom).

theorem existsUnique_schemeHom_twoIso_smallEtaleRingedToposHom (B : BigEtaleSite.{u})
    {X Y : B.Scheme}
    (g : RingedToposHom (RingedSite.toRingedTopos (smallEtaleRingedSite B X.obj X.property))
      (RingedSite.toRingedTopos (smallEtaleRingedSite B Y.obj Y.property)))
    (hg : g.IsLocallyRinged) :
    ∃! f : X ⟶ Y, Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
      (smallEtaleRingedToposHom B f))

Declarations registered for the tag:

• AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/RingedToposTwoIso.lean, line 113 (StacksFrontier): “the uniqueness clause, i.e. the faithfulness half of the full faithfulness asserted by the theorem”.

Sources

• Section 59.40, Tag 04JH
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.smallEtaleRingedSiteHom_isLocallyRinged · AlgebraicGeometry.Space.schemeSmallEtaleRingedToposHom_twoMorphism_eq_id · AlgebraicGeometry.Space.schemeSmallEtaleRingedToposHom_twoMorphismOfRingedTopoi_eq_id · AlgebraicGeometry.eq_of_smallEtale_twoIso · AlgebraicGeometry.eq_of_smallEtale_twoIso_comm · AlgebraicGeometry.eq_of_smallEtaleRingedToposHom_twoIso · AlgebraicGeometry.eq_of_twoIso_smallEtaleRingedToposHom · AlgebraicGeometry.exists_schemeHom_twoIso_of_isLocallyRinged

Section59.42 Property (A)#

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

Tag 04DK, a lemma

Tag 04DK in the Stacks Project.

Stacks.EtaleCohomology.smallEtalePushforwardAb_properties_of_hasPropertyA, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PropertyAPushforward.lean, line 281.

Stacks Project, Tag 04DK. Let f : X ⟶ Y be a morphism of schemes with property (A). Then direct image of abelian sheaves on the small étale sites reflects injections and surjections, the counit f^{-1} f_* F ⟶ F is surjective for every abelian sheaf F on the small étale site of X, and direct image is faithful.

public theorem smallEtalePushforwardAb_properties_of_hasPropertyA {X Y : Scheme.{u}}
    (f : X ⟶ Y) (hf : HasPropertyA f) :
    (smallEtalePushforwardAb f).ReflectsMonomorphisms ∧
      (smallEtalePushforwardAb f).ReflectsEpimorphisms ∧
      (∀ F : Sheaf (smallEtaleTopology X) Ab.{u + 1},
          Epi ((smallEtaleAdjunctionAb f).counit.app F)) ∧
      (smallEtalePushforwardAb f).Faithful

Tag 04DL, a lemma

Tag 04DL in the Stacks Project.

AlgebraicGeometry.hasPropertyA_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PropertyA.lean, line 413.

Stacks Project, Tag 04DL. A separated locally quasi-finite morphism of schemes has property (A).

theorem hasPropertyA_of_locallyQuasiFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsSeparated f] [LocallyOfFiniteType f] [LocallyQuasiFinite f] : HasPropertyA f

Tag 04DM, a lemma

Tag 04DM in the Stacks Project.

AlgebraicGeometry.hasPropertyA_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PropertyA.lean, line 672.

Stacks Project, Tag 04DM. Every integral morphism of schemes has property (A).

theorem hasPropertyA_of_isIntegralHom {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] :
    HasPropertyA f

Tag 04C9, a lemma

Tag 04C9 in the Stacks Project.

Stacks.EtaleCohomology.smallEtalePushforwardAb_properties_of_isIntegralHom_or_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralQuasiFinitePushforward.lean, line 70.

Let f : X ⟶ Y be a morphism of schemes which is either integral, or separated and locally quasi-finite. Then the counit f^{-1} f_* F ⟶ F is surjective for every abelian sheaf F on the small étale site of X, direct image of abelian sheaves along the small étale sites is faithful, and it reflects injections and surjections.

public theorem smallEtalePushforwardAb_properties_of_isIntegralHom_or_locallyQuasiFinite
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : IsIntegralHom f ∨ (IsSeparated f ∧ LocallyOfFiniteType f ∧ LocallyQuasiFinite f)) :
    (∀ F : Sheaf (smallEtaleTopology X) Ab.{u + 1},
        Epi ((smallEtaleAdjunctionAb f).counit.app F)) ∧
      (smallEtalePushforwardAb f).Faithful ∧
      (smallEtalePushforwardAb f).ReflectsMonomorphisms ∧
      (smallEtalePushforwardAb f).ReflectsEpimorphisms

Sources

• Section 59.42, Tag 04DJ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.smallEtalePushforwardAb_properties_of_hasPropertyA · AlgebraicGeometry.hasPropertyA_of_locallyQuasiFinite · AlgebraicGeometry.hasPropertyA_of_isIntegralHom · Stacks.EtaleCohomology.smallEtalePushforwardAb_properties_of_isIntegralHom_or_locallyQuasiFinite

Section59.43 Property (B)#

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

Tag 04DO, a lemma

Tag 04DO in the Stacks Project.

Stacks.EtaleCohomology.smallEtalePushforward_preservesEpimorphisms_of_hasPropertyB, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/PropertyB.lean, line 485.

Stacks Project, Tag 04DO. Let f : X ⟶ Y be a morphism of schemes with property (B). Then direct image along the induced morphism of small étale sites transforms surjections of sheaves of sets into surjections.

theorem smallEtalePushforward_preservesEpimorphisms_of_hasPropertyB {X Y : Scheme.{u}}
    (f : X ⟶ Y) (hf : HasPropertyB f) :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous
      (Type v) (smallEtaleTopology Y) (smallEtaleTopology X)).PreservesEpimorphisms

Tag 04DP, a lemma

Tag 04DP in the Stacks Project.

Stacks.EtaleCohomology.hasPropertyB_of_etaleNeighborhood_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/Basic.lean, line 333.

A morphism f : X ⟶ Y has property (B) as soon as, for every étale g : V ⟶ Y, every étale covering U of X ×ₗᵧ V and every point v of V, there is a single étale neighborhood of v over which X ×ₗᵧ V breaks up into pieces subordinate to U.

theorem hasPropertyB_of_etaleNeighborhood_decomposition
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (h : ∀ {V : Scheme.{u}} (g : V ⟶ Y) [Etale g]
      (U : (pullback f g).Cover.{u} Scheme.etalePrecoverage) (v : V),
      ∃ (N : EtaleNeighborhood V v)
        (q : pullback f (N.toBase ≫ g) ⟶ pullback f g),
        q ≫ pullback.fst f g = pullback.fst f (N.toBase ≫ g) ∧
        q ≫ pullback.snd f g = pullback.snd f (N.toBase ≫ g) ≫ N.toBase ∧
        ∃ (W : U.I₀ → Scheme.{u}) (e : (∐ W) ≅ pullback f (N.toBase ≫ g))
          (a : ∀ i, W i ⟶ U.X i),
          ∀ i, a i ≫ U.f i = Sigma.ι W i ≫ e.hom ≫ q) :
    HasPropertyB f

Tag 04DQ, a lemma

Tag 04DQ in the Stacks Project.

Stacks.EtaleCohomology.hasPropertyB_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/FiniteCaseTrim.lean, line 454.

Property (B) for a finite morphism of schemes. Every étale covering of the base change of a finite morphism admits, after a further étale covering of the base, a componentwise subordinate disjoint-union decomposition.

This is [Stacks, Tag 04DQ]. It is Stacks.EtaleCohomology.hasPropertyB_of_isFinite_of_idempotents with its one remaining input, Stacks.EtaleCohomology.HasFiniteCaseDecompositionOfIdempotents, discharged by Stacks.EtaleCohomology.hasFiniteCaseDecompositionOfIdempotents.

theorem hasPropertyB_of_isFinite {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f] : HasPropertyB f

Tag 04DR, a lemma

Tag 04DR in the Stacks Project.

Stacks.EtaleCohomology.hasPropertyB_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/FiniteCaseTrim.lean, line 467.

Property (B) for an integral morphism of schemes. Every étale covering of the base change of an integral morphism admits, after a further étale covering of the base, a componentwise subordinate disjoint-union decomposition.

This is [Stacks, Tag 04DR]. The integral case is deduced from the finite case Stacks.EtaleCohomology.hasPropertyB_of_isFinite by the limit argument Stacks.EtaleCohomology.hasPropertyB_of_isIntegralHom_of_finite: an integral morphism over an affine base is a directed limit of finite ones, a finite affine étale cover of the limit descends to a finite stage, and the decomposition supplied there is transported back.

theorem hasPropertyB_of_isIntegralHom {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] :
    HasPropertyB f

Tag 04C2, a lemma

Tag 04C2 in the Stacks Project.

Stacks.EtaleCohomology.smallEtalePushforwardAb_properties_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralPushforwardExact.lean, line 151.

Stacks Project, Tag 04C2. Let f : X ⟶ Y be an integral morphism of schemes — a finite morphism, for instance. Then

1. f_{small, *} transforms surjections into surjections, on sheaves of sets and on abelian sheaves,
2. the counit f^{-1} f_* F ⟶ F is surjective for every abelian sheaf F on X_étale,
3. f_{small, *} : Ab(X_étale) ⥤ Ab(Y_étale) is faithful and reflects injections and surjections, and
4. f_{small, *} : Ab(X_étale) ⥤ Ab(Y_étale) is exact.

The seven conjuncts are, in order: part (1) on sheaves of sets, part (1) on abelian sheaves, part (2), the three assertions of part (3), and part (4).

public theorem smallEtalePushforwardAb_properties_of_isIntegralHom {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsIntegralHom f] :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (u + 1)) (smallEtaleTopology Y)
        (smallEtaleTopology X)).PreservesEpimorphisms ∧
      (smallEtalePushforwardAb f).PreservesEpimorphisms ∧
      (∀ F : Sheaf (smallEtaleTopology X) Ab.{u + 1},
          Epi ((smallEtaleAdjunctionAb f).counit.app F)) ∧
        (smallEtalePushforwardAb f).Faithful ∧
          (smallEtalePushforwardAb f).ReflectsMonomorphisms ∧
            (smallEtalePushforwardAb f).ReflectsEpimorphisms ∧
              exactFunctor (Sheaf (smallEtaleTopology X) Ab.{u + 1})
                (Sheaf (smallEtaleTopology Y) Ab.{u + 1}) (smallEtalePushforwardAb f)

Stacks.EtaleCohomology.etaleAbelianDirectImage_preservesEpimorphisms_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ProperBaseChange/IntegralDirectImageAcyclic.lean, line 98. The attribute's comment: “part (1) for abelian sheaves, at the coefficients of proper base change”.

Stacks 04C2, part (1), at the coefficients of the proper base change development. For an integral morphism of schemes f : X ⟶ Y — a finite morphism, for instance — direct image f_* : Ab(X_étale) ⥤ Ab(Y_étale) carries surjections of abelian sheaves with values in AddCommGrpCat.{max (u + 1) v} to surjections.

A morphism of abelian sheaves is epimorphic exactly when it is locally surjective, and local surjectivity is a property of the underlying morphism of sheaves of sets. Since the underlying sheaf of sets of a direct image is the direct image of the underlying sheaf of sets, the statement reduces to its set-valued counterpart, which is stated for an arbitrary coefficient universe.

public theorem etaleAbelianDirectImage_preservesEpimorphisms_of_isIntegralHom
    (f : X ⟶ Y) [IsIntegralHom f] :
    (etaleAbelianDirectImage.{u, v} f).PreservesEpimorphisms

Stacks.EtaleCohomology.preservesFiniteColimits_etaleAbelianDirectImage_of_isIntegralHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ProperBaseChange/IntegralDirectImageAcyclic.lean, line 134. The attribute's comment: “part (2) for abelian sheaves, at the coefficients of proper base change”.

Stacks 04C2, part (2), at the coefficients of the proper base change development. For an integral morphism f : X ⟶ Y, direct image of abelian sheaves on the small étale sites preserves finite colimits.

Direct image is a right adjoint, so it preserves finite limits and is therefore additive; it preserves epimorphisms because f is integral; and an additive functor between abelian categories which preserves kernels and epimorphisms preserves homology, hence finite colimits as well.

public instance preservesFiniteColimits_etaleAbelianDirectImage_of_isIntegralHom
    (f : X ⟶ Y) [IsIntegralHom f] :
    PreservesFiniteColimits (etaleAbelianDirectImage.{u, v} f)

AlgebraicGeometry.Space.smallEtalePushforward_preservesEpimorphisms_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralPushforwardExact.lean, line 70. The attribute's comment: “part (1), for an integral morphism of algebraic spaces”.

Stacks 04C2, part (1), for an integral morphism of algebraic spaces. The small étale direct image of sheaves of sets along an integral morphism of algebraic spaces over S transforms surjections into surjections.

A scheme atlas a : yoneda.obj T ⟶ Y of the target is chosen, and the base change of f along it is taken from the representability witness that Stacks 03ZQ attaches to an integral morphism: that produces an object P of the site, a morphism s : P ⟶ T and a Cartesian square exhibiting yoneda.map s as the base change. Its underlying morphism of schemes is integral, so AlgebraicGeometry.Space.representedSmallEtalePushforward_preservesEpimorphisms applies, and AlgebraicGeometry.Space.smallEtalePushforward_preservesEpimorphisms_of_etaleCover carries the conclusion back to f.

theorem smallEtalePushforward_preservesEpimorphisms_of_isIntegralHom
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom) :
    Functor.PreservesEpimorphisms (smallToposMorphism B S hS f).pushforward

Sources

• Section 59.43, Tag 04DN
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.smallEtalePushforward_preservesEpimorphisms_of_hasPropertyB · Stacks.EtaleCohomology.hasPropertyB_of_etaleNeighborhood_decomposition · Stacks.EtaleCohomology.hasPropertyB_of_isFinite · Stacks.EtaleCohomology.hasPropertyB_of_isIntegralHom · Stacks.EtaleCohomology.smallEtalePushforwardAb_properties_of_isIntegralHom · Stacks.EtaleCohomology.etaleAbelianDirectImage_preservesEpimorphisms_of_isIntegralHom · Stacks.EtaleCohomology.preservesFiniteColimits_etaleAbelianDirectImage_of_isIntegralHom · AlgebraicGeometry.Space.smallEtalePushforward_preservesEpimorphisms_of_isIntegralHom

Section59.44 Property (C)#

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

Tag 04DT, a lemma

Tag 04DT in the Stacks Project.

Stacks.EtaleCohomology.smallEtalePushforward_reflectsMonomorphisms_of_hasPropertyC, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/PropertyCPushforward.lean, line 87. The attribute's comment: “reflects injections”.

Stacks Project, Tag 04DT. If f : X ⟶ Y has property (C), then direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) on sheaves of sets reflects injections.

theorem smallEtalePushforward_reflectsMonomorphisms_of_hasPropertyC
    {X Y : Scheme.{u}} (f : X ⟶ Y) (hC : HasPropertyC f) :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type v)
      (smallEtaleTopology Y) (smallEtaleTopology X)).ReflectsMonomorphisms

Stacks.EtaleCohomology.smallEtalePushforward_reflectsEpimorphisms_of_hasPropertyC, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/PropertyCPushforward.lean, line 97. The attribute's comment: “reflects surjections”.

Stacks Project, Tag 04DT. If f : X ⟶ Y has property (C), then direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) on sheaves of sets reflects surjections.

theorem smallEtalePushforward_reflectsEpimorphisms_of_hasPropertyC
    {X Y : Scheme.{u}} (f : X ⟶ Y) (hC : HasPropertyC f) :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type v)
      (smallEtaleTopology Y) (smallEtaleTopology X)).ReflectsEpimorphisms

Tag 04DV, a lemma

Tag 04DV in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleBaseChange_isAlmostCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/PropertyCAlmostCocontinuous.lean, line 82.

Stacks Project, Tag 04DV. If every étale base change X ×_Y V ⟶ V of f : X ⟶ Y has property (C) and is a closed map, then base change Y.Etale ⥤ X.Etale, V ↦ X ×_Y V, is an almost cocontinuous functor of small étale sites.

theorem smallEtaleBaseChange_isAlmostCocontinuous
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hC : ∀ {V : Scheme.{u}} (v : V ⟶ Y), Etale v →
      HasPropertyC (pullback.snd f v))
    (hclosed : ∀ {V : Scheme.{u}} (v : V ⟶ Y), Etale v →
      IsClosedMap (pullback.snd f v).base) :
    IsAlmostCocontinuous (smallEtaleBaseChange f)
      (smallEtaleTopology Y) (smallEtaleTopology X)

Tag 04DW, a lemma

Tag 04DW in the Stacks Project.

Stacks.EtaleCohomology.hasPropertyC_of_isIntegralHom_of_isClosedEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/PropertyC.lean, line 341.

Stacks Project, Tag 04DW. An integral morphism of schemes which is a homeomorphism onto a closed subset of its target has property (C): every scheme étale over the source is dominated, by a surjection over the source, by the base change of a scheme étale over the target.

The étale scheme over the target is the coproduct of the one-point constructions of Stacks.EtaleCohomology.exists_etale_dominating_at_point, indexed by the points of the given étale scheme; its base change is the coproduct of their base changes by Stacks.EtaleCohomology.isPullback_pullbackFactorMap, so the one-point morphisms assemble into a single morphism, and it is surjective because every point was hit.

theorem hasPropertyC_of_isIntegralHom_of_isClosedEmbedding
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] (hf : Topology.IsClosedEmbedding f) :
    HasPropertyC f

Tag 04DX, a lemma

Tag 04DX in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleBaseChange_isAlmostCocontinuous_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 165. The attribute's comment: “(7) almost cocontinuous”.

Stacks Project, Tag 04DX, part (7). For an integral universally injective morphism of schemes f : X ⟶ Y, base change Y.Etale ⥤ X.Etale, V ↦ X ×_Y V, is almost cocontinuous as a functor of small étale sites.

Every étale base change of f has property (C) and is a closed map, which is the hypothesis of [Stacks, Tag 04DV].

public theorem
    smallEtaleBaseChange_isAlmostCocontinuous_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    IsAlmostCocontinuous (smallEtaleBaseChange f) (smallEtaleTopology Y) (smallEtaleTopology X)

Stacks.EtaleCohomology.smallEtalePushforward_reflectsMonomorphisms_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 181. The attribute's comment: “(1) reflects injections”.

Stacks Project, Tag 04DX, part (1). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) on sheaves of sets reflects injections.

This is property (C) fed to [Stacks, Tag 04DT].

public theorem
    smallEtalePushforward_reflectsMonomorphisms_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type v) (smallEtaleTopology Y)
      (smallEtaleTopology X)).ReflectsMonomorphisms

Stacks.EtaleCohomology.smallEtalePushforward_reflectsEpimorphisms_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 195. The attribute's comment: “(1) reflects surjections”.

Stacks Project, Tag 04DX, part (1). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) on sheaves of sets reflects surjections.

This is property (C) fed to [Stacks, Tag 04DT].

public theorem
    smallEtalePushforward_reflectsEpimorphisms_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type v) (smallEtaleTopology Y)
      (smallEtaleTopology X)).ReflectsEpimorphisms

Stacks.EtaleCohomology.smallEtalePushforward_preservesConnectedColimits_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 212. The attribute's comment: “(2) finite connected colimits”.

Stacks Project, Tag 04DX, part (2). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) on sheaves of sets preserves colimits of every connected shape whose colimits exist. In particular it commutes with pushouts and coequalizers, and more generally with finite connected colimits.

This is almost cocontinuity of the base-change functor fed to [Stacks, Tag 04BA].

public theorem
    smallEtalePushforward_preservesConnectedColimits_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f]
    (I : Type) [SmallCategory I] [IsConnected I]
    [HasColimitsOfShape I (Type (max (u + 1) v))] :
    PreservesColimitsOfShape I
      ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
        (smallEtaleTopology Y) (smallEtaleTopology X))

Stacks.EtaleCohomology.smallEtalePushforward_preservesEpimorphisms_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 236. The attribute's comment: “(3) preserves surjections”.

Stacks Project, Tag 04DX, part (3). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) carries surjections of sheaves of sets to surjections.

Universal injectivity is not needed here: integrality alone gives property (B), which is the hypothesis of [Stacks, Tag 04DO].

public theorem
    smallEtalePushforward_preservesEpimorphisms_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type v) (smallEtaleTopology Y)
      (smallEtaleTopology X)).PreservesEpimorphisms

Stacks.EtaleCohomology.smallEtalePushforwardAb_preservesEpimorphisms_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 252. The attribute's comment: “(3) preserves surjections”.

Stacks Project, Tag 04DX, part (3). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Ab(X_étale) ⥤ Ab(Y_étale) carries surjections of abelian sheaves to surjections.

A morphism of abelian sheaves is epimorphic exactly when it is locally surjective, and local surjectivity is a property of the underlying morphism of sheaves of sets. Since the underlying sheaf of sets of a direct image is the direct image of the underlying sheaf of sets, the statement reduces to its set-valued counterpart.

public theorem
    smallEtalePushforwardAb_preservesEpimorphisms_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    (smallEtalePushforwardAb f).PreservesEpimorphisms

Stacks.EtaleCohomology.smallEtaleAdjunction_counit_epi_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 276. The attribute's comment: “(4) surjective counit”.

Stacks Project, Tag 04DX, part (4). For an integral universally injective morphism of schemes f : X ⟶ Y, the counit f^{-1} f_* F ⟶ F of the inverse-image/direct-image adjunction is surjective for every sheaf of sets F on the small étale site of X.

A right adjoint which reflects surjections has surjective counit, by [Stacks, Tag 04D6]; direct image reflects surjections by part (1).

public theorem smallEtaleAdjunction_counit_epi_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f]
    (F : Sheaf (smallEtaleTopology X) (Type (max (u + 1) v))) :
    Epi ((Functor.sheafAdjunctionContinuous (smallEtaleBaseChange f) (Type (max (u + 1) v))
      (smallEtaleTopology Y) (smallEtaleTopology X)).counit.app F)

Stacks.EtaleCohomology.smallEtaleAdjunctionAb_counit_epi_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 293. The attribute's comment: “(4) surjective counit”.

Stacks Project, Tag 04DX, part (4). For an integral universally injective morphism of schemes f : X ⟶ Y, the counit f^{-1} f_* F ⟶ F of the inverse-image/direct-image adjunction is surjective for every abelian sheaf F on the small étale site of X.

Integrality alone gives property (A), from which this is one of the conclusions of [Stacks, Tag 04DK].

public theorem smallEtaleAdjunctionAb_counit_epi_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f]
    (F : Sheaf (smallEtaleTopology X) Ab.{u + 1}) :
    Epi ((smallEtaleAdjunctionAb f).counit.app F)

Stacks.EtaleCohomology.smallEtalePushforward_faithful_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 307. The attribute's comment: “(5) faithful”.

Stacks Project, Tag 04DX, part (5). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Sh(X_étale) ⥤ Sh(Y_étale) on sheaves of sets is faithful.

A right adjoint with surjective counit is faithful, by [Stacks, Tag 04D6]; the counit is surjective by part (4).

public theorem smallEtalePushforward_faithful_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
      (smallEtaleTopology Y) (smallEtaleTopology X)).Faithful

Stacks.EtaleCohomology.smallEtalePushforwardAb_faithful_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 323. The attribute's comment: “(5) faithful”.

Stacks Project, Tag 04DX, part (5). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Ab(X_étale) ⥤ Ab(Y_étale) on abelian sheaves is faithful.

Integrality alone gives property (A), from which this is one of the conclusions of [Stacks, Tag 04DK].

public theorem smallEtalePushforwardAb_faithful_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    (smallEtalePushforwardAb f).Faithful

Stacks.EtaleCohomology.smallEtalePushforwardAb_exact_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Descent/IntegralUniversallyInjective.lean, line 337. The attribute's comment: “(6) exact on abelian sheaves”.

Stacks Project, Tag 04DX, part (6). For an integral universally injective morphism of schemes f : X ⟶ Y, direct image f_{small, *} : Ab(X_étale) ⥤ Ab(Y_étale) is an exact functor.

Direct image is a right adjoint, so it preserves finite limits and is therefore additive; it preserves epimorphisms by part (3); and an additive functor between abelian categories which preserves finite limits and epimorphisms preserves finite colimits as well.

public theorem smallEtalePushforwardAb_exact_of_isIntegralHom_of_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] :
    exactFunctor (Sheaf (smallEtaleTopology X) Ab.{u + 1})
      (Sheaf (smallEtaleTopology Y) Ab.{u + 1}) (smallEtalePushforwardAb f)

AlgebraicGeometry.Space.smallBaseChange_isAlmostCocontinuous_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartBaseChangeAlmostCocontinuous.lean, line 482. The attribute's comment: “part (7) for algebraic spaces: chart base change is almost cocontinuous”.

The space-level analogue of [Stacks, Tag 04DX], part (7). Let f : Z ⟶ X be a representable morphism of algebraic spaces over S such that every base-change projection of schemes U ×_X Z ⟶ U at an étale chart U of X is integral and universally injective — for instance a closed immersion. Then base change of étale scheme charts along f,

X_étale ⥤ Z_étale, U ↦ U ×_X Z,

is almost cocontinuous for the small étale topologies.

Integrality makes each chart base change universally closed, hence a closed map, and together with universal injectivity a homeomorphism onto a closed subset of the chart, which is the hypothesis of [Stacks, Tag 04DW] and so gives property (C). Those are the two inputs of the space-level [Stacks, Tag 04DV].

theorem smallBaseChange_isAlmostCocontinuous_of_isIntegralHom_of_universallyInjective
    (f : Z ⟶ X) (hf : yoneda.relativelyRepresentable f.hom)
    (hint : ∀ U : SmallEtale B S hS X.1, AlgebraicGeometry.IsIntegralHom
      ((BigFppfOver.toScheme B S hS).map (hf.snd U.1.hom)))
    (huniv : ∀ U : SmallEtale B S hS X.1, AlgebraicGeometry.UniversallyInjective
      ((BigFppfOver.toScheme B S hS).map (hf.snd U.1.hom))) :
    IsAlmostCocontinuous (smallBaseChange B S hS f hf)
      (SmallEtale.topology B S hS X.1) (SmallEtale.topology B S hS Z.1)

Sources

• Section 59.44, Tag 04DS
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.smallEtalePushforward_reflectsMonomorphisms_of_hasPropertyC · Stacks.EtaleCohomology.smallEtalePushforward_reflectsEpimorphisms_of_hasPropertyC · Stacks.EtaleCohomology.smallEtaleBaseChange_isAlmostCocontinuous · Stacks.EtaleCohomology.hasPropertyC_of_isIntegralHom_of_isClosedEmbedding · Stacks.EtaleCohomology.smallEtaleBaseChange_isAlmostCocontinuous_of_isIntegralHom_of_universallyInjective · Stacks.EtaleCohomology.smallEtalePushforward_reflectsMonomorphisms_of_isIntegralHom_of_universallyInjective · Stacks.EtaleCohomology.smallEtalePushforward_reflectsEpimorphisms_of_isIntegralHom_of_universallyInjective · Stacks.EtaleCohomology.smallEtalePushforward_preservesConnectedColimits_of_isIntegralHom_of_universallyInjective

Section59.45 Topological invariance of the small étale site#

Section 59.45 of the Stacks Project, Tag 04DY. 6 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BTY, a theorem

Tag 0BTY in the Stacks Project.

Stacks.Etale.bijective_baseChange_hom_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance.lean, line 209. References: EGA IV (18.1.3), “more general”; SGA 3 X (2.0), “full faithfulness”.

Stacks Project, Tag 0BTY. Let g : S' ⟶ S be a universal homeomorphism and let X be a scheme étale over S. For every scheme Y over S, base change along g is a bijection from the S-morphisms Y ⟶ X to the S'-morphisms between the base changes of Y and X.

theorem bijective_baseChange_hom_of_universalHomeomorphism
    {S S' : Scheme.{u}} (g : S' ⟶ S) [UniversalHomeomorphism g] (X Y : Over S) [Etale X.hom] :
    Function.Bijective (fun f : Y ⟶ X => (Over.pullback g).map f)

Stacks.EtaleCohomology.smallEtaleBaseChange_full_of_universalHomeomorphism, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/Fullness.lean, line 78. The attribute's comment: “fullness of base change on the small étale site”.

Base change along a universal homeomorphism is full on small étale sites. For V and W étale over Y, every morphism X ×_Y V ⟶ X ×_Y W over X is the base change of a morphism V ⟶ W over Y.

This is Stacks Project, Tag 0BTY read on the small étale site; the content is Stacks.Etale.bijective_pullbackHom_of_universalHomeomorphism.

instance smallEtaleBaseChange_full_of_universalHomeomorphism (f : X ⟶ Y)
    [UniversalHomeomorphism f] : (smallEtaleBaseChange f).Full

Stacks.Etale.bijective_pullbackHom_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/MorphismDescent.lean, line 256. References: EGA IV (18.1.3), “more general”; EGA IV (2.2.16), “special case”; SGA 1 IX (3.1), “special case”; SGA 1 IX (4.10), “full faithfulness”; SGA 3 X (2.0), “full faithfulness”.

Stacks Project, Tag 0BTY. Let f : X ⟶ Y be a universal homeomorphism and let A be a scheme étale over Y. For every scheme B over Y, base change along f is a bijection from the Y-morphisms B ⟶ A to the X-morphisms between the base changes.

Injectivity holds for any surjective f, by Stacks.Etale.injective_baseChange_hom_of_universalHomeomorphism; surjectivity is Stacks.Etale.exists_hom_of_pullbackHom_of_universalHomeomorphism.

theorem bijective_pullbackHom_of_universalHomeomorphism {X Y : Scheme.{u}} (f : X ⟶ Y)
    [UniversalHomeomorphism f] (A B : Over Y) [Etale A.hom] :
    Function.Bijective (fun h : B ⟶ A => (Over.pullback f).map h)

Tag 0BTZ, an equation

Tag 0BTZ in the Stacks Project.

AlgebraicGeometry.etaleDescentDataForget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Descent.lean, line 79.

The functor forgetting the descent isomorphism of an étale descent datum relative to S' ⟶ S, retaining its underlying étale scheme over S'.

def etaleDescentDataForget {S S' : Scheme.{u}} (g : S' ⟶ S)
    [UniversalHomeomorphism g] : EtaleDescentData g ⥤ EtaleOver S'

Tag 04DZ, a theorem

Tag 04DZ in the Stacks Project.

Stacks.Etale.isEquivalence_etalePullback_of_integral_universallyInjective_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/AffineEtaleDescentStep.lean, line 427. The attribute's comment: “base change V ↦ X ×_Y V along an integral, universally injective and surjective morphism f : X ⟶ Y is an equivalence Y_étale ⥤ X_étale: full faithfulness is Tag 0BTY, and essential surjectivity is glued, by Schemes 01JA and 01JC, from the affine case, the induction Stacks.Etale.essSurjAffineEtalePullback_of_etaleDescent of the source's second proof on a bound for the degree of the fibres, descending at each step by Tag 0245 as Stacks.Etale.etaleDescentAlongAffineEtaleSurjection.”. References: EGA IV (18.1.2), “more general”; SGA 1 IX (4.10); SGA 4 VIII (1.1), “partial”.

Topological invariance of the small étale site, Stacks Project, Tag 04DZ. Let f : X ⟶ Y be integral, universally injective and surjective. Then V ↦ X ×_Y V is an equivalence from the category of schemes étale over Y to the category of schemes étale over X.

The reduction to the affine case, Stacks.Etale.exists_etale_pullback_iso_of_essSurjAffine, is supplied with that affine case (Stacks Project, Tag 04E0), obtained here from Stacks.Etale.essSurjAffineEtalePullback_of_etaleDescent and the descent step Stacks.Etale.etaleDescentAlongAffineEtaleSurjection.

theorem isEquivalence_etalePullback_of_integral_universallyInjective_surjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] [UniversallyInjective f] [Surjective f] :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) f := ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun pb hg ↦ MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    (show Y.Etale ⥤ X.Etale from
      MorphismProperty.Over.pullback
        (@Etale : MorphismProperty Scheme.{u}) ⊤ f).IsEquivalence

Stacks.Etale.etalePullback_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/DescentEffective.lean, line 546. The attribute's comment: “the equivalence, unconditionally. Full faithfulness is Tag 0BTY; essential surjectivity is the affine case Stacks.Etale.essSurjAffineEtalePullback glued over an affine cover by Stacks.Etale.exists_etale_pullback_iso_of_essSurjAffine. The name Stacks.Etale.etalePullback_isEquivalence_of_integral_universallyInjective_surjective is an alias of this declaration and keeps the tag as well.”. References: EGA IV (18.1.2), “more general”; SGA 1 IX (4.10); SGA 4 VIII (1.1), “partial”.

Topological invariance of the small étale site. Let f : X ⟶ Y be integral, universally injective and surjective. Then V ↦ X ×_Y V is an equivalence from the category of schemes étale over Y to the category of schemes étale over X.

Essential surjectivity is Stacks.Etale.exists_etale_pullback_iso_of_essSurjAffine with its hypothesis discharged by Stacks.Etale.essSurjAffineEtalePullback.

theorem etalePullback_isEquivalence (f : X ⟶ Y) [IsIntegralHom f]
    [UniversallyInjective f] [Surjective f] :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) f := ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun pb hg ↦ MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    (show Y.Etale ⥤ X.Etale from
      MorphismProperty.Over.pullback
        (@Etale : MorphismProperty Scheme.{u}) ⊤ f).IsEquivalence

Stacks.Etale.etalePullback_isEquivalence_of_integral_universallyInjective_surjective, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/DescentEffective.lean, line 574. The attribute's comment: “Full faithfulness is unconditional, from Tag 0BTY. A scheme etale over X is covered by affine opens lying over affine opens of Y, and the glueing of Schemes 01JA and 01JC -- in this library exists_etale_pullback_iso_of_descendedOpens_cover -- assembles the local descents into a global one. Essential surjectivity is thereby reduced to the affine case, the essential surjectivity of the correspondence displayed as Tag 04E0, which is proved unconditionally as Stacks.Etale.essSurjAffineEtalePullback by the source's induction on a bound for the degree of the fibres of an etale morphism of affine schemes. This name is an alias of Stacks.Etale.etalePullback_isEquivalence. The source's hypotheses are stated in their own form, as integrality, universal injectivity and surjectivity, and converted by Tag 04DF.”.

Topological invariance of the small étale site. Let f : X ⟶ Y be integral, universally injective and surjective. Then V ↦ X ×_Y V is an equivalence from the category of schemes étale over Y to the category of schemes étale over X.

alias etalePullback_isEquivalence_of_integral_universallyInjective_surjective

Tag 04E0, an equation

Tag 04E0 in the Stacks Project.

Stacks.Etale.affineEtalePullback_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/AffineCase.lean, line 234. The attribute's comment: “Full faithfulness of the displayed correspondence and the preservation of affineness only, both unconditional: full faithfulness is Tag 0BTY read on the affine objects, and base change carries an affine etale Y-scheme to an affine etale X-scheme because a universal homeomorphism is an affine morphism (Tag 04DF). Essential surjectivity, which is the content the source proves about this correspondence, is NOT delivered here. The source obtains it by induction on a bound for the degree of the fibres of an etale morphism of affine schemes, descending at each step by effectivity of affine descent, Tag 0245; that induction is not formalized in this library, although Tag 0245 itself is carried, by AlgebraicGeometry.DescentData.isFamilyEffective_of_isAffineHom, as are the other tags it cites (04DW, 03WS, 03JA, 03WU, 02VN). The alternative route, through effectivity of etale descent along a surjective integral morphism (Tag 0BTP), has only its fully faithful half carried, by AlgebraicGeometry.fullyFaithful_quasiCompactSeparatedEtaleDescentFunctor_of_isIntegralHom. Given essential surjectivity, this restricted functor is an equivalence, by affineEtalePullback_isEquivalence_of_essSurjAffine.”.

The affine correspondence of Stacks Project, Tag 04E0: its unconditional half. Let f : X ⟶ Y be a universal homeomorphism of affine schemes. Base change along f carries an affine scheme étale over Y to an affine scheme étale over X, and the induced functor between the affine objects of the two small étale sites is full and faithful.

theorem affineEtalePullback_fullyFaithful (f : X ⟶ Y) [UniversalHomeomorphism f]
    [IsAffine X] [IsAffine Y] :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) f := ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun pb hg ↦ MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    let F : Y.Etale ⥤ X.Etale :=
      MorphismProperty.Over.pullback (@Etale : MorphismProperty Scheme.{u}) ⊤ f
    let PY : ObjectProperty Y.Etale := fun V ↦ IsAffine V.left
    let PX : ObjectProperty X.Etale := fun U ↦ IsAffine U.left
    ∃ h : ∀ V : PY.FullSubcategory, PX (F.obj V.obj),
      (PX.lift (PY.ι ⋙ F) h).Full ∧ (PX.lift (PY.ι ⋙ F) h).Faithful

Stacks.Etale.affineEtalePullback_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/DescentEffective.lean, line 517. The attribute's comment: “the displayed correspondence, in full and unconditionally. Its three clauses are covered as follows. Preservation of affineness and full faithfulness are Stacks.Etale.affineEtalePullback_fullyFaithful, which carries the tag too. Essential surjectivity -- the content the source proves, by induction on a bound for the degree of the fibres of an etale morphism of affine schemes, descending at each step by effectivity of descent -- is Stacks.Etale.essSurjAffineEtalePullback. This declaration is the equivalence the three together give, assembled by Stacks.Etale.affineEtalePullback_isEquivalence_of_essSurjAffine. The source's induction runs through Stacks.Etale.essSurjAffineEtalePullback_of_inductiveStep_surjective, whose step is Stacks.Etale.exists_affine_etale_pullback_iso_of_surjective; its one descent along an etale covering of the target is Stacks.Etale.exists_affine_etale_pullback_iso_of_descentIso, where effectivity enters as Tag 02W8 rather than as the source's Tag 0245.”.

The affine correspondence of Stacks Project, Tag 04E0. Let f : X ⟶ Y be a universal homeomorphism of affine schemes. Base change along f carries an affine scheme étale over Y to an affine scheme étale over X, and the induced functor between the affine objects of the two small étale sites is an equivalence.

This is Stacks.Etale.affineEtalePullback_isEquivalence_of_essSurjAffine with its hypothesis discharged by Stacks.Etale.essSurjAffineEtalePullback.

theorem affineEtalePullback_isEquivalence (f : X ⟶ Y) [UniversalHomeomorphism f]
    [IsAffine X] [IsAffine Y] :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) f := ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun pb hg ↦ MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    let F : Y.Etale ⥤ X.Etale :=
      MorphismProperty.Over.pullback (@Etale : MorphismProperty Scheme.{u}) ⊤ f
    let PY : ObjectProperty Y.Etale := fun V ↦ IsAffine V.left
    let PX : ObjectProperty X.Etale := fun U ↦ IsAffine U.left
    ∃ h : ∀ V : PY.FullSubcategory, PX (F.obj V.obj),
      (PX.lift (PY.ι ⋙ F) h).IsEquivalence

Tag 05YX, a remark

Tag 05YX in the Stacks Project.

Stacks.Etale.affineEtalePullback_isEquivalence_of_essSurj_of_h09YZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvarianceAffine.lean, line 81. The attribute's comment: “assuming essential surjectivity of etale pullback (the content of Stacks 04DZ) and Stacks 09YZ over a qcqs base”.

Topological invariance of the étale site on affine objects. Base change along a universal homeomorphism f : X ⟶ Y restricts to an equivalence between the full subcategory of affine objects of the small étale site of Y and the full subcategory of affine objects of the small étale site of X.

The hypothesis hessSurj is essential surjectivity of base change on the whole small étale site, part of Stacks Project, Tag 04DZ, and h09YZ is Stacks Project, Tag 09YZ over a quasi-compact quasi-separated base, the input of Stacks Project, Tag 05YU.

theorem affineEtalePullback_isEquivalence_of_essSurj_of_h09YZ
    {X Y : Scheme.{u}} (f : X ⟶ Y) [UniversalHomeomorphism f]
    (hessSurj :
      letI : MorphismProperty.HasPullbacksAlong
          (@Etale : MorphismProperty Scheme.{u}) f := ⟨fun _ _ ↦ inferInstance⟩
      letI : MorphismProperty.IsStableUnderBaseChangeAlong
          (@Etale : MorphismProperty Scheme.{u}) f :=
        ⟨fun pb hg ↦ MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
      (show Y.Etale ⥤ X.Etale from
        MorphismProperty.Over.pullback
          (@Etale : MorphismProperty Scheme.{u}) ⊤ f).EssSurj)
    (h09YZ : IntegralHasFinitePresentationLimit.{u}) :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun pb hg ↦
        MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    let F : Y.Etale ⥤ X.Etale :=
      MorphismProperty.Over.pullback
        (@Etale : MorphismProperty Scheme.{u}) ⊤ f
    let PY : ObjectProperty Y.Etale := fun V ↦ IsAffine V.left
    let PX : ObjectProperty X.Etale := fun U ↦ IsAffine U.left
    ∃ (h : ∀ V : PY.FullSubcategory, PX (F.obj V.obj)),
      (PX.lift (PY.ι ⋙ F) h).IsEquivalence

Stacks.Etale.affineEtalePullback_isEquivalence_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvarianceAffineEquivalence.lean, line 46. The attribute's comment: “base change along a universal homeomorphism restricts to an equivalence between the affine schemes etale over the target and the affine schemes etale over the source”. References: SGA 4½ Th finitude (2.7), “partial”.

Topological invariance of the étale site on affine objects. Let f : X ⟶ Y be a universal homeomorphism. Base change V ↦ X ×_Y V along f carries an affine scheme étale over Y to an affine scheme étale over X, and the induced functor from the full subcategory of affine objects of the small étale site of Y to the full subcategory of affine objects of the small étale site of X is an equivalence.

theorem affineEtalePullback_isEquivalence_of_universalHomeomorphism
    {X Y : Scheme.{u}} (f : X ⟶ Y) [UniversalHomeomorphism f] :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) f :=
      ⟨fun pb hg ↦
        MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    let F : Y.Etale ⥤ X.Etale :=
      MorphismProperty.Over.pullback
        (@Etale : MorphismProperty Scheme.{u}) ⊤ f
    let PY : ObjectProperty Y.Etale := fun V ↦ IsAffine V.left
    let PX : ObjectProperty X.Etale := fun U ↦ IsAffine U.left
    ∃ (h : ∀ V : PY.FullSubcategory, PX (F.obj V.obj)),
      (PX.lift (PY.ι ⋙ F) h).IsEquivalence

Tag 03SI, a proposition

Tag 03SI in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleSite_iso_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/SiteIsomorphism.lean, line 88. The attribute's comment: “part (1): the isomorphism of sites, as the equivalence of the small etale categories induced by base change together with the correspondence of covering sieves. The source's hypothesis is a universal homeomorphism, which is this statement's hypothesis as well.”. References: SGA 1 IX (1.7), “more general”; SGA 1 IX (4.10); SGA 4 XIV (1.11), “more general”; SGA 4½ Th finitude (2.7), “more general”.

Part (1) of Stacks Project, Tag 03SI: the small étale sites of a universal homeomorphism are isomorphic. Let f : X ⟶ Y be a universal homeomorphism. Base change along f is an equivalence from the small étale category of Y to that of X, and a sieve on a scheme étale over Y is covering exactly when its image under base change is covering.

The equivalence of categories is Stacks Project, Tag 04DZ; the correspondence of coverings holds for any surjection.

theorem smallEtaleSite_iso_of_universalHomeomorphism (f : X ⟶ Y) [UniversalHomeomorphism f] :
    (smallEtaleBaseChange f).IsEquivalence ∧
      ∀ (V : Y.Etale) (S : Sieve V),
        S.functorPushforward (smallEtaleBaseChange f) ∈
            smallEtaleTopology X ((smallEtaleBaseChange f).obj V) ↔
          S ∈ smallEtaleTopology Y V

Stacks.EtaleCohomology.smallEtaleInverseImage_isEquivalence_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvarianceCohomology.lean, line 65. The attribute's comment: “part (2), equivalence of the small étale topoi”.

Stacks 03SI, part (2). For a universal homeomorphism f : X ⟶ Y the small étale topoi of X and Y are equivalent: the canonical inverse-image functor on sheaves of types is an equivalence of categories.

theorem smallEtaleInverseImage_isEquivalence_of_universalHomeomorphism :
    (smallEtaleInverseImage.{u, v} f).IsEquivalence

Stacks.EtaleCohomology.etaleCohomologyRestrictionMap_bijective_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvarianceCohomology.lean, line 82. The attribute's comment: “part (3), agreement of étale cohomology”.

Stacks 03SI, part (3). For a universal homeomorphism f : X ⟶ Y étale cohomology agrees in every degree: restriction along f is bijective on H^q of every abelian sheaf on the small étale site of Y.

theorem etaleCohomologyRestrictionMap_bijective_of_universalHomeomorphism
    [HasSheafify X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}]
    [HasSheafify Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}]
    [HasExt.{w} (Sheaf Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    (F : Sheaf Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) (q : ℕ) :
    Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} f F q)

Sources

• Section 59.45, Tag 04DY
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Etale.bijective_baseChange_hom_of_universalHomeomorphism · Stacks.EtaleCohomology.smallEtaleBaseChange_full_of_universalHomeomorphism · Stacks.Etale.bijective_pullbackHom_of_universalHomeomorphism · AlgebraicGeometry.etaleDescentDataForget · Stacks.Etale.isEquivalence_etalePullback_of_integral_universallyInjective_surjective · Stacks.Etale.etalePullback_isEquivalence · Stacks.Etale.etalePullback_isEquivalence_of_integral_universallyInjective_surjective · Stacks.Etale.affineEtalePullback_fullyFaithful

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.