feat(hott): additions, mostly to types.trunc
This commit is contained in:
Floris van Doorn
parent
ea775092bb
commit
671ef077b9
17 changed files with 269 additions and 83 deletions
|
|
@ -47,15 +47,13 @@ namespace eq
|
|||
|
||||
definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
|
||||
: π*[n] A ≃* π*[n] B :=
|
||||
ptrunc_pequiv 0 (iterated_loop_space_pequiv n H)
|
||||
ptrunc_pequiv_ptrunc 0 (iterated_loop_space_pequiv n H)
|
||||
|
||||
set_option pp.coercions true
|
||||
set_option pp.numerals false
|
||||
definition phomotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) :
|
||||
π*[k] A ≃* Ω[k] (ptrunc k A) :=
|
||||
begin
|
||||
refine !iterated_loop_ptrunc_pequiv⁻¹ᵉ* ⬝e* _,
|
||||
rewrite [trunc_index.zero_add]
|
||||
exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end)
|
||||
end
|
||||
|
||||
open equiv unit
|
||||
|
|
@ -113,6 +111,9 @@ namespace eq
|
|||
definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X :=
|
||||
ptrunc_functor 0 pinverse
|
||||
|
||||
definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) :=
|
||||
by apply @is_equiv_trunc_functor; apply is_equiv_eq_inverse
|
||||
|
||||
definition ptrunc_functor_pinverse [constructor] {X : Type*}
|
||||
: ptrunc_functor 0 (@pinverse X) ~* @tinverse X :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -13,27 +13,29 @@ open eq is_trunc trunc
|
|||
namespace algebra
|
||||
|
||||
section
|
||||
parameters (A : Type) (mul : A → A → A) (inv : A → A) (one : A)
|
||||
{mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c)}
|
||||
{one_mul : ∀a, mul one a = a} {mul_one : ∀a, mul a one = a}
|
||||
{mul_left_inv : ∀a, mul (inv a) a = one}
|
||||
parameters (n : trunc_index) {A : Type} (mul : A → A → A) (inv : A → A) (one : A)
|
||||
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
|
||||
(one_mul : ∀a, mul one a = a) (mul_one : ∀a, mul a one = a)
|
||||
(mul_left_inv : ∀a, mul (inv a) a = one)
|
||||
|
||||
local abbreviation G := trunc 0 A
|
||||
local abbreviation G := trunc n A
|
||||
|
||||
include mul_assoc one_mul mul_one mul_left_inv
|
||||
include mul
|
||||
definition trunc_mul [unfold 9 10] (g h : G) : G :=
|
||||
begin
|
||||
apply trunc.rec_on g, intro p,
|
||||
apply trunc.rec_on h, intro q,
|
||||
induction g with p,
|
||||
induction h with q,
|
||||
exact tr (mul p q)
|
||||
end
|
||||
|
||||
omit mul include inv
|
||||
definition trunc_inv [unfold 9] (g : G) : G :=
|
||||
begin
|
||||
apply trunc.rec_on g, intro p,
|
||||
induction g with p,
|
||||
exact tr (inv p)
|
||||
end
|
||||
|
||||
omit inv include one
|
||||
definition trunc_one [constructor] : G :=
|
||||
tr one
|
||||
|
||||
|
|
@ -41,56 +43,62 @@ namespace algebra
|
|||
local postfix ⁻¹ := trunc_inv
|
||||
local infix * := trunc_mul
|
||||
|
||||
parameters {mul} {inv} {one}
|
||||
omit one include mul_assoc
|
||||
theorem trunc_mul_assoc (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
||||
begin
|
||||
apply trunc.rec_on g₁, intro p₁,
|
||||
apply trunc.rec_on g₂, intro p₂,
|
||||
apply trunc.rec_on g₃, intro p₃,
|
||||
induction g₁ with p₁,
|
||||
induction g₂ with p₂,
|
||||
induction g₃ with p₃,
|
||||
exact ap tr !mul_assoc,
|
||||
end
|
||||
|
||||
omit mul_assoc include one_mul
|
||||
theorem trunc_one_mul (g : G) : 1 * g = g :=
|
||||
begin
|
||||
apply trunc.rec_on g, intro p,
|
||||
induction g with p,
|
||||
exact ap tr !one_mul
|
||||
end
|
||||
|
||||
omit one_mul include mul_one
|
||||
theorem trunc_mul_one (g : G) : g * 1 = g :=
|
||||
begin
|
||||
apply trunc.rec_on g, intro p,
|
||||
induction g with p,
|
||||
exact ap tr !mul_one
|
||||
end
|
||||
|
||||
omit mul_one include mul_left_inv
|
||||
theorem trunc_mul_left_inv (g : G) : g⁻¹ * g = 1 :=
|
||||
begin
|
||||
apply trunc.rec_on g, intro p,
|
||||
induction g with p,
|
||||
exact ap tr !mul_left_inv
|
||||
end
|
||||
|
||||
omit mul_left_inv
|
||||
theorem trunc_mul_comm (mul_comm : ∀a b, mul a b = mul b a) (g h : G)
|
||||
: g * h = h * g :=
|
||||
begin
|
||||
apply trunc.rec_on g, intro p,
|
||||
apply trunc.rec_on h, intro q,
|
||||
induction g with p,
|
||||
induction h with q,
|
||||
exact ap tr !mul_comm
|
||||
end
|
||||
|
||||
parameters (mul_assoc) (one_mul) (mul_one) (mul_left_inv) {A}
|
||||
parameters (mul) (inv) (one)
|
||||
|
||||
definition trunc_group [constructor] : group G :=
|
||||
definition trunc_group [constructor] : group (trunc 0 A) :=
|
||||
⦃group,
|
||||
mul := trunc_mul,
|
||||
mul_assoc := trunc_mul_assoc,
|
||||
one := trunc_one,
|
||||
one_mul := trunc_one_mul,
|
||||
mul_one := trunc_mul_one,
|
||||
inv := trunc_inv,
|
||||
mul_left_inv := trunc_mul_left_inv,
|
||||
mul := algebra.trunc_mul 0 mul,
|
||||
mul_assoc := algebra.trunc_mul_assoc 0 mul_assoc,
|
||||
one := algebra.trunc_one 0 one,
|
||||
one_mul := algebra.trunc_one_mul 0 one_mul,
|
||||
mul_one := algebra.trunc_mul_one 0 mul_one,
|
||||
inv := algebra.trunc_inv 0 inv,
|
||||
mul_left_inv := algebra.trunc_mul_left_inv 0 mul_left_inv,
|
||||
is_set_carrier := _⦄
|
||||
|
||||
|
||||
definition trunc_comm_group [constructor] (mul_comm : ∀a b, mul a b = mul b a) : comm_group G :=
|
||||
⦃comm_group, trunc_group, mul_comm := trunc_mul_comm mul_comm⦄
|
||||
definition trunc_comm_group [constructor] (mul_comm : ∀a b, mul a b = mul b a)
|
||||
: comm_group (trunc 0 A) :=
|
||||
⦃comm_group, trunc_group, mul_comm := algebra.trunc_mul_comm 0 mul_comm⦄
|
||||
|
||||
end
|
||||
end algebra
|
||||
|
|
|
|||
10
hott/book.md
10
hott/book.md
|
|
@ -18,7 +18,7 @@ The rows indicate the chapters, the columns the sections.
|
|||
| Ch 1 | . | . | . | . | + | + | + | + | + | . | + | + | | | |
|
||||
| Ch 2 | + | + | + | + | . | + | + | + | + | + | + | + | + | + | + |
|
||||
| Ch 3 | + | + | + | + | ½ | + | + | + | + | . | + | | | | |
|
||||
| Ch 4 | - | + | + | + | . | + | ½ | + | + | | | | | | |
|
||||
| Ch 4 | - | + | + | + | . | + | + | + | + | | | | | | |
|
||||
| Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | |
|
||||
| Ch 6 | . | + | + | + | + | ½ | ½ | + | ¾ | ¼ | ¾ | + | . | | |
|
||||
| Ch 7 | + | + | + | - | ¾ | - | - | | | | | | | | |
|
||||
|
|
@ -75,7 +75,7 @@ Chapter 3: Sets and logic
|
|||
- 3.2 (Propositions as types?): [types.univ](types/univ.hlean)
|
||||
- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [prop_trunc](prop_trunc.hlean) (Lemma 3.3.5).
|
||||
- 3.4 (Classical vs. intuitionistic logic): decidable is defined in [init.logic](init/logic.hlean)
|
||||
- 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean), we don't have propositional resizing as axiom yet.
|
||||
- 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean). We have not declared propositional resizing as an axiom.
|
||||
- 3.6 (The logic of mere propositions): in the corresponding file in the [types](types/types.md) folder. (is_trunc_prod is defined in [types.sigma](types/sigma.hlean))
|
||||
- 3.7 (Propositional truncation): [init.hit](init/hit.hlean) and [hit.trunc](hit/trunc.hlean)
|
||||
- 3.8 (The axiom of choice): [choice](choice.hlean)
|
||||
|
|
@ -92,7 +92,7 @@ Chapter 4: Equivalences
|
|||
- 4.4 (Contractible fibers): [types.equiv](types/equiv.hlean)
|
||||
- 4.5 (On the definition of equivalences): no formalizable content
|
||||
- 4.6 (Surjections and embeddings): [function](function.hlean)
|
||||
- 4.7 (Closure properties of equivalences): 4.7.1 in [init.equiv](init/equiv.hlean); 4.7.2 in [function](function.hlean); 4.7.5 and 4.7.7 in [types.sigma](types/sigma.hlean) (sigma_functor is a generalization of total(f)); and 4.7.6 in 4.7.6 in [types.fiber](types/fiber.hlean).
|
||||
- 4.7 (Closure properties of equivalences): 4.7.1 in [init.equiv](init/equiv.hlean); 4.7.2 in [function](function.hlean); 4.7.3 and 4.7.4 in [types.arrow_2](types/arrow_2.hlean) 4.7.5 in [types.sigma](types/sigma.hlean) (sigma_functor is a generalization of total(f)); 4.7.6 in [types.fiber](types/fiber.hlean) and 4.7.7 in [types.equiv](types/equiv.hlean).
|
||||
- 4.8 (The object classifier): 4.8.1 and 4.8.2 in [types.fiber](types/fiber.hlean); 4.8.3 and 4.8.4 in [types.univ](types/univ.hlean)
|
||||
- 4.9 (Univalence implies function extensionality): [init.funext](init/funext.hlean)
|
||||
|
||||
|
|
@ -132,7 +132,7 @@ Chapter 7: Homotopy n-types
|
|||
- 7.2 (Uniqueness of identity proofs and Hedberg’s theorem): [init.hedberg](init/hedberg.hlean) and [types.trunc](types/trunc.hlean)
|
||||
- 7.3 (Truncations): [init.hit](init/hit.hlean), [hit.trunc](hit/trunc.hlean) and [types.trunc](types/trunc.hlean)
|
||||
- 7.4 (Colimits of n-types): not formalized
|
||||
- 7.5 (Connectedness): [homotopy.connectedness](homotopy/connectedness.hlean) (the main "induction principle" Lemma 7.5.7)
|
||||
- 7.5 (Connectedness): [homotopy.connectedness](homotopy/connectedness.hlean) (missing theorems: 6, 8, 9, 10, 12, 13)
|
||||
- 7.6 (Orthogonal factorization): not formalized
|
||||
- 7.7 (Modalities): not formalized, and may be unformalizable in general because it's unclear how to define modalities
|
||||
|
||||
|
|
@ -142,7 +142,7 @@ Chapter 8: Homotopy theory
|
|||
Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy.md)
|
||||
|
||||
- 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only the encode-decode proof)
|
||||
- 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof)
|
||||
- 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof of Theorem 8.2.1)
|
||||
- 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): [homotopy.homotopy_group](homotopy/homotopy_group.hlean)
|
||||
- 8.4 (Fiber sequences and the long exact sequence): not formalized
|
||||
- 8.5 (The Hopf fibration): [homotopy.circle](homotopy/circle.hlean) (H-space structure on the circle, Lemma 8.5.8), [homotopy.join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), the rest is not formalized
|
||||
|
|
|
|||
|
|
@ -116,6 +116,14 @@ namespace function
|
|||
definition is_prop_is_surjective [instance] : is_prop (is_surjective f) :=
|
||||
by unfold is_surjective; exact _
|
||||
|
||||
definition is_surjective_cancel_right {A B C : Type} (g : B → C) (f : A → B)
|
||||
[H : is_surjective (g ∘ f)] : is_surjective g :=
|
||||
begin
|
||||
intro c,
|
||||
induction H c with v, induction v with a p,
|
||||
exact tr (fiber.mk (f a) p)
|
||||
end
|
||||
|
||||
definition is_weakly_constant_ap [instance] [H : is_weakly_constant f] (a a' : A) :
|
||||
is_weakly_constant (ap f : a = a' → f a = f a') :=
|
||||
take p q : a = a',
|
||||
|
|
@ -222,7 +230,7 @@ namespace function
|
|||
(λb,
|
||||
((trunc_functor_compose n (sect r) r) b)⁻¹
|
||||
⬝ trunc_homotopy n (right_inverse r) b
|
||||
⬝ trunc_functor_id B n b)
|
||||
⬝ trunc_functor_id n B b)
|
||||
|
||||
-- Lemma 3.11.7
|
||||
definition is_contr_retract (r : A → B) [H : is_retraction r] : is_contr A → is_contr B :=
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ attribute trunc.elim [recursor 6] [unfold 6]
|
|||
|
||||
namespace trunc
|
||||
|
||||
variables {X Y Z : Type} {P : X → Type} (A B : Type) (n : trunc_index)
|
||||
variables {X Y Z : Type} {P : X → Type} (n : trunc_index) (A B : Type)
|
||||
|
||||
local attribute is_trunc_eq [instance]
|
||||
|
||||
|
|
|
|||
|
|
@ -238,12 +238,12 @@ namespace circle
|
|||
open algebra trunc
|
||||
|
||||
definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ :=
|
||||
trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv ℤ _) proof _ qed
|
||||
trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed
|
||||
|
||||
definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p :=
|
||||
eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])
|
||||
|
||||
definition fundamental_group_of_circle : π₁(S¹.) = group_integers :=
|
||||
definition fundamental_group_of_circle : π₁(S¹.) = gℤ :=
|
||||
begin
|
||||
apply (Group_eq fg_carrier_equiv_int),
|
||||
intros g h,
|
||||
|
|
|
|||
|
|
@ -21,9 +21,19 @@ namespace homotopy
|
|||
assumption
|
||||
end
|
||||
|
||||
definition is_conn_map (n : ℕ₋₂) {A B : Type} (f : A → B) : Type :=
|
||||
definition is_conn_map [reducible] (n : ℕ₋₂) {A B : Type} (f : A → B) : Type :=
|
||||
Πb : B, is_conn n (fiber f b)
|
||||
|
||||
theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A :=
|
||||
begin
|
||||
apply is_contr_equiv_closed,
|
||||
apply trunc_trunc_equiv_left _ n k H
|
||||
end
|
||||
|
||||
theorem is_conn_map_of_le {A B : Type} (f : A → B) {n k : ℕ₋₂} (H : n ≤ k)
|
||||
[is_conn_map k f] : is_conn_map n f :=
|
||||
λb, is_conn_of_le _ H
|
||||
|
||||
namespace is_conn_map
|
||||
section
|
||||
parameters {n : ℕ₋₂} {A B : Type} {h : A → B}
|
||||
|
|
@ -131,7 +141,7 @@ namespace homotopy
|
|||
parameters (n : ℕ₋₂) (A : Type)
|
||||
|
||||
definition is_conn_of_map_to_unit
|
||||
: is_conn_map n (λx : A, unit.star) → is_conn n A :=
|
||||
: is_conn_map n (const A unit.star) → is_conn n A :=
|
||||
begin
|
||||
intro H, unfold is_conn_map at H,
|
||||
rewrite [-(ua (fiber.fiber_star_equiv A))],
|
||||
|
|
@ -239,7 +249,7 @@ namespace homotopy
|
|||
@retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
|
||||
|
||||
-- all types are -2-connected
|
||||
definition minus_two_conn [instance] (A : Type) : is_conn -2 A :=
|
||||
definition is_conn_minus_two (A : Type) : is_conn -2 A :=
|
||||
_
|
||||
|
||||
-- Theorem 8.2.1
|
||||
|
|
@ -274,13 +284,34 @@ namespace homotopy
|
|||
}
|
||||
end
|
||||
|
||||
open trunc_index
|
||||
-- Lemma 7.5.14
|
||||
theorem is_equiv_trunc_functor_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B)
|
||||
[H : is_conn_map n f] : is_equiv (trunc_functor n f) :=
|
||||
begin
|
||||
fapply adjointify,
|
||||
{ intro b, induction b with b, exact trunc_functor n point (center (trunc n (fiber f b)))},
|
||||
{ intro b, induction b with b, esimp, generalize center (trunc n (fiber f b)), intro v,
|
||||
induction v with v, induction v with a p, esimp, exact ap tr p},
|
||||
{ intro a, induction a with a, esimp, rewrite [center_eq (tr (fiber.mk a idp))]}
|
||||
end
|
||||
|
||||
theorem trunc_equiv_trunc_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B)
|
||||
[H : is_conn_map n f] : trunc n A ≃ trunc n B :=
|
||||
equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_map n f)
|
||||
|
||||
open trunc_index pointed sphere.ops
|
||||
-- Corollary 8.2.2
|
||||
theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (sphere n) :=
|
||||
theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (S n) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ apply minus_two_conn},
|
||||
{ apply is_conn_minus_two},
|
||||
{ rewrite [succ_sub_one, sphere.sphere_succ], apply is_conn_susp}
|
||||
end
|
||||
|
||||
section
|
||||
open sphere_index
|
||||
theorem is_conn_psphere [instance] (n : ℕ) : is_conn (n.-1) (S. n) :=
|
||||
transport (λx, is_conn x (sphere n)) (of_nat_sub_one n) (is_conn_sphere n)
|
||||
end
|
||||
|
||||
end homotopy
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Authors: Floris van Doorn, Clive Newstead
|
|||
|
||||
import algebra.homotopy_group .connectedness
|
||||
|
||||
open eq is_trunc trunc_index pointed algebra trunc nat homotopy
|
||||
open eq is_trunc trunc_index pointed algebra trunc nat homotopy fiber pointed
|
||||
|
||||
namespace is_trunc
|
||||
-- Lemma 8.3.1
|
||||
|
|
@ -25,19 +25,14 @@ namespace is_trunc
|
|||
theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A]
|
||||
: is_contr (π[k] A) :=
|
||||
begin
|
||||
have H2 : of_nat k ≤ of_nat n, from of_nat_le_of_nat H,
|
||||
have H3 : is_contr (ptrunc k A),
|
||||
begin
|
||||
fapply is_contr_equiv_closed,
|
||||
{ apply trunc_trunc_equiv_left _ k n H2}
|
||||
end,
|
||||
have H4 : is_contr (Ω[k](ptrunc k A)),
|
||||
from !is_trunc_loop_of_is_trunc,
|
||||
have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H),
|
||||
have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loop_of_is_trunc,
|
||||
apply is_trunc_equiv_closed_rev,
|
||||
{ apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)}
|
||||
end
|
||||
|
||||
-- Corollary 8.3.3
|
||||
section
|
||||
open sphere.ops sphere_index
|
||||
theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) :=
|
||||
begin
|
||||
|
|
@ -47,5 +42,11 @@ namespace is_trunc
|
|||
apply @(trivial_homotopy_group_of_is_conn _ H2),
|
||||
rewrite [-trunc_index.of_sphere_index_of_nat, -trunc_index.succ_sub_one], apply is_conn_sphere}
|
||||
end
|
||||
end
|
||||
|
||||
theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (k n : ℕ) (f : A →* B)
|
||||
[H : is_conn_map n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) :=
|
||||
@(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)
|
||||
|
||||
|
||||
end is_trunc
|
||||
|
|
|
|||
|
|
@ -153,7 +153,27 @@ weak_order.mk le sphere_index.le.sp_refl @sphere_index.le_trans @sphere_index.le
|
|||
|
||||
namespace trunc_index
|
||||
definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n..-1..-1 :=
|
||||
nat.rec_on n idp (λn p, ap trunc_index.succ p)
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap trunc_index.succ IH}
|
||||
end
|
||||
|
||||
definition of_nat_sub_one (n : ℕ)
|
||||
: (sphere_index.of_nat n)..-1 = (trunc_index.sub_two n).+1 :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap trunc_index.succ IH}
|
||||
end
|
||||
|
||||
definition sub_one_of_sphere_index (n : ℕ)
|
||||
: of_sphere_index n..-1 = (trunc_index.sub_two n).+1 :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap trunc_index.succ IH}
|
||||
end
|
||||
|
||||
definition succ_sub_one (n : ℕ₋₁) : n.+1..-1 = n :> ℕ₋₂ :=
|
||||
idp
|
||||
|
|
@ -180,7 +200,7 @@ definition sphere : ℕ₋₁ → Type₀
|
|||
|
||||
namespace sphere
|
||||
|
||||
export [notation] [coercion] sphere_index
|
||||
export [notation] sphere_index
|
||||
|
||||
definition base {n : ℕ} : sphere n := north
|
||||
definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) :=
|
||||
|
|
|
|||
|
|
@ -185,6 +185,18 @@ namespace eq
|
|||
definition idp_eq_con {p : x = y} {q : y = x} (r : p⁻¹ = q) : idp = q ⬝ p :=
|
||||
by cases p; exact r
|
||||
|
||||
definition eq_idp_of_con_right {p : x = x} {q : x = y} (r : p ⬝ q = q) : p = idp :=
|
||||
by cases q; exact r
|
||||
|
||||
definition eq_idp_of_con_left {p : x = x} {q : y = x} (r : q ⬝ p = q) : p = idp :=
|
||||
by cases q; exact (idp_con p)⁻¹ ⬝ r
|
||||
|
||||
definition idp_eq_of_con_right {p : x = x} {q : x = y} (r : q = p ⬝ q) : idp = p :=
|
||||
by cases q; exact r
|
||||
|
||||
definition idp_eq_of_con_left {p : x = x} {q : y = x} (r : q = q ⬝ p) : idp = p :=
|
||||
by cases q; exact r ⬝ idp_con p
|
||||
|
||||
/- Transport -/
|
||||
|
||||
definition transport [subst] [reducible] [unfold 5] (P : A → Type) {x y : A} (p : x = y)
|
||||
|
|
|
|||
|
|
@ -48,6 +48,12 @@ ap to_fun (equiv_of_eq_ua f)
|
|||
definition cast_ua {A B : Type} (f : A ≃ B) (a : A) : cast (ua f) a = f a :=
|
||||
ap10 (cast_ua_fn f) a
|
||||
|
||||
definition cast_ua_inv_fn {A B : Type} (f : A ≃ B) : cast (ua f)⁻¹ = to_inv f :=
|
||||
ap to_inv (equiv_of_eq_ua f)
|
||||
|
||||
definition cast_ua_inv {A B : Type} (f : A ≃ B) (b : B) : cast (ua f)⁻¹ b = to_inv f b :=
|
||||
ap10 (cast_ua_inv_fn f) b
|
||||
|
||||
definition ua_equiv_of_eq [reducible] {A B : Type} (p : A = B) : ua (equiv_of_eq p) = p :=
|
||||
left_inv equiv_of_eq p
|
||||
|
||||
|
|
|
|||
|
|
@ -472,9 +472,10 @@ namespace eq
|
|||
{ exact decode},
|
||||
{ intro c,
|
||||
unfold [encode, decode, decode'],
|
||||
induction p, esimp, rewrite [is_prop_elim_self,▸*,+idp_con], apply tr_eq_of_pathover,
|
||||
induction p, esimp, rewrite [is_prop_elim_self,▸*,+idp_con],
|
||||
apply tr_eq_of_pathover,
|
||||
eapply @sigma.rec_on _ _ (λx, x.2 =[(is_prop.elim ⟨x.1, x.2⟩ ⟨a, c⟩)..1] c)
|
||||
(center (sigma code)), -- BUG(?): induction fails
|
||||
(center (sigma code)),
|
||||
intro a c, apply eq_pr2},
|
||||
{ intro q, induction q, esimp, apply con.left_inv, },
|
||||
end
|
||||
|
|
|
|||
|
|
@ -16,6 +16,8 @@ namespace int
|
|||
open algebra
|
||||
definition group_integers : Group :=
|
||||
Group.mk ℤ (group_of_add_group _)
|
||||
|
||||
notation `gℤ` := group_integers
|
||||
end
|
||||
|
||||
definition is_equiv_succ [instance] : is_equiv succ :=
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ namespace pointed
|
|||
attribute pType.carrier [coercion]
|
||||
variables {A B : Type}
|
||||
|
||||
definition pt [unfold 2] [H : pointed A] := point A
|
||||
definition Point [unfold 1] (A : Type*) := pType.Point A
|
||||
definition pt [reducible] [unfold 2] [H : pointed A] := point A
|
||||
definition Point [reducible] [unfold 1] (A : Type*) := pType.Point A
|
||||
abbreviation carrier [unfold 1] (A : Type*) := pType.carrier A
|
||||
protected definition Mk [constructor] {A : Type} (a : A) := pType.mk A a
|
||||
protected definition MK [constructor] (A : Type) (a : A) := pType.mk A a
|
||||
|
|
@ -90,13 +90,16 @@ namespace pointed
|
|||
definition iterated_ploop_space_succ [unfold_full] (k : ℕ) (A : Type*)
|
||||
: Ω[succ k] A = Ω Ω[k] A := rfl
|
||||
|
||||
definition rfln [constructor] [reducible] {A : Type*} {n : ℕ} : Ω[n] A := pt
|
||||
definition refln [constructor] [reducible] (A : Type*) (n : ℕ) : Ω[n] A := pt
|
||||
definition rfln [constructor] [reducible] {n : ℕ} {A : Type*} : Ω[n] A := pt
|
||||
definition refln [constructor] [reducible] (n : ℕ) (A : Type*) : Ω[n] A := pt
|
||||
definition refln_eq_refl (A : Type*) (n : ℕ) : rfln = rfl :> Ω[succ n] A := rfl
|
||||
|
||||
definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type :=
|
||||
Ω[n] (pointed.mk' A)
|
||||
|
||||
definition loop_mul {k : ℕ} {A : Type*} (mul : A → A → A) : Ω[k] A → Ω[k] A → Ω[k] A :=
|
||||
begin cases k with k, exact mul, exact concat end
|
||||
|
||||
definition pType_eq {A B : Type*} (f : A ≃ B) (p : f pt = pt) : A = B :=
|
||||
begin
|
||||
cases A with A a, cases B with B b, esimp at *,
|
||||
|
|
|
|||
|
|
@ -217,6 +217,11 @@ namespace pointed
|
|||
{ exact loop_pequiv_loop IH}
|
||||
end
|
||||
|
||||
definition loopn_pequiv_loopn_con (n : ℕ) (f : A ≃* B) (p q : Ω[n+1] A)
|
||||
: loopn_pequiv_loopn (n+1) f (p ⬝ q) =
|
||||
loopn_pequiv_loopn (n+1) f p ⬝ loopn_pequiv_loopn (n+1) f q :=
|
||||
ap1_con (loopn_pequiv_loopn n f) p q
|
||||
|
||||
definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') :
|
||||
ppmap A B →* ppmap A' B' :=
|
||||
pmap.mk (λh, g ∘* h ∘* f)
|
||||
|
|
|
|||
|
|
@ -209,9 +209,8 @@ namespace sigma
|
|||
definition sigma_functor [unfold 7] (u : Σa, B a) : Σa', B' a' :=
|
||||
⟨f u.1, g u.1 u.2⟩
|
||||
|
||||
definition total [reducible] [unfold 5] {B' : A → Type} (g : Πa, B a → B' a) (u : Σa, B a)
|
||||
: Σa', B' a' :=
|
||||
sigma_functor id g u
|
||||
definition total [reducible] [unfold 5] {B' : A → Type} (g : Πa, B a → B' a) : (Σa, B a) → (Σa, B' a) :=
|
||||
sigma_functor id g
|
||||
|
||||
/- Equivalences -/
|
||||
definition is_equiv_sigma_functor [constructor] [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ Copyright (c) 2015 Jakob von Raumer. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Floris van Doorn
|
||||
|
||||
Properties of is_trunc and trunctype
|
||||
Properties of trunc_index, is_trunc, trunctype, trunc, and the pointed versions of these
|
||||
-/
|
||||
|
||||
-- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .prop_trunc
|
||||
|
|
@ -275,7 +275,7 @@ namespace is_trunc
|
|||
|
||||
/- theorems about decidable equality and axiom K -/
|
||||
theorem is_set_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_set A :=
|
||||
is_set.mk _ (λa b p q, eq.rec_on q K p)
|
||||
is_set.mk _ (λa b p q, eq.rec K q p)
|
||||
|
||||
theorem is_set_of_relation.{u} {A : Type.{u}} (R : A → A → Type.{u})
|
||||
(mere : Π(a b : A), is_prop (R a b)) (refl : Π(a : A), R a a)
|
||||
|
|
@ -296,10 +296,8 @@ namespace is_trunc
|
|||
definition relation_equiv_eq {A : Type} (R : A → A → Type)
|
||||
(mere : Π(a b : A), is_prop (R a b)) (refl : Π(a : A), R a a)
|
||||
(imp : Π{a b : A}, R a b → a = b) (a b : A) : R a b ≃ a = b :=
|
||||
@equiv_of_is_prop _ _ _
|
||||
(@is_trunc_eq _ _ (is_set_of_relation R mere refl @imp) a b)
|
||||
imp
|
||||
(λp, p ▸ refl a)
|
||||
have is_set A, from is_set_of_relation R mere refl @imp,
|
||||
equiv_of_is_prop imp (λp, p ▸ refl a)
|
||||
|
||||
local attribute not [reducible]
|
||||
theorem is_set_of_double_neg_elim {A : Type} (H : Π(a b : A), ¬¬a = b → a = b)
|
||||
|
|
@ -377,17 +375,20 @@ namespace is_trunc
|
|||
end is_trunc open is_trunc
|
||||
|
||||
namespace trunc
|
||||
variable {A : Type}
|
||||
universe variable u
|
||||
variable {A : Type.{u}}
|
||||
|
||||
protected definition code (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : n-Type :=
|
||||
trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a'))))
|
||||
/- characterization of equality in truncated types -/
|
||||
protected definition code [unfold 3 4] (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : trunctype.{u} n :=
|
||||
by induction aa with a; induction aa' with a'; exact trunctype.mk' n (trunc n (a = a'))
|
||||
|
||||
protected definition encode (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' :=
|
||||
protected definition encode [unfold 3 5] {n : ℕ₋₂} {aa aa' : trunc n.+1 A}
|
||||
: aa = aa' → trunc.code n aa aa' :=
|
||||
begin
|
||||
intro p, induction p, induction aa with a, esimp [trunc.code,trunc.rec_on], exact (tr idp)
|
||||
intro p, induction p, induction aa with a, esimp, exact (tr idp)
|
||||
end
|
||||
|
||||
protected definition decode (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' :=
|
||||
protected definition decode {n : ℕ₋₂} (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' :=
|
||||
begin
|
||||
induction aa' with a', induction aa with a,
|
||||
esimp [trunc.code, trunc.rec_on], intro x,
|
||||
|
|
@ -412,6 +413,33 @@ namespace trunc
|
|||
: (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') :=
|
||||
!trunc_eq_equiv
|
||||
|
||||
definition trunc_functor2 [unfold 6 7] {n : ℕ₋₂} {A B C : Type} (f : A → B → C)
|
||||
(x : trunc n A) (y : trunc n B) : trunc n C :=
|
||||
by induction x with a; induction y with b; exact tr (f a b)
|
||||
|
||||
definition trunc_concat [unfold 6 7] {n : ℕ₋₂} {A : Type} {a₁ a₂ a₃ : A}
|
||||
(p : trunc n (a₁ = a₂)) (q : trunc n (a₂ = a₃)) : trunc n (a₁ = a₃) :=
|
||||
trunc_functor2 concat p q
|
||||
|
||||
definition code_mul {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A}
|
||||
(g : trunc.code n aa₁ aa₂) (h : trunc.code n aa₂ aa₃) : trunc.code n aa₁ aa₃ :=
|
||||
begin
|
||||
induction aa₁ with a₁, induction aa₂ with a₂, induction aa₃ with a₃,
|
||||
esimp at *, induction g with p, induction h with q,
|
||||
exact tr (p ⬝ q)
|
||||
end
|
||||
|
||||
definition encode_con' {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A} (p : aa₁ = aa₂) (q : aa₂ = aa₃)
|
||||
: trunc.encode (p ⬝ q) = code_mul (trunc.encode p) (trunc.encode q) :=
|
||||
begin
|
||||
induction p, induction q, induction aa₁ with a₁, reflexivity
|
||||
end
|
||||
|
||||
definition encode_con {n : ℕ₋₂} {a₁ a₂ a₃ : A} (p : tr a₁ = tr a₂ :> trunc (n.+1) A)
|
||||
(q : tr a₂ = tr a₃ :> trunc (n.+1) A)
|
||||
: trunc.encode (p ⬝ q) = trunc_concat (trunc.encode p) (trunc.encode q) :=
|
||||
encode_con' p q
|
||||
|
||||
definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type)
|
||||
(n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (trunc m A) :=
|
||||
begin
|
||||
|
|
@ -437,6 +465,12 @@ namespace trunc
|
|||
: transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
|
||||
by induction p; reflexivity
|
||||
|
||||
/- pathover over a truncated family -/
|
||||
definition trunc_pathover {A : Type} {B : A → Type} {n : ℕ₋₂} {a a' : A} {p : a = a'}
|
||||
{b : B a} {b' : B a'} (q : b =[p] b') : @tr n _ b =[p] @tr n _ b' :=
|
||||
by induction q; constructor
|
||||
|
||||
/- equivalences between truncated types (see also hit.trunc) -/
|
||||
definition trunc_trunc_equiv_left [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m)
|
||||
: trunc n (trunc m A) ≃ trunc n A :=
|
||||
begin
|
||||
|
|
@ -455,13 +489,41 @@ namespace trunc
|
|||
exact is_trunc_of_le _ H,
|
||||
end
|
||||
|
||||
definition trunc_equiv_trunc_of_le {n m : ℕ₋₂} {A B : Type} (H : n ≤ m)
|
||||
(f : trunc m A ≃ trunc m B) : trunc n A ≃ trunc n B :=
|
||||
(trunc_trunc_equiv_left A _ _ H)⁻¹ᵉ ⬝e trunc_equiv_trunc n f ⬝e trunc_trunc_equiv_left B _ _ H
|
||||
|
||||
definition trunc_trunc_equiv_trunc_trunc [constructor] (n m : ℕ₋₂) (A : Type)
|
||||
: trunc n (trunc m A) ≃ trunc m (trunc n A) :=
|
||||
begin
|
||||
fapply equiv.MK: intro x; induction x with x; induction x with x,
|
||||
{ exact tr (tr x)},
|
||||
{ exact tr (tr x)},
|
||||
{ reflexivity},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
/- trunc_functor preserves surjectivity -/
|
||||
|
||||
definition is_surjective_trunc_functor {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_surjective f]
|
||||
: is_surjective (trunc_functor n f) :=
|
||||
begin
|
||||
cases n with n: intro b,
|
||||
{ exact tr (fiber.mk !center !is_prop.elim)},
|
||||
{ refine @trunc.rec _ _ _ _ _ b, {intro x, exact is_trunc_of_le _ !minus_one_le_succ},
|
||||
clear b, intro b, induction H b with v, induction v with a p,
|
||||
exact tr (fiber.mk (tr a) (ap tr p))}
|
||||
end
|
||||
|
||||
|
||||
/- the image of a map is the (-1)-truncated fiber -/
|
||||
definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥
|
||||
|
||||
definition image.mk [constructor] {A B : Type} {f : A → B} {b : B} (a : A) (p : f a = b)
|
||||
: image f b :=
|
||||
tr (fiber.mk a p)
|
||||
|
||||
-- truncation of pointed types
|
||||
/- truncation of pointed types and its functorial action -/
|
||||
definition ptrunc [constructor] (n : ℕ₋₂) (X : Type*) : n-Type* :=
|
||||
ptrunctype.mk (trunc n X) _ (tr pt)
|
||||
|
||||
|
|
@ -469,15 +531,42 @@ namespace trunc
|
|||
: ptrunc n X →* ptrunc n Y :=
|
||||
pmap.mk (trunc_functor n f) (ap tr (respect_pt f))
|
||||
|
||||
definition ptrunc_pequiv [constructor] (n : ℕ₋₂) {X Y : Type*} (H : X ≃* Y)
|
||||
definition ptrunc_pequiv_ptrunc [constructor] (n : ℕ₋₂) {X Y : Type*} (H : X ≃* Y)
|
||||
: ptrunc n X ≃* ptrunc n Y :=
|
||||
pequiv_of_equiv (trunc_equiv_trunc n H) (ap tr (respect_pt H))
|
||||
|
||||
definition ptrunc_pequiv [constructor] (n : ℕ₋₂) (X : Type*) (H : is_trunc n X)
|
||||
: ptrunc n X ≃* X :=
|
||||
pequiv_of_equiv (trunc_equiv n X) idp
|
||||
|
||||
definition ptrunc_ptrunc_pequiv_left [constructor] (A : Type*) (n m : ℕ₋₂) (H : n ≤ m)
|
||||
: ptrunc n (ptrunc m A) ≃* ptrunc n A :=
|
||||
pequiv_of_equiv (trunc_trunc_equiv_left A n m H) idp
|
||||
|
||||
definition ptrunc_ptrunc_pequiv_right [constructor] (A : Type*) (n m : ℕ₋₂) (H : n ≤ m)
|
||||
: ptrunc m (ptrunc n A) ≃* ptrunc n A :=
|
||||
pequiv_of_equiv (trunc_trunc_equiv_right A n m H) idp
|
||||
|
||||
definition ptrunc_pequiv_ptrunc_of_le {n m : ℕ₋₂} {A B : Type*} (H : n ≤ m)
|
||||
(f : ptrunc m A ≃* ptrunc m B) : ptrunc n A ≃* ptrunc n B :=
|
||||
(ptrunc_ptrunc_pequiv_left A _ _ H)⁻¹ᵉ* ⬝e*
|
||||
ptrunc_pequiv_ptrunc n f ⬝e*
|
||||
ptrunc_ptrunc_pequiv_left B _ _ H
|
||||
|
||||
definition ptrunc_ptrunc_pequiv_ptrunc_ptrunc [constructor] (n m : ℕ₋₂) (A : Type*)
|
||||
: ptrunc n (ptrunc m A) ≃ ptrunc m (ptrunc n A) :=
|
||||
pequiv_of_equiv (trunc_trunc_equiv_trunc_trunc n m A) idp
|
||||
|
||||
definition loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A : Type*) :
|
||||
Ω (ptrunc (n+1) A) ≃* ptrunc n (Ω A) :=
|
||||
pequiv_of_equiv !tr_eq_tr_equiv idp
|
||||
|
||||
definition iterated_loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (k : ℕ) (A : Type*) :
|
||||
definition loop_ptrunc_pequiv_con {n : ℕ₋₂} {A : Type*} (p q : Ω (ptrunc (n+1) A)) :
|
||||
loop_ptrunc_pequiv n A (p ⬝ q) =
|
||||
trunc_concat (loop_ptrunc_pequiv n A p) (loop_ptrunc_pequiv n A q) :=
|
||||
encode_con p q
|
||||
|
||||
definition iterated_loop_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) :
|
||||
Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) :=
|
||||
begin
|
||||
revert n, induction k with k IH: intro n,
|
||||
|
|
|
|||
Loading…
Reference in a new issue