EtaleFundamentalGroups.Cohomology.hom_ext_finiteLocallyConstant_abelianStalk
Morphisms of finite locally constant abelian sheaves on a connected scheme are determined by their maps on one actual geometric stalk.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)Lean source · statement
theorem hom_ext_finiteLocallyConstant_abelianStalk
{F G : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}} (f g : F ⟶ G)
(hF : IsEtaleFiniteLocallyConstantSet
((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj F))
(hG : IsEtaleFiniteLocallyConstantSet
((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj G))
(h : (Scheme.pointSmallEtale ξ).sheafFiber.map f =
(Scheme.pointSmallEtale ξ).sheafFiber.map g) : f = g