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

feat(hott/algebra) show that functors preserve inverses and isos

Browse source
This commit is contained in:
Jakob von Raumer 2015-03-19 16:35:38 -04:00 committed by Leonardo de Moura
parent 74824078a8
commit 97a1cc8edb
1 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
hott/algebra/precategory/functor.hlean
View file

@ -87,6 +87,30 @@ namespace functor
: functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
functor_eq (λc, idp) (λa b f, !id_leftright ⬝ !pH)
protected definition preserve_iso (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] :
is_iso (F f) :=
begin
fapply @is_iso.mk, apply (F (f⁻¹)),
repeat (apply concat ; apply inverse ; apply (respect_comp F) ;
apply concat ; apply (ap (λ x, to_fun_hom F x)) ;
[apply left_inverse | apply right_inverse] ;
apply (respect_id F) ),
end
attribute preserve_iso [instance]
protected definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] :
F (f⁻¹) = (F f)⁻¹ :=
begin
fapply @left_inverse_eq_right_inverse, apply (F f),
apply concat, apply inverse, apply (respect_comp F),
apply concat, apply (ap (λ x, to_fun_hom F x)),
apply left_inverse, apply respect_id,
apply concat, apply inverse, apply (respect_comp F),
apply concat, apply (ap (λ x, to_fun_hom F x)),
apply right_inverse, apply respect_id,
end
protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
!functor_mk_eq_constant (λa b f, idp)