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

refactor(hott/algebra/category/adjoint): rewrite expensive proof

Browse source 
see #815
This commit is contained in:
Leonardo de Moura 2015-09-01 16:57:49 -07:00
parent a8964adb9c
commit cae2271818
1 changed files with 68 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -68,57 +68,74 @@ namespace category
definition is_iso_counit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (counit F) :=
!is_equivalence.is_iso_counit
-- theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
-- : is_hprop (is_left_adjoint F) :=
-- begin
-- apply is_hprop.mk,
-- intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K',
-- assert lem : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε'
-- → is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K',
-- { intros p q r, induction p, induction q, induction r, esimp,
-- apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim},
-- fapply lem,
-- { fapply functor.eq_of_pointwise_iso,
-- { fapply change_natural_map,
-- { exact (G' ∘fn1 ε) ∘n !assoc_natural_rev ∘n (η' ∘1nf G)},
-- { intro d, exact (G' (ε d) ∘ η' (G d))},
-- { intro d, exact ap (λx, _ ∘ x) !id_left}},
-- { intro d, fconstructor,
-- { exact (G (ε' d) ∘ η (G' d))},
-- { krewrite [▸*,assoc,-assoc (G (ε' d))],
-- krewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
-- krewrite [assoc,-assoc],
-- rewrite [↑functor.compose, -respect_comp G],
-- krewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
-- rewrite [respect_comp G],
-- krewrite [assoc,-assoc (G (ε d))],
-- rewrite [↑functor.compose, -respect_comp G],
-- krewrite [H' (G d)],
-- rewrite [respect_id,id_right],
-- apply K},
-- { krewrite [▸*,assoc,-assoc (G' (ε d))],
-- krewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
-- krewrite [assoc,-assoc],
-- rewrite [↑functor.compose, -respect_comp G'],
-- krewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d),▸*],
-- rewrite [respect_comp G'],
-- krewrite [assoc,-assoc (G' (ε' d))],
-- rewrite [↑functor.compose, -respect_comp G'],
-- krewrite [H (G' d)],
-- rewrite [respect_id,id_right],
-- apply K'}}},
-- { clear lem, refine transport_hom_of_eq_right _ η ⬝ _,
-- krewrite hom_of_eq_compose_right,
-- rewrite functor.hom_of_eq_eq_of_pointwise_iso,
-- apply nat_trans_eq, intro c, esimp,
-- refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
-- rewrite [▸*,-respect_comp G',H c,respect_id G',id_left]},
-- { clear lem, refine transport_hom_of_eq_left _ ε ⬝ _,
-- krewrite inv_of_eq_compose_left,
-- rewrite functor.inv_of_eq_eq_of_pointwise_iso,
-- apply nat_trans_eq, intro d, esimp,
-- rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]},
-- end
theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
: is_hprop (is_left_adjoint F) :=
begin
apply is_hprop.mk,
intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K',
assert lem₁ : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε'
→ is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K',
{ intros p q r, induction p, induction q, induction r, esimp,
apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim},
assert lem₂ : Π (d : carrier D),
(to_fun_hom G (natural_map ε' d) ∘
natural_map η (to_fun_ob G' d)) ∘
to_fun_hom G' (natural_map ε d) ∘
natural_map η' (to_fun_ob G d) = id,
{ intro d, esimp,
rewrite [assoc],
rewrite [-assoc (G (ε' d))],
esimp, rewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
esimp, rewrite [assoc],
esimp, rewrite [-assoc],
rewrite [↑functor.compose, -respect_comp G],
rewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
rewrite [respect_comp G],
rewrite [assoc,-assoc (G (ε d))],
rewrite [↑functor.compose, -respect_comp G],
rewrite [H' (G d)],
rewrite [respect_id,id_right],
apply K},
assert lem₃ : Π (d : carrier D),
(to_fun_hom G' (natural_map ε d) ∘
natural_map η' (to_fun_ob G d)) ∘
to_fun_hom G (natural_map ε' d) ∘
natural_map η (to_fun_ob G' d) = id,
{ intro d, esimp,
rewrite [assoc, -assoc (G' (ε d))],
esimp, rewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
esimp, rewrite [assoc], esimp, rewrite [-assoc],
rewrite [↑functor.compose, -respect_comp G'],
rewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d)],
esimp,
rewrite [respect_comp G'],
rewrite [assoc,-assoc (G' (ε' d))],
rewrite [↑functor.compose, -respect_comp G'],
rewrite [H (G' d)],
rewrite [respect_id,id_right],
apply K'},
fapply lem₁,
{ fapply functor.eq_of_pointwise_iso,
{ fapply change_natural_map,
{ exact (G' ∘fn1 ε) ∘n !assoc_natural_rev ∘n (η' ∘1nf G)},
{ intro d, exact (G' (ε d) ∘ η' (G d))},
{ intro d, exact ap (λx, _ ∘ x) !id_left}},
{ intro d, fconstructor,
{ exact (G (ε' d) ∘ η (G' d))},
{ exact lem₂ d },
{ exact lem₃ d }}},
{ clear lem₁, refine transport_hom_of_eq_right _ η ⬝ _,
krewrite hom_of_eq_compose_right,
rewrite functor.hom_of_eq_eq_of_pointwise_iso,
apply nat_trans_eq, intro c, esimp,
refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
esimp, rewrite [-respect_comp G',H c,respect_id G',id_left]},
{ clear lem₁, refine transport_hom_of_eq_left _ ε ⬝ _,
krewrite inv_of_eq_compose_left,
rewrite functor.inv_of_eq_eq_of_pointwise_iso,
apply nat_trans_eq, intro d, esimp,
rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}
end
definition full_of_fully_faithful (H : fully_faithful F) : full F :=
λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv))