Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-- presheaf of types basics and equivalence
import topology.opens topology.constructions
universes u v u₁ v₁ u₂ v₂
open topological_space
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 (le_trans hVW hUV) x)
instance (X : Type u) [topological_space X] : has_coe_to_fun (presheaf_of_typesU X) :=
⟨_, presheaf_of_typesU.F⟩
namespace topological_space.opens
variables {α : Type*} {β : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ]
def comap (f : α → β) (hf : continuous f) (U : opens β) : opens α :=
⟨f ⁻¹' U, hf _ U.2
theorem comap_id (U : opens α) : comap id continuous_id U = U := ext rfl
theorem comap_comp {f : α → β} {g : β → γ}
{hf : continuous f} {hg : continuous g} (U : opens γ) :
comap _ (hf.comp hg) U = comap _ hf (comap _ hg U) := ext rfl
theorem comap_mono {α β} [topological_space α] [topological_space β]
{f : α → β} {hf : continuous f} {U V : opens β}
(h : U ≤ V) : U.comap f hf ≤ V.comap f hf :=
λ x hx, h hx
end topological_space.opens
namespace presheaf_of_typesU
open topological_space.opens
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)
@[simp] theorem id' (U : opens X) (x : ℱ.F U) (h) : ℱ.res h x = x := ℱ.id _ _
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 ⟨f ⁻¹' V, hf _ V.2⟩,
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 (comap_mono hUV) (ρ U x))
namespace f_map
variables {𝒢 ℱ}
theorem ext {α β : f_map 𝒢 ℱ} (hf : α.f = β.f)
( : ∀ V x, α.ρ V x = ℱ.res (le_of_eq (by congr')) (β.ρ V x)) : α = β :=
begin
cases α with αf αhf αρ αnat, cases β with βf βhf βρ βnat,
cases hf,
congr', funext V x,
simpa using hρ V x
end
variables (𝒢 ℱ)
def id (ℱ : presheaf_of_typesU X) : f_map ℱ ℱ :=
{ f := λ x, x,
hf := continuous_id,
ρ := λ V x, ℱ.res (le_of_eq (comap_id _)) 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 (le_of_eq (comap_comp _)) (f𝒢ℋ.ρ _ (fℱ𝒢.ρ U x)),
nat := λ U V hUV x, by rw [fℱ𝒢.nat, f𝒢ℋ.nat, ℋ.comp, ℋ.comp] }
--set_option pp.implicit true
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ℋ𝒥) :=
f_map.ext rfl $ λ V x, begin
simp, dsimp [comp], simp [𝒥.comp], refl
end
lemma id_comp (fℱ𝒢 : f_map ℱ 𝒢) : comp (f_map.id ℱ) fℱ𝒢 = fℱ𝒢 :=
f_map.ext rfl $ λ V x, begin
simp, dsimp [comp, id], simp [𝒢.comp], rw [fℱ𝒢.nat, 𝒢.id']
end
lemma comp_id (fℱ𝒢 : f_map ℱ 𝒢) : comp fℱ𝒢 (f_map.id 𝒢) = fℱ𝒢 :=
f_map.ext rfl $ λ V x, begin
simp, dsimp [comp, id], simp [𝒢.comp]
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 := f_map.id_comp _ _ _,
right_inv := f_map.id_comp _ _ _ }
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