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

feat(category.limit): prove that the limit functor is right adjoint to the diagonal map

Browse source
This commit is contained in:
Floris van Doorn 2015-10-27 22:43:47 -04:00 committed by Leonardo de Moura
parent 36dfb61a3e
commit 49cb516c71
5 changed files with 103 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

71
hott/algebra/category/functor/adjoint.hlean
View file

@ -6,9 +6,9 @@ Authors: Floris van Doorn
Adjoint functors
-/
import .attributes
import .attributes .examples
open functor nat_trans is_trunc eq iso
open functor nat_trans is_trunc eq iso prod
namespace category
@ -108,4 +108,71 @@ namespace category
rewrite [assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}
end
section
universe variables u v
parameters {C D : Precategory.{u v}} {F : C ⇒ D} {G : D ⇒ C}
(θ : hom_functor D ∘f prod_functor_prod Fᵒᵖᶠ 1 ≅ hom_functor C ∘f prod_functor_prod 1 G)
include θ
/- θ : _ ⟹[Cᵒᵖ × D ⇒ set] _-/
definition adj_unit [constructor] : 1 ⟹ G ∘f F :=
begin
fapply nat_trans.mk: esimp,
{ intro c, exact natural_map (to_hom θ) (c, F c) id},
{ intro c c' f,
let H := naturality (to_hom θ) (ID c, F f),
let K := ap10 H id,
rewrite [▸* at K, id_right at K, ▸*, K, respect_id, +id_right],
clear H K,
let H := naturality (to_hom θ) (f, ID (F c')),
let K := ap10 H id,
rewrite [▸* at K, respect_id at K,+id_left at K, K]}
end
definition adj_counit [constructor] : F ∘f G ⟹ 1 :=
begin
fapply nat_trans.mk: esimp,
{ intro d, exact natural_map (to_inv θ) (G d, d) id, },
{ intro d d' g,
let H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'),
let K := ap10 H id,
rewrite [▸* at K, id_left at K, ▸*, K, respect_id, +id_left],
clear H K,
let H := naturality (to_inv θ) (ID (G d), g),
let K := ap10 H id,
rewrite [▸* at K, respect_id at K,+id_right at K, K]}
end
theorem adj_eq_unit (c : C) (d : D) (f : F c ⟶ d)
: natural_map (to_hom θ) (c, d) f = G f ∘ adj_unit c :=
begin
esimp,
let H := naturality (to_hom θ) (ID c, f),
let K := ap10 H id,
rewrite [▸* at K, id_right at K, K, respect_id, +id_right],
end
theorem adj_eq_counit (c : C) (d : D) (g : c ⟶ G d)
: natural_map (to_inv θ) (c, d) g = adj_counit d ∘ F g :=
begin
esimp,
let H := naturality (to_inv θ) (g, ID d),
let K := ap10 H id,
rewrite [▸* at K, id_left at K, K, respect_id, +id_left],
end
definition adjoint.mk' [constructor] : F ⊣ G :=
begin
fapply adjoint.mk,
{ exact adj_unit},
{ exact adj_counit},
{ intro c, esimp, refine (adj_eq_counit c (F c) (adj_unit c))⁻¹ ⬝ _,
apply ap10 (to_left_inverse (componentwise_iso θ (c, F c)))},
{ intro d, esimp, refine (adj_eq_unit (G d) d (adj_counit d))⁻¹ ⬝ _,
apply ap10 (to_right_inverse (componentwise_iso θ (G d, d)))},
end
end
end category

65
hott/algebra/category/functor/adjoint2.hlean
View file

@ -12,71 +12,6 @@ open eq functor nat_trans iso prod is_trunc
namespace category
section
universe variables u v
parameters {C D : Precategory.{u v}} {F : C ⇒ D} {G : D ⇒ C}
(θ : hom_functor D ∘f prod_functor_prod Fᵒᵖᶠ 1 ≅ hom_functor C ∘f prod_functor_prod 1 G)
include θ
/- θ : _ ⟹[Cᵒᵖ × D ⇒ set] _-/
definition adj_unit [constructor] : 1 ⟹ G ∘f F :=
begin
fapply nat_trans.mk: esimp,
{ intro c, exact natural_map (to_hom θ) (c, F c) id},
{ intro c c' f,
let H := naturality (to_hom θ) (ID c, F f),
let K := ap10 H id,
rewrite [▸* at K, id_right at K, ▸*, K, respect_id, +id_right],
clear H K,
let H := naturality (to_hom θ) (f, ID (F c')),
let K := ap10 H id,
rewrite [▸* at K, respect_id at K,+id_left at K, K]}
end
definition adj_counit [constructor] : F ∘f G ⟹ 1 :=
begin
fapply nat_trans.mk: esimp,
{ intro d, exact natural_map (to_inv θ) (G d, d) id, },
{ intro d d' g,
let H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'),
let K := ap10 H id,
rewrite [▸* at K, id_left at K, ▸*, K, respect_id, +id_left],
clear H K,
let H := naturality (to_inv θ) (ID (G d), g),
let K := ap10 H id,
rewrite [▸* at K, respect_id at K,+id_right at K, K]}
end
theorem adj_eq_unit (c : C) (d : D) (f : F c ⟶ d)
: natural_map (to_hom θ) (c, d) f = G f ∘ adj_unit c :=
begin
esimp,
let H := naturality (to_hom θ) (ID c, f),
let K := ap10 H id,
rewrite [▸* at K, id_right at K, K, respect_id, +id_right],
end
theorem adj_eq_counit (c : C) (d : D) (g : c ⟶ G d)
: natural_map (to_inv θ) (c, d) g = adj_counit d ∘ F g :=
begin
esimp,
let H := naturality (to_inv θ) (g, ID d),
let K := ap10 H id,
rewrite [▸* at K, id_left at K, K, respect_id, +id_left],
end
definition adjoint.mk' [constructor] : F ⊣ G :=
begin
fapply adjoint.mk,
{ exact adj_unit},
{ exact adj_counit},
{ intro c, esimp, refine (adj_eq_counit c (F c) (adj_unit c))⁻¹ ⬝ _,
apply ap10 (to_left_inverse (componentwise_iso θ (c, F c)))},
{ intro d, esimp, refine (adj_eq_unit (G d) d (adj_counit d))⁻¹ ⬝ _,
apply ap10 (to_right_inverse (componentwise_iso θ (G d, d)))},
end
end

10
hott/algebra/category/functor/exponential_laws.hlean
View file

@ -35,9 +35,9 @@ namespace category
begin
fapply functor.mk: esimp,
{ intro F, exact F c},
{ intro F, apply empty.elim (F c)},
{ intro F, apply empty.elim (F c)},
{ intro F, apply empty.elim (F c)},
{ intro F, eapply empty.elim (F c)},
{ intro F, eapply empty.elim (F c)},
{ intro F, eapply empty.elim (F c)},
end
definition zero_functor_iso_zero [constructor] (C : Precategory) (c : C) : 0 ^c C ≅c 0 :=
@ -66,9 +66,9 @@ namespace category
{ intro u v f, induction u, induction v, induction f, esimp, rewrite [+id_id,-respect_id]}},
{ intro F G η, apply nat_trans_eq, intro u, esimp,
rewrite [natural_map_hom_of_eq _ u, natural_map_inv_of_eq _ u,▸*,+ap010_functor_eq _ _ u],
induction u, rewrite [▸*, id_leftright], }},
induction u, rewrite [▸*, id_leftright]}},
{ fapply functor_eq: esimp,
{ intro c d f, rewrite [▸*, id_leftright] }},
{ intro c d f, rewrite [▸*, id_leftright]}},
end
/- 1 ^ C ≅ 1 -/

34
hott/algebra/category/limits/adjoint.hlean
View file

@ -6,27 +6,33 @@ Authors: Floris van Doorn
colimit_functor ⊣ Δ ⊣ limit_functor
-/
import .colimits ..functor.adjoint2
import .colimits ..functor.adjoint
open functor category is_trunc prod
open eq functor category is_trunc prod nat_trans
namespace category
definition limit_functor_adjoint [constructor] (D I : Precategory) [H : has_limits_of_shape D I] :
limit_functor D I ⊣ constant_diagram D I :=
constant_diagram D I ⊣ limit_functor D I :=
adjoint.mk'
begin
fapply natural_iso.MK: esimp,
{ intro Fd f, induction Fd with F d, esimp at *,
exact sorry},
{ exact sorry},
{ exact sorry},
{ exact sorry},
{ exact sorry}
fapply natural_iso.MK,
{ intro dF η, induction dF with d F, esimp at *,
fapply hom_limit,
{ exact natural_map η},
{ intro i j f, exact !naturality ⬝ !id_right}},
{ esimp, intro dF dF' fθ, induction dF with d F, induction dF' with d' F',
induction fθ with f θ, esimp at *, apply eq_of_homotopy, intro η,
apply eq_hom_limit, intro i,
rewrite [assoc, limit_hom_limit_commute,
-assoc, assoc (limit_morphism F i), hom_limit_commute]},
{ esimp, intro dF f, induction dF with d F, esimp at *,
refine !limit_nat_trans ∘n constant_nat_trans I f},
{ esimp, intro dF, induction dF with d F, esimp, apply eq_of_homotopy, intro η,
apply nat_trans_eq, intro i, esimp, apply hom_limit_commute},
{ esimp, intro dF, induction dF with d F, esimp, apply eq_of_homotopy, intro f,
symmetry, apply eq_hom_limit, intro i, reflexivity}
end
-- set_option pp.universes true
-- print Precategory_functor
-- print limit_functor_adjoint
-- print adjoint.mk'
end category

9
hott/algebra/category/limits/limits.hlean
View file

@ -212,6 +212,15 @@ namespace category
hom_limit _ (λi, η i ∘ limit_morphism F i)
abstract by intro i j f; rewrite [assoc,naturality,-assoc,limit_commute] end
theorem limit_hom_limit_commute {F G : I ⇒ D} (η : F ⟹ G)
: limit_morphism G i ∘ limit_hom_limit η = η i ∘ limit_morphism F i :=
!hom_limit_commute
-- theorem hom_limit_commute {d : D} (η : Πi, d ⟶ F i)
-- (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) (i : I)
-- : limit_morphism F i ∘ hom_limit F η p = η i :=
-- cone_to_eq (@(terminal_morphism (limit_cone_obj F p) _) (is_terminal_limit_cone _)) i
omit H
variable (F)