Etale space of a presheaf

Given a presheaf F on a topological space X, its etale space is the space of pairs (base, germ), where base is a point of X, and germ is an element of the stalk of F at base.

This space is equipped with the following topology. For each open set U and a section s of F over U, the set of germs of s at points x ∈ U is an open set in the etale space.

Main results

• TopCat.Presheaf.EtaleSpace.eventually_nhds. If s is a section of F over U with germ at g.base equal to g.germ, then a neighborhood of g consists of germs of s at points x ∈ U.

• TopCat.Presheaf.EtaleSpace.isCoveringMap_base. Let F be a presheaf with the following property.

  For each x, there exists an open neighborhood U ∋ x such that for each y ∈ U, the map Presheaf.germ F U y hyU from sections of F over U to the stalk at y is bijective.

  Then the projection from the etale space of F to the base is a covering map.

structure TopCat.Presheaf.EtaleSpace {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] (F : Presheaf C X) : Type v

Etale space of a presheaf.

• base : ↑X

  The base point.

• germ : CategoryTheory.ToType (F.stalk self.base)

  A germ at base (formally, an element of the stalk of F at base).

@[implicit_reducible]

instance TopCat.Presheaf.EtaleSpace.instTopologicalSpace {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] (F : Presheaf C X) : TopologicalSpace F.EtaleSpace

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.Presheaf.EtaleSpace.eventually_nhds {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : Presheaf C X} (g : F.EtaleSpace) {U : TopologicalSpace.Opens ↑X} (h : g.base ∈ U) (s : CategoryTheory.ToType (F.obj (Opposite.op U))) (hs : (CategoryTheory.ConcreteCategory.hom (F.germ U g.base h)) s = g.germ) : ∀ᶠ (g' : F.EtaleSpace) in nhds g, ∃ (hgU : g'.base ∈ U), g'.germ = (CategoryTheory.ConcreteCategory.hom (F.germ U g'.base hgU)) s

If s is a section of a presheaf F over U with germ at g.base equal to g.germ, then a neighborhood of g consists of germs of s at points x ∈ U.

theorem TopCat.Presheaf.EtaleSpace.continuous_base {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] (F : Presheaf C X) [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] : Continuous base

theorem TopCat.Presheaf.EtaleSpace.exists_section_of_tendsto {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : Presheaf C X} [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {α : Type u_1} {l : Filter α} {g : α → F.EtaleSpace} {g₀ : F.EtaleSpace} (h : Filter.Tendsto g l (nhds g₀)) : ∃ (U : TopologicalSpace.Opens ↑X), g₀.base ∈ U ∧ ∃ (f : CategoryTheory.ToType (F.obj (Opposite.op U))), ∀ᶠ (a : α) in l, ∃ (ha : (g a).base ∈ U), (g a).germ = (CategoryTheory.ConcreteCategory.hom (F.germ U (g a).base ha)) f

noncomputable def TopCat.Presheaf.EtaleSpace.homeomorph {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : Presheaf C X} [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (U : TopologicalSpace.Opens ↑X) (hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U x hx))) (x : ↑X) (hx : x ∈ U) : ↑(base ⁻¹' ↑U) ≃ₜ ↥U × WithDiscreteTopology (CategoryTheory.ToType (F.stalk x))

Let F be a C-valued presheaf on X. Let U be an open set on X such that for each x ∈ U, the germ map is bijective, i.e., every germ can be extended to a unique section over U.

Then for each x ∈ U, the preimage of U under EtaleSpace.base is homeomorphic to the product of U and the stalk of F at x with discrete topology.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Presheaf.EtaleSpace.homeomorph_apply_fst {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : Presheaf C X} [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (U : TopologicalSpace.Opens ↑X) (hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U x hx))) (x : ↑X) (hx : x ∈ U) (s : ↑(base ⁻¹' ↑U)) : ((homeomorph U hF_bij x hx) s).1 = ⟨(↑s).base, ⋯⟩

theorem TopCat.Presheaf.EtaleSpace.isCoveringMap_base {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasColimits C] {F : Presheaf C X} [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (hF_bij : ∀ (x : ↑X), ∃ (U : TopologicalSpace.Opens ↑X), x ∈ U ∧ ∀ (y : ↑X) (hyU : y ∈ U), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U y hyU))) : IsCoveringMap base

Let F be a presheaf with the following property.

For each x, there exists an open neighborhood U ∋ x such that for each y ∈ U, the map Presheaf.germ F U y hyU from sections of F over U to the stalk at y is bijective.

Then the projection from the etale space of F to the base is a covering map.