feat(library/hott): add adjointification and closure properties for equivalences
Port features from the Coq Hott library
This commit is contained in:
Jakob von Raumer
Leonardo de Moura
parent
5a553603d1
commit
a169f791df
1 changed files with 156 additions and 23 deletions
|
|
@ -3,7 +3,7 @@
|
||||||
-- Author: Jeremy Avigad
|
-- Author: Jeremy Avigad
|
||||||
-- Ported from Coq HoTT
|
-- Ported from Coq HoTT
|
||||||
import .path
|
import .path
|
||||||
open path
|
open path function
|
||||||
|
|
||||||
-- Equivalences
|
-- Equivalences
|
||||||
-- ------------
|
-- ------------
|
||||||
|
|
@ -15,27 +15,32 @@ definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈
|
||||||
|
|
||||||
-- Structure IsEquiv
|
-- Structure IsEquiv
|
||||||
|
|
||||||
inductive IsEquiv {A B : Type} (f : A → B) :=
|
inductive IsEquiv [class] {A B : Type} (f : A → B) :=
|
||||||
IsEquiv_mk : Π
|
IsEquiv_mk : Π
|
||||||
(equiv_inv : B → A)
|
(inv : B → A)
|
||||||
(eisretr : Sect equiv_inv f)
|
(retr : Sect inv f)
|
||||||
(eissect : Sect f equiv_inv)
|
(sect : Sect f inv)
|
||||||
(eisadj : Πx, eisretr (f x) ≈ ap f (eissect x)),
|
(adj : Πx, retr (f x) ≈ ap f (sect x)),
|
||||||
IsEquiv f
|
IsEquiv f
|
||||||
|
|
||||||
definition equiv_inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
|
|
||||||
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
|
|
||||||
|
|
||||||
-- TODO: note: does not type check without giving the type
|
namespace IsEquiv
|
||||||
definition eisretr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (equiv_inv H) f :=
|
|
||||||
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eisretr) H
|
|
||||||
|
|
||||||
definition eissect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (equiv_inv H) :=
|
definition inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
|
||||||
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eissect) H
|
IsEquiv.rec (λinv retr sect adj, inv) H
|
||||||
|
|
||||||
definition eisadj {A B : Type} {f : A → B} (H : IsEquiv f) :
|
-- TODO: note: does not type check without giving the type
|
||||||
Πx, eisretr H (f x) ≈ ap f (eissect H x) :=
|
definition retr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (inv H) f :=
|
||||||
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eisadj) H
|
IsEquiv.rec (λinv retr sect adj, retr) H
|
||||||
|
|
||||||
|
definition sect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (inv H) :=
|
||||||
|
IsEquiv.rec (λinv retr sect adj, sect) H
|
||||||
|
|
||||||
|
definition adj {A B : Type} {f : A → B} (H : IsEquiv f) :
|
||||||
|
Πx, retr H (f x) ≈ ap f (sect H x) :=
|
||||||
|
IsEquiv.rec (λinv retr sect adj, adj) H
|
||||||
|
|
||||||
|
end IsEquiv
|
||||||
|
|
||||||
-- Structure Equiv
|
-- Structure Equiv
|
||||||
|
|
||||||
|
|
@ -45,12 +50,140 @@ Equiv_mk : Π
|
||||||
(equiv_isequiv : IsEquiv equiv_fun),
|
(equiv_isequiv : IsEquiv equiv_fun),
|
||||||
Equiv A B
|
Equiv A B
|
||||||
|
|
||||||
definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B :=
|
namespace Equiv
|
||||||
Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
|
|
||||||
|
|
||||||
definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
|
definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B :=
|
||||||
Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
|
Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
|
||||||
|
|
||||||
-- TODO: better symbol
|
definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
|
||||||
infix `<~>`:25 := Equiv
|
Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
|
||||||
notation H ⁻¹ := equiv_inv H
|
|
||||||
|
infix `≃`:25 := Equiv
|
||||||
|
notation e `⁻¹` := IsEquiv.inv e
|
||||||
|
|
||||||
|
end Equiv
|
||||||
|
|
||||||
|
-- Some instances and closure properties of equivalences
|
||||||
|
|
||||||
|
namespace IsEquiv
|
||||||
|
variables {A B C : Type} {f : A → B} {g : B → C} {f' : A → B}
|
||||||
|
|
||||||
|
-- The identity function is an equivalence.
|
||||||
|
|
||||||
|
definition idIsEquiv [instance] : (@IsEquiv A A id) := IsEquiv_mk id (λa, idp) (λa, idp) (λa, idp)
|
||||||
|
|
||||||
|
-- The composition of two equivalences is, again, an equivalence.
|
||||||
|
|
||||||
|
definition comp_closed [instance] (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) :=
|
||||||
|
IsEquiv_mk ((inv Hf) ∘ (inv Hg))
|
||||||
|
(λc, ap g (retr Hf ((inv Hg) c)) @ retr Hg c)
|
||||||
|
(λa, ap (inv Hf) (sect Hg (f a)) @ sect Hf a)
|
||||||
|
(λa, (whiskerL _ (adj Hg (f a))) @
|
||||||
|
(ap_pp g _ _)^ @
|
||||||
|
ap02 g (concat_A1p (retr Hf) (sect Hg (f a))^ @
|
||||||
|
(ap_compose (inv Hf) f _ @@ adj Hf a) @
|
||||||
|
(ap_pp f _ _)^
|
||||||
|
) @
|
||||||
|
(ap_compose f g _)^
|
||||||
|
)
|
||||||
|
|
||||||
|
-- Any function equal to an equivalence is an equivlance as well.
|
||||||
|
definition path_closed (Hf : IsEquiv f) (Heq : f ≈ f') : (IsEquiv f') :=
|
||||||
|
path.induction_on Heq Hf
|
||||||
|
|
||||||
|
-- Any function pointwise equal to an equivalence is an equivalence as well.
|
||||||
|
definition homotopic (Hf : IsEquiv f) (Heq : f ∼ f') : (IsEquiv f') :=
|
||||||
|
let sect' := (λ b, (Heq (inv Hf b))^ @ retr Hf b) in
|
||||||
|
let retr' := (λ a, (ap (inv Hf) (Heq a))^ @ sect Hf a) in
|
||||||
|
let adj' := (λ (a : A),
|
||||||
|
let ff'a := Heq a in
|
||||||
|
let invf := inv Hf in
|
||||||
|
let secta := sect Hf a in
|
||||||
|
let retrfa := retr Hf (f a) in
|
||||||
|
let retrf'a := retr Hf (f' a) in
|
||||||
|
have eq1 : ap f secta @ ff'a ≈ ap f (ap invf ff'a) @ retr Hf (f' a),
|
||||||
|
from calc ap f secta @ ff'a
|
||||||
|
≈ retrfa @ ff'a : (ap _ (adj Hf _ ))^
|
||||||
|
... ≈ ap (f ∘ invf) ff'a @ retrf'a : !concat_A1p^
|
||||||
|
... ≈ ap f (ap invf ff'a) @ retr Hf (f' a) : {ap_compose invf f ff'a},
|
||||||
|
have eq2 : retrf'a ≈ Heq (invf (f' a)) @ ((ap f' (ap invf ff'a))^ @ ap f' secta),
|
||||||
|
from calc retrf'a
|
||||||
|
≈ (ap f (ap invf ff'a))^ @ (ap f secta @ ff'a) : moveL_Vp _ _ _ (eq1^)
|
||||||
|
... ≈ ap f (ap invf ff'a)^ @ (ap f secta @ Heq a) : {ap_V invf ff'a}
|
||||||
|
... ≈ ap f (ap invf ff'a)^ @ (Heq (invf (f a)) @ ap f' secta) : {!concat_Ap}
|
||||||
|
... ≈ ap f (ap invf ff'a)^ @ Heq (invf (f a)) @ ap f' secta : {!concat_pp_p^}
|
||||||
|
... ≈ ap f ((ap invf ff'a)^) @ Heq (invf (f a)) @ ap f' secta : {!ap_V^}
|
||||||
|
... ≈ Heq (invf (f' a)) @ ap f' ((ap invf ff'a)^) @ ap f' secta : {!concat_Ap}
|
||||||
|
... ≈ Heq (invf (f' a)) @ (ap f' (ap invf ff'a))^ @ ap f' secta : {!ap_V}
|
||||||
|
... ≈ Heq (invf (f' a)) @ ((ap f' (ap invf ff'a))^ @ ap f' secta) : !concat_pp_p,
|
||||||
|
have eq3 : (Heq (invf (f' a)))^ @ retr Hf (f' a) ≈ ap f' ((ap invf ff'a)^ @ secta),
|
||||||
|
from calc (Heq (invf (f' a)))^ @ retr Hf (f' a)
|
||||||
|
≈ (ap f' (ap invf ff'a))^ @ ap f' secta : moveR_Vp _ _ _ eq2
|
||||||
|
... ≈ (ap f' ((ap invf ff'a)^)) @ ap f' secta : {!ap_V^}
|
||||||
|
... ≈ ap f' ((ap invf ff'a)^ @ secta) : !ap_pp^,
|
||||||
|
eq3) in
|
||||||
|
IsEquiv_mk (inv Hf) sect' retr' adj'
|
||||||
|
|
||||||
|
--TODO: Maybe wait until rewrite rules are available.
|
||||||
|
definition inv_closed (Hf : IsEquiv f) : (IsEquiv (inv Hf)) :=
|
||||||
|
IsEquiv_mk sorry sorry sorry sorry
|
||||||
|
|
||||||
|
definition cancel_R (Hf : IsEquiv f) (Hgf : IsEquiv (g ∘ f)) : (IsEquiv g) :=
|
||||||
|
homotopic (comp_closed (inv_closed Hf) Hgf) (λb, ap g (retr Hf b))
|
||||||
|
|
||||||
|
definition cancel_L (Hg : IsEquiv g) (Hgf : IsEquiv (g ∘ f)) : (IsEquiv f) :=
|
||||||
|
homotopic (comp_closed Hgf (inv_closed Hg)) (λa, sect Hg (f a))
|
||||||
|
|
||||||
|
definition transport (P : A → Type) {x y : A} (p : x ≈ y) : (IsEquiv (transport P p)) :=
|
||||||
|
IsEquiv_mk (transport P (p^)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
|
||||||
|
|
||||||
|
--Rewrite rules
|
||||||
|
section
|
||||||
|
variables {Hf : IsEquiv f}
|
||||||
|
|
||||||
|
definition moveR_M {x : A} {y : B} (p : x ≈ (inv Hf) y) : (f x ≈ y) :=
|
||||||
|
ap f p @ retr Hf y
|
||||||
|
|
||||||
|
definition moveL_M {x : A} {y : B} (p : (inv Hf) y ≈ x) : (y ≈ f x) :=
|
||||||
|
(moveR_M (p^))^
|
||||||
|
|
||||||
|
definition moveR_V {x : B} {y : A} (p : x ≈ f y) : (inv Hf) x ≈ y :=
|
||||||
|
ap (inv Hf) p @ sect Hf y
|
||||||
|
|
||||||
|
definition moveL_V {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv Hf) x :=
|
||||||
|
(moveR_V (p^))^
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
end IsEquiv
|
||||||
|
|
||||||
|
namespace Equiv
|
||||||
|
|
||||||
|
variables {A B C : Type} (eqf : A ≃ B)
|
||||||
|
|
||||||
|
theorem id : A ≃ A := Equiv_mk id IsEquiv.idIsEquiv
|
||||||
|
|
||||||
|
theorem compose (eqg: B ≃ C) : A ≃ C :=
|
||||||
|
Equiv_mk ((equiv_fun eqg) ∘ (equiv_fun eqf))
|
||||||
|
(IsEquiv.comp_closed (equiv_isequiv eqf) (equiv_isequiv eqg))
|
||||||
|
|
||||||
|
check IsEquiv.path_closed
|
||||||
|
|
||||||
|
theorem path_closed (f' : A → B) (Heq : equiv_fun eqf ≈ f') : A ≃ B :=
|
||||||
|
Equiv_mk f' (IsEquiv.path_closed (equiv_isequiv eqf) Heq)
|
||||||
|
|
||||||
|
theorem inv_closed : B ≃ A :=
|
||||||
|
Equiv_mk (IsEquiv.inv (equiv_isequiv eqf)) (IsEquiv.inv_closed (equiv_isequiv eqf))
|
||||||
|
|
||||||
|
theorem cancel_L {f : A → B} {g : B → C}
|
||||||
|
(Hf : IsEquiv f) (Hgf : IsEquiv (g ∘ f)) : B ≃ C :=
|
||||||
|
Equiv_mk g (IsEquiv.cancel_R _ _)
|
||||||
|
|
||||||
|
theorem cancel_R {f : A → B} {g : B → C}
|
||||||
|
(Hg : IsEquiv g) (Hgf : IsEquiv (g ∘ f)) : A ≃ B :=
|
||||||
|
Equiv_mk f (!IsEquiv.cancel_L _ _)
|
||||||
|
|
||||||
|
theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
|
||||||
|
Equiv_mk (transport P p) (IsEquiv.transport P p)
|
||||||
|
|
||||||
|
end Equiv
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue