Library UniMath.CategoryTheory.Retracts
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Local Open Scope cat.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Local Open Scope cat.
Section SectionsAndRetractions.
Context {C : precategory}.
Definition is_retraction
{A B : C}
(s : A --> B)
(r : B --> A)
: UU
:= s · r = identity A.
Lemma isaprop_is_retraction
{A B : C}
(s : A --> B)
(r : B --> A)
(H : has_homsets C)
: isaprop (is_retraction s r).
Show proof.
Context {C : precategory}.
Definition is_retraction
{A B : C}
(s : A --> B)
(r : B --> A)
: UU
:= s · r = identity A.
Lemma isaprop_is_retraction
{A B : C}
(s : A --> B)
(r : B --> A)
(H : has_homsets C)
: isaprop (is_retraction s r).
Show proof.
apply H.
A retraction of B onto A
Definition retraction
(A B : C)
: UU
:= ∑ (s : A --> B)
(r : B --> A),
is_retraction s r.
Section Accessors.
Context {A B : C}.
Context (H : retraction A B).
Definition retraction_section
: A --> B
:= pr1 H.
Definition retraction_retraction
: B --> A
:= pr12 H.
Definition retraction_is_retraction
: retraction_section · retraction_retraction = identity A
:= pr22 H.
End Accessors.
Coercion retraction_retraction
: retraction >-> precategory_morphisms.
Lemma isaset_retraction
(A B : ob C)
(H : has_homsets C)
: isaset (retraction A B).
Show proof.
End SectionsAndRetractions.
(A B : C)
: UU
:= ∑ (s : A --> B)
(r : B --> A),
is_retraction s r.
Section Accessors.
Context {A B : C}.
Context (H : retraction A B).
Definition retraction_section
: A --> B
:= pr1 H.
Definition retraction_retraction
: B --> A
:= pr12 H.
Definition retraction_is_retraction
: retraction_section · retraction_retraction = identity A
:= pr22 H.
End Accessors.
Coercion retraction_retraction
: retraction >-> precategory_morphisms.
Lemma isaset_retraction
(A B : ob C)
(H : has_homsets C)
: isaset (retraction A B).
Show proof.
do 2 (apply isaset_total2; [apply H | intro]).
apply isasetaprop.
apply isaprop_is_retraction.
apply H.
apply isasetaprop.
apply isaprop_is_retraction.
apply H.
End SectionsAndRetractions.
Section Idempotents.
Context {C : precategory}.
Definition is_idempotent
{c : C}
(e : c --> c)
: UU
:= e · e = e.
Definition idempotent
(c : C)
: UU
:= ∑ (e : c --> c), is_idempotent e.
#[reversible] Coercion idempotent_morphism
{c : C}
(e : idempotent c)
: c --> c
:= pr1 e.
Definition idempotent_is_idempotent
{c : C}
(e : idempotent c)
: is_idempotent e
:= pr2 e.
Definition is_split_idempotent
{c : C}
(e : c --> c)
: UU
:= ∑ c' (H : retraction c' c), e = retraction_retraction H · retraction_section H.
Definition split_idempotent
(c : C)
: UU
:= ∑ (e : c --> c), is_split_idempotent e.
#[reversible] Coercion split_idempotent_morphism
{c : C}
(e : split_idempotent c)
: c --> c
:= pr1 e.
Definition split_idempotent_is_split_idempotent
{c : C}
(e : split_idempotent c)
: is_split_idempotent e
:= pr2 e.
Definition split_idempotent_object
{c : C}
(e : split_idempotent c)
: C
:= pr12 e.
Definition split_idempotent_retraction
{c : C}
(e : split_idempotent c)
: retraction (split_idempotent_object e) c
:= pr122 e.
Definition split_idempotent_is_split
{c : C}
(e : split_idempotent c)
: split_idempotent_morphism e = split_idempotent_retraction e · retraction_section (split_idempotent_retraction e)
:= pr222 e.
Context {C : precategory}.
Definition is_idempotent
{c : C}
(e : c --> c)
: UU
:= e · e = e.
Definition idempotent
(c : C)
: UU
:= ∑ (e : c --> c), is_idempotent e.
#[reversible] Coercion idempotent_morphism
{c : C}
(e : idempotent c)
: c --> c
:= pr1 e.
Definition idempotent_is_idempotent
{c : C}
(e : idempotent c)
: is_idempotent e
:= pr2 e.
Definition is_split_idempotent
{c : C}
(e : c --> c)
: UU
:= ∑ c' (H : retraction c' c), e = retraction_retraction H · retraction_section H.
Definition split_idempotent
(c : C)
: UU
:= ∑ (e : c --> c), is_split_idempotent e.
#[reversible] Coercion split_idempotent_morphism
{c : C}
(e : split_idempotent c)
: c --> c
:= pr1 e.
Definition split_idempotent_is_split_idempotent
{c : C}
(e : split_idempotent c)
: is_split_idempotent e
:= pr2 e.
Definition split_idempotent_object
{c : C}
(e : split_idempotent c)
: C
:= pr12 e.
Definition split_idempotent_retraction
{c : C}
(e : split_idempotent c)
: retraction (split_idempotent_object e) c
:= pr122 e.
Definition split_idempotent_is_split
{c : C}
(e : split_idempotent c)
: split_idempotent_morphism e = split_idempotent_retraction e · retraction_section (split_idempotent_retraction e)
:= pr222 e.
Lemma split_idempotent_is_idempotent
{c : C}
(e : split_idempotent c)
: is_idempotent e.
Show proof.
End Idempotents.
{c : C}
(e : split_idempotent c)
: is_idempotent e.
Show proof.
induction (!split_idempotent_is_split e).
refine (assoc _ _ _ @ _).
refine (maponpaths (λ x, x · _) _).
refine (assoc' _ _ _ @ _).
refine (maponpaths _ (retraction_is_retraction _) @ _).
apply id_right.
refine (assoc _ _ _ @ _).
refine (maponpaths (λ x, x · _) _).
refine (assoc' _ _ _ @ _).
refine (maponpaths _ (retraction_is_retraction _) @ _).
apply id_right.
End Idempotents.
Lemma functor_preserves_is_retraction
{a b : C}
(f : retraction b a)
: is_retraction (#F (retraction_section f)) (#F f).
Show proof.
Definition functor_preserves_retraction
{a b : C}
(H : retraction b a)
: retraction (F b) (F a)
:= _ ,, _ ,, functor_preserves_is_retraction H.
{a b : C}
(f : retraction b a)
: is_retraction (#F (retraction_section f)) (#F f).
Show proof.
refine (!functor_comp _ _ _ @ _).
refine (maponpaths _ (retraction_is_retraction f) @ _).
apply functor_id.
refine (maponpaths _ (retraction_is_retraction f) @ _).
apply functor_id.
Definition functor_preserves_retraction
{a b : C}
(H : retraction b a)
: retraction (F b) (F a)
:= _ ,, _ ,, functor_preserves_is_retraction H.
Lemma functor_preserves_is_idempotent
{c : C}
(f : idempotent c)
: is_idempotent (#F f).
Show proof.
Definition functor_preserves_idempotent
{c : C}
(H : idempotent c)
: idempotent (F c)
:= _ ,, functor_preserves_is_idempotent H.
{c : C}
(f : idempotent c)
: is_idempotent (#F f).
Show proof.
Definition functor_preserves_idempotent
{c : C}
(H : idempotent c)
: idempotent (F c)
:= _ ,, functor_preserves_is_idempotent H.
Lemma functor_preserves_is_split_idempotent
{c : C}
(f : split_idempotent c)
: is_split_idempotent (#F f).
Show proof.
Definition functor_preserves_split_idempotent
{c : C}
(f : split_idempotent c)
: split_idempotent (F c)
:= _ ,, (functor_preserves_is_split_idempotent f).
End Functors.
{c : C}
(f : split_idempotent c)
: is_split_idempotent (#F f).
Show proof.
unfold is_split_idempotent.
exists (F (split_idempotent_object f)).
exists (functor_preserves_retraction (split_idempotent_retraction f)).
refine (_ @ functor_comp _ _ _).
apply maponpaths.
apply split_idempotent_is_split.
exists (F (split_idempotent_object f)).
exists (functor_preserves_retraction (split_idempotent_retraction f)).
refine (_ @ functor_comp _ _ _).
apply maponpaths.
apply split_idempotent_is_split.
Definition functor_preserves_split_idempotent
{c : C}
(f : split_idempotent c)
: split_idempotent (F c)
:= _ ,, (functor_preserves_is_split_idempotent f).
End Functors.