feat(category): define colimits as dual of limits
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
df73931a6d
commit
2264759060
4 changed files with 396 additions and 84 deletions
311
hott/algebra/category/colimits.hlean
Normal file
311
hott/algebra/category/colimits.hlean
Normal file
|
|
@ -0,0 +1,311 @@
|
|||
/-
|
||||
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
|
||||
|
||||
Colimits in a category
|
||||
-/
|
||||
|
||||
import .limits .constructions.opposite
|
||||
|
||||
open is_trunc functor nat_trans eq
|
||||
|
||||
-- we define colimits to be the dual of a limit
|
||||
|
||||
namespace category
|
||||
|
||||
variables {ob : Type} [C : precategory ob] {c c' : ob} (D I : Precategory)
|
||||
include C
|
||||
|
||||
definition is_initial [reducible] (c : ob) := @is_terminal _ (opposite C) c
|
||||
|
||||
definition is_contr_of_is_initial [instance] (c d : ob) [H : is_initial d]
|
||||
: is_contr (d ⟶ c) :=
|
||||
H c
|
||||
|
||||
definition initial_morphism (c c' : ob) [H : is_initial c'] : c' ⟶ c :=
|
||||
!center
|
||||
|
||||
definition hom_initial_eq [H : is_initial c'] (f f' : c' ⟶ c) : f = f' :=
|
||||
!is_hprop.elim
|
||||
|
||||
definition eq_initial_morphism [H : is_initial c'] (f : c' ⟶ c) : f = initial_morphism c c' :=
|
||||
!is_hprop.elim
|
||||
|
||||
definition initial_iso_initial {c c' : ob} (H : is_initial c) (K : is_initial c') : c ≅ c' :=
|
||||
iso_of_opposite_iso (@terminal_iso_terminal _ (opposite C) _ _ H K)
|
||||
|
||||
theorem is_hprop_is_initial [instance] : is_hprop (is_initial c) := _
|
||||
|
||||
omit C
|
||||
|
||||
definition has_initial_object [reducible] : Type := has_terminal_object Dᵒᵖ
|
||||
|
||||
definition initial_object [unfold 2] [reducible] [H : has_initial_object D] : D :=
|
||||
has_terminal_object.d Dᵒᵖ
|
||||
|
||||
definition has_initial_object.is_initial [H : has_initial_object D]
|
||||
: is_initial (initial_object D) :=
|
||||
@has_terminal_object.is_terminal (Opposite D) H
|
||||
|
||||
variable {D}
|
||||
definition initial_object_iso_initial_object (H₁ H₂ : has_initial_object D)
|
||||
: @initial_object D H₁ ≅ @initial_object D H₂ :=
|
||||
initial_iso_initial (@has_initial_object.is_initial D H₁) (@has_initial_object.is_initial D H₂)
|
||||
|
||||
set_option pp.coercions true
|
||||
theorem is_hprop_has_initial_object [instance] (D : Category)
|
||||
: is_hprop (has_initial_object D) :=
|
||||
is_hprop_has_terminal_object (Category_opposite D)
|
||||
|
||||
variable (D)
|
||||
definition has_colimits_of_shape [reducible] := has_limits_of_shape Dᵒᵖ Iᵒᵖ
|
||||
|
||||
/-
|
||||
The next definitions states that a category is cocomplete with respect to diagrams
|
||||
in a certain universe. "is_cocomplete.{o₁ h₁ o₂ h₂}" means that D is cocomplete
|
||||
with respect to diagrams of type Precategory.{o₂ h₂}
|
||||
-/
|
||||
|
||||
definition is_cocomplete [reducible] (D : Precategory) := is_complete Dᵒᵖ
|
||||
|
||||
definition has_colimits_of_shape_of_is_cocomplete [instance] [H : is_cocomplete D]
|
||||
(I : Precategory) : has_colimits_of_shape D I := H Iᵒᵖ
|
||||
|
||||
section
|
||||
open pi
|
||||
theorem is_hprop_has_colimits_of_shape [instance] (D : Category) (I : Precategory)
|
||||
: is_hprop (has_colimits_of_shape D I) :=
|
||||
is_hprop_has_limits_of_shape (Category_opposite D) _
|
||||
|
||||
theorem is_hprop_is_cocomplete [instance] (D : Category) : is_hprop (is_cocomplete D) :=
|
||||
is_hprop_is_complete (Category_opposite D)
|
||||
end
|
||||
|
||||
variables {D I} (F : I ⇒ D) [H : has_colimits_of_shape D I] {i j : I}
|
||||
include H
|
||||
|
||||
definition cocone [reducible] := (cone Fᵒᵖ)ᵒᵖ
|
||||
|
||||
definition has_initial_object_cocone [H : has_colimits_of_shape D I]
|
||||
(F : I ⇒ D) : has_initial_object (cocone F) :=
|
||||
begin
|
||||
unfold [has_colimits_of_shape,has_limits_of_shape] at H,
|
||||
exact H Fᵒᵖ
|
||||
end
|
||||
local attribute has_initial_object_cocone [instance]
|
||||
|
||||
definition colimit_cocone : cocone F := limit_cone Fᵒᵖ
|
||||
|
||||
definition is_initial_colimit_cocone [instance] : is_initial (colimit_cocone F) :=
|
||||
is_terminal_limit_cone Fᵒᵖ
|
||||
|
||||
definition colimit_object : D :=
|
||||
limit_object Fᵒᵖ
|
||||
|
||||
definition colimit_nat_trans : constant_functor Iᵒᵖ (colimit_object F) ⟹ Fᵒᵖ :=
|
||||
limit_nat_trans Fᵒᵖ
|
||||
|
||||
definition colimit_morphism (i : I) : F i ⟶ colimit_object F :=
|
||||
limit_morphism Fᵒᵖ i
|
||||
|
||||
variable {H}
|
||||
theorem colimit_commute {i j : I} (f : i ⟶ j)
|
||||
: colimit_morphism F j ∘ to_fun_hom F f = colimit_morphism F i :=
|
||||
by rexact limit_commute Fᵒᵖ f
|
||||
|
||||
variable [H]
|
||||
definition colimit_cone_obj [constructor] {d : D} {η : Πi, F i ⟶ d}
|
||||
(p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : cone_obj Fᵒᵖ :=
|
||||
limit_cone_obj Fᵒᵖ proof p qed
|
||||
|
||||
variable {H}
|
||||
definition colimit_hom {d : D} (η : Πi, F i ⟶ d)
|
||||
(p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : colimit_object F ⟶ d :=
|
||||
hom_limit Fᵒᵖ η proof p qed
|
||||
|
||||
theorem colimit_hom_commute {d : D} (η : Πi, F i ⟶ d)
|
||||
(p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) (i : I)
|
||||
: colimit_hom F η p ∘ colimit_morphism F i = η i :=
|
||||
by rexact hom_limit_commute Fᵒᵖ η proof p qed i
|
||||
|
||||
definition colimit_cone_hom [constructor] {d : D} {η : Πi, F i ⟶ d}
|
||||
(p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h : colimit_object F ⟶ d}
|
||||
(q : Πi, h ∘ colimit_morphism F i = η i)
|
||||
: cone_hom (colimit_cone_obj F p) (colimit_cocone F) :=
|
||||
by rexact limit_cone_hom Fᵒᵖ proof p qed proof q qed
|
||||
|
||||
variable {F}
|
||||
theorem eq_colimit_hom {d : D} {η : Πi, F i ⟶ d}
|
||||
(p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h : colimit_object F ⟶ d}
|
||||
(q : Πi, h ∘ colimit_morphism F i = η i) : h = colimit_hom F η p :=
|
||||
by rexact @eq_hom_limit _ _ Fᵒᵖ _ _ _ proof p qed _ proof q qed
|
||||
|
||||
theorem colimit_cocone_unique {d : D} {η : Πi, F i ⟶ d}
|
||||
(p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i)
|
||||
{h₁ : colimit_object F ⟶ d} (q₁ : Πi, h₁ ∘ colimit_morphism F i = η i)
|
||||
{h₂ : colimit_object F ⟶ d} (q₂ : Πi, h₂ ∘ colimit_morphism F i = η i) : h₁ = h₂ :=
|
||||
@limit_cone_unique _ _ Fᵒᵖ _ _ _ proof p qed _ proof q₁ qed _ proof q₂ qed
|
||||
|
||||
omit H
|
||||
|
||||
variable (F)
|
||||
definition colimit_object_iso_colimit_object [constructor] (H₁ H₂ : has_colimits_of_shape D I) :
|
||||
@(colimit_object F) H₁ ≅ @(colimit_object F) H₂ :=
|
||||
iso_of_opposite_iso (limit_object_iso_limit_object Fᵒᵖ H₁ H₂)
|
||||
|
||||
section bin_coproducts
|
||||
open bool prod.ops
|
||||
definition has_binary_coproducts [reducible] (D : Precategory) := has_colimits_of_shape D c2
|
||||
variables [K : has_binary_coproducts D] (d d' : D)
|
||||
include K
|
||||
|
||||
definition coproduct_object : D :=
|
||||
colimit_object (c2_functor D d d')
|
||||
|
||||
infixr + := coproduct_object
|
||||
|
||||
definition inl : d ⟶ d + d' :=
|
||||
colimit_morphism (c2_functor D d d') ff
|
||||
|
||||
definition inr : d' ⟶ d + d' :=
|
||||
colimit_morphism (c2_functor D d d') tt
|
||||
|
||||
variables {d d'}
|
||||
definition coproduct_hom {x : D} (f : d ⟶ x) (g : d' ⟶ x) : d + d' ⟶ x :=
|
||||
colimit_hom (c2_functor D d d') (bool.rec f g)
|
||||
(by intro b₁ b₂ f; induction b₁: induction b₂: esimp at *; try contradiction: apply id_right)
|
||||
|
||||
theorem coproduct_hom_inl {x : D} (f : d ⟶ x) (g : d' ⟶ x) : coproduct_hom f g ∘ !inl = f :=
|
||||
colimit_hom_commute (c2_functor D d d') (bool.rec f g) _ ff
|
||||
|
||||
theorem coproduct_hom_inr {x : D} (f : d ⟶ x) (g : d' ⟶ x) : coproduct_hom f g ∘ !inr = g :=
|
||||
colimit_hom_commute (c2_functor D d d') (bool.rec f g) _ tt
|
||||
|
||||
theorem eq_coproduct_hom {x : D} {f : d ⟶ x} {g : d' ⟶ x} {h : d + d' ⟶ x}
|
||||
(p : h ∘ !inl = f) (q : h ∘ !inr = g) : h = coproduct_hom f g :=
|
||||
eq_colimit_hom _ (bool.rec p q)
|
||||
|
||||
theorem coproduct_cocone_unique {x : D} {f : d ⟶ x} {g : d' ⟶ x}
|
||||
{h₁ : d + d' ⟶ x} (p₁ : h₁ ∘ !inl = f) (q₁ : h₁ ∘ !inr = g)
|
||||
{h₂ : d + d' ⟶ x} (p₂ : h₂ ∘ !inl = f) (q₂ : h₂ ∘ !inr = g) : h₁ = h₂ :=
|
||||
eq_coproduct_hom p₁ q₁ ⬝ (eq_coproduct_hom p₂ q₂)⁻¹
|
||||
|
||||
variable (D)
|
||||
definition coproduct_functor [constructor] : D ×c D ⇒ D :=
|
||||
functor.mk
|
||||
(λx, coproduct_object x.1 x.2)
|
||||
(λx y f, coproduct_hom (!inl ∘ f.1) (!inr ∘ f.2))
|
||||
abstract begin intro x, symmetry, apply eq_coproduct_hom: apply id_comp_eq_comp_id end end
|
||||
abstract begin intro x y z g f, symmetry, apply eq_coproduct_hom,
|
||||
rewrite [-assoc,coproduct_hom_inl,assoc,coproduct_hom_inl,-assoc],
|
||||
rewrite [-assoc,coproduct_hom_inr,assoc,coproduct_hom_inr,-assoc] end end
|
||||
omit K
|
||||
variables {D} (d d')
|
||||
|
||||
definition coproduct_object_iso_coproduct_object [constructor] (H₁ H₂ : has_binary_coproducts D) :
|
||||
@coproduct_object D H₁ d d' ≅ @coproduct_object D H₂ d d' :=
|
||||
colimit_object_iso_colimit_object _ H₁ H₂
|
||||
|
||||
end bin_coproducts
|
||||
|
||||
/-
|
||||
intentionally we define coproducts in terms of colimits,
|
||||
but coequalizers in terms of equalizers, to see which characterization is more useful
|
||||
-/
|
||||
|
||||
section coequalizers
|
||||
open bool prod.ops sum equalizer_category_hom
|
||||
|
||||
definition has_coequalizers [reducible] (D : Precategory) := has_equalizers Dᵒᵖ
|
||||
variables [K : has_coequalizers D]
|
||||
include K
|
||||
|
||||
variables {d d' x : D} (f g : d ⟶ d')
|
||||
definition coequalizer_object : D :=
|
||||
!(@equalizer_object Dᵒᵖ) f g
|
||||
|
||||
definition coequalizer : d' ⟶ coequalizer_object f g :=
|
||||
!(@equalizer Dᵒᵖ)
|
||||
|
||||
theorem coequalizes : coequalizer f g ∘ f = coequalizer f g ∘ g :=
|
||||
by rexact !(@equalizes Dᵒᵖ)
|
||||
|
||||
variables {f g}
|
||||
definition coequalizer_hom (h : d' ⟶ x) (p : h ∘ f = h ∘ g) : coequalizer_object f g ⟶ x :=
|
||||
!(@hom_equalizer Dᵒᵖ) proof p qed
|
||||
|
||||
theorem coequalizer_hom_coequalizer (h : d' ⟶ x) (p : h ∘ f = h ∘ g)
|
||||
: coequalizer_hom h p ∘ coequalizer f g = h :=
|
||||
by rexact !(@equalizer_hom_equalizer Dᵒᵖ)
|
||||
|
||||
theorem eq_coequalizer_hom {h : d' ⟶ x} (p : h ∘ f = h ∘ g) {i : coequalizer_object f g ⟶ x}
|
||||
(q : i ∘ coequalizer f g = h) : i = coequalizer_hom h p :=
|
||||
by rexact !(@eq_hom_equalizer Dᵒᵖ) proof q qed
|
||||
|
||||
theorem coequalizer_cocone_unique {h : d' ⟶ x} (p : h ∘ f = h ∘ g)
|
||||
{i₁ : coequalizer_object f g ⟶ x} (q₁ : i₁ ∘ coequalizer f g = h)
|
||||
{i₂ : coequalizer_object f g ⟶ x} (q₂ : i₂ ∘ coequalizer f g = h) : i₁ = i₂ :=
|
||||
!(@equalizer_cone_unique Dᵒᵖ) proof p qed proof q₁ qed proof q₂ qed
|
||||
|
||||
omit K
|
||||
variables (f g)
|
||||
definition coequalizer_object_iso_coequalizer_object [constructor] (H₁ H₂ : has_coequalizers D) :
|
||||
@coequalizer_object D H₁ _ _ f g ≅ @coequalizer_object D H₂ _ _ f g :=
|
||||
iso_of_opposite_iso !(@equalizer_object_iso_equalizer_object Dᵒᵖ)
|
||||
|
||||
end coequalizers
|
||||
|
||||
section pushouts
|
||||
open bool prod.ops sum pullback_category_hom
|
||||
|
||||
definition has_pushouts [reducible] (D : Precategory) := has_pullbacks Dᵒᵖ
|
||||
variables [K : has_pushouts D]
|
||||
include K
|
||||
|
||||
variables {d₁ d₂ d₃ x : D} (f : d₁ ⟶ d₂) (g : d₁ ⟶ d₃)
|
||||
definition pushout_object : D :=
|
||||
!(@pullback_object Dᵒᵖ) f g
|
||||
|
||||
definition pushout : d₃ ⟶ pushout_object f g :=
|
||||
!(@pullback Dᵒᵖ)
|
||||
|
||||
definition pushout_rev : d₂ ⟶ pushout_object f g :=
|
||||
!(@pullback_rev Dᵒᵖ)
|
||||
|
||||
theorem pushout_commutes : pushout_rev f g ∘ f = pushout f g ∘ g :=
|
||||
by rexact !(@pullback_commutes Dᵒᵖ)
|
||||
|
||||
variables {f g}
|
||||
definition pushout_hom (h₁ : d₂ ⟶ x) (h₂ : d₃ ⟶ x) (p : h₁ ∘ f = h₂ ∘ g)
|
||||
: pushout_object f g ⟶ x :=
|
||||
!(@hom_pullback Dᵒᵖ) proof p qed
|
||||
|
||||
theorem pushout_hom_pushout (h₁ : d₂ ⟶ x) (h₂ : d₃ ⟶ x) (p : h₁ ∘ f = h₂ ∘ g)
|
||||
: pushout_hom h₁ h₂ p ∘ pushout f g = h₂ :=
|
||||
by rexact !(@pullback_hom_pullback Dᵒᵖ)
|
||||
|
||||
theorem pushout_hom_pushout_rev (h₁ : d₂ ⟶ x) (h₂ : d₃ ⟶ x) (p : h₁ ∘ f = h₂ ∘ g)
|
||||
: pushout_hom h₁ h₂ p ∘ pushout_rev f g = h₁ :=
|
||||
by rexact !(@pullback_rev_hom_pullback Dᵒᵖ)
|
||||
|
||||
theorem eq_pushout_hom {h₁ : d₂ ⟶ x} {h₂ : d₃ ⟶ x} (p : h₁ ∘ f = h₂ ∘ g)
|
||||
{i : pushout_object f g ⟶ x} (q : i ∘ pushout f g = h₂) (r : i ∘ pushout_rev f g = h₁)
|
||||
: i = pushout_hom h₁ h₂ p :=
|
||||
by rexact !(@eq_hom_pullback Dᵒᵖ) proof q qed proof r qed
|
||||
|
||||
theorem pushout_cocone_unique {h₁ : d₂ ⟶ x} {h₂ : d₃ ⟶ x} (p : h₁ ∘ f = h₂ ∘ g)
|
||||
{i₁ : pushout_object f g ⟶ x} (q₁ : i₁ ∘ pushout f g = h₂) (r₁ : i₁ ∘ pushout_rev f g = h₁)
|
||||
{i₂ : pushout_object f g ⟶ x} (q₂ : i₂ ∘ pushout f g = h₂) (r₂ : i₂ ∘ pushout_rev f g = h₁)
|
||||
: i₁ = i₂ :=
|
||||
!(@pullback_cone_unique Dᵒᵖ) proof p qed proof q₁ qed proof r₁ qed proof q₂ qed proof r₂ qed
|
||||
|
||||
omit K
|
||||
variables (f g)
|
||||
definition pushout_object_iso_pushout_object [constructor] (H₁ H₂ : has_pushouts D) :
|
||||
@pushout_object D H₁ _ _ _ f g ≅ @pushout_object D H₂ _ _ _ f g :=
|
||||
iso_of_opposite_iso !(@pullback_object_iso_pullback_object (Opposite D))
|
||||
|
||||
end pushouts
|
||||
|
||||
end category
|
||||
|
|
@ -18,8 +18,8 @@ namespace category
|
|||
|
||||
include H HR HA
|
||||
|
||||
-- we call a diagram (or category) sparse if you cannot compose two morphism, except the ones which come from equality
|
||||
definition sparse_diagram' [constructor] : precategory A :=
|
||||
-- we call a category sparse if you cannot compose two morphism, except the ones which come from equality
|
||||
definition sparse_category' [constructor] : precategory A :=
|
||||
precategory.mk
|
||||
(λa b, R a b ⊎ a = b)
|
||||
begin
|
||||
|
|
@ -38,11 +38,11 @@ namespace category
|
|||
abstract by intros a b f; induction f with rf pf: reflexivity end
|
||||
abstract by intros a b f; (induction f with rf pf: esimp); rewrite idp_con end
|
||||
|
||||
definition sparse_diagram [constructor] : Precategory :=
|
||||
precategory.Mk (sparse_diagram' R @H)
|
||||
definition sparse_category [constructor] : Precategory :=
|
||||
precategory.Mk (sparse_category' R @H)
|
||||
|
||||
definition sparse_diagram_functor [constructor] (C : Precategory) (f : A → C)
|
||||
(g : Π{a b} (r : R a b), f a ⟶ f b) : sparse_diagram R H ⇒ C :=
|
||||
definition sparse_category_functor [constructor] (C : Precategory) (f : A → C)
|
||||
(g : Π{a b} (r : R a b), f a ⟶ f b) : sparse_category R H ⇒ C :=
|
||||
functor.mk f
|
||||
(λa b, sum.rec g (eq.rec id))
|
||||
(λa, idp)
|
||||
|
|
@ -58,14 +58,14 @@ namespace category
|
|||
omit H HR HA
|
||||
|
||||
section equalizer
|
||||
inductive equalizer_diagram_hom : bool → bool → Type :=
|
||||
| f1 : equalizer_diagram_hom ff tt
|
||||
| f2 : equalizer_diagram_hom ff tt
|
||||
inductive equalizer_category_hom : bool → bool → Type :=
|
||||
| f1 : equalizer_category_hom ff tt
|
||||
| f2 : equalizer_category_hom ff tt
|
||||
|
||||
open equalizer_diagram_hom
|
||||
theorem is_hset_equalizer_diagram_hom (b₁ b₂ : bool) : is_hset (equalizer_diagram_hom b₁ b₂) :=
|
||||
open equalizer_category_hom
|
||||
theorem is_hset_equalizer_category_hom (b₁ b₂ : bool) : is_hset (equalizer_category_hom b₁ b₂) :=
|
||||
begin
|
||||
assert H : Πb b', equalizer_diagram_hom b b' ≃ bool.rec (bool.rec empty bool) (λb, empty) b b',
|
||||
assert H : Πb b', equalizer_category_hom b b' ≃ bool.rec (bool.rec empty bool) (λb, empty) b b',
|
||||
{ intro b b', fapply equiv.MK,
|
||||
{ intro x, induction x, exact ff, exact tt},
|
||||
{ intro v, induction b: induction b': induction v, exact f1, exact f2},
|
||||
|
|
@ -75,44 +75,44 @@ namespace category
|
|||
induction b₁: induction b₂: exact _
|
||||
end
|
||||
|
||||
local attribute is_hset_equalizer_diagram_hom [instance]
|
||||
definition equalizer_diagram [constructor] : Precategory :=
|
||||
sparse_diagram
|
||||
equalizer_diagram_hom
|
||||
local attribute is_hset_equalizer_category_hom [instance]
|
||||
definition equalizer_category [constructor] : Precategory :=
|
||||
sparse_category
|
||||
equalizer_category_hom
|
||||
begin intro a b c g f; cases g: cases f end
|
||||
|
||||
definition equalizer_diagram_functor [constructor] (C : Precategory) {x y : C} (f g : x ⟶ y)
|
||||
: equalizer_diagram ⇒ C :=
|
||||
sparse_diagram_functor _ _ C
|
||||
definition equalizer_category_functor [constructor] (C : Precategory) {x y : C} (f g : x ⟶ y)
|
||||
: equalizer_category ⇒ C :=
|
||||
sparse_category_functor _ _ C
|
||||
(bool.rec x y)
|
||||
begin intro a b h; induction h, exact f, exact g end
|
||||
end equalizer
|
||||
|
||||
section pullback
|
||||
inductive pullback_diagram_ob : Type :=
|
||||
| TR : pullback_diagram_ob
|
||||
| BL : pullback_diagram_ob
|
||||
| BR : pullback_diagram_ob
|
||||
inductive pullback_category_ob : Type :=
|
||||
| TR : pullback_category_ob
|
||||
| BL : pullback_category_ob
|
||||
| BR : pullback_category_ob
|
||||
|
||||
theorem pullback_diagram_ob_decidable_equality : decidable_eq pullback_diagram_ob :=
|
||||
theorem pullback_category_ob_decidable_equality : decidable_eq pullback_category_ob :=
|
||||
begin
|
||||
intro x y; induction x: induction y:
|
||||
try exact decidable.inl idp:
|
||||
apply decidable.inr; contradiction
|
||||
end
|
||||
|
||||
open pullback_diagram_ob
|
||||
inductive pullback_diagram_hom : pullback_diagram_ob → pullback_diagram_ob → Type :=
|
||||
| f1 : pullback_diagram_hom TR BR
|
||||
| f2 : pullback_diagram_hom BL BR
|
||||
open pullback_category_ob
|
||||
inductive pullback_category_hom : pullback_category_ob → pullback_category_ob → Type :=
|
||||
| f1 : pullback_category_hom TR BR
|
||||
| f2 : pullback_category_hom BL BR
|
||||
|
||||
open pullback_diagram_hom
|
||||
theorem is_hset_pullback_diagram_hom (b₁ b₂ : pullback_diagram_ob)
|
||||
: is_hset (pullback_diagram_hom b₁ b₂) :=
|
||||
open pullback_category_hom
|
||||
theorem is_hset_pullback_category_hom (b₁ b₂ : pullback_category_ob)
|
||||
: is_hset (pullback_category_hom b₁ b₂) :=
|
||||
begin
|
||||
assert H : Πb b', pullback_diagram_hom b b' ≃
|
||||
pullback_diagram_ob.rec (λb, empty) (λb, empty)
|
||||
(pullback_diagram_ob.rec unit unit empty) b' b,
|
||||
assert H : Πb b', pullback_category_hom b b' ≃
|
||||
pullback_category_ob.rec (λb, empty) (λb, empty)
|
||||
(pullback_category_ob.rec unit unit empty) b' b,
|
||||
{ intro b b', fapply equiv.MK,
|
||||
{ intro x, induction x: exact star},
|
||||
{ intro v, induction b: induction b': induction v, exact f1, exact f2},
|
||||
|
|
@ -122,16 +122,16 @@ namespace category
|
|||
induction b₁: induction b₂: exact _
|
||||
end
|
||||
|
||||
local attribute is_hset_pullback_diagram_hom pullback_diagram_ob_decidable_equality [instance]
|
||||
definition pullback_diagram [constructor] : Precategory :=
|
||||
sparse_diagram
|
||||
pullback_diagram_hom
|
||||
local attribute is_hset_pullback_category_hom pullback_category_ob_decidable_equality [instance]
|
||||
definition pullback_category [constructor] : Precategory :=
|
||||
sparse_category
|
||||
pullback_category_hom
|
||||
begin intro a b c g f; cases g: cases f end
|
||||
|
||||
definition pullback_diagram_functor [constructor] (C : Precategory) {x y z : C}
|
||||
(f : x ⟶ z) (g : y ⟶ z) : pullback_diagram ⇒ C :=
|
||||
sparse_diagram_functor _ _ C
|
||||
(pullback_diagram_ob.rec x y z)
|
||||
definition pullback_category_functor [constructor] (C : Precategory) {x y z : C}
|
||||
(f : x ⟶ z) (g : y ⟶ z) : pullback_category ⇒ C :=
|
||||
sparse_category_functor _ _ C
|
||||
(pullback_category_ob.rec x y z)
|
||||
begin intro a b h; induction h, exact f, exact g end
|
||||
end pullback
|
||||
|
||||
|
|
|
|||
|
|
@ -117,7 +117,7 @@ namespace category
|
|||
esimp, apply p}}
|
||||
end
|
||||
|
||||
definition is_complete_set.{u v w} : is_complete.{(max u v w)+1 (max u v w) v w} set :=
|
||||
definition is_complete_set.{u v w} [instance] : is_complete.{(max u v w)+1 (max u v w) v w} set :=
|
||||
begin
|
||||
intro I F, fapply has_terminal_object.mk,
|
||||
{ exact is_complete_set_cone.{u v w} I F},
|
||||
|
|
@ -137,4 +137,5 @@ namespace category
|
|||
apply is_trunc_pi, intro f,
|
||||
apply is_trunc_eq}}}
|
||||
end
|
||||
|
||||
end category
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ namespace category
|
|||
/-
|
||||
The next definitions states that a category is complete with respect to diagrams
|
||||
in a certain universe. "is_complete.{o₁ h₁ o₂ h₂}" means that D is complete
|
||||
with respect to diagrams of type Precategory.{o₂ h₂}
|
||||
with respect to diagrams with shape in Precategory.{o₂ h₂}
|
||||
-/
|
||||
|
||||
definition is_complete.{o₁ h₁ o₂ h₂} [class] (D : Precategory.{o₁ h₁}) :=
|
||||
|
|
@ -86,7 +86,7 @@ namespace category
|
|||
theorem is_hprop_is_complete [instance] (D : Category) : is_hprop (is_complete D) := _
|
||||
end
|
||||
|
||||
variables {I D}
|
||||
variables {D I}
|
||||
definition has_terminal_object_cone [H : has_limits_of_shape D I]
|
||||
(F : I ⇒ D) : has_terminal_object (cone F) := H F
|
||||
local attribute has_terminal_object_cone [instance]
|
||||
|
|
@ -123,7 +123,7 @@ namespace category
|
|||
(p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) : d ⟶ limit_object F :=
|
||||
cone_hom.f (@(terminal_morphism (limit_cone_obj F p) _) (is_terminal_limit_cone _))
|
||||
|
||||
definition hom_limit_commute {d : D} (η : Πi, d ⟶ F i)
|
||||
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_hom.p (@(terminal_morphism (limit_cone_obj F p) _) (is_terminal_limit_cone _)) i
|
||||
|
|
@ -189,10 +189,10 @@ namespace category
|
|||
hom_limit (c2_functor D d d') (bool.rec f g)
|
||||
(by intro b₁ b₂ f; induction b₁: induction b₂: esimp at *; try contradiction: apply id_left)
|
||||
|
||||
definition pr1_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr1 ∘ hom_product f g = f :=
|
||||
theorem pr1_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr1 ∘ hom_product f g = f :=
|
||||
hom_limit_commute (c2_functor D d d') (bool.rec f g) _ ff
|
||||
|
||||
definition pr2_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr2 ∘ hom_product f g = g :=
|
||||
theorem pr2_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr2 ∘ hom_product f g = g :=
|
||||
hom_limit_commute (c2_functor D d d') (bool.rec f g) _ tt
|
||||
|
||||
theorem eq_hom_product {x : D} {f : x ⟶ d} {g : x ⟶ d'} {h : x ⟶ d × d'}
|
||||
|
|
@ -201,8 +201,7 @@ namespace category
|
|||
|
||||
theorem product_cone_unique {x : D} {f : x ⟶ d} {g : x ⟶ d'}
|
||||
{h₁ : x ⟶ d × d'} (p₁ : !pr1 ∘ h₁ = f) (q₁ : !pr2 ∘ h₁ = g)
|
||||
{h₂ : x ⟶ d × d'} (p₂ : !pr1 ∘ h₂ = f) (q₂ : !pr2 ∘ h₂ = g)
|
||||
: h₁ = h₂ :=
|
||||
{h₂ : x ⟶ d × d'} (p₂ : !pr1 ∘ h₂ = f) (q₂ : !pr2 ∘ h₂ = g) : h₁ = h₂ :=
|
||||
eq_hom_product p₁ q₁ ⬝ (eq_hom_product p₂ q₂)⁻¹
|
||||
|
||||
variable (D)
|
||||
|
|
@ -224,25 +223,25 @@ namespace category
|
|||
end bin_products
|
||||
|
||||
section equalizers
|
||||
open bool prod.ops sum equalizer_diagram_hom
|
||||
definition has_equalizers [reducible] (D : Precategory) := has_limits_of_shape D equalizer_diagram
|
||||
open bool prod.ops sum equalizer_category_hom
|
||||
definition has_equalizers [reducible] (D : Precategory) := has_limits_of_shape D equalizer_category
|
||||
variables [K : has_equalizers D]
|
||||
include K
|
||||
|
||||
variables {d d' x : D} (f g : d ⟶ d')
|
||||
definition equalizer_object : D :=
|
||||
limit_object (equalizer_diagram_functor D f g)
|
||||
limit_object (equalizer_category_functor D f g)
|
||||
|
||||
definition equalizer : equalizer_object f g ⟶ d :=
|
||||
limit_morphism (equalizer_diagram_functor D f g) ff
|
||||
limit_morphism (equalizer_category_functor D f g) ff
|
||||
|
||||
theorem equalizes : f ∘ equalizer f g = g ∘ equalizer f g :=
|
||||
limit_commute (equalizer_diagram_functor D f g) (inl f1) ⬝
|
||||
(limit_commute (equalizer_diagram_functor D f g) (inl f2))⁻¹
|
||||
limit_commute (equalizer_category_functor D f g) (inl f1) ⬝
|
||||
(limit_commute (equalizer_category_functor D f g) (inl f2))⁻¹
|
||||
|
||||
variables {f g}
|
||||
definition hom_equalizer (h : x ⟶ d) (p : f ∘ h = g ∘ h) : x ⟶ equalizer_object f g :=
|
||||
hom_limit (equalizer_diagram_functor D f g)
|
||||
hom_limit (equalizer_category_functor D f g)
|
||||
(bool.rec h (g ∘ h))
|
||||
begin
|
||||
intro b₁ b₂ i; induction i with j j: induction j,
|
||||
|
|
@ -250,15 +249,15 @@ namespace category
|
|||
exact p, reflexivity, apply id_left
|
||||
end
|
||||
|
||||
definition equalizer_hom_equalizer (h : x ⟶ d) (p : f ∘ h = g ∘ h)
|
||||
theorem equalizer_hom_equalizer (h : x ⟶ d) (p : f ∘ h = g ∘ h)
|
||||
: equalizer f g ∘ hom_equalizer h p = h :=
|
||||
hom_limit_commute (equalizer_diagram_functor D f g) (bool.rec h (g ∘ h)) _ ff
|
||||
hom_limit_commute (equalizer_category_functor D f g) (bool.rec h (g ∘ h)) _ ff
|
||||
|
||||
theorem eq_hom_equalizer {h : x ⟶ d} (p : f ∘ h = g ∘ h) {i : x ⟶ equalizer_object f g}
|
||||
(q : equalizer f g ∘ i = h) : i = hom_equalizer h p :=
|
||||
eq_hom_limit _ (bool.rec q
|
||||
begin
|
||||
refine ap (λx, x ∘ i) (limit_commute (equalizer_diagram_functor D f g) (inl f2))⁻¹ ⬝ _,
|
||||
refine ap (λx, x ∘ i) (limit_commute (equalizer_category_functor D f g) (inl f2))⁻¹ ⬝ _,
|
||||
refine !assoc⁻¹ ⬝ _,
|
||||
exact ap (λx, _ ∘ x) q
|
||||
end)
|
||||
|
|
@ -268,6 +267,7 @@ namespace category
|
|||
{i₂ : x ⟶ equalizer_object f g} (q₂ : equalizer f g ∘ i₂ = h) : i₁ = i₂ :=
|
||||
eq_hom_equalizer p q₁ ⬝ (eq_hom_equalizer p q₂)⁻¹
|
||||
|
||||
omit K
|
||||
variables (f g)
|
||||
definition equalizer_object_iso_equalizer_object [constructor] (H₁ H₂ : has_equalizers D) :
|
||||
@equalizer_object D H₁ _ _ f g ≅ @equalizer_object D H₂ _ _ f g :=
|
||||
|
|
@ -276,56 +276,56 @@ namespace category
|
|||
end equalizers
|
||||
|
||||
section pullbacks
|
||||
open sum prod.ops pullback_diagram_ob pullback_diagram_hom
|
||||
definition has_pullbacks [reducible] (D : Precategory) := has_limits_of_shape D pullback_diagram
|
||||
open sum prod.ops pullback_category_ob pullback_category_hom
|
||||
definition has_pullbacks [reducible] (D : Precategory) := has_limits_of_shape D pullback_category
|
||||
variables [K : has_pullbacks D]
|
||||
include K
|
||||
|
||||
variables {d₁ d₂ d₃ x : D} (f : d₁ ⟶ d₃) (g : d₂ ⟶ d₃)
|
||||
definition pullback_object : D :=
|
||||
limit_object (pullback_diagram_functor D f g)
|
||||
limit_object (pullback_category_functor D f g)
|
||||
|
||||
definition pullback : pullback_object f g ⟶ d₁ :=
|
||||
limit_morphism (pullback_diagram_functor D f g) TR
|
||||
definition pullback : pullback_object f g ⟶ d₂ :=
|
||||
limit_morphism (pullback_category_functor D f g) BL
|
||||
|
||||
definition pullback_rev : pullback_object f g ⟶ d₂ :=
|
||||
limit_morphism (pullback_diagram_functor D f g) BL
|
||||
definition pullback_rev : pullback_object f g ⟶ d₁ :=
|
||||
limit_morphism (pullback_category_functor D f g) TR
|
||||
|
||||
theorem pullback_commutes : f ∘ pullback f g = g ∘ pullback_rev f g :=
|
||||
limit_commute (pullback_diagram_functor D f g) (inl f1) ⬝
|
||||
(limit_commute (pullback_diagram_functor D f g) (inl f2))⁻¹
|
||||
theorem pullback_commutes : f ∘ pullback_rev f g = g ∘ pullback f g :=
|
||||
limit_commute (pullback_category_functor D f g) (inl f1) ⬝
|
||||
(limit_commute (pullback_category_functor D f g) (inl f2))⁻¹
|
||||
|
||||
variables {f g}
|
||||
definition hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
|
||||
: x ⟶ pullback_object f g :=
|
||||
hom_limit (pullback_diagram_functor D f g)
|
||||
(pullback_diagram_ob.rec h₁ h₂ (g ∘ h₂))
|
||||
hom_limit (pullback_category_functor D f g)
|
||||
(pullback_category_ob.rec h₁ h₂ (g ∘ h₂))
|
||||
begin
|
||||
intro i₁ i₂ k; induction k with j j: induction j,
|
||||
exact p, reflexivity, apply id_left
|
||||
end
|
||||
|
||||
definition pullback_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
|
||||
: pullback f g ∘ hom_pullback h₁ h₂ p = h₁ :=
|
||||
hom_limit_commute (pullback_diagram_functor D f g) (pullback_diagram_ob.rec h₁ h₂ (g ∘ h₂)) _ TR
|
||||
theorem pullback_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
|
||||
: pullback f g ∘ hom_pullback h₁ h₂ p = h₂ :=
|
||||
hom_limit_commute (pullback_category_functor D f g) (pullback_category_ob.rec h₁ h₂ (g ∘ h₂)) _ BL
|
||||
|
||||
definition pullback_rev_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
|
||||
: pullback_rev f g ∘ hom_pullback h₁ h₂ p = h₂ :=
|
||||
hom_limit_commute (pullback_diagram_functor D f g) (pullback_diagram_ob.rec h₁ h₂ (g ∘ h₂)) _ BL
|
||||
theorem pullback_rev_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
|
||||
: pullback_rev f g ∘ hom_pullback h₁ h₂ p = h₁ :=
|
||||
hom_limit_commute (pullback_category_functor D f g) (pullback_category_ob.rec h₁ h₂ (g ∘ h₂)) _ TR
|
||||
|
||||
theorem eq_hom_pullback {h₁ : x ⟶ d₁} {h₂ : x ⟶ d₂} (p : f ∘ h₁ = g ∘ h₂)
|
||||
{k : x ⟶ pullback_object f g} (q : pullback f g ∘ k = h₁) (r : pullback_rev f g ∘ k = h₂)
|
||||
{k : x ⟶ pullback_object f g} (q : pullback f g ∘ k = h₂) (r : pullback_rev f g ∘ k = h₁)
|
||||
: k = hom_pullback h₁ h₂ p :=
|
||||
eq_hom_limit _ (pullback_diagram_ob.rec q r
|
||||
eq_hom_limit _ (pullback_category_ob.rec r q
|
||||
begin
|
||||
refine ap (λx, x ∘ k) (limit_commute (pullback_diagram_functor D f g) (inl f2))⁻¹ ⬝ _,
|
||||
refine ap (λx, x ∘ k) (limit_commute (pullback_category_functor D f g) (inl f2))⁻¹ ⬝ _,
|
||||
refine !assoc⁻¹ ⬝ _,
|
||||
exact ap (λx, _ ∘ x) r
|
||||
exact ap (λx, _ ∘ x) q
|
||||
end)
|
||||
|
||||
theorem pullback_cone_unique {h₁ : x ⟶ d₁} {h₂ : x ⟶ d₂} (p : f ∘ h₁ = g ∘ h₂)
|
||||
{k₁ : x ⟶ pullback_object f g} (q₁ : pullback f g ∘ k₁ = h₁) (r₁ : pullback_rev f g ∘ k₁ = h₂)
|
||||
{k₂ : x ⟶ pullback_object f g} (q₂ : pullback f g ∘ k₂ = h₁) (r₂ : pullback_rev f g ∘ k₂ = h₂)
|
||||
{k₁ : x ⟶ pullback_object f g} (q₁ : pullback f g ∘ k₁ = h₂) (r₁ : pullback_rev f g ∘ k₁ = h₁)
|
||||
{k₂ : x ⟶ pullback_object f g} (q₂ : pullback f g ∘ k₂ = h₂) (r₂ : pullback_rev f g ∘ k₂ = h₁)
|
||||
: k₁ = k₂ :=
|
||||
(eq_hom_pullback p q₁ r₁) ⬝ (eq_hom_pullback p q₂ r₂)⁻¹
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue