Documentation

TauCeti.Topology.Sheaves.EtaleSpace

Local charts on the étalé space of a presheaf #

This file supplies the local-homeomorphism API for the étalé space of a presheaf. A section over an open set determines a continuous section of the étalé projection, whose range consists of its germs. This range is open and gives a local chart. Consequently, the projection from the étalé space to its base is a local homeomorphism.

The construction extends the étalé-space topology and germ API in Mathlib.Topology.Sheaves.EtaleSpace. It is the topological prerequisite for applying Mathlib's abstract IsLocalHomeomorph.monodromy_theorem to analytic continuation: the remaining analytic input is separatedness of the projection, supplied by the identity theorem for holomorphic functions.

source
noncomputable def TauCeti.TopCat.Presheaf.EtaleSpace.germSection {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) :
↥U → F.EtaleSpace

A section of a presheaf, viewed as a section of the étalé projection.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.TopCat.Presheaf.EtaleSpace.germSection_apply {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) (x : ↥U) :
    germSection F U s x = { base := ↑x, germ := (CategoryTheory.ConcreteCategory.hom (F.germ U ↑x ⋯)) s }

    The germ section written out: over x, it is the pair of x and the germ of s at x. This is the characteristic property of TauCeti.TopCat.Presheaf.EtaleSpace.germSection, and the form in which a concrete germ map is identified with it.

    source
    theorem TauCeti.TopCat.Presheaf.EtaleSpace.base_germSection {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) (x : ↥U) :
    (germSection F U s x).base = ↑x
    source
    @[simp]
    theorem TauCeti.TopCat.Presheaf.EtaleSpace.germ_germSection {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) (x : ↥U) :
    cast ⋯ (germSection F U s x).germ = (CategoryTheory.ConcreteCategory.hom (F.germ U ↑x ⋯)) s
    source
    def TauCeti.TopCat.Presheaf.EtaleSpace.sectionRange {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) :
    Set F.EtaleSpace

    The open set in the étalé space swept out by the germs of a section.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.TopCat.Presheaf.EtaleSpace.mem_sectionRange_iff {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} {U : TopologicalSpace.Opens ↑X} {s : CategoryTheory.ToType (F.obj (Opposite.op U))} {g : F.EtaleSpace} :
      g ∈ sectionRange F U s ↔ ∃ (h : g.base ∈ U), g.germ = (CategoryTheory.ConcreteCategory.hom (F.germ U g.base h)) s

      Membership in the range of a germ section means being the germ of that section at the underlying base point.

      source
      theorem TauCeti.TopCat.Presheaf.EtaleSpace.isOpen_sectionRange {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) :
      IsOpen (sectionRange F U s)

      The germs of a section form an open subset of the étalé space.

      source
      theorem TauCeti.TopCat.Presheaf.EtaleSpace.germSection_injective {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) :
      Function.Injective (germSection F U s)

      A germ section is injective because the étalé projection recovers its argument.

      source
      theorem TauCeti.TopCat.Presheaf.EtaleSpace.continuous_germSection {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) :
      Continuous (germSection F U s)

      The map taking a point to the germ of a fixed section there is continuous.

      source
      theorem TauCeti.TopCat.Presheaf.EtaleSpace.isOpenEmbedding_germSection {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (U : TopologicalSpace.Opens ↑X) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) :
      Topology.IsOpenEmbedding (germSection F U s)

      A germ section is an open embedding of its domain into the étalé space.

      source
      theorem TauCeti.TopCat.Presheaf.EtaleSpace.isLocalHomeomorph_base {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(A B : C) → FunLike (FC A B) (CC A) (CC B)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X) :
      IsLocalHomeomorph TopCat.Presheaf.EtaleSpace.base

      The projection from the étalé space of a presheaf to the base is a local homeomorphism.