Idempotent maps

Content created by Fredrik Bakke.

Created on 2024-04-17.
Last modified on 2024-04-17.

module foundation.idempotent-maps where
Imports 
open import foundation.dependent-pair-types
open import foundation.homotopy-algebra
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.retractions
open import foundation-core.sets

Idea

An idempotent map is a map f : A → A equipped with a homotopy

  f ∘ f ~ f.

While this definition corresponds to the classical concept of an idempotent map in set-level mathematics, a homotopy I : f ∘ f ~ f may fail to be coherent with itself in Homotopy Type Theory. For instance, one may ask for a second-order coherence

  J : f ·r I ~ I ·l f

giving the definition of a quasicoherently idempotent map.

The situation may be compared against that of invertible maps vs. coherently invertible maps. Recall that an invertible map is a map f : A → B equipped with a converse map g : B → A and homotopies S : f ∘ g ~ id and R : g ∘ f ~ id witnessing that g is an inverse of f, while a coherently invertible map has an additional coherence f ·r R ~ S ·l f.

It is true that every invertible map is coherently invertible, but no such construction preserves both of the homotopies S and R. Likewise, every quasicoherently idempotent map is also coherently idempotent, although again the coherence J is replaced as part of this construction. On the other hand, in contrast to invertible maps, not every idempotent map can be made to be fully coherent or even quasicoherent. For a counterexample see Section 4 of [Shu17].

Terminology. Our definition of an idempotent map corresponds to the definition of a preidempotent map in and , while their definition of an idempotent map corresponds in our terminology to a coherently idempotent map.

Definitions

The structure on a map of idempotence

is-idempotent : {l : Level} {A : UU l} → (A → A) → UU l
is-idempotent f = f ∘ f ~ f

The type of idempotent maps on a type

idempotent-map : {l : Level} (A : UU l) → UU l
idempotent-map A = Σ (A → A) (is-idempotent)

module _
  {l : Level} {A : UU l} (f : idempotent-map A)
  where

  map-idempotent-map : A → A
  map-idempotent-map = pr1 f

  is-idempotent-idempotent-map :
    is-idempotent map-idempotent-map
  is-idempotent-idempotent-map = pr2 f

Properties

Being an idempotent operation on a set is a property

module _
  {l : Level} {A : UU l} (is-set-A : is-set A) (f : A → A)
  where

  is-prop-is-idempotent-is-set : is-prop (is-idempotent f)
  is-prop-is-idempotent-is-set =
    is-prop-Π (λ x → is-set-A (f (f x)) (f x))

  is-idempotent-is-set-Prop : Prop l
  is-idempotent-is-set-Prop =
    ( is-idempotent f , is-prop-is-idempotent-is-set)

module _
  {l : Level} (A : Set l) (f : type-Set A → type-Set A)
  where

  is-prop-is-idempotent-Set : is-prop (is-idempotent f)
  is-prop-is-idempotent-Set =
    is-prop-is-idempotent-is-set (is-set-type-Set A) f

  is-idempotent-prop-Set : Prop l
  is-idempotent-prop-Set =
    ( is-idempotent f , is-prop-is-idempotent-Set)

If i and r is an inclusion-retraction pair, then i ∘ r is idempotent

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (i : B → A) (r : A → B) (H : is-retraction i r)
  where

  is-idempotent-inclusion-retraction : is-idempotent (i ∘ r)
  is-idempotent-inclusion-retraction = i ·l H ·r r

Idempotence is preserved by homotopies

If a map g is homotopic to an idempotent map f, then g is also idempotent.

module _
  {l : Level} {A : UU l} {f g : A → A} (F : is-idempotent f)
  where

  is-idempotent-htpy : g ~ f → is-idempotent g
  is-idempotent-htpy H =
    horizontal-concat-htpy H H ∙h F ∙h inv-htpy H

  is-idempotent-inv-htpy : f ~ g → is-idempotent g
  is-idempotent-inv-htpy H =
    horizontal-concat-htpy (inv-htpy H) (inv-htpy H) ∙h F ∙h H

See also

References

[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