refactor(category): merge precategory/ and category/, organize construction files differently.
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
23e6a3131d
commit
797a2d2047
20 changed files with 459 additions and 462 deletions
|
|
@ -4,9 +4,7 @@ algebra
|
|||
* [binary](binary.hlean) : properties of binary operations
|
||||
* [relation](relation.hlean) : properties of relations
|
||||
* [group](group.hlean)
|
||||
* [groupoid](groupoid.hlean)
|
||||
|
||||
Subfolders:
|
||||
|
||||
* [precategory](precategory/precategory.md)
|
||||
* [category](category/category.md)
|
||||
* [category](category/category.md) : Category Theory
|
||||
|
|
|
|||
|
|
@ -2,11 +2,11 @@
|
|||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.yoneda
|
||||
Module: algebra.category.adjoint
|
||||
Authors: Floris van Doorn
|
||||
-/
|
||||
|
||||
import algebra.category.basic .constructions
|
||||
import .constructions.functor
|
||||
|
||||
open category functor nat_trans eq is_trunc iso equiv prod
|
||||
|
||||
|
|
@ -2,11 +2,11 @@
|
|||
Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.basic
|
||||
Module: algebra.category.category
|
||||
Author: Jakob von Raumer
|
||||
-/
|
||||
|
||||
import algebra.precategory.iso
|
||||
import .iso
|
||||
|
||||
open iso is_equiv eq is_trunc
|
||||
|
||||
|
|
@ -18,15 +18,15 @@ namespace category
|
|||
Π(a b : ob), is_equiv (@iso_of_eq ob C a b)
|
||||
|
||||
structure category [class] (ob : Type) extends parent : precategory ob :=
|
||||
(iso_of_path_equiv : is_univalent parent)
|
||||
mk' :: (iso_of_path_equiv : is_univalent parent)
|
||||
|
||||
attribute category [multiple-instances]
|
||||
|
||||
abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
|
||||
|
||||
definition category.mk' [reducible] (ob : Type) (C : precategory ob)
|
||||
(H : Π (a b : ob), is_equiv (@iso_of_eq ob C a b)) : category ob :=
|
||||
precategory.rec_on C category.mk H
|
||||
definition category.mk [reducible] {ob : Type} (C : precategory ob)
|
||||
(H : Π (a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b)) : category ob :=
|
||||
precategory.rec_on C category.mk' H
|
||||
|
||||
section basic
|
||||
variables {ob : Type} [C : category ob]
|
||||
|
|
@ -61,7 +61,7 @@ namespace category
|
|||
|
||||
definition category.Mk [reducible] := Category.mk
|
||||
definition category.MK [reducible] (C : Precategory)
|
||||
(H : is_univalent C) : Category := Category.mk C (category.mk' C C H)
|
||||
(H : is_univalent C) : Category := Category.mk C (category.mk C H)
|
||||
|
||||
definition Category.eta (C : Category) : Category.mk C C = C :=
|
||||
Category.rec (λob c, idp) C
|
||||
|
|
@ -1,5 +1,15 @@
|
|||
algebra.category
|
||||
================
|
||||
|
||||
* [basic](basic.hlean)
|
||||
* [constructions](constructions.hlean)
|
||||
Development of Category Theory. The following files are in this folder (sorted such that files only import previous files).
|
||||
|
||||
* [precategory](precategory.hlean)
|
||||
* [iso](iso.hlean) : iso, mono, epi, split mono, split epi
|
||||
* [category](category.hlean) : Categories (i.e. univalent or Rezk-complete precategories)
|
||||
* [groupoid](groupoid.hlean)
|
||||
* [functor](functor.hlean)
|
||||
* [nat_trans](nat_trans.hlean) : Natural transformations
|
||||
* [strict](strict.hlean) : Strict categories
|
||||
* [constructions](constructions/constructions.md) (subfolder) : basic constructions on categories and examples of categories
|
||||
* [adjoint](adjoint.hlean) : Adjoint functors and Equivalences (TODO)
|
||||
* [yoneda](yoneda.hlean) : Yoneda Embedding (TODO)
|
||||
|
|
|
|||
9
hott/algebra/category/constructions/constructions.md
Normal file
9
hott/algebra/category/constructions/constructions.md
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
algebra.category.constructions
|
||||
==============================
|
||||
|
||||
Common categories and constructions on categories. The following files are in this folder.
|
||||
|
||||
* [opposite](opposite.hlean) : Opposite category
|
||||
* [product](product.hlean) : Product category
|
||||
* [hset](hset.hlean) : Category of sets
|
||||
* [functor](functor.hlean) : Functor category
|
||||
9
hott/algebra/category/constructions/default.hlean
Normal file
9
hott/algebra/category/constructions/default.hlean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.constructions.default
|
||||
Authors: Floris van Doorn
|
||||
-/
|
||||
|
||||
import .functor .hset .opposite .product
|
||||
173
hott/algebra/category/constructions/functor.hlean
Normal file
173
hott/algebra/category/constructions/functor.hlean
Normal file
|
|
@ -0,0 +1,173 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.constructions.functor
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
Functor precategory and category
|
||||
-/
|
||||
|
||||
import ..nat_trans ..category
|
||||
|
||||
open eq functor is_trunc nat_trans iso is_equiv
|
||||
|
||||
namespace category
|
||||
|
||||
definition precategory_functor [instance] [reducible] (D C : Precategory)
|
||||
: precategory (functor C D) :=
|
||||
precategory.mk (λa b, nat_trans a b)
|
||||
(λ a b c g f, nat_trans.compose g f)
|
||||
(λ a, nat_trans.id)
|
||||
(λ a b c d h g f, !nat_trans.assoc)
|
||||
(λ a b f, !nat_trans.id_left)
|
||||
(λ a b f, !nat_trans.id_right)
|
||||
|
||||
definition Precategory_functor [reducible] (D C : Precategory) : Precategory :=
|
||||
precategory.Mk (precategory_functor D C)
|
||||
|
||||
infixr `^c`:35 := Precategory_functor
|
||||
|
||||
section
|
||||
/- we prove that if a natural transformation is pointwise an iso, then it is an iso -/
|
||||
variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)]
|
||||
include iso
|
||||
|
||||
definition nat_trans_inverse : G ⟹ F :=
|
||||
nat_trans.mk
|
||||
(λc, (η c)⁻¹)
|
||||
(λc d f,
|
||||
begin
|
||||
apply comp_inverse_eq_of_eq_comp,
|
||||
apply concat, rotate_left 1, apply assoc,
|
||||
apply eq_inverse_comp_of_comp_eq,
|
||||
apply inverse,
|
||||
apply naturality,
|
||||
end)
|
||||
|
||||
definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = nat_trans.id :=
|
||||
begin
|
||||
fapply (apd011 nat_trans.mk),
|
||||
apply eq_of_homotopy, intro c, apply left_inverse,
|
||||
apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros,
|
||||
apply is_hset.elim
|
||||
end
|
||||
|
||||
definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = nat_trans.id :=
|
||||
begin
|
||||
fapply (apd011 nat_trans.mk),
|
||||
apply eq_of_homotopy, intro c, apply right_inverse,
|
||||
apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros,
|
||||
apply is_hset.elim
|
||||
end
|
||||
|
||||
definition is_iso_nat_trans : is_iso η :=
|
||||
is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η)
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
/- and conversely, if a natural transformation is an iso, it is componentwise an iso -/
|
||||
variables {C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C)
|
||||
include isoη
|
||||
definition componentwise_is_iso : is_iso (η c) :=
|
||||
@is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c)
|
||||
(ap010 natural_map (right_inverse η) c)
|
||||
|
||||
local attribute componentwise_is_iso [instance]
|
||||
|
||||
definition natural_map_inverse : natural_map η⁻¹ c = (η c)⁻¹ := idp
|
||||
|
||||
definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ :=
|
||||
calc
|
||||
G f = (G f ∘ η c) ∘ (η c)⁻¹ : comp_inverse_cancel_right
|
||||
... = (η c' ∘ F f) ∘ (η c)⁻¹ : by rewrite naturality
|
||||
... = η c' ∘ F f ∘ (η c)⁻¹ : assoc
|
||||
|
||||
definition naturality_iso' {c c' : C} (f : c ⟶ c') : (η c')⁻¹ ∘ G f ∘ η c = F f :=
|
||||
calc
|
||||
(η c')⁻¹ ∘ G f ∘ η c = (η c')⁻¹ ∘ η c' ∘ F f : by rewrite naturality
|
||||
... = F f : inverse_comp_cancel_left
|
||||
|
||||
omit isoη
|
||||
|
||||
definition componentwise_iso (η : F ≅ G) (c : C) : F c ≅ G c :=
|
||||
@iso.mk _ _ _ _ (natural_map (to_hom η) c)
|
||||
(@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c)
|
||||
|
||||
definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) :=
|
||||
iso.eq_mk (idpath (ID (F c)))
|
||||
|
||||
definition componentwise_iso_iso_of_eq (p : F = G) (c : C)
|
||||
: componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) :=
|
||||
eq.rec_on p !componentwise_iso_id
|
||||
|
||||
definition natural_map_hom_of_eq (p : F = G) (c : C)
|
||||
: natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) :=
|
||||
eq.rec_on p idp
|
||||
|
||||
definition natural_map_inv_of_eq (p : F = G) (c : C)
|
||||
: natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ :=
|
||||
eq.rec_on p idp
|
||||
|
||||
end
|
||||
|
||||
namespace functor
|
||||
|
||||
variables {C : Precategory} {D : Category} {F G : D ^c C}
|
||||
definition eq_of_iso_ob (η : F ≅ G) (c : C) : F c = G c :=
|
||||
by apply eq_of_iso; apply componentwise_iso; exact η
|
||||
|
||||
local attribute functor.to_fun_hom [quasireducible]
|
||||
definition eq_of_iso (η : F ≅ G) : F = G :=
|
||||
begin
|
||||
fapply functor_eq,
|
||||
{exact (eq_of_iso_ob η)},
|
||||
{intros [c, c', f], --unfold eq_of_iso_ob, --TODO: report: this fails
|
||||
apply concat,
|
||||
{apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)},
|
||||
apply concat,
|
||||
{apply (ap (λx, _ ∘ to_fun_hom F f ∘ (to_hom x)⁻¹)), apply (retr iso_of_eq)},
|
||||
apply inverse, apply naturality_iso}
|
||||
end
|
||||
|
||||
definition iso_of_eq_eq_of_iso (η : F ≅ G) : iso_of_eq (eq_of_iso η) = η :=
|
||||
begin
|
||||
apply iso.eq_mk,
|
||||
apply nat_trans_eq_mk,
|
||||
intro c,
|
||||
rewrite natural_map_hom_of_eq, esimp [eq_of_iso],
|
||||
rewrite ap010_functor_eq, esimp [hom_of_eq,eq_of_iso_ob],
|
||||
rewrite (retr iso_of_eq),
|
||||
end
|
||||
|
||||
definition eq_of_iso_iso_of_eq (p : F = G) : eq_of_iso (iso_of_eq p) = p :=
|
||||
begin
|
||||
apply functor_eq2,
|
||||
intro c,
|
||||
esimp [eq_of_iso],
|
||||
rewrite ap010_functor_eq,
|
||||
esimp [eq_of_iso_ob],
|
||||
rewrite componentwise_iso_iso_of_eq,
|
||||
rewrite (sect iso_of_eq)
|
||||
end
|
||||
|
||||
definition is_univalent (D : Category) (C : Precategory) : is_univalent (D ^c C) :=
|
||||
λF G, adjointify _ eq_of_iso
|
||||
iso_of_eq_eq_of_iso
|
||||
eq_of_iso_iso_of_eq
|
||||
|
||||
end functor
|
||||
|
||||
definition Category_functor_of_precategory (D : Category) (C : Precategory) : Category :=
|
||||
category.MK (D ^c C) (functor.is_univalent D C)
|
||||
|
||||
definition Category_functor (D : Category) (C : Category) : Category :=
|
||||
Category_functor_of_precategory D C
|
||||
|
||||
namespace ops
|
||||
infixr `^c2`:35 := Category_functor_of_precategory
|
||||
end ops
|
||||
|
||||
|
||||
end category
|
||||
|
|
@ -1,18 +1,31 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.constructions
|
||||
Authors: Floris van Doorn
|
||||
Module: algebra.category.constructions.hset
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
Category of hsets
|
||||
-/
|
||||
|
||||
import .basic algebra.precategory.constructions types.equiv types.trunc
|
||||
import ..category types.equiv
|
||||
|
||||
--open eq eq.ops equiv category.ops iso category is_trunc
|
||||
open eq category equiv iso is_equiv category.ops is_trunc iso.iso function sigma
|
||||
--open eq is_trunc sigma equiv iso is_equiv
|
||||
open eq category equiv iso is_equiv is_trunc function sigma
|
||||
|
||||
namespace category
|
||||
|
||||
definition precategory_hset [reducible] : precategory hset :=
|
||||
precategory.mk (λx y : hset, x → y)
|
||||
(λx y z g f a, g (f a))
|
||||
(λx a, a)
|
||||
(λx y z w h g f, eq_of_homotopy (λa, idp))
|
||||
(λx y f, eq_of_homotopy (λa, idp))
|
||||
(λx y f, eq_of_homotopy (λa, idp))
|
||||
|
||||
definition Precategory_hset [reducible] : Precategory :=
|
||||
Precategory.mk hset precategory_hset
|
||||
|
||||
namespace set
|
||||
local attribute is_equiv_subtype_eq [instance]
|
||||
definition iso_of_equiv {A B : Precategory_hset} (f : A ≃ B) : A ≅ B :=
|
||||
|
|
@ -70,75 +83,13 @@ namespace category
|
|||
!univalence)
|
||||
!is_equiv_iso_of_equiv,
|
||||
(iso_of_eq_eq_compose A B)⁻¹ ▹ H
|
||||
|
||||
end set
|
||||
|
||||
definition category_hset [reducible] [instance] : category hset :=
|
||||
category.mk' hset precategory_hset set.is_univalent_hset
|
||||
category.mk precategory_hset set.is_univalent_hset
|
||||
|
||||
definition Category_hset [reducible] : Category :=
|
||||
Category.mk hset category_hset
|
||||
|
||||
namespace ops
|
||||
abbreviation set := Category_hset
|
||||
end ops
|
||||
|
||||
section functor
|
||||
open functor nat_trans
|
||||
|
||||
variables {C : Precategory} {D : Category} {F G : D ^c C}
|
||||
definition eq_of_iso_functor_ob (η : F ≅ G) (c : C) : F c = G c :=
|
||||
by apply eq_of_iso; apply componentwise_iso; exact η
|
||||
|
||||
local attribute functor.to_fun_hom [quasireducible]
|
||||
definition eq_of_iso_functor (η : F ≅ G) : F = G :=
|
||||
begin
|
||||
fapply functor_eq,
|
||||
{exact (eq_of_iso_functor_ob η)},
|
||||
{intros [c, c', f], --unfold eq_of_iso_functor_ob, --TODO: report: this fails
|
||||
apply concat,
|
||||
{apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)},
|
||||
apply concat,
|
||||
{apply (ap (λx, _ ∘ to_fun_hom F f ∘ (to_hom x)⁻¹)), apply (retr iso_of_eq)},
|
||||
apply inverse, apply naturality_iso}
|
||||
end
|
||||
|
||||
definition iso_of_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η :=
|
||||
begin
|
||||
apply iso.eq_mk,
|
||||
apply nat_trans_eq_mk,
|
||||
intro c,
|
||||
rewrite natural_map_hom_of_eq, esimp [eq_of_iso_functor],
|
||||
rewrite ap010_functor_eq, esimp [hom_of_eq,eq_of_iso_functor_ob],
|
||||
rewrite (retr iso_of_eq),
|
||||
end
|
||||
|
||||
definition eq_of_iso_functor_iso_of_eq (p : F = G) : eq_of_iso_functor (iso_of_eq p) = p :=
|
||||
begin
|
||||
apply functor_eq2,
|
||||
intro c,
|
||||
esimp [eq_of_iso_functor],
|
||||
rewrite ap010_functor_eq,
|
||||
esimp [eq_of_iso_functor_ob],
|
||||
rewrite componentwise_iso_iso_of_eq,
|
||||
rewrite (sect iso_of_eq)
|
||||
end
|
||||
|
||||
definition is_univalent_functor (D : Category) (C : Precategory) : is_univalent (D ^c C) :=
|
||||
λF G, adjointify _ eq_of_iso_functor
|
||||
iso_of_eq_eq_of_iso_functor
|
||||
eq_of_iso_functor_iso_of_eq
|
||||
|
||||
end functor
|
||||
|
||||
definition Category_functor_of_precategory (D : Category) (C : Precategory) : Category :=
|
||||
category.MK (D ^c C) (is_univalent_functor D C)
|
||||
|
||||
definition Category_functor (D : Category) (C : Category) : Category :=
|
||||
Category_functor_of_precategory D C
|
||||
|
||||
namespace ops
|
||||
infixr `^c2`:35 := Category_functor
|
||||
end ops
|
||||
|
||||
abbreviation set := Category_hset
|
||||
end category
|
||||
53
hott/algebra/category/constructions/opposite.hlean
Normal file
53
hott/algebra/category/constructions/opposite.hlean
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.constructions.opposite
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
Opposite precategory and (TODO) category
|
||||
-/
|
||||
|
||||
import ..functor ..category
|
||||
|
||||
open eq functor
|
||||
|
||||
namespace category
|
||||
|
||||
definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob :=
|
||||
precategory.mk' (λ a b, hom b a)
|
||||
(λ a b c f g, g ∘ f)
|
||||
(λ a, id)
|
||||
(λ a b c d f g h, !assoc')
|
||||
(λ a b c d f g h, !assoc)
|
||||
(λ a b f, !id_right)
|
||||
(λ a b f, !id_left)
|
||||
(λ a, !id_id)
|
||||
(λ a b, !is_hset_hom)
|
||||
|
||||
definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C)
|
||||
|
||||
infixr `∘op`:60 := @comp _ (opposite _) _ _ _
|
||||
|
||||
variables {C : Precategory} {a b c : C}
|
||||
|
||||
definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp
|
||||
|
||||
definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
|
||||
by cases C; apply idp
|
||||
|
||||
definition opposite_opposite : Opposite (Opposite C) = C :=
|
||||
(ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta
|
||||
|
||||
postfix `ᵒᵖ`:(max+1) := Opposite
|
||||
|
||||
definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
|
||||
begin
|
||||
apply (@functor.mk (Cᵒᵖ) (Dᵒᵖ)),
|
||||
intro a, apply (respect_id F),
|
||||
intros, apply (@respect_comp C D)
|
||||
end
|
||||
|
||||
infixr `ᵒᵖᶠ`:(max+1) := opposite_functor
|
||||
|
||||
end category
|
||||
42
hott/algebra/category/constructions/product.hlean
Normal file
42
hott/algebra/category/constructions/product.hlean
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.constructions.product
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
Functor product precategory and (TODO) category
|
||||
-/
|
||||
|
||||
import ..category ..functor
|
||||
|
||||
open eq prod is_trunc functor
|
||||
|
||||
namespace category
|
||||
definition precategory_product [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))
|
||||
(λ a, (id, id))
|
||||
(λ a b c d h g f, pair_eq !assoc !assoc )
|
||||
(λ a b c d h g f, pair_eq !assoc' !assoc' )
|
||||
(λ a b f, prod_eq !id_left !id_left )
|
||||
(λ a b f, prod_eq !id_right !id_right)
|
||||
(λ a, prod_eq !id_id !id_id)
|
||||
_
|
||||
|
||||
definition Precategory_product [reducible] (C D : Precategory) : Precategory :=
|
||||
precategory.Mk (precategory_product C D)
|
||||
|
||||
infixr `×c`:30 := Precategory_product
|
||||
|
||||
definition prod_functor [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)))
|
||||
(λ a, pair_eq !respect_id !respect_id)
|
||||
(λ a b c g f, pair_eq !respect_comp !respect_comp)
|
||||
|
||||
infixr `×f`:30 := prod_functor
|
||||
|
||||
end category
|
||||
|
|
@ -2,11 +2,11 @@
|
|||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.functor
|
||||
Module: algebra.category.functor
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
|
||||
import .basic types.pi .iso
|
||||
import .iso types.pi
|
||||
|
||||
open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext iso
|
||||
open pi
|
||||
|
|
@ -153,7 +153,7 @@ namespace functor
|
|||
local attribute precategory.is_hset_hom [priority 1001]
|
||||
protected theorem is_hset_functor [instance]
|
||||
[HD : is_hset D] : is_hset (functor C D) :=
|
||||
by apply is_trunc_equiv_closed; apply sigma_char
|
||||
by apply is_trunc_equiv_closed; apply functor.sigma_char
|
||||
end
|
||||
|
||||
definition functor_mk_eq'_idp (F : C → D) (H : Π(a b : C), hom a b → hom (F a) (F b))
|
||||
|
|
@ -2,13 +2,13 @@
|
|||
Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.groupoid
|
||||
Module: algebra.category.groupoid
|
||||
Author: Jakob von Raumer
|
||||
|
||||
Ported from Coq HoTT
|
||||
-/
|
||||
|
||||
import .precategory.iso .group
|
||||
import .iso ..group
|
||||
|
||||
open eq is_trunc iso category path_algebra nat unit
|
||||
|
||||
|
|
@ -2,16 +2,14 @@
|
|||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.iso
|
||||
Module: algebra.category.iso
|
||||
Author: Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
|
||||
import algebra.precategory.basic types.sigma arity
|
||||
import .precategory types.sigma arity
|
||||
|
||||
open eq category prod equiv is_equiv sigma sigma.ops is_trunc
|
||||
|
||||
|
||||
|
||||
namespace iso
|
||||
structure split_mono [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
|
||||
{retraction_of : b ⟶ a}
|
||||
|
|
@ -113,20 +111,6 @@ namespace iso
|
|||
[Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) :=
|
||||
!is_iso_of_split_epi_of_split_mono
|
||||
|
||||
-- "is_iso f" is equivalent to a certain sigma type
|
||||
-- definition is_iso.sigma_char (f : hom a b) :
|
||||
-- (Σ (g : hom b a), (g ∘ f = id) × (f ∘ g = id)) ≃ is_iso f :=
|
||||
-- begin
|
||||
-- fapply equiv.MK,
|
||||
-- {intro S, apply is_iso.mk,
|
||||
-- exact (pr₁ S.2),
|
||||
-- exact (pr₂ S.2)},
|
||||
-- {intro H, cases H with (g, η, ε),
|
||||
-- exact (sigma.mk g (pair η ε))},
|
||||
-- {intro H, cases H, apply idp},
|
||||
-- {intro S, cases S with (g, ηε), cases ηε, apply idp},
|
||||
-- end
|
||||
|
||||
definition is_hprop_is_iso [instance] (f : hom a b) : is_hprop (is_iso f) :=
|
||||
begin
|
||||
apply is_hprop.mk, intros [H, H'],
|
||||
|
|
@ -138,52 +122,55 @@ namespace iso
|
|||
apply is_hprop.elim,
|
||||
apply is_hprop.elim,
|
||||
end
|
||||
end iso open iso
|
||||
|
||||
/- iso objects -/
|
||||
structure iso (a b : ob) :=
|
||||
(to_hom : hom a b)
|
||||
[struct : is_iso to_hom]
|
||||
/- isomorphic objects -/
|
||||
structure iso {ob : Type} [C : precategory ob] (a b : ob) :=
|
||||
(to_hom : hom a b)
|
||||
[struct : is_iso to_hom]
|
||||
|
||||
infix `≅`:50 := iso.iso
|
||||
namespace iso
|
||||
variables {ob : Type} [C : precategory ob]
|
||||
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
|
||||
include C
|
||||
|
||||
infix `≅`:50 := iso
|
||||
attribute iso.struct [instance] [priority 400]
|
||||
|
||||
namespace iso
|
||||
attribute to_hom [coercion]
|
||||
attribute to_hom [coercion]
|
||||
|
||||
protected definition MK (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
|
||||
@mk _ _ _ _ f (is_iso.mk H1 H2)
|
||||
protected definition MK (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
|
||||
@mk _ _ _ _ f (is_iso.mk H1 H2)
|
||||
|
||||
definition to_inv (f : a ≅ b) : b ⟶ a :=
|
||||
(to_hom f)⁻¹
|
||||
definition to_inv (f : a ≅ b) : b ⟶ a :=
|
||||
(to_hom f)⁻¹
|
||||
|
||||
protected definition refl (a : ob) : a ≅ a :=
|
||||
mk (ID a)
|
||||
protected definition refl (a : ob) : a ≅ a :=
|
||||
mk (ID a)
|
||||
|
||||
protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
|
||||
mk (to_hom H)⁻¹
|
||||
protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
|
||||
mk (to_hom H)⁻¹
|
||||
|
||||
protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
|
||||
mk (to_hom H2 ∘ to_hom H1)
|
||||
protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
|
||||
mk (to_hom H2 ∘ to_hom H1)
|
||||
|
||||
protected definition eq_mk' {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
|
||||
: iso.mk f = iso.mk f' :=
|
||||
apd011 iso.mk p !is_hprop.elim
|
||||
protected definition eq_mk' {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
|
||||
: iso.mk f = iso.mk f' :=
|
||||
apd011 iso.mk p !is_hprop.elim
|
||||
|
||||
protected definition eq_mk {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' :=
|
||||
by (cases f; cases f'; apply (iso.eq_mk' p))
|
||||
protected definition eq_mk {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' :=
|
||||
by (cases f; cases f'; apply (iso.eq_mk' p))
|
||||
|
||||
-- The structure for isomorphism can be characterized up to equivalence by a sigma type.
|
||||
definition sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
|
||||
begin
|
||||
fapply (equiv.mk),
|
||||
{intro S, apply iso.mk, apply (S.2)},
|
||||
{fapply adjointify,
|
||||
{intro p, cases p with [f, H], exact (sigma.mk f H)},
|
||||
{intro p, cases p, apply idp},
|
||||
{intro S, cases S, apply idp}},
|
||||
end
|
||||
|
||||
end iso
|
||||
-- The structure for isomorphism can be characterized up to equivalence by a sigma type.
|
||||
protected definition sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
|
||||
begin
|
||||
fapply (equiv.mk),
|
||||
{intro S, apply iso.mk, apply (S.2)},
|
||||
{fapply adjointify,
|
||||
{intro p, cases p with [f, H], exact (sigma.mk f H)},
|
||||
{intro p, cases p, apply idp},
|
||||
{intro S, cases S, apply idp}},
|
||||
end
|
||||
|
||||
-- The type of isomorphisms between two objects is a set
|
||||
definition is_hset_iso [instance] : is_hset (a ≅ b) :=
|
||||
|
|
@ -2,7 +2,7 @@
|
|||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.nat_trans
|
||||
Module: algebra.category.nat_trans
|
||||
Author: Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
import .functor .iso
|
||||
|
|
@ -2,7 +2,7 @@
|
|||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.basic
|
||||
Module: algebra.category.precategory
|
||||
Authors: Floris van Doorn
|
||||
-/
|
||||
import types.trunc types.pi arity
|
||||
82
hott/algebra/category/strict.hlean
Normal file
82
hott/algebra/category/strict.hlean
Normal file
|
|
@ -0,0 +1,82 @@
|
|||
/-
|
||||
Copyright (c) 2015 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.category.strict
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
|
||||
import .precategory .functor
|
||||
|
||||
open is_trunc eq
|
||||
|
||||
namespace category
|
||||
structure strict_precategory [class] (ob : Type) extends precategory ob :=
|
||||
mk' :: (is_hset_ob : is_hset ob)
|
||||
|
||||
attribute strict_precategory.is_hset_ob [instance]
|
||||
|
||||
definition strict_precategory.mk [reducible] {ob : Type} (C : precategory ob)
|
||||
(H : is_hset ob) : strict_precategory ob :=
|
||||
precategory.rec_on C strict_precategory.mk' H
|
||||
|
||||
structure Strict_precategory : Type :=
|
||||
(carrier : Type)
|
||||
(struct : strict_precategory carrier)
|
||||
|
||||
attribute Strict_precategory.struct [instance] [coercion]
|
||||
|
||||
definition Strict_precategory.to_Precategory [coercion] [reducible]
|
||||
(C : Strict_precategory) : Precategory :=
|
||||
Precategory.mk (Strict_precategory.carrier C) C
|
||||
|
||||
open functor
|
||||
|
||||
definition precat_strict_precat : precategory Strict_precategory :=
|
||||
precategory.mk (λ a b, functor a b)
|
||||
(λ a b c g f, functor.compose g f)
|
||||
(λ a, functor.id)
|
||||
(λ a b c d h g f, !functor.assoc)
|
||||
(λ a b f, !functor.id_left)
|
||||
(λ a b f, !functor.id_right)
|
||||
|
||||
definition Precat_of_strict_precats := precategory.Mk precat_strict_precat
|
||||
|
||||
namespace ops
|
||||
abbreviation SPreCat := Precat_of_strict_precats
|
||||
--attribute precat_strict_precat [instance]
|
||||
end ops
|
||||
|
||||
end category
|
||||
|
||||
/-section
|
||||
open decidable unit empty
|
||||
variables {A : Type} [H : decidable_eq A]
|
||||
include H
|
||||
definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
|
||||
theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
|
||||
definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
|
||||
decidable.rec_on
|
||||
(H b c)
|
||||
(λ Hbc g, decidable.rec_on
|
||||
(H a b)
|
||||
(λ Hab f, rec_on_true (trans Hab Hbc) ⋆)
|
||||
(λh f, empty.rec _ f) f)
|
||||
(λh (g : empty), empty.rec _ g) g
|
||||
omit H
|
||||
definition discrete_precategory (A : Type) [H : decidable_eq A] : precategory A :=
|
||||
mk (λa b, set_hom a b)
|
||||
(λ a b c g f, set_compose g f)
|
||||
(λ a, decidable.rec_on_true rfl ⋆)
|
||||
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
|
||||
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
|
||||
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
|
||||
definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
|
||||
end
|
||||
section
|
||||
open unit bool
|
||||
definition category_one := discrete_category unit
|
||||
definition Category_one := Mk category_one
|
||||
definition category_two := discrete_category bool
|
||||
definition Category_two := Mk category_two
|
||||
end-/
|
||||
|
|
@ -2,16 +2,15 @@
|
|||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.yoneda
|
||||
Module: algebra.category.yoneda
|
||||
Authors: Floris van Doorn
|
||||
-/
|
||||
|
||||
--note: modify definition in category.set
|
||||
import algebra.category.constructions .iso
|
||||
import .constructions.functor .constructions.hset .constructions.product .constructions.opposite
|
||||
|
||||
open category eq category.ops functor prod.ops is_trunc iso
|
||||
|
||||
set_option pp.beta true
|
||||
namespace yoneda
|
||||
set_option class.conservative false
|
||||
|
||||
|
|
@ -1,255 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.constructions
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
This file contains basic constructions on precategories, including common precategories
|
||||
-/
|
||||
|
||||
import .nat_trans
|
||||
import types.prod types.sigma types.pi
|
||||
|
||||
open eq prod eq eq.ops equiv is_trunc
|
||||
|
||||
namespace category
|
||||
namespace opposite
|
||||
|
||||
definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob :=
|
||||
precategory.mk' (λ a b, hom b a)
|
||||
(λ a b c f g, g ∘ f)
|
||||
(λ a, id)
|
||||
(λ a b c d f g h, !assoc')
|
||||
(λ a b c d f g h, !assoc)
|
||||
(λ a b f, !id_right)
|
||||
(λ a b f, !id_left)
|
||||
(λ a, !id_id)
|
||||
(λ a b, !is_hset_hom)
|
||||
|
||||
definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C)
|
||||
|
||||
infixr `∘op`:60 := @comp _ (opposite _) _ _ _
|
||||
|
||||
variables {C : Precategory} {a b c : C}
|
||||
|
||||
definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp
|
||||
|
||||
definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
|
||||
by cases C; apply idp
|
||||
|
||||
definition opposite_opposite : Opposite (Opposite C) = C :=
|
||||
(ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta
|
||||
|
||||
end opposite
|
||||
|
||||
-- Note: Discrete precategory doesn't really make sense in HoTT,
|
||||
-- We'll define a discrete _category_ later.
|
||||
/-section
|
||||
open decidable unit empty
|
||||
variables {A : Type} [H : decidable_eq A]
|
||||
include H
|
||||
definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
|
||||
theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
|
||||
definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
|
||||
decidable.rec_on
|
||||
(H b c)
|
||||
(λ Hbc g, decidable.rec_on
|
||||
(H a b)
|
||||
(λ Hab f, rec_on_true (trans Hab Hbc) ⋆)
|
||||
(λh f, empty.rec _ f) f)
|
||||
(λh (g : empty), empty.rec _ g) g
|
||||
omit H
|
||||
definition discrete_precategory (A : Type) [H : decidable_eq A] : precategory A :=
|
||||
mk (λa b, set_hom a b)
|
||||
(λ a b c g f, set_compose g f)
|
||||
(λ a, decidable.rec_on_true rfl ⋆)
|
||||
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
|
||||
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
|
||||
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
|
||||
definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
|
||||
end
|
||||
section
|
||||
open unit bool
|
||||
definition category_one := discrete_category unit
|
||||
definition Category_one := Mk category_one
|
||||
definition category_two := discrete_category bool
|
||||
definition Category_two := Mk category_two
|
||||
end-/
|
||||
|
||||
namespace product
|
||||
section
|
||||
open prod is_trunc
|
||||
|
||||
definition precategory_prod [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))
|
||||
(λ a, (id, id))
|
||||
(λ a b c d h g f, pair_eq !assoc !assoc )
|
||||
(λ a b f, prod_eq !id_left !id_left )
|
||||
(λ a b f, prod_eq !id_right !id_right)
|
||||
|
||||
definition Precategory_prod [reducible] (C D : Precategory) : Precategory :=
|
||||
precategory.Mk (precategory_prod C D)
|
||||
|
||||
end
|
||||
end product
|
||||
|
||||
namespace ops
|
||||
--notation 1 := Category_one
|
||||
--notation 2 := Category_two
|
||||
postfix `ᵒᵖ`:max := opposite.Opposite
|
||||
infixr `×c`:30 := product.Precategory_prod
|
||||
--instance [persistent] type_category category_one
|
||||
-- category_two product.prod_category
|
||||
end ops
|
||||
|
||||
open ops
|
||||
namespace opposite
|
||||
open ops functor
|
||||
definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
|
||||
begin
|
||||
apply (@functor.mk (Cᵒᵖ) (Dᵒᵖ)),
|
||||
intro a, apply (respect_id F),
|
||||
intros, apply (@respect_comp C D)
|
||||
end
|
||||
|
||||
end opposite
|
||||
|
||||
namespace product
|
||||
section
|
||||
open ops functor
|
||||
definition prod_functor [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)))
|
||||
(λ a, pair_eq !respect_id !respect_id)
|
||||
(λ a b c g f, pair_eq !respect_comp !respect_comp)
|
||||
end
|
||||
end product
|
||||
|
||||
definition precategory_hset [reducible] : precategory hset :=
|
||||
precategory.mk (λx y : hset, x → y)
|
||||
(λx y z g f a, g (f a))
|
||||
(λx a, a)
|
||||
(λx y z w h g f, eq_of_homotopy (λa, idp))
|
||||
(λx y f, eq_of_homotopy (λa, idp))
|
||||
(λx y f, eq_of_homotopy (λa, idp))
|
||||
|
||||
definition Precategory_hset [reducible] : Precategory :=
|
||||
Precategory.mk hset precategory_hset
|
||||
|
||||
section
|
||||
open iso functor nat_trans
|
||||
definition precategory_functor [instance] [reducible] (D C : Precategory)
|
||||
: precategory (functor C D) :=
|
||||
precategory.mk (λa b, nat_trans a b)
|
||||
(λ a b c g f, nat_trans.compose g f)
|
||||
(λ a, nat_trans.id)
|
||||
(λ a b c d h g f, !nat_trans.assoc)
|
||||
(λ a b f, !nat_trans.id_left)
|
||||
(λ a b f, !nat_trans.id_right)
|
||||
|
||||
definition Precategory_functor [reducible] (D C : Precategory) : Precategory :=
|
||||
precategory.Mk (precategory_functor D C)
|
||||
|
||||
end
|
||||
namespace ops
|
||||
infixr `^c`:35 := Precategory_functor
|
||||
end ops
|
||||
|
||||
section
|
||||
open iso functor nat_trans
|
||||
/- we prove that if a natural transformation is pointwise an to_fun, then it is an to_fun -/
|
||||
variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)]
|
||||
include iso
|
||||
definition nat_trans_inverse : G ⟹ F :=
|
||||
nat_trans.mk
|
||||
(λc, (η c)⁻¹)
|
||||
(λc d f,
|
||||
begin
|
||||
apply comp_inverse_eq_of_eq_comp,
|
||||
apply concat, rotate_left 1, apply assoc,
|
||||
apply eq_inverse_comp_of_comp_eq,
|
||||
apply inverse,
|
||||
apply naturality,
|
||||
end)
|
||||
definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = nat_trans.id :=
|
||||
begin
|
||||
fapply (apd011 nat_trans.mk),
|
||||
apply eq_of_homotopy, intro c, apply left_inverse,
|
||||
apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros,
|
||||
apply is_hset.elim
|
||||
end
|
||||
|
||||
definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = nat_trans.id :=
|
||||
begin
|
||||
fapply (apd011 nat_trans.mk),
|
||||
apply eq_of_homotopy, intro c, apply right_inverse,
|
||||
apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros,
|
||||
apply is_hset.elim
|
||||
end
|
||||
|
||||
definition is_iso_nat_trans : is_iso η :=
|
||||
is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η)
|
||||
|
||||
omit iso
|
||||
-- local attribute is_iso_nat_trans [instance]
|
||||
-- definition functor_iso_functor (H : Π(a : C), F a ≅ G a) : F ≅ G := -- is this true?
|
||||
-- iso.mk _
|
||||
end
|
||||
|
||||
section
|
||||
open iso functor category.ops nat_trans iso.iso
|
||||
/- and conversely, if a natural transformation is an iso, it is componentwise an iso -/
|
||||
variables {C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C)
|
||||
include isoη
|
||||
definition componentwise_is_iso : is_iso (η c) :=
|
||||
@is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c)
|
||||
(ap010 natural_map (right_inverse η) c)
|
||||
|
||||
local attribute componentwise_is_iso [instance]
|
||||
|
||||
definition natural_map_inverse : natural_map η⁻¹ c = (η c)⁻¹ := idp
|
||||
|
||||
definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ :=
|
||||
calc
|
||||
G f = (G f ∘ η c) ∘ (η c)⁻¹ : comp_inverse_cancel_right
|
||||
... = (η c' ∘ F f) ∘ (η c)⁻¹ : by rewrite naturality
|
||||
... = η c' ∘ F f ∘ (η c)⁻¹ : assoc
|
||||
|
||||
definition naturality_iso' {c c' : C} (f : c ⟶ c') : (η c')⁻¹ ∘ G f ∘ η c = F f :=
|
||||
calc
|
||||
(η c')⁻¹ ∘ G f ∘ η c = (η c')⁻¹ ∘ η c' ∘ F f : by rewrite naturality
|
||||
... = F f : inverse_comp_cancel_left
|
||||
|
||||
omit isoη
|
||||
|
||||
definition componentwise_iso (η : F ≅ G) (c : C) : F c ≅ G c :=
|
||||
@iso.mk _ _ _ _ (natural_map (to_hom η) c)
|
||||
(@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c)
|
||||
|
||||
definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) :=
|
||||
iso.eq_mk (idpath (ID (F c)))
|
||||
|
||||
definition componentwise_iso_iso_of_eq (p : F = G) (c : C)
|
||||
: componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) :=
|
||||
eq.rec_on p !componentwise_iso_id
|
||||
|
||||
definition natural_map_hom_of_eq (p : F = G) (c : C)
|
||||
: natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) :=
|
||||
eq.rec_on p idp
|
||||
|
||||
definition natural_map_inv_of_eq (p : F = G) (c : C)
|
||||
: natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ :=
|
||||
eq.rec_on p idp
|
||||
|
||||
end
|
||||
|
||||
namespace ops
|
||||
infixr `×f`:30 := product.prod_functor
|
||||
infixr `ᵒᵖᶠ`:(max+1) := opposite.opposite_functor
|
||||
end ops
|
||||
|
||||
|
||||
end category
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
algebra.precategory
|
||||
===================
|
||||
|
||||
* [basic](basic.hlean)
|
||||
* [functor](functor.hlean)
|
||||
* [constructions](constructions.hlean)
|
||||
* [iso](iso.hlean)
|
||||
* [nat_trans](nat_trans.hlean)
|
||||
* [yoneda](yoneda.hlean)
|
||||
|
|
@ -1,52 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2015 Jakob von Raumer. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.functor
|
||||
Authors: Floris van Doorn, Jakob von Raumer
|
||||
-/
|
||||
|
||||
import .basic .functor
|
||||
|
||||
open category is_trunc eq function sigma sigma.ops
|
||||
|
||||
namespace category
|
||||
structure strict_precategory[class] (ob : Type) extends precategory ob :=
|
||||
(is_hset_ob : is_hset ob)
|
||||
|
||||
attribute strict_precategory.is_hset_ob [instance]
|
||||
|
||||
definition strict_precategory.mk' [reducible] (ob : Type) (C : precategory ob)
|
||||
(H : is_hset ob) : strict_precategory ob :=
|
||||
precategory.rec_on C strict_precategory.mk H
|
||||
|
||||
structure Strict_precategory : Type :=
|
||||
(carrier : Type)
|
||||
(struct : strict_precategory carrier)
|
||||
|
||||
attribute Strict_precategory.struct [instance] [coercion]
|
||||
|
||||
definition Strict_precategory.to_Precategory [coercion] [reducible]
|
||||
(C : Strict_precategory) : Precategory :=
|
||||
Precategory.mk (Strict_precategory.carrier C) C
|
||||
|
||||
open functor
|
||||
|
||||
definition precat_strict_precat : precategory Strict_precategory :=
|
||||
precategory.mk (λ a b, functor a b)
|
||||
(λ a b c g f, functor.compose g f)
|
||||
(λ a, functor.id)
|
||||
(λ a b c d h g f, !functor.assoc)
|
||||
(λ a b f, !functor.id_left)
|
||||
(λ a b f, !functor.id_right)
|
||||
|
||||
definition Precat_of_strict_precats := precategory.Mk precat_strict_precat
|
||||
|
||||
namespace ops
|
||||
|
||||
abbreviation SPreCat := Precat_of_strict_precats
|
||||
--attribute precat_strict_precat [instance]
|
||||
|
||||
end ops
|
||||
|
||||
end category
|
||||
Loading…
Reference in a new issue