michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(category): define terminal, initial, indiscrete and sum category

Browse source
This commit is contained in:
Floris van Doorn 2015-09-22 13:11:33 -04:00 committed by Leonardo de Moura
parent 3c4c722afd
commit 6e23305c5d
9 changed files with 285 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
hott/algebra/category/adjoint.hlean
View file

@ -58,10 +58,14 @@ namespace category
infix `⋍`:25 := equivalence -- \backsimeq or \equiv
infix `≌`:25 := isomorphism -- \backcong or \iso
definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] (c c' : C)
: is_equiv (@(to_fun_hom F) c c') :=
definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F]
(c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
!H
definition hom_inv [reducible] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) (f : F c ⟶ F c')
: c ⟶ c' :=
(to_fun_hom F)⁻¹ᶠ f
definition hom_equiv_F_hom_F [constructor] (F : C ⇒ D)
[H : fully_faithful F] (c c' : C) : (c ⟶ c') ≃ (F c ⟶ F c') :=
equiv.mk _ !H
@ -70,17 +74,17 @@ namespace category
[H : fully_faithful F] (c c' : C) (g : F c ≅ F c') : c ≅ c' :=
begin
induction g with g G, induction G with h p q, fapply iso.MK,
{ rexact (@(to_fun_hom F) c c')⁻¹ᶠ g},
{ rexact (@(to_fun_hom F) c' c)⁻¹ᶠ h},
{ rexact (to_fun_hom F)⁻¹ᶠ g},
{ rexact (to_fun_hom F)⁻¹ᶠ h},
{ exact abstract begin
apply eq_of_fn_eq_fn' (@(to_fun_hom F) c c),
apply eq_of_fn_eq_fn' (to_fun_hom F),
rewrite [respect_comp, respect_id,
right_inv (@(to_fun_hom F) c c'), right_inv (@(to_fun_hom F) c' c), p],
right_inv (to_fun_hom F), right_inv (to_fun_hom F), p],
end end},
{ exact abstract begin
apply eq_of_fn_eq_fn' (@(to_fun_hom F) c' c'),
apply eq_of_fn_eq_fn' (to_fun_hom F),
rewrite [respect_comp, respect_id,
right_inv (@(to_fun_hom F) c c'), right_inv (@(to_fun_hom F) c' c), q],
right_inv (to_fun_hom F), right_inv (@(to_fun_hom F) c' c), q],
end end}
end
@ -197,6 +201,31 @@ namespace category
{ exact componentwise_iso (@(iso.mk (counit F)) !is_iso_counit) d}
end
definition reflect_is_iso [constructor] (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c')
[H : is_iso (F f)] : is_iso f :=
begin
fconstructor,
{ exact (to_fun_hom F)⁻¹ᶠ (F f)⁻¹},
{ apply eq_of_fn_eq_fn' (to_fun_hom F),
rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,left_inverse]},
{ apply eq_of_fn_eq_fn' (to_fun_hom F),
rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,right_inverse]},
end
definition reflect_iso [constructor] (F : C ⇒ D) [H : fully_faithful F] {c c' : C}
(f : F c ≅ F c') : c ≅ c' :=
begin
fconstructor,
{ exact (to_fun_hom F)⁻¹ᶠ f},
{ assert H : is_iso (F ((to_fun_hom F)⁻¹ᶠ f)),
{ have H' : is_iso (to_hom f), from _, exact (right_inv (to_fun_hom F) (to_hom f))⁻¹ ▸ H'},
exact reflect_is_iso F _},
end
theorem reflect_inverse (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c')
[H : is_iso f] : (to_fun_hom F)⁻¹ᶠ (F f)⁻¹ = f⁻¹ :=
inverse_eq_inverse (idp : to_hom (@(iso.mk f) (reflect_is_iso F f)) = f)
/-
section
variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) -- we need some kind of naturality

31
hott/algebra/category/constructions/indiscrete.hlean Normal file
View file

@ -0,0 +1,31 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Indiscrete category
-/
import .opposite
open functor is_trunc unit eq
namespace category
variable (X : Type)
definition indiscrete_precategory [constructor] : precategory X :=
precategory.mk (λx y, unit)
(λx y z f g, star)
(λx, star)
(λx y z w f g h, idp)
(λx y f, by induction f; reflexivity)
(λx y f, by induction f; reflexivity)
definition Indiscrete_precategory [constructor] : Precategory :=
precategory.Mk (indiscrete_precategory X)
definition indiscrete_op : (Indiscrete_precategory X)ᵒᵖ = Indiscrete_precategory X := idp
end category

47
hott/algebra/category/constructions/initial.hlean Normal file
View file

@ -0,0 +1,47 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Initial category
-/
import .indiscrete
open functor is_trunc eq
namespace category
definition initial_precategory [constructor] : precategory empty :=
indiscrete_precategory empty
definition Initial_precategory [constructor] : Precategory :=
precategory.Mk initial_precategory
notation 0 := Initial_precategory
definition zero_op : 0ᵒᵖ = 0 := idp
definition initial_functor [constructor] (C : Precategory) : 0 ⇒ C :=
functor.mk (λx, empty.elim x)
(λx y f, empty.elim x)
(λx, empty.elim x)
(λx y z g f, empty.elim x)
definition is_contr_zero_functor [instance] (C : Precategory) : is_contr (0 ⇒ C) :=
is_contr.mk (initial_functor C)
begin
intro F, fapply functor_eq,
{ intro x, exact empty.elim x},
{ intro x y f, exact empty.elim x}
end
definition initial_functor_op (C : Precategory)
: (initial_functor C)ᵒᵖ = initial_functor Cᵒᵖ :=
by apply @is_hprop.elim (0 ⇒ Cᵒᵖ)
definition initial_functor_comp {C D : Precategory} (F : C ⇒ D)
: F ∘f initial_functor C = initial_functor D :=
by apply @is_hprop.elim (0 ⇒ D)
end category

11
hott/algebra/category/constructions/opposite.hlean
View file

@ -12,7 +12,7 @@ open eq functor
namespace category
definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob :=
definition opposite [reducible] [constructor] {ob : Type} (C : precategory ob) : precategory ob :=
precategory.mk' (λ a b, hom b a)
(λ a b c f g, g ∘ f)
(λ a, id)
@ -23,9 +23,11 @@ namespace category
(λ a, !id_id)
(λ a b, !is_hset_hom)
definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C)
definition Opposite [reducible] [constructor] (C : Precategory) : Precategory :=
precategory.Mk (opposite C)
infixr `∘op`:60 := @comp _ (opposite _) _ _ _
postfix `ᵒᵖ`:(max+2) := Opposite
variables {C : Precategory} {a b c : C}
@ -35,10 +37,9 @@ namespace category
definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
by cases C; apply idp
definition opposite_opposite : Opposite (Opposite C) = C :=
definition opposite_opposite : (Cᵒᵖ)ᵒᵖ = C :=
(ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta
postfix `ᵒᵖ`:(max+2) := Opposite
definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
begin
@ -47,6 +48,6 @@ namespace category
intros, apply (@respect_comp C D)
end
infixr `ᵒᵖᶠ`:(max+2) := opposite_functor
postfix `ᵒᵖ`:(max+2) := opposite_functor
end category

11
hott/algebra/category/constructions/product.hlean
View file

@ -11,7 +11,7 @@ import ..category ..functor
open eq prod is_trunc functor
namespace category
definition precategory_product [reducible] {obC obD : Type}
definition precategory_prod [constructor] [reducible] {obC obD : Type}
(C : precategory obC) (D : precategory obD) : precategory (obC × obD) :=
precategory.mk' (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
(λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f))
@ -22,13 +22,12 @@ namespace category
(λ a b f, prod_eq !id_right !id_right)
(λ a, prod_eq !id_id !id_id)
_
definition Precategory_prod [reducible] [constructor] (C D : Precategory) : Precategory :=
precategory.Mk (precategory_prod C D)
definition Precategory_product [reducible] (C D : Precategory) : Precategory :=
precategory.Mk (precategory_product C D)
infixr `×c`:30 := Precategory_prod
infixr `×c`:30 := Precategory_product
definition prod_functor [reducible] {C C' D D' : Precategory}
definition prod_functor [constructor] [reducible] {C C' D D' : Precategory}
(F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a)))
(λ a b f, pair (F (pr1 f)) (G (pr2 f)))

61
hott/algebra/category/constructions/sum.hlean Normal file
View file

@ -0,0 +1,61 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Jakob von Raumer
Functor product precategory and (TODO) category
-/
import ..category ..functor types.sum
open eq sum is_trunc functor lift
namespace category
--set_option pp.universes true
definition sum_hom.{u v w x} [unfold 5 6] {obC : Type.{u}} {obD : Type.{v}}
(C : precategory.{u w} obC) (D : precategory.{v x} obD)
: obC + obD → obC + obD → Type.{max w x} :=
sum.rec (λc, sum.rec (λc', lift (c ⟶ c')) (λd, lift empty))
(λd, sum.rec (λc, lift empty) (λd', lift (d ⟶ d')))
theorem is_hset_sum_hom {obC : Type} {obD : Type}
(C : precategory obC) (D : precategory obD) (x y : obC + obD)
: is_hset (sum_hom C D x y) :=
by induction x: induction y: esimp at *: exact _
local attribute is_hset_sum_hom [instance]
definition precategory_sum [constructor] {obC obD : Type}
(C : precategory obC) (D : precategory obD) : precategory (obC + obD) :=
precategory.mk (sum_hom C D)
(λ a b c g f, begin induction a: induction b: induction c: esimp at *;
induction f with f; induction g with g; (contradiction | exact up (g ∘ f)) end)
(λ a, by induction a: exact up id)
(λ a b c d h g f,
abstract begin induction a: induction b: induction c: induction d:
esimp at *; induction f with f; induction g with g; induction h with h;
esimp at *; try contradiction: apply ap up !assoc end end)
(λ a b f, abstract begin induction a: induction b: esimp at *;
induction f with f; esimp; try contradiction: exact ap up !id_left end end)
(λ a b f, abstract begin induction a: induction b: esimp at *;
induction f with f; esimp; try contradiction: exact ap up !id_right end end)
definition Precategory_sum [constructor] (C D : Precategory) : Precategory :=
precategory.Mk (precategory_sum C D)
infixr `+c`:27 := Precategory_sum
definition sum_functor [constructor] {C C' D D' : Precategory}
(F : C ⇒ D) (G : C' ⇒ D') : C +c C' ⇒ D +c D' :=
functor.mk (λ a, by induction a: (exact inl (F a)|exact inr (G a)))
(λ a b f, begin induction a: induction b: esimp at *;
induction f with f; esimp; try contradiction: (exact up (F f)|exact up (G f)) end)
(λ a, abstract by induction a: esimp; exact ap up !respect_id end)
(λ a b c g f, abstract begin induction a: induction b: induction c: esimp at *;
induction f with f; induction g with g; try contradiction:
esimp; exact ap up !respect_comp end end)
infixr `+f`:27 := sum_functor
end category

57
hott/algebra/category/constructions/terminal.hlean Normal file
View file

@ -0,0 +1,57 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Terminal category
-/
import .indiscrete
open functor is_trunc unit eq
namespace category
definition terminal_precategory [constructor] : precategory unit :=
indiscrete_precategory unit
definition Terminal_precategory [constructor] : Precategory :=
precategory.Mk terminal_precategory
notation 1 := Terminal_precategory
definition one_op : 1ᵒᵖ = 1 := idp
definition terminal_functor [constructor] (C : Precategory) : C ⇒ 1 :=
functor.mk (λx, star)
(λx y f, star)
(λx, idp)
(λx y z g f, idp)
definition is_contr_functor_one [instance] (C : Precategory) : is_contr (C ⇒ 1) :=
is_contr.mk (terminal_functor C)
begin
intro F, fapply functor_eq,
{ intro x, apply @is_hprop.elim unit},
{ intro x y f, apply @is_hprop.elim unit}
end
definition terminal_functor_op (C : Precategory)
: (terminal_functor C)ᵒᵖ = terminal_functor Cᵒᵖ := idp
definition terminal_functor_comp {C D : Precategory} (F : C ⇒ D)
: (terminal_functor D) ∘f F = terminal_functor C := idp
definition point (C : Precategory) (c : C) : 1 ⇒ C :=
functor.mk (λx, c)
(λx y f, id)
(λx, idp)
(λx y z g f, !id_id⁻¹)
-- we need id_id in the declaration of precategory to make this to hold definitionally
definition point_op (C : Precategory) (c : C) : (point C c)ᵒᵖ = point Cᵒᵖ c := idp
definition point_comp {C D : Precategory} (F : C ⇒ D) (c : C)
: F ∘f point C c = point D (F c) := idp
end category

23
hott/algebra/category/functor.hlean
View file

@ -11,7 +11,7 @@ open pi
structure functor (C D : Precategory) : Type :=
(to_fun_ob : C → D)
(to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b))
(to_fun_hom : Π {a b : C}, hom a b → hom (to_fun_ob a) (to_fun_ob b))
(respect_id : Π (a : C), to_fun_hom (ID a) = ID (to_fun_ob a))
(respect_comp : Π {a b c : C} (g : hom b c) (f : hom a b),
to_fun_hom (g ∘ f) = to_fun_hom g ∘ to_fun_hom f)
@ -52,9 +52,8 @@ namespace functor
: functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
apd01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim
definition functor_eq' {F₁ F₂ : C ⇒ D}
: Π(p : to_fun_ob F₁ = to_fun_ob F₂),
(transport (λx, Πa b f, hom (x a) (x b)) p (to_fun_hom F₁) = to_fun_hom F₂) → F₁ = F₂ :=
definition functor_eq' {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ = to_fun_ob F₂),
(transport (λx, Πa b f, hom (x a) (x b)) p @(to_fun_hom F₁) = @(to_fun_hom F₂)) → F₁ = F₂ :=
by induction F₁; induction F₂; apply functor_mk_eq'
definition functor_mk_eq {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
@ -141,13 +140,11 @@ namespace functor
to_fun_hom (g ∘ f) = to_fun_hom g ∘ to_fun_hom f)) ≃ (functor C D) :=
begin
fapply equiv.MK,
{intro S, fapply functor.mk,
exact (S.1), exact (S.2.1),
-- TODO(Leo): investigate why we need to use relaxed-exact (rexact) tactic here
exact (pr₁ S.2.2), rexact (pr₂ S.2.2)},
{intro F, cases F with d1 d2 d3 d4, exact ⟨d1, d2, (d3, @d4)⟩},
{intro F, cases F, reflexivity},
{intro S, cases S with d1 S2, cases S2 with d2 P1, cases P1, reflexivity},
{intro S, induction S with d1 S2, induction S2 with d2 P1, induction P1 with P11 P12,
exact functor.mk d1 d2 P11 @P12},
{intro F, induction F with d1 d2 d3 d4, exact ⟨d1, @d2, (d3, @d4)⟩},
{intro F, induction F, reflexivity},
{intro S, induction S with d1 S2, induction S2 with d2 P1, induction P1, reflexivity},
end
section
@ -199,8 +196,8 @@ namespace functor
by induction pF; induction pH; induction pid; induction pcomp; reflexivity
definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ~ to_fun_ob F₂)
(q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ~3 to_fun_hom F₂) (c : C) :
ap010 to_fun_ob (functor_eq p q) c = p c :=
(q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ~3 @(to_fun_hom F₂))
(c : C) : ap010 to_fun_ob (functor_eq p q) c = p c :=
begin
cases F₁ with F₁o F₁h F₁id F₁comp, cases F₂ with F₂o F₂h F₂id F₂comp,
esimp [functor_eq,functor_mk_eq,functor_mk_eq'],

41
hott/algebra/category/yoneda.hlean
View file

@ -208,7 +208,7 @@ namespace yoneda
local attribute Category.to.precategory category.to_precategory [constructor]
-- should this be defined as "yoneda_embedding Cᵒᵖ"?
definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
definition contravariant_yoneda_embedding [reducible] (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
functor_curry !hom_functor
definition yoneda_embedding (C : Precategory) : C ⇒ set ^c Cᵒᵖ :=
@ -226,10 +226,9 @@ namespace yoneda
exact ap10 !(@respect_comp Cᵒᵖ set)⁻¹ x}
end
definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) :
homset (ɏ c) F ≅ lift_functor (F c) :=
definition yoneda_lemma_equiv [constructor] {C : Precategory} (c : C)
(F : Cᵒᵖ ⇒ set) : hom (ɏ c) F ≃ lift (F c) :=
begin
apply iso_of_equiv, esimp,
fapply equiv.MK,
{ intro η, exact up (η c id)},
{ intro x, induction x with x, exact yoneda_lemma_hom c F x},
@ -242,10 +241,16 @@ namespace yoneda
rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left end end},
end
definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) :
homset (ɏ c) F ≅ lift_functor (F c) :=
begin
apply iso_of_equiv, esimp, apply yoneda_lemma_equiv,
end
theorem yoneda_lemma_natural_ob {C : Precategory} (F : Cᵒᵖ ⇒ set) {c c' : C} (f : c' ⟶ c)
(η : ɏ c ⟹ F) :
to_fun_hom (lift_functor ∘f F) f (to_hom (yoneda_lemma c F) η) =
proof to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) qed :=
to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) :=
begin
esimp [yoneda_lemma,yoneda_embedding], apply ap up,
transitivity (F f ∘ η c) id, reflexivity,
@ -256,12 +261,29 @@ namespace yoneda
rewrite [+id_left,+id_right],
end
-- TODO: Investigate what is the bottleneck to type check the next theorem
-- attribute yoneda_lemma lift_functor Precategory_hset precategory_hset homset
-- yoneda_embedding nat_trans.compose functor_nat_trans_compose [reducible]
-- attribute tlift functor.compose [reducible]
theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set)
(θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) :
proof (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) qed =
(to_hom (yoneda_lemma c F') proof (θ ∘n η : (to_fun_ob ɏ c : Cᵒᵖ ⇒ set) ⟹ F') qed) :=
(lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) =
proof to_hom (yoneda_lemma c F') (θ ∘n η) qed :=
by reflexivity
-- theorem xx.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set)
-- (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) :
-- proof _ qed =
-- to_hom (yoneda_lemma c F') (θ ∘n η) :=
-- by reflexivity
-- theorem yy.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set)
-- (θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) :
-- (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) =
-- proof _ qed :=
-- by reflexivity
definition fully_faithful_yoneda_embedding [instance] (C : Precategory) :
fully_faithful (ɏ : C ⇒ set ^c Cᵒᵖ) :=
begin
@ -275,7 +297,7 @@ namespace yoneda
rewrite [id_left,id_right]}
end
definition embedding_on_objects_yoneda_embedding (C : Category) :
definition is_embedding_yoneda_embedding (C : Category) :
is_embedding (ɏ : C → Cᵒᵖ ⇒ set) :=
begin
intro c c', fapply is_equiv_of_equiv_of_homotopy,
@ -298,8 +320,7 @@ namespace yoneda
{ transitivity _, rotate 1,
{ apply sigma.sigma_equiv_sigma_id, intro c, exact !eq_equiv_iso},
{ apply fiber.sigma_char}},
{ apply function.is_hprop_fiber_of_is_embedding,
apply embedding_on_objects_yoneda_embedding}
{ apply function.is_hprop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding}
end
end yoneda