add file on binary pointed maps
This commit is contained in:
Floris van Doorn
parent
ba5648fb87
commit
f7e0ce0e20
1 changed files with 164 additions and 0 deletions
164
pointed_binary.hlean
Normal file
164
pointed_binary.hlean
Normal file
|
|
@ -0,0 +1,164 @@
|
|||
/-
|
||||
Copyright (c) 2018 Ulrik Buchholtz. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Floris van Doorn
|
||||
-/
|
||||
|
||||
import .pointed_pi
|
||||
|
||||
open eq pointed equiv sigma is_equiv trunc option pi function fiber sigma.ops
|
||||
|
||||
namespace pointed
|
||||
|
||||
/- binary pointed maps -/
|
||||
structure bpmap (A B C : Type*) : Type :=
|
||||
(f : A → B →* C)
|
||||
(q : Πb, f pt b = pt)
|
||||
(r : q pt = respect_pt (f pt))
|
||||
|
||||
attribute [coercion] bpmap.f
|
||||
variables {A B C D A' B' C' : Type*} {f f' : bpmap A B C}
|
||||
definition respect_pt1 [unfold 4] (f : bpmap A B C) (b : B) : f pt b = pt :=
|
||||
bpmap.q f b
|
||||
|
||||
definition respect_pt2 [unfold 4] (f : bpmap A B C) (a : A) : f a pt = pt :=
|
||||
respect_pt (f a)
|
||||
|
||||
definition respect_ptpt [unfold 4] (f : bpmap A B C) : respect_pt1 f pt = respect_pt2 f pt :=
|
||||
bpmap.r f
|
||||
|
||||
definition bpconst [constructor] (A B C : Type*) : bpmap A B C :=
|
||||
bpmap.mk (λa, pconst B C) (λb, idp) idp
|
||||
|
||||
definition bppmap [constructor] (A B C : Type*) : Type* :=
|
||||
pointed.MK (bpmap A B C) (bpconst A B C)
|
||||
|
||||
definition pmap_of_bpmap [constructor] (f : bppmap A B C) : ppmap A (ppmap B C) :=
|
||||
begin
|
||||
fapply pmap.mk,
|
||||
{ intro a, exact pmap.mk (f a) (respect_pt2 f a) },
|
||||
{ exact eq_of_phomotopy (phomotopy.mk (respect_pt1 f) (respect_ptpt f)) }
|
||||
end
|
||||
|
||||
definition bpmap_of_pmap [constructor] (f : ppmap A (ppmap B C)) : bppmap A B C :=
|
||||
begin
|
||||
apply bpmap.mk (λa, f a) (ap010 pmap.to_fun (respect_pt f)),
|
||||
exact respect_pt (phomotopy_of_eq (respect_pt f))
|
||||
end
|
||||
|
||||
protected definition bpmap.sigma_char [constructor] (A B C : Type*) :
|
||||
bpmap A B C ≃ Σ(f : A → B →* C) (q : Πb, f pt b = pt), q pt = respect_pt (f pt) :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro f, exact ⟨f, respect_pt1 f, respect_ptpt f⟩ },
|
||||
{ intro fqr, exact bpmap.mk fqr.1 fqr.2.1 fqr.2.2 },
|
||||
{ intro fqr, induction fqr with f qr, induction qr with q r, reflexivity },
|
||||
{ intro f, induction f, reflexivity }
|
||||
end
|
||||
|
||||
definition to_homotopy_pt_square {f g : A →* B} (h : f ~* g) :
|
||||
square (respect_pt f) (respect_pt g) (h pt) idp :=
|
||||
square_of_eq (to_homotopy_pt h)⁻¹
|
||||
|
||||
definition bpmap_eq_equiv [constructor] (f f' : bpmap A B C):
|
||||
f = f' ≃ Σ(h : Πa, f a ~* f' a) (q : Πb, square (respect_pt1 f b) (respect_pt1 f' b) (h pt b) idp), cube (vdeg_square (respect_ptpt f)) (vdeg_square (respect_ptpt f'))
|
||||
vrfl ids
|
||||
(q pt) (to_homotopy_pt_square (h pt)) :=
|
||||
begin
|
||||
refine eq_equiv_fn_eq (bpmap.sigma_char A B C) f f' ⬝e _,
|
||||
refine !sigma_eq_equiv ⬝e _, esimp,
|
||||
refine sigma_equiv_sigma (!eq_equiv_homotopy ⬝e pi_equiv_pi_right (λa, !pmap_eq_equiv)) _,
|
||||
intro h, exact sorry
|
||||
end
|
||||
|
||||
definition bpmap_eq [constructor] (h : Πa, f a ~* f' a)
|
||||
(q : Πb, square (respect_pt1 f b) (respect_pt1 f' b) (h pt b) idp)
|
||||
(r : cube (vdeg_square (respect_ptpt f)) (vdeg_square (respect_ptpt f'))
|
||||
vrfl ids
|
||||
(q pt) (to_homotopy_pt_square (h pt))) : f = f' :=
|
||||
(bpmap_eq_equiv f f')⁻¹ᵉ ⟨h, q, r⟩
|
||||
|
||||
definition pmap_equiv_bpmap [constructor] (A B C : Type*) : pmap A (ppmap B C) ≃ bpmap A B C :=
|
||||
begin
|
||||
refine !pmap.sigma_char ⬝e _ ⬝e !bpmap.sigma_char⁻¹ᵉ,
|
||||
refine sigma_equiv_sigma_right (λf, pmap_eq_equiv (f pt) !pconst) ⬝e _,
|
||||
refine sigma_equiv_sigma_right (λf, !phomotopy.sigma_char)
|
||||
end
|
||||
|
||||
definition pmap_equiv_bpmap' [constructor] (A B C : Type*) : pmap A (ppmap B C) ≃ bpmap A B C :=
|
||||
begin
|
||||
refine equiv_change_fun (pmap_equiv_bpmap A B C) _,
|
||||
exact bpmap_of_pmap, intro f, reflexivity
|
||||
end
|
||||
|
||||
definition ppmap_pequiv_bppmap [constructor] (A B C : Type*) :
|
||||
ppmap A (ppmap B C) ≃* bppmap A B C :=
|
||||
pequiv_of_equiv (pmap_equiv_bpmap' A B C) idp
|
||||
|
||||
definition bpmap_functor [constructor] (f : A' →* A) (g : B' →* B) (h : C →* C')
|
||||
(k : bpmap A B C) : bpmap A' B' C' :=
|
||||
begin
|
||||
fapply bpmap.mk (λa', h ∘* k (f a') ∘* g),
|
||||
{ intro b', refine ap h _ ⬝ respect_pt h,
|
||||
exact ap010 (λa b, k a b) (respect_pt f) (g b') ⬝ respect_pt1 k (g b') },
|
||||
{ apply whisker_right, apply ap02 h, esimp,
|
||||
induction A with A a₀, induction B with B b₀, induction f with f f₀, induction g with g g₀,
|
||||
esimp at *, induction f₀, induction g₀, esimp, apply whisker_left, exact respect_ptpt k },
|
||||
end
|
||||
|
||||
definition bppmap_functor [constructor] (f : A' →* A) (g : B' →* B) (h : C →* C') :
|
||||
bppmap A B C →* bppmap A' B' C' :=
|
||||
begin
|
||||
apply pmap.mk (bpmap_functor f g h),
|
||||
induction A with A a₀, induction B with B b₀, induction C' with C' c₀',
|
||||
induction f with f f₀, induction g with g g₀, induction h with h h₀, esimp at *,
|
||||
induction f₀, induction g₀, induction h₀,
|
||||
reflexivity
|
||||
end
|
||||
|
||||
definition ppcompose_left' [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=
|
||||
pmap.mk (pcompose g)
|
||||
begin induction C with C c₀, induction g with g g₀, esimp at *, induction g₀, reflexivity end
|
||||
|
||||
definition ppcompose_right' [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
|
||||
pmap.mk (λg, g ∘* f)
|
||||
begin induction B with B b₀, induction f with f f₀, esimp at *, induction f₀, reflexivity end
|
||||
|
||||
definition ppmap_pequiv_bppmap_natural (f : A' →* A) (g : B' →* B) (h : C →* C') :
|
||||
psquare (ppmap_pequiv_bppmap A B C) (ppmap_pequiv_bppmap A' B' C')
|
||||
(ppcompose_right' f ∘* ppcompose_left' (ppcompose_right' g ∘* ppcompose_left' h))
|
||||
(bppmap_functor f g h) :=
|
||||
begin
|
||||
induction A with A a₀, induction B with B b₀, induction C' with C' c₀',
|
||||
induction f with f f₀, induction g with g g₀, induction h with h h₀, esimp at *,
|
||||
induction f₀, induction g₀, induction h₀,
|
||||
fapply phomotopy.mk,
|
||||
{ intro k, fapply bpmap_eq,
|
||||
{ intro a, exact !passoc⁻¹* },
|
||||
{ intro b, apply vdeg_square, esimp,
|
||||
refine ap02 _ !idp_con ⬝ _ ⬝ (ap (λx, ap010 pmap.to_fun x b) !idp_con)⁻¹ᵖ,
|
||||
refine ap02 _ !ap_eq_ap010⁻¹ ⬝ !ap_compose' ⬝ !ap_compose ⬝ !ap_eq_ap010 },
|
||||
{ exact sorry }},
|
||||
{ exact sorry }
|
||||
end
|
||||
|
||||
/- maybe this is useful for pointed naturality in C? -/
|
||||
definition ppmap_pequiv_bppmap_natural_right (h : C →* C') :
|
||||
psquare (ppmap_pequiv_bppmap A B C) (ppmap_pequiv_bppmap A B C')
|
||||
(ppcompose_left' (ppcompose_left' h))
|
||||
(bppmap_functor !pid !pid h) :=
|
||||
begin
|
||||
induction A with A a₀, induction B with B b₀, induction C' with C' c₀',
|
||||
induction h with h h₀, esimp at *, induction h₀,
|
||||
fapply phomotopy.mk,
|
||||
{ intro k, fapply bpmap_eq,
|
||||
{ intro a, exact pwhisker_left _ !pcompose_pid },
|
||||
{ intro b, apply vdeg_square, esimp,
|
||||
refine ap02 _ !idp_con ⬝ _,
|
||||
refine ap02 _ !ap_eq_ap010⁻¹ ⬝ !ap_compose' ⬝ !ap_compose ⬝ !ap_eq_ap010 },
|
||||
{ exact sorry }},
|
||||
{ exact sorry }
|
||||
end
|
||||
|
||||
|
||||
end pointed
|
||||
Loading…
Reference in a new issue