Split idempotent maps
Content created by Fredrik Bakke.
Created on 2024-04-17.
Last modified on 2024-06-04.
module foundation.split-idempotent-maps where
Imports
open import elementary-number-theory.natural-numbers open import foundation.action-on-higher-identifications-functions open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fixed-points-endofunctions open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.homotopy-algebra open import foundation.homotopy-induction open import foundation.idempotent-maps open import foundation.inverse-sequential-diagrams open import foundation.path-algebra open import foundation.quasicoherently-idempotent-maps open import foundation.retracts-of-types open import foundation.sequential-limits open import foundation.structure-identity-principle open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels open import foundation.weakly-constant-maps open import foundation.whiskering-homotopies-composition open import foundation-core.commuting-squares-of-homotopies open import foundation-core.contractible-types open import foundation-core.equality-dependent-pair-types open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.retractions open import foundation-core.sections open import foundation-core.sets open import foundation-core.small-types open import foundation-core.torsorial-type-families
Idea
An endomap f : A → A is
split idempotent¶
if there is a type B and an inclusion-retraction pair i , r displaying B
as a retract of A, and such that
H : i ∘ r ~ f. In other words, if we have a commutative diagram
f
A ----> A
∧ \ ∧
i / \r / i
/ ∨ /
B ====== B.
Observe that split idempotent maps are indeed idempotent, as witnessed by the composite
(H◽H)⁻¹ iRr H
f ∘ f ~ i ∘ r ∘ i ∘ r ~ i ∘ r ~ f
where H : i ∘ r ~ f and R : r ∘ i ~ id.
One important fact about split idempotent maps is that every
quasicoherently idempotent map
splits, and conversely, every split idempotent map is quasicoherently
idempotent. In fact, the type of proofs of split idempotence for an endomap f
is a retract of the type of proofs of quasicoherent idempotence.
Definitions
The structure on a map of being split idempotent
is-split-idempotent : {l1 : Level} (l2 : Level) {A : UU l1} → (A → A) → UU (l1 ⊔ lsuc l2) is-split-idempotent l2 {A} f = Σ ( UU l2) ( λ B → Σ ( B retract-of A) ( λ R → inclusion-retract R ∘ map-retraction-retract R ~ f)) module _ {l1 l2 : Level} {A : UU l1} {f : A → A} (H : is-split-idempotent l2 f) where splitting-type-is-split-idempotent : UU l2 splitting-type-is-split-idempotent = pr1 H retract-is-split-idempotent : splitting-type-is-split-idempotent retract-of A retract-is-split-idempotent = pr1 (pr2 H) inclusion-is-split-idempotent : splitting-type-is-split-idempotent → A inclusion-is-split-idempotent = inclusion-retract retract-is-split-idempotent map-retraction-is-split-idempotent : A → splitting-type-is-split-idempotent map-retraction-is-split-idempotent = map-retraction-retract retract-is-split-idempotent retraction-is-split-idempotent : retraction inclusion-is-split-idempotent retraction-is-split-idempotent = retraction-retract retract-is-split-idempotent is-retraction-map-retraction-is-split-idempotent : is-retraction ( inclusion-is-split-idempotent) ( map-retraction-is-split-idempotent) is-retraction-map-retraction-is-split-idempotent = is-retraction-map-retraction-retract retract-is-split-idempotent htpy-is-split-idempotent : inclusion-is-split-idempotent ∘ map-retraction-is-split-idempotent ~ f htpy-is-split-idempotent = pr2 (pr2 H)
The type of split idempotent maps on a type
split-idempotent-map : {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) split-idempotent-map l2 A = Σ (A → A) (is-split-idempotent l2) module _ {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A) where map-split-idempotent-map : A → A map-split-idempotent-map = pr1 H is-split-idempotent-split-idempotent-map : is-split-idempotent l2 map-split-idempotent-map is-split-idempotent-split-idempotent-map = pr2 H splitting-type-split-idempotent-map : UU l2 splitting-type-split-idempotent-map = splitting-type-is-split-idempotent ( is-split-idempotent-split-idempotent-map) retract-split-idempotent-map : splitting-type-split-idempotent-map retract-of A retract-split-idempotent-map = retract-is-split-idempotent is-split-idempotent-split-idempotent-map inclusion-split-idempotent-map : splitting-type-split-idempotent-map → A inclusion-split-idempotent-map = inclusion-is-split-idempotent is-split-idempotent-split-idempotent-map map-retraction-split-idempotent-map : A → splitting-type-split-idempotent-map map-retraction-split-idempotent-map = map-retraction-is-split-idempotent ( is-split-idempotent-split-idempotent-map) retraction-split-idempotent-map : retraction inclusion-split-idempotent-map retraction-split-idempotent-map = retraction-is-split-idempotent is-split-idempotent-split-idempotent-map is-retraction-map-retraction-split-idempotent-map : is-retraction ( inclusion-split-idempotent-map) ( map-retraction-split-idempotent-map) is-retraction-map-retraction-split-idempotent-map = is-retraction-map-retraction-is-split-idempotent ( is-split-idempotent-split-idempotent-map) htpy-split-idempotent-map : inclusion-split-idempotent-map ∘ map-retraction-split-idempotent-map ~ map-split-idempotent-map htpy-split-idempotent-map = htpy-is-split-idempotent is-split-idempotent-split-idempotent-map
Properties
Split idempotence is closed under homotopies of functions
module _ {l1 l2 l3 : Level} {A : UU l1} {f g : A → A} (H : f ~ g) (S : is-split-idempotent l3 f) where is-split-idempotent-htpy : is-split-idempotent l3 g is-split-idempotent-htpy = ( splitting-type-is-split-idempotent S , retract-is-split-idempotent S , htpy-is-split-idempotent S ∙h H)
Split idempotence is closed under equivalences of splitting types
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A → A} (H : is-split-idempotent l3 f) (e : B ≃ splitting-type-is-split-idempotent H) where inclusion-is-split-idempotent-equiv-splitting-type : B → A inclusion-is-split-idempotent-equiv-splitting-type = inclusion-is-split-idempotent H ∘ map-equiv e map-retraction-is-split-idempotent-equiv-splitting-type : A → B map-retraction-is-split-idempotent-equiv-splitting-type = map-inv-equiv e ∘ map-retraction-is-split-idempotent H htpy-is-split-idempotent-equiv-splitting-type : inclusion-is-split-idempotent-equiv-splitting-type ∘ map-retraction-is-split-idempotent-equiv-splitting-type ~ f htpy-is-split-idempotent-equiv-splitting-type = ( double-whisker-comp ( inclusion-is-split-idempotent H) ( is-section-map-section-map-equiv e) ( map-retraction-is-split-idempotent H)) ∙h ( htpy-is-split-idempotent H) is-split-idempotent-equiv-splitting-type : is-split-idempotent l2 f is-split-idempotent-equiv-splitting-type = ( B , comp-retract (retract-is-split-idempotent H) (retract-equiv e) , htpy-is-split-idempotent-equiv-splitting-type)
The splitting type of a split idempotent map is essentially unique
This is Lemma 3.4 in [Shu17]. Note that it does not require any postulates.
Proof. Given two splittings of an endomap f : A → A, with
inclusion-retraction pairs i , r and i' , r', we get mutual inverse maps
between the splitting types
r' ∘ i : B → B' and r ∘ i' : B' → B.
The computation that they form mutual inverses is straightforward:
rR'i R
r ∘ i' ∘ r' ∘ i ~ r ∘ i ~ id.
module _ {l1 : Level} {A : UU l1} {f : A → A} where map-essentially-unique-splitting-type-is-split-idempotent : {l2 l3 : Level} (H : is-split-idempotent l2 f) (H' : is-split-idempotent l3 f) → splitting-type-is-split-idempotent H → splitting-type-is-split-idempotent H' map-essentially-unique-splitting-type-is-split-idempotent H H' = map-retraction-is-split-idempotent H' ∘ inclusion-is-split-idempotent H is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' : {l2 l3 : Level} (H : is-split-idempotent l2 f) (H' : is-split-idempotent l3 f) → is-section ( map-essentially-unique-splitting-type-is-split-idempotent H H') ( map-essentially-unique-splitting-type-is-split-idempotent H' H) is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' H H' = ( map-retraction-is-split-idempotent H' ·l ( ( htpy-is-split-idempotent H) ∙h ( inv-htpy (htpy-is-split-idempotent H'))) ·r inclusion-is-split-idempotent H') ∙h ( horizontal-concat-htpy ( is-retraction-map-retraction-is-split-idempotent H') ( is-retraction-map-retraction-is-split-idempotent H')) is-equiv-map-essentially-unique-splitting-type-is-split-idempotent : {l2 l3 : Level} (H : is-split-idempotent l2 f) (H' : is-split-idempotent l3 f) → is-equiv ( map-essentially-unique-splitting-type-is-split-idempotent H H') is-equiv-map-essentially-unique-splitting-type-is-split-idempotent H H' = is-equiv-is-invertible ( map-essentially-unique-splitting-type-is-split-idempotent H' H) ( is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' ( H) ( H')) ( is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' ( H') ( H)) essentially-unique-splitting-type-is-split-idempotent : {l2 l3 : Level} (H : is-split-idempotent l2 f) (H' : is-split-idempotent l3 f) → splitting-type-is-split-idempotent H ≃ splitting-type-is-split-idempotent H' essentially-unique-splitting-type-is-split-idempotent H H' = ( map-essentially-unique-splitting-type-is-split-idempotent H H' , is-equiv-map-essentially-unique-splitting-type-is-split-idempotent ( H) ( H'))
The type of split idempotent maps on A is equivalent to retracts of A
Note that the proof relies on the function extensionality axiom.
module _ {l1 l2 : Level} {A : UU l1} where compute-split-idempotent-map : split-idempotent-map l2 A ≃ retracts l2 A compute-split-idempotent-map = equivalence-reasoning Σ ( A → A) ( λ f → Σ ( UU l2) ( λ B → Σ ( B retract-of A) ( λ (i , r , R) → i ∘ r ~ f))) ≃ Σ (A → A) (λ f → (Σ (retracts l2 A) (λ (B , i , r , R) → i ∘ r ~ f))) by equiv-tot ( λ f → inv-associative-Σ ( UU l2) ( _retract-of A) ( λ (B , i , r , R) → i ∘ r ~ f)) ≃ Σ (retracts l2 A) (λ (B , i , r , R) → Σ (A → A) (λ f → i ∘ r ~ f)) by equiv-left-swap-Σ ≃ retracts l2 A by equiv-pr1 (λ (B , i , r , R) → is-torsorial-htpy (i ∘ r))
Characterizing equality of split idempotence structures
We characterize equality of witnesses that an endomap f is split idempotent as
equivalences of splitting types such that the evident retracts are homotopic. In
particular, this characterization relies on the univalence axiom.
module _ {l1 l2 : Level} {A : UU l1} {f : A → A} where coherence-equiv-is-split-idempotent : {l3 : Level} (R : is-split-idempotent l2 f) (S : is-split-idempotent l3 f) → (e : splitting-type-is-split-idempotent R ≃ splitting-type-is-split-idempotent S) ( H : htpy-retract ( retract-is-split-idempotent R) ( comp-retract (retract-is-split-idempotent S) (retract-equiv e))) → UU l1 coherence-equiv-is-split-idempotent R S e H = htpy-is-split-idempotent R ~ horizontal-concat-htpy (pr1 H) (pr1 (pr2 H)) ∙h htpy-is-split-idempotent-equiv-splitting-type S e equiv-is-split-idempotent : {l3 : Level} (R : is-split-idempotent l2 f) (S : is-split-idempotent l3 f) → UU (l1 ⊔ l2 ⊔ l3) equiv-is-split-idempotent R S = Σ ( splitting-type-is-split-idempotent R ≃ splitting-type-is-split-idempotent S) ( λ e → Σ ( htpy-retract ( retract-is-split-idempotent R) ( comp-retract ( retract-is-split-idempotent S) ( retract-equiv e))) ( coherence-equiv-is-split-idempotent R S e)) id-equiv-is-split-idempotent : (R : is-split-idempotent l2 f) → equiv-is-split-idempotent R R id-equiv-is-split-idempotent R = ( ( id-equiv) , ( refl-htpy , refl-htpy , ( inv-htpy ( left-unit-law-left-whisker-comp ( is-retraction-map-retraction-is-split-idempotent R)) ∙h inv-htpy-right-unit-htpy)) , ( refl-htpy)) equiv-eq-is-split-idempotent : (R S : is-split-idempotent l2 f) → R ＝ S → equiv-is-split-idempotent R S equiv-eq-is-split-idempotent R .R refl = id-equiv-is-split-idempotent R abstract is-torsorial-equiv-is-split-idempotent : (R : is-split-idempotent l2 f) → is-torsorial (equiv-is-split-idempotent {l2} R) is-torsorial-equiv-is-split-idempotent R = is-torsorial-Eq-structure ( is-torsorial-equiv (splitting-type-is-split-idempotent R)) ( splitting-type-is-split-idempotent R , id-equiv) ( is-torsorial-Eq-structure ( is-contr-equiv ( Σ ( (splitting-type-is-split-idempotent R) retract-of A) ( htpy-retract (retract-is-split-idempotent R))) ( equiv-tot ( λ S → equiv-tot ( λ I → equiv-tot ( λ J → equiv-concat-htpy' ( is-retraction-map-retraction-is-split-idempotent ( R)) ( ap-concat-htpy ( horizontal-concat-htpy J I) ( right-unit-htpy ∙h left-unit-law-left-whisker-comp ( is-retraction-map-retraction-retract S))))))) ( is-torsorial-htpy-retract (retract-is-split-idempotent R))) ( ( retract-is-split-idempotent R) , ( ( refl-htpy) , ( refl-htpy) , ( inv-htpy ( left-unit-law-left-whisker-comp ( is-retraction-map-retraction-is-split-idempotent R)) ∙h inv-htpy-right-unit-htpy))) ( is-torsorial-htpy (htpy-is-split-idempotent R))) is-equiv-equiv-eq-is-split-idempotent : (R S : is-split-idempotent l2 f) → is-equiv (equiv-eq-is-split-idempotent R S) is-equiv-equiv-eq-is-split-idempotent R = fundamental-theorem-id ( is-torsorial-equiv-is-split-idempotent R) ( equiv-eq-is-split-idempotent R) equiv-equiv-eq-is-split-idempotent : (R S : is-split-idempotent l2 f) → (R ＝ S) ≃ equiv-is-split-idempotent R S equiv-equiv-eq-is-split-idempotent R S = ( equiv-eq-is-split-idempotent R S , is-equiv-equiv-eq-is-split-idempotent R S) eq-equiv-is-split-idempotent : (R S : is-split-idempotent l2 f) → equiv-is-split-idempotent R S → R ＝ S eq-equiv-is-split-idempotent R S = map-inv-is-equiv (is-equiv-equiv-eq-is-split-idempotent R S)
Split idempotent maps are idempotent
This is Lemma 3.3 in [Shu17].
Proof. Given a split idempotent map f with splitting R : r ∘ i ~ id and
homotopy H : i ∘ r ~ f, then f is idempotent via the following witness
(H◽H)⁻¹ iRr H
f ∘ f ~ i ∘ r ∘ i ∘ r ~ i ∘ r ~ f.
module _ {l1 l2 : Level} {A : UU l1} {f : A → A} (H : is-split-idempotent l2 f) where is-idempotent-is-split-idempotent : is-idempotent f is-idempotent-is-split-idempotent = is-idempotent-inv-htpy ( is-idempotent-inclusion-retraction ( inclusion-is-split-idempotent H) ( map-retraction-is-split-idempotent H) ( is-retraction-map-retraction-is-split-idempotent H)) ( htpy-is-split-idempotent H) module _ {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A) where is-idempotent-split-idempotent-map : is-idempotent (map-split-idempotent-map H) is-idempotent-split-idempotent-map = is-idempotent-is-split-idempotent ( is-split-idempotent-split-idempotent-map H)
Split idempotent maps are quasicoherently idempotent
This is Lemma 3.6 in [Shu17].
Proof. Inclusion-retraction composites are quasicoherently idempotent, so since quasicoherently idempotent maps are closed under homotopy we are done.
module _ {l1 l2 : Level} {A : UU l1} {f : A → A} (H : is-split-idempotent l2 f) where abstract quasicoherence-is-idempotent-is-split-idempotent : quasicoherence-is-idempotent f ( is-idempotent-is-split-idempotent H) quasicoherence-is-idempotent-is-split-idempotent = quasicoherence-is-idempotent-is-idempotent-htpy ( is-quasicoherently-idempotent-inv-htpy ( is-quasicoherently-idempotent-inclusion-retraction ( inclusion-is-split-idempotent H) ( map-retraction-is-split-idempotent H) (is-retraction-map-retraction-is-split-idempotent H)) ( htpy-is-split-idempotent H)) ( is-idempotent-is-split-idempotent H) ( ap-concat-htpy _ (inv-inv-htpy (htpy-is-split-idempotent H))) is-quasicoherently-idempotent-is-split-idempotent : is-quasicoherently-idempotent f is-quasicoherently-idempotent-is-split-idempotent = ( is-idempotent-is-split-idempotent H , quasicoherence-is-idempotent-is-split-idempotent) module _ {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A) where is-quasicoherently-idempotent-split-idempotent-map : is-quasicoherently-idempotent (map-split-idempotent-map H) is-quasicoherently-idempotent-split-idempotent-map = is-quasicoherently-idempotent-is-split-idempotent ( is-split-idempotent-split-idempotent-map H)
Every idempotent map on a set splits
This is Theorem 3.7 of [Shu17].
module _ {l : Level} {A : UU l} {f : A → A} (is-set-A : is-set A) (H : is-idempotent f) where splitting-type-is-split-idempotent-is-idempotent-is-set : UU l splitting-type-is-split-idempotent-is-idempotent-is-set = fixed-point f inclusion-is-split-idempotent-is-idempotent-is-set : splitting-type-is-split-idempotent-is-idempotent-is-set → A inclusion-is-split-idempotent-is-idempotent-is-set = pr1 map-retraction-is-split-idempotent-is-idempotent-is-set : A → splitting-type-is-split-idempotent-is-idempotent-is-set map-retraction-is-split-idempotent-is-idempotent-is-set x = (f x , H x) is-retraction-map-retraction-is-split-idempotent-is-idempotent-is-set : is-retraction ( inclusion-is-split-idempotent-is-idempotent-is-set) ( map-retraction-is-split-idempotent-is-idempotent-is-set) is-retraction-map-retraction-is-split-idempotent-is-idempotent-is-set (x , p) = eq-pair-Σ p (eq-is-prop (is-set-A (f x) x)) retraction-is-split-idempotent-is-idempotent-is-set : retraction (inclusion-is-split-idempotent-is-idempotent-is-set) retraction-is-split-idempotent-is-idempotent-is-set = ( map-retraction-is-split-idempotent-is-idempotent-is-set , is-retraction-map-retraction-is-split-idempotent-is-idempotent-is-set) retract-is-split-idempotent-is-idempotent-is-set : splitting-type-is-split-idempotent-is-idempotent-is-set retract-of A retract-is-split-idempotent-is-idempotent-is-set = ( inclusion-is-split-idempotent-is-idempotent-is-set , retraction-is-split-idempotent-is-idempotent-is-set) htpy-is-split-idempotent-is-idempotent-is-set : inclusion-is-split-idempotent-is-idempotent-is-set ∘ map-retraction-is-split-idempotent-is-idempotent-is-set ~ f htpy-is-split-idempotent-is-idempotent-is-set = refl-htpy is-split-idempotent-is-idempotent-is-set : is-split-idempotent l f is-split-idempotent-is-idempotent-is-set = ( splitting-type-is-split-idempotent-is-idempotent-is-set , retract-is-split-idempotent-is-idempotent-is-set , htpy-is-split-idempotent-is-idempotent-is-set)
Weakly constant idempotent maps split
This is Theorem 3.9 of [Shu17].
module _ {l : Level} {A : UU l} {f : A → A} (H : is-idempotent f) (W : is-weakly-constant f) where splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent : UU l splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent = fixed-point f inclusion-is-split-idempotent-is-weakly-constant-is-idempotent : splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent → A inclusion-is-split-idempotent-is-weakly-constant-is-idempotent = pr1 map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent : A → splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent x = ( f x , H x) is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent : is-retraction ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent) ( map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent) is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent _ = eq-is-prop (is-prop-fixed-point-is-weakly-constant W) retraction-is-split-idempotent-is-weakly-constant-is-idempotent : retraction ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent) retraction-is-split-idempotent-is-weakly-constant-is-idempotent = ( map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent , is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent) retract-is-split-idempotent-is-weakly-constant-is-idempotent : retract ( A) ( splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent) retract-is-split-idempotent-is-weakly-constant-is-idempotent = ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent , retraction-is-split-idempotent-is-weakly-constant-is-idempotent) htpy-is-split-idempotent-is-weakly-constant-is-idempotent : inclusion-is-split-idempotent-is-weakly-constant-is-idempotent ∘ map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent ~ f htpy-is-split-idempotent-is-weakly-constant-is-idempotent = refl-htpy is-split-idempotent-is-weakly-constant-is-idempotent : is-split-idempotent l f is-split-idempotent-is-weakly-constant-is-idempotent = ( splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent , retract-is-split-idempotent-is-weakly-constant-is-idempotent , htpy-is-split-idempotent-is-weakly-constant-is-idempotent)
Quasicoherently idempotent maps split
This is Theorem 5.3 of [Shu17].
As per Remark 5.4 [Shu17], the inclusion of A into the splitting type
can be constructed for any endofunction f.
module _ {l : Level} {A : UU l} (f : A → A) where inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' : inverse-sequential-diagram l inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' = ( (λ _ → A) , (λ _ → f)) splitting-type-is-quasicoherently-idempotent' : UU l splitting-type-is-quasicoherently-idempotent' = standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent') inclusion-splitting-type-is-quasicoherently-idempotent' : splitting-type-is-quasicoherently-idempotent' → A inclusion-splitting-type-is-quasicoherently-idempotent' (a , α) = a 0
Moreover, again by Remark 5.4 [Shu17], given only the idempotence
homotopy f ∘ f ~ f, we can construct the converse map to this inclusion and
show that this gives a factorization of f. Indeed, this factorization is
strict.
module _ {l : Level} {A : UU l} {f : A → A} (I : is-idempotent f) where map-retraction-splitting-type-is-quasicoherently-idempotent' : A → splitting-type-is-quasicoherently-idempotent' f map-retraction-splitting-type-is-quasicoherently-idempotent' x = ( (λ _ → f x) , (λ _ → inv (I x))) htpy-is-split-idempotent-is-quasicoherently-idempotent' : inclusion-splitting-type-is-quasicoherently-idempotent' f ∘ map-retraction-splitting-type-is-quasicoherently-idempotent' ~ f htpy-is-split-idempotent-is-quasicoherently-idempotent' = refl-htpy
However, to show that these maps form an inclusion-retraction pair, we use the coherence of quasicoherent idempotents as well as the function extensionality axiom.
module _ {l : Level} {A : UU l} {f : A → A} (H : is-quasicoherently-idempotent f) where inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent : inverse-sequential-diagram l inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent = inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' ( f) splitting-type-is-quasicoherently-idempotent : UU l splitting-type-is-quasicoherently-idempotent = splitting-type-is-quasicoherently-idempotent' f inclusion-splitting-type-is-quasicoherently-idempotent : splitting-type-is-quasicoherently-idempotent → A inclusion-splitting-type-is-quasicoherently-idempotent = inclusion-splitting-type-is-quasicoherently-idempotent' f map-retraction-splitting-type-is-quasicoherently-idempotent : A → splitting-type-is-quasicoherently-idempotent map-retraction-splitting-type-is-quasicoherently-idempotent = map-retraction-splitting-type-is-quasicoherently-idempotent' ( is-idempotent-is-quasicoherently-idempotent H) htpy-is-split-idempotent-is-quasicoherently-idempotent : inclusion-splitting-type-is-quasicoherently-idempotent ∘ map-retraction-splitting-type-is-quasicoherently-idempotent ~ f htpy-is-split-idempotent-is-quasicoherently-idempotent = htpy-is-split-idempotent-is-quasicoherently-idempotent' ( is-idempotent-is-quasicoherently-idempotent H)
Now, to construct the desired retracting homotopy
r ∘ i ~ id
we subdivide the problem into two. First, we show that shifting the sequence and
whiskering by f ∘ f is homotopic to the identity
((f (f a₍₋₎₊₁)) , (f ∘ f) ·l α₍₋₎₊₁) ~ (a , α).
shift-retraction-splitting-type-is-quasicoherently-idempotent : standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) → standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) shift-retraction-splitting-type-is-quasicoherently-idempotent (a , α) = ((f ∘ f ∘ a ∘ succ-ℕ) , ( (f ∘ f) ·l (α ∘ succ-ℕ))) htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent : ((a , α) : standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent)) → f ∘ f ∘ a ∘ succ-ℕ ~ a htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) n = is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n)) ∙ inv (α n) abstract htpy-coherence-shift-retraction-splitting-type-is-quasicoherently-idempotent : (x : standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent)) → coherence-Eq-standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) ( shift-retraction-splitting-type-is-quasicoherently-idempotent x) ( x) ( htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent ( x)) htpy-coherence-shift-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) n = ( ap ( ap (f ∘ f) (α (succ-ℕ n)) ∙_) ( ( ap-concat f ( is-idempotent-is-quasicoherently-idempotent H ( a (second-succ-ℕ n))) ( inv (α (succ-ℕ n)))) ∙ ( ap ( _∙ ap f (inv (α (succ-ℕ n)))) ( coh-is-quasicoherently-idempotent H ( a (second-succ-ℕ n)))))) ∙ ( inv ( assoc ( ap (f ∘ f) (α (succ-ℕ n))) ( is-idempotent-is-quasicoherently-idempotent H ( f (a (second-succ-ℕ n)))) ( ap f (inv (α (succ-ℕ n)))))) ∙ ( ap ( _∙ ap f (inv (α (succ-ℕ n)))) ( inv ( nat-htpy ( is-idempotent-is-quasicoherently-idempotent H) ( α (succ-ℕ n))))) ∙ ( assoc ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n))) ( ap f (α (succ-ℕ n))) ( ap f (inv (α (succ-ℕ n))))) ∙ ( ap ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n)) ∙_) ( ( inv (ap-concat f (α (succ-ℕ n)) (inv (α (succ-ℕ n))))) ∙ ( ap² f (right-inv (α (succ-ℕ n)))) ∙ inv (left-inv (α n)))) ∙ ( inv ( assoc ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n))) ( inv (α n)) ( α n))) compute-shift-retraction-splitting-type-is-quasicoherently-idempotent : shift-retraction-splitting-type-is-quasicoherently-idempotent ~ id compute-shift-retraction-splitting-type-is-quasicoherently-idempotent x = eq-Eq-standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) ( shift-retraction-splitting-type-is-quasicoherently-idempotent x) ( x) ( ( htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent x) , ( htpy-coherence-shift-retraction-splitting-type-is-quasicoherently-idempotent x))
Then we show that r ∘ i is homotopic to this operation. This time we proceed
by induction on n.
htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent : ( (a , α) : standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' ( f))) → ( λ _ → f (inclusion-splitting-type-is-quasicoherently-idempotent (a , α))) ~ ( f ∘ f ∘ a ∘ succ-ℕ) htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) 0 = ap f (α 0) htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) (succ-ℕ n) = ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) n) ∙ ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n))) ∙ ( ap f (α (succ-ℕ n))) abstract htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent : ((a , α) : standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent)) → coherence-square-homotopies ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α)) ( λ n → inv ( is-idempotent-is-quasicoherently-idempotent H ( inclusion-splitting-type-is-quasicoherently-idempotent ( a , α)))) ( λ n → ap (f ∘ f) (α (succ-ℕ n))) ( λ n → ap f ( ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) ( n)) ∙ ( is-idempotent-is-quasicoherently-idempotent H ( a (succ-ℕ n))) ∙ ( ap f (α (succ-ℕ n))))) htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) 0 = ( ap ( inv (is-idempotent-is-quasicoherently-idempotent H (a 0)) ∙_) ( ( ap-concat f ( ap f (α 0) ∙ is-idempotent-is-quasicoherently-idempotent H (a 1)) ( ap f (α 1))) ∙ ( ap-binary (_∙_) ( ap-concat f ( ap f (α 0)) ( is-idempotent-is-quasicoherently-idempotent H (a 1))) ( inv (ap-comp f f (α 1)))))) ∙ ( inv ( assoc ( inv (is-idempotent-is-quasicoherently-idempotent H (a 0))) ( ap f (ap f (α 0)) ∙ ap f (is-idempotent-is-quasicoherently-idempotent H (a 1))) ( ap (f ∘ f) (α 1)))) ∙ ( ap ( _∙ ap (f ∘ f) (α 1)) ( ap ( inv (is-idempotent-is-quasicoherently-idempotent H (a 0)) ∙_) ( ( ap-binary (_∙_) ( inv (ap-comp f f (α 0))) ( coh-is-quasicoherently-idempotent H (a 1))) ∙ ( inv ( nat-htpy ( is-idempotent-is-quasicoherently-idempotent H) (α 0)))) ∙ ( is-retraction-inv-concat ( is-idempotent-is-quasicoherently-idempotent H (a 0)) ( ap f (α 0)))))
For the inductive step we fill the following diagram as prescribed, in the notation of [Shu17]:
ξₙ₊₁ I aₙ₊₁ f (αₙ₊₁)⁻¹
f a₀ ------------> f (f aₙ₊₁) ---> f aₙ₊₁ --------------------> f (f aₙ₊₂)
| | [nat-htpy] ___refl___/ |
(I⁻¹ a₀) [Ξₙ] | I (f aₙ₊₂) / (f ∘ f)(αₙ₊₂)
∨ ∨ ------> / ∨
f (f a₀) --------> f (f (f aₙ₊₂)) [J] f (f aₙ₊₂) ----------> f (f (f aₙ₊₃))
(f (ξₙ ∙ I aₙ₊₁ ∙ f αₙ₊₁)) ------> (f ∘ f) (αₙ₊₂)
f (I aₙ₊₂)
where the symbols translate to code as follows:
I = is-idempotent-is-quasicoherently-idempotent H
J = coh-is-quasicoherently-idempotent H
ξ = htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent (a , α)
Ξ = htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent (a , α).
Note, in particular, that the left-hand square is the inductive hypothesis.
htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) (succ-ℕ n) = ( ap ( inv (I (a 0)) ∙_) ( ( ap-concat f ( ξ (succ-ℕ n) ∙ I (a (second-succ-ℕ n))) ( ap f (α (second-succ-ℕ n)))) ∙ ( ap-binary (_∙_) ( ap-concat f (ξ (succ-ℕ n)) (I (a (second-succ-ℕ n)))) ( inv (ap-comp f f (α (second-succ-ℕ n))))))) ∙ ( inv ( assoc ( inv (I (a 0))) ( ap f ( ξ n ∙ I (a (succ-ℕ n)) ∙ ap f (α (succ-ℕ n))) ∙ ap f (I (a (second-succ-ℕ n)))) ( ap (f ∘ f) (α (second-succ-ℕ n))))) ∙ ( ap ( _∙ ap (f ∘ f) (α (second-succ-ℕ n))) ( ( inv ( assoc ( inv (I (a 0))) ( ap f (ξ n ∙ I (a (succ-ℕ n)) ∙ ap f (α (succ-ℕ n)))) ( ap f (I (a (second-succ-ℕ n)))))) ∙ ( ap ( _∙ ap f (I ( a (second-succ-ℕ n)))) ( htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) ( n))) ∙ ( assoc ( ξ n) ( ap (f ∘ f) (α (succ-ℕ n))) ( ap f (I (a (second-succ-ℕ n))))) ∙ ( ap ( ξ n ∙_) ( ap ( ap (f ∘ f) (α (succ-ℕ n)) ∙_) ( coh-is-quasicoherently-idempotent H ( a (succ-ℕ (succ-ℕ n)))) ∙ ( inv (nat-htpy I (α (succ-ℕ n)))))) ∙ ( inv (assoc (ξ n) (I (a (succ-ℕ n))) (ap f (α (succ-ℕ n))))))) where ξ : ( λ _ → f ( inclusion-splitting-type-is-quasicoherently-idempotent ( a , α))) ~ ( f ∘ f ∘ a ∘ succ-ℕ) ξ = htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( a , α) I : is-idempotent f I = pr1 H
Now it only remains to put it all together.
abstract compute-retraction-splitting-type-is-quasicoherently-idempotent : map-retraction-splitting-type-is-quasicoherently-idempotent ∘ inclusion-splitting-type-is-quasicoherently-idempotent ~ shift-retraction-splitting-type-is-quasicoherently-idempotent compute-retraction-splitting-type-is-quasicoherently-idempotent x = eq-Eq-standard-sequential-limit ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) ( map-retraction-splitting-type-is-quasicoherently-idempotent ( inclusion-splitting-type-is-quasicoherently-idempotent x)) ( shift-retraction-splitting-type-is-quasicoherently-idempotent ( x)) ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( x) , htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent ( x)) is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent : is-retraction ( inclusion-splitting-type-is-quasicoherently-idempotent) ( map-retraction-splitting-type-is-quasicoherently-idempotent) is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent = compute-retraction-splitting-type-is-quasicoherently-idempotent ∙h compute-shift-retraction-splitting-type-is-quasicoherently-idempotent retraction-splitting-type-is-quasicoherently-idempotent : retraction (inclusion-splitting-type-is-quasicoherently-idempotent) retraction-splitting-type-is-quasicoherently-idempotent = ( map-retraction-splitting-type-is-quasicoherently-idempotent , is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent) retract-splitting-type-is-quasicoherently-idempotent : splitting-type-is-quasicoherently-idempotent retract-of A retract-splitting-type-is-quasicoherently-idempotent = ( inclusion-splitting-type-is-quasicoherently-idempotent , retraction-splitting-type-is-quasicoherently-idempotent) splitting-is-quasicoherently-idempotent : retracts l A splitting-is-quasicoherently-idempotent = ( splitting-type-is-quasicoherently-idempotent , retract-splitting-type-is-quasicoherently-idempotent) is-split-idempotent-is-quasicoherently-idempotent : is-split-idempotent l f is-split-idempotent-is-quasicoherently-idempotent = ( splitting-type-is-quasicoherently-idempotent , retract-splitting-type-is-quasicoherently-idempotent , htpy-is-split-idempotent-is-quasicoherently-idempotent)
We record these same facts for the bundled data of a quasicoherently idempotent
map on A.
module _ {l : Level} {A : UU l} (f : quasicoherently-idempotent-map A) where splitting-type-quasicoherently-idempotent-map : UU l splitting-type-quasicoherently-idempotent-map = splitting-type-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) inclusion-splitting-type-quasicoherently-idempotent-map : splitting-type-quasicoherently-idempotent-map → A inclusion-splitting-type-quasicoherently-idempotent-map = inclusion-splitting-type-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) map-retraction-splitting-type-quasicoherently-idempotent-map : A → splitting-type-quasicoherently-idempotent-map map-retraction-splitting-type-quasicoherently-idempotent-map = map-retraction-splitting-type-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) is-retraction-map-retraction-splitting-type-quasicoherently-idempotent-map : is-retraction ( inclusion-splitting-type-quasicoherently-idempotent-map) ( map-retraction-splitting-type-quasicoherently-idempotent-map) is-retraction-map-retraction-splitting-type-quasicoherently-idempotent-map = is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) retraction-splitting-type-quasicoherently-idempotent-map : retraction (inclusion-splitting-type-quasicoherently-idempotent-map) retraction-splitting-type-quasicoherently-idempotent-map = retraction-splitting-type-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) retract-splitting-type-quasicoherently-idempotent-map : splitting-type-quasicoherently-idempotent-map retract-of A retract-splitting-type-quasicoherently-idempotent-map = retract-splitting-type-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) splitting-quasicoherently-idempotent-map : retracts l A splitting-quasicoherently-idempotent-map = splitting-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) htpy-is-split-idempotent-quasicoherently-idempotent-map : inclusion-splitting-type-quasicoherently-idempotent-map ∘ map-retraction-splitting-type-quasicoherently-idempotent-map ~ map-quasicoherently-idempotent-map f htpy-is-split-idempotent-quasicoherently-idempotent-map = htpy-is-split-idempotent-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) is-split-idempotent-quasicoherently-idempotent-map : is-split-idempotent l (map-quasicoherently-idempotent-map f) is-split-idempotent-quasicoherently-idempotent-map = is-split-idempotent-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f)
If a map is split idempotent at any universe level, it is split idempotent at its own universe level
module _ {l1 l2 : Level} {A : UU l1} {f : A → A} (S : is-split-idempotent l2 f) where is-small-split-idempotent-is-split-idempotent : is-split-idempotent l1 f is-small-split-idempotent-is-split-idempotent = is-split-idempotent-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-is-split-idempotent S)
Small types are closed under retracts
This is Theorem 2.13 of [dJE23]. Note, in particular, that it does not rely on univalence.
Proof: Assume given an inclusion-retraction pair i , r that displays B
as a retract of the small type A. By essential uniqueness of splitting types,
B is equivalent to every other splitting type of i ∘ r. Now, another
splitting type of i ∘ r is the splitting type as constructed for the witness
is-split-idempotent-is-quasicoherently-idempotent
( is-quasicoherently-idempotent-inclusion-retraction i r ...),
and this is a small sequential limit. Hence B is equivalent to a small type,
and so is itself small.
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-small-retract' : B retract-of A → is-small l1 B pr1 (is-small-retract' R) = splitting-type-is-quasicoherently-idempotent' ( inclusion-retract R ∘ map-retraction-retract R) pr2 (is-small-retract' R) = essentially-unique-splitting-type-is-split-idempotent ( B , R , refl-htpy) ( is-split-idempotent-is-quasicoherently-idempotent ( is-quasicoherently-idempotent-inclusion-retraction ( inclusion-retract R) ( map-retraction-retract R) ( is-retraction-map-retraction-retract R))) module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} where is-small-retract : is-small l3 A → B retract-of A → is-small l3 B is-small-retract is-small-A r = is-small-retract' ( comp-retract (retract-equiv (equiv-is-small is-small-A)) r)
References
- [dJE23]
- Tom de Jong and Martín Hötzel Escardó. On Small Types in Univalent Foundations. Logical Methods in Computer Science, 05 2023. URL: https://lmcs.episciences.org/11270, arXiv:2111.00482, doi:10.46298/lmcs-19(2:8)2023.
- [Shu17]
- Michael Shulman. Idempotents in intensional type theory. Logical Methods in Computer Science, 12:1–24, 04 2017. arXiv:1507.03634, doi:10.2168/LMCS-12(3:9)2016.
- [Shu14]
- Mike Shulman. Splitting Idempotents. Blog post, 12 2014. URL: https://homotopytypetheory.org/2014/12/08/splitting-idempotents/.
Recent changes
- 2024-06-04. Fredrik Bakke. Quasiidempotence is not a proposition (#1127).
- 2024-04-17. Fredrik Bakke. Splitting idempotents (#1105).