# Idempotent maps

Content created by Fredrik Bakke.

Created 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