198 lines
7.4 KiB
Text
198 lines
7.4 KiB
Text
/-
|
||
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
|
||
|
||
Definition of general colimits and sequential colimits.
|
||
-/
|
||
|
||
/- definition of a general colimit -/
|
||
open eq nat quotient sigma equiv equiv.ops is_trunc
|
||
|
||
namespace colimit
|
||
section
|
||
parameters {I J : Type} (A : I → Type) (dom cod : J → I)
|
||
(f : Π(j : J), A (dom j) → A (cod j))
|
||
variables {i : I} (a : A i) (j : J) (b : A (dom j))
|
||
|
||
local abbreviation B := Σ(i : I), A i
|
||
inductive colim_rel : B → B → Type :=
|
||
| Rmk : Π{j : J} (a : A (dom j)), colim_rel ⟨cod j, f j a⟩ ⟨dom j, a⟩
|
||
open colim_rel
|
||
local abbreviation R := colim_rel
|
||
|
||
-- TODO: define this in root namespace
|
||
definition colimit : Type :=
|
||
quotient colim_rel
|
||
|
||
definition incl : colimit :=
|
||
class_of R ⟨i, a⟩
|
||
abbreviation ι := @incl
|
||
|
||
definition cglue : ι (f j b) = ι b :=
|
||
eq_of_rel colim_rel (Rmk f b)
|
||
|
||
protected definition rec {P : colimit → Type}
|
||
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x)
|
||
(y : colimit) : P y :=
|
||
begin
|
||
fapply (quotient.rec_on y),
|
||
{ intro a, cases a, apply Pincl},
|
||
{ intro a a' H, cases H, apply Pglue}
|
||
end
|
||
|
||
protected definition rec_on [reducible] {P : colimit → Type} (y : colimit)
|
||
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) : P y :=
|
||
rec Pincl Pglue y
|
||
|
||
theorem rec_cglue {P : colimit → Type}
|
||
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x)
|
||
{j : J} (x : A (dom j)) : apdo (rec Pincl Pglue) (cglue j x) = Pglue j x :=
|
||
!rec_eq_of_rel
|
||
|
||
protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) (y : colimit) : P :=
|
||
rec Pincl (λj a, pathover_of_eq (Pglue j a)) y
|
||
|
||
protected definition elim_on [reducible] {P : Type} (y : colimit)
|
||
(Pincl : Π⦃i : I⦄ (x : A i), P)
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) : P :=
|
||
elim Pincl Pglue y
|
||
|
||
theorem elim_cglue {P : Type}
|
||
(Pincl : Π⦃i : I⦄ (x : A i), P)
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x)
|
||
{j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x :=
|
||
begin
|
||
apply eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)),
|
||
rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cglue],
|
||
end
|
||
|
||
protected definition elim_type (Pincl : Π⦃i : I⦄ (x : A i), Type)
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) ≃ Pincl x) (y : colimit) : Type :=
|
||
elim Pincl (λj a, ua (Pglue j a)) y
|
||
|
||
protected definition elim_type_on [reducible] (y : colimit)
|
||
(Pincl : Π⦃i : I⦄ (x : A i), Type)
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) ≃ Pincl x) : Type :=
|
||
elim_type Pincl Pglue y
|
||
|
||
theorem elim_type_cglue (Pincl : Π⦃i : I⦄ (x : A i), Type)
|
||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) ≃ Pincl x)
|
||
{j : J} (x : A (dom j)) : transport (elim_type Pincl Pglue) (cglue j x) = Pglue j x :=
|
||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_cglue];apply cast_ua_fn
|
||
|
||
protected definition rec_hprop {P : colimit → Type} [H : Πx, is_hprop (P x)]
|
||
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) (y : colimit) : P y :=
|
||
rec Pincl (λa b, !is_hprop.elimo) y
|
||
|
||
protected definition elim_hprop {P : Type} [H : is_hprop P] (Pincl : Π⦃i : I⦄ (x : A i), P)
|
||
(y : colimit) : P :=
|
||
elim Pincl (λa b, !is_hprop.elim) y
|
||
|
||
end
|
||
end colimit
|
||
|
||
/- definition of a sequential colimit -/
|
||
namespace seq_colim
|
||
section
|
||
/-
|
||
we define it directly in terms of quotients. An alternative definition could be
|
||
definition seq_colim := colimit.colimit A id succ f
|
||
-/
|
||
parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n))
|
||
variables {n : ℕ} (a : A n)
|
||
|
||
local abbreviation B := Σ(n : ℕ), A n
|
||
inductive seq_rel : B → B → Type :=
|
||
| Rmk : Π{n : ℕ} (a : A n), seq_rel ⟨succ n, f a⟩ ⟨n, a⟩
|
||
open seq_rel
|
||
local abbreviation R := seq_rel
|
||
|
||
-- TODO: define this in root namespace
|
||
definition seq_colim : Type :=
|
||
quotient seq_rel
|
||
|
||
definition inclusion : seq_colim :=
|
||
class_of R ⟨n, a⟩
|
||
|
||
abbreviation sι := @inclusion
|
||
|
||
definition glue : sι (f a) = sι a :=
|
||
eq_of_rel seq_rel (Rmk f a)
|
||
|
||
protected definition rec {P : seq_colim → Type}
|
||
(Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
|
||
(Pglue : Π(n : ℕ) (a : A n), Pincl (f a) =[glue a] Pincl a) (aa : seq_colim) : P aa :=
|
||
begin
|
||
fapply (quotient.rec_on aa),
|
||
{ intro a, cases a, apply Pincl},
|
||
{ intro a a' H, cases H, apply Pglue}
|
||
end
|
||
|
||
protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim)
|
||
(Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a)
|
||
: P aa :=
|
||
rec Pincl Pglue aa
|
||
|
||
theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a) {n : ℕ} (a : A n)
|
||
: apdo (rec Pincl Pglue) (glue a) = Pglue a :=
|
||
!rec_eq_of_rel
|
||
|
||
protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P :=
|
||
rec Pincl (λn a, pathover_of_eq (Pglue a))
|
||
|
||
protected definition elim_on [reducible] {P : Type} (aa : seq_colim)
|
||
(Pincl : Π⦃n : ℕ⦄ (a : A n), P)
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : P :=
|
||
elim Pincl Pglue aa
|
||
|
||
theorem elim_glue {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
|
||
: ap (elim Pincl Pglue) (glue a) = Pglue a :=
|
||
begin
|
||
apply eq_of_fn_eq_fn_inv !(pathover_constant (glue a)),
|
||
rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_glue],
|
||
end
|
||
|
||
protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) : seq_colim → Type :=
|
||
elim Pincl (λn a, ua (Pglue a))
|
||
|
||
protected definition elim_type_on [reducible] (aa : seq_colim)
|
||
(Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) : Type :=
|
||
elim_type Pincl Pglue aa
|
||
|
||
theorem elim_type_glue (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
|
||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) {n : ℕ} (a : A n)
|
||
: transport (elim_type Pincl Pglue) (glue a) = Pglue a :=
|
||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn
|
||
|
||
protected definition rec_hprop {P : seq_colim → Type} [H : Πx, is_hprop (P x)]
|
||
(Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) (aa : seq_colim) : P aa :=
|
||
rec Pincl (λa b, !is_hprop.elimo) aa
|
||
|
||
protected definition elim_hprop {P : Type} [H : is_hprop P] (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
|
||
: seq_colim → P :=
|
||
elim Pincl (λa b, !is_hprop.elim)
|
||
|
||
|
||
end
|
||
end seq_colim
|
||
|
||
attribute colimit.incl seq_colim.inclusion [constructor]
|
||
attribute colimit.rec colimit.elim [unfold 10] [recursor 10]
|
||
attribute colimit.elim_type [unfold 9]
|
||
attribute colimit.rec_on colimit.elim_on [unfold 8]
|
||
attribute colimit.elim_type_on [unfold 7]
|
||
attribute seq_colim.rec seq_colim.elim [unfold 6] [recursor 6]
|
||
attribute seq_colim.elim_type [unfold 5]
|
||
attribute seq_colim.rec_on seq_colim.elim_on [unfold 4]
|
||
attribute seq_colim.elim_type_on [unfold 3]
|