Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
presheaves of types (unbundled)
-- presheaf of types basics and equivalence
import topology.opens topology.constructions
universes u v u₁ v₁ u₂ v₂
open topological_space
def topological_space.opens.comap {α β} [topological_space α] [topological_space β]
(f : α → β) (hf : continuous f) (U : opens β) : opens α :=
⟨f ⁻¹' U, hf _ U.2
lemma topological_space.opens.comap_id {α} [topological_space α] (U : opens α) :
topological_space.opens.comap (λ (x : α), x) (continuous_id) U = U :=
by {ext, exact iff.rfl }
structure presheaf_of_typesT (X : Type) [topological_space X] :=
(F : opens X → Type)
(res : ∀ {U V : opens X} (h : V ⊆ U), F U → F V)
(id : ∀ (U : opens X) (x : F U), res (le_refl U) x = x)
(comp : ∀ {U V W : opens X} (hUV : V ⊆ U) (hVW : W ⊆ V) (x : F U),
res hVW (res hUV x) = res (set.subset.trans hVW hUV) x)
structure presheaf_of_typesU (X : Type u) [topological_space X] :=
(F : opens X → Type u)
(res : ∀ {U V : opens X} (h : V ⊆ U), F U → F V)
(id : ∀ (U : opens X) (x : F U), res (le_refl U) x = x)
(comp : ∀ {U V W : opens X} (hUV : V ⊆ U) (hVW : W ⊆ V) (x : F U),
res hVW (res hUV x) = res (set.subset.trans hVW hUV) x)
structure presheaf_of_typesV (X : Type u) [topological_space X] :=
(F : opens X → Type v)
(res : ∀ {U V : opens X} (h : V ⊆ U), F U → F V)
(id : ∀ (U : opens X) (x : F U), res (le_refl U) x = x)
(comp : ∀ {U V W : opens X} (hUV : V ⊆ U) (hVW : W ⊆ V) (x : F U),
res hVW (res hUV x) = res (set.subset.trans hVW hUV) x)
structure presheaf_of_typesB :=
(X : Type u)
[TX : topological_space X]
(F : opens X → Type v)
(res : ∀ {U V : opens X} (h : V ⊆ U), F U → F V)
(id : ∀ (U : opens X) (x : F U), res (le_refl U) x = x)
(comp : ∀ {U V W : opens X} (hUV : V ⊆ U) (hVW : W ⊆ V) (x : F U),
res hVW (res hUV x) = res (set.subset.trans hVW hUV) x)
-- (TODO) Can't use has_coe_to_fun because I want a function on opens X, not X
/-
instance (X : Type u) [topological_space X] : has_coe_to_fun (presheaf_of_types X) :=
{ F := λ _, Type u,
coe := ...umm... }
-/
namespace presheaf_of_typesU
variables {X : Type u} {Y : Type u} {Z : Type u} {W : Type u}
[topological_space X] [topological_space Y] [topological_space Z] [topological_space W]
(ℱ : presheaf_of_typesU X) (𝒢 : presheaf_of_typesU Y) (ℋ : presheaf_of_typesU Z)
(𝒥 : presheaf_of_typesU W)
structure morphism (ℱ 𝒢 : presheaf_of_typesU X) :=
(ρ : ∀ U : opens X, ℱ.F U → 𝒢.F U)
(nat : ∀ U V : opens X, ∀ h : V ⊆ U,
x : ℱ.F U, ρ V (ℱ.res h x) = 𝒢.res h (ρ U x))
def morphism.id (ℱ : presheaf_of_typesU X) : morphism ℱ ℱ :=
{ ρ := λ U x, x,
nat := λ U V h x, rfl
}
def morphism.comp (ℱ 𝒢 ℋ : presheaf_of_typesU X) (fℱ𝒢 : morphism ℱ 𝒢) (f𝒢ℋ : morphism 𝒢 ℋ) :
morphism ℱ ℋ :=
{ ρ := λ U x, f𝒢ℋ.ρ U (fℱ𝒢.ρ U x),
nat := λ U V h x, by rw [fℱ𝒢.nat, f𝒢ℋ.nat]
}
def pushforward {f : X → Y} (hf : continuous f) (ℱ : presheaf_of_typesU X) :
presheaf_of_typesU Y :=
{ F := λ V, ℱ.F $ V.comap f hf,
res := λ _ _ hUV, ℱ.res (λ _ hx, hUV hx),
id := λ _, ℱ.id _,
comp := λ U V W hUV hVW, ℱ.comp _ _,
}
structure f_map (𝒢 : presheaf_of_typesU Y) (ℱ : presheaf_of_typesU X) :=
(f : X → Y)
(hf : continuous f)
(ρ : ∀ V : opens Y, 𝒢.F V → ℱ.F (V.comap f hf))
(nat : ∀ U V : opens Y, ∀ hUV : V ⊆ U,
x : 𝒢.F U, ρ V (𝒢.res hUV x) = ℱ.res (by {intros x hx, exact hUV hx}) (ρ U x))
namespace f_map
def ext (α β : f_map 𝒢 ℱ) (hf : α.f = β.f) ( : α.ρ == β.ρ) : α = β :=
begin
cases α with αf αhf αρ αnat, cases β with βf βhf βρ βnat,
rw presheaf_of_typesU.f_map.mk.inj_eq,
exact ⟨hf, hρ⟩,
end
def id (ℱ : presheaf_of_typesU X) : f_map ℱ ℱ :=
{ f := λ x, x,
hf := continuous_id,
ρ := λ V x, ℱ.res (λ y hy, by rwa topological_space.opens.comap_id V at hy) x,
nat := λ U V hUV x, by rw [ℱ.comp, ℱ.comp],
}
def comp {ℱ : presheaf_of_typesU X} {𝒢 : presheaf_of_typesU Y} {ℋ : presheaf_of_typesU Z}
(fℱ𝒢 : f_map ℱ 𝒢) (f𝒢ℋ : f_map 𝒢 ℋ) : f_map ℱ ℋ :=
{ f := λ z, fℱ𝒢.f (f𝒢ℋ.f z),
hf := continuous.comp f𝒢ℋ.hf fℱ𝒢.hf,
ρ := λ U x, ℋ.res (λ y hy, by convert hy) (f𝒢ℋ.ρ _ (fℱ𝒢.ρ U x)),
nat := λ U V hUV x, by {rw [fℱ𝒢.nat, f𝒢ℋ.nat, ℋ.comp, ℋ.comp], refl} }
lemma comp_assoc {ℱ : presheaf_of_typesU X} {𝒢 : presheaf_of_typesU Y} {ℋ : presheaf_of_typesU Z}
{𝒥 : presheaf_of_typesU W} (fℱ𝒢 : f_map ℱ 𝒢) (f𝒢ℋ : f_map 𝒢 ℋ) (fℋ𝒥 : f_map ℋ 𝒥) :
comp (comp fℱ𝒢 f𝒢ℋ) fℋ𝒥 = comp fℱ𝒢 (comp f𝒢ℋ fℋ𝒥) :=
begin
apply f_map.ext, refl,
apply heq_of_eq,
ext U x,
change 𝒥.res _ _ = 𝒥.res _ (𝒥.res _ _),
rw 𝒥.comp,
congr' 2,
exact ℋ.id _ _,
end
lemma id_comp (fℱ𝒢 : f_map ℱ 𝒢) : comp (f_map.id ℱ) fℱ𝒢 = fℱ𝒢 :=
begin
unfold comp,
apply f_map.ext, refl,
apply heq_of_eq,
ext U x,
change 𝒢.res _ (fℱ𝒢.ρ ⟨(λ (x : X), x) ⁻¹' ↑U, _⟩ (ℱ.res _ x)) = fℱ𝒢.ρ U x,
rw [fℱ𝒢.nat, 𝒢.comp],
exact 𝒢.id _ _,
end
end f_map
structure presheaf_of_types_equiv (ℱ : presheaf_of_typesU X) (𝒢 : presheaf_of_typesU Y) :=
( to_fun : f_map ℱ 𝒢)
( inv_fun : f_map 𝒢 ℱ)
( left_inv : f_map.comp inv_fun to_fun = f_map.id 𝒢)
( right_inv : f_map.comp to_fun inv_fun = f_map.id ℱ)
def presheaf_of_types_equiv.refl (ℱ : presheaf_of_typesU X) :
presheaf_of_types_equiv ℱ ℱ :=
{ to_fun := f_map.id ℱ,
inv_fun := f_map.id ℱ,
left_inv := begin
unfold f_map.comp,
apply f_map.ext, refl,
apply heq_of_eq,
ext U x,
change ℱ.res _ (ℱ.res _ (ℱ.res _ x)) = ℱ.res _ x,
rw [ℱ.comp, ℱ.comp],
refl,
end,
right_inv := begin
unfold f_map.comp,
apply f_map.ext, refl,
apply heq_of_eq,
ext U x,
change ℱ.res _ (ℱ.res _ (ℱ.res _ x)) = ℱ.res _ x,
rw [ℱ.comp, ℱ.comp],
refl
end }
def presheaf_of_types_equiv.symm (ℱ : presheaf_of_typesU X) (𝒢 : presheaf_of_typesU Y)
(h : presheaf_of_types_equiv ℱ 𝒢) : presheaf_of_types_equiv 𝒢 ℱ :=
{ to_fun := h.inv_fun,
inv_fun := h.to_fun,
left_inv := h.right_inv,
right_inv := h.left_inv }
--local infix ` ** `:50 := f_map.comp
def presheaf_of_types_equiv.trans (ℱ : presheaf_of_typesU X)
(𝒢 : presheaf_of_typesU Y)
(ℋ : presheaf_of_typesU Z)
(hℱ𝒢 : presheaf_of_types_equiv ℱ 𝒢)
(h𝒢ℋ : presheaf_of_types_equiv 𝒢 ℋ)
: presheaf_of_types_equiv ℱ ℋ :=
{ to_fun := f_map.comp hℱ𝒢.to_fun h𝒢ℋ.to_fun,
inv_fun := f_map.comp h𝒢ℋ.inv_fun hℱ𝒢.inv_fun,
left_inv := by
rw [f_map.comp_assoc, ←f_map.comp_assoc hℱ𝒢.inv_fun, hℱ𝒢.left_inv,
f_map.id_comp, h𝒢ℋ.left_inv],
right_inv := by
rw [f_map.comp_assoc, ←f_map.comp_assoc h𝒢ℋ.to_fun,
h𝒢ℋ.right_inv, f_map.id_comp, hℱ𝒢.right_inv] }
end presheaf_of_typesU
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment