Perfect images

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-20.
Last modified on 2024-02-06.

module foundation.perfect-images where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.double-negation
open import foundation.iterated-dependent-product-types
open import foundation.iterating-functions
open import foundation.law-of-excluded-middle
open import foundation.negated-equality
open import foundation.negation
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.embeddings
open import foundation-core.empty-types
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.transport-along-identifications

Idea

Consider two maps f : A → B and g : B → A. For (g ◦ f)ⁿ(a₀) ＝ a, consider also the following chain

      f          g            f               g       g
  a₀ --> f (a₀) --> g(f(a₀)) --> f(g(f(a₀))) --> ... --> (g ◦ f)ⁿ(a₀) ＝ a

We say a₀ is an origin for a, and a is a perfect image for g if any origin of a is in the image of g.

Definition

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
  where

  is-perfect-image : (a : A) → UU (l1 ⊔ l2)
  is-perfect-image a =
    (a₀ : A) (n : ℕ) → (iterate n (g ∘ f)) a₀ ＝ a → fiber g a₀

Properties

If g is an embedding, then is-perfect-image a is a proposition. In this case, if we assume the law of exluded middle, we can show is-perfect-image a is a decidable type for any a : A.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  {f : A → B} {g : B → A} (is-emb-g : is-emb g)
  where

  is-prop-is-perfect-image-is-emb :
    (a : A) → is-prop (is-perfect-image f g a)
  is-prop-is-perfect-image-is-emb a =
    is-prop-iterated-Π 3 (λ a₀ n p → is-prop-map-is-emb is-emb-g a₀)

  is-perfect-image-Prop : A → Prop (l1 ⊔ l2)
  pr1 (is-perfect-image-Prop a) = is-perfect-image f g a
  pr2 (is-perfect-image-Prop a) = is-prop-is-perfect-image-is-emb a

  is-decidable-is-perfect-image-is-emb :
    LEM (l1 ⊔ l2) → (a : A) → is-decidable (is-perfect-image f g a)
  is-decidable-is-perfect-image-is-emb lem a =
    lem (is-perfect-image-Prop a)

If a is a perfect image for g, then a has a preimage under g. Just take n = zero in the definition.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-perfect-image-is-fiber :
    {f : A → B} {g : B → A} → (a : A) →
    is-perfect-image f g a → fiber g a
  is-perfect-image-is-fiber a ρ = ρ a 0 refl

One can define a map from A to B restricting the domain to the perfect images of g. This gives a kind of section of g. When g is also an embedding, the map gives a kind of retraction of g.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  where

  inverse-of-perfect-image :
    (a : A) → (is-perfect-image f g a) → B
  inverse-of-perfect-image a ρ =
    pr1 (is-perfect-image-is-fiber a ρ)

  is-section-inverse-of-perfect-image :
    (a : A) (ρ : is-perfect-image f g a) →
    g (inverse-of-perfect-image a ρ) ＝ a
  is-section-inverse-of-perfect-image a ρ =
    pr2 (is-perfect-image-is-fiber a ρ)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  {f : A → B} {g : B → A} {is-emb-g : is-emb g}
  where

  is-retraction-inverse-of-perfect-image :
    (b : B) (ρ : is-perfect-image f g (g b)) →
    inverse-of-perfect-image (g b) ρ ＝ b
  is-retraction-inverse-of-perfect-image b ρ =
    is-injective-is-emb
      is-emb-g
      (is-section-inverse-of-perfect-image (g b) ρ)

If g(f(a)) is a perfect image for g, so is a.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  where

  previous-perfect-image :
    (a : A) →
    is-perfect-image f g (g (f (a))) →
    is-perfect-image f g a
  previous-perfect-image a γ a₀ n p = γ a₀ (succ-ℕ n) (ap (g ∘ f) p)

Perfect images goes to a disjoint place under inverse-of-perfect-image than f

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  where

  perfect-image-has-distinct-image :
    (a a₀ : A) → ¬ (is-perfect-image f g a) → (ρ : is-perfect-image f g a₀) →
    f a ≠ inverse-of-perfect-image a₀ ρ
  perfect-image-has-distinct-image a a₀ nρ ρ p =
    v ρ
    where
    q : g (f a) ＝ a₀
    q = ap g p ∙ is-section-inverse-of-perfect-image a₀ ρ

    s : ¬ (is-perfect-image f g (g (f a)))
    s = λ η → nρ (previous-perfect-image a η)

    v : ¬ (is-perfect-image f g a₀)
    v = tr (λ _ → ¬ (is-perfect-image f g _)) q s

Using the property above, we can talk about origins of a which are not images of g.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  where

  is-not-perfect-image : (a : A) → UU (l1 ⊔ l2)
  is-not-perfect-image a =
    Σ A (λ a₀ → (Σ ℕ (λ n → ((iterate n (g ∘ f)) a₀ ＝ a) × ¬ (fiber g a₀))))

If we assume the law of excluded middle and g is an embedding, we can prove that if is-not-perfect-image a does not hold, we have is-perfect-image a.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  {f : A → B} {g : B → A} (is-emb-g : is-emb g)
  (lem : LEM (l1 ⊔ l2))
  where

  is-perfect-not-not-is-perfect-image :
    (a : A) → ¬ (is-not-perfect-image a) → is-perfect-image f g a
  is-perfect-not-not-is-perfect-image a nρ a₀ n p =
    rec-coproduct
      ( id)
      ( λ a₁ → ex-falso (nρ (a₀ , n , p , a₁)))
      ( lem (fiber g a₀ , is-prop-map-is-emb is-emb-g a₀))

The following property states that if g (b) is not a perfect image, then b has an f fiber a that is not a perfect image for g. Again, we need to assume law of excluded middle and that both g and f are embedding.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  {f : A → B} {g : B → A}
  (is-emb-f : is-emb f) (is-emb-g : is-emb g)
  (lem : LEM (l1 ⊔ l2))
  where

  not-perfect-image-has-not-perfect-fiber :
      (b : B) →
      ¬ (is-perfect-image f g (g b)) →
      Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
  not-perfect-image-has-not-perfect-fiber b nρ = v
      where
      i : ¬¬ (is-not-perfect-image {f = f} (g b))
      i = λ nμ → nρ (is-perfect-not-not-is-perfect-image is-emb-g lem (g b) nμ)

      ii :
        is-not-perfect-image (g b) →
        Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
      ii (x₀ , 0 , u) =
        ex-falso (pr2 u (b , inv (pr1 u)))
      ii (x₀ , succ-ℕ n , u) =
        a , w
        where
        q : f (iterate n (g ∘ f) x₀) ＝ b
        q = is-injective-is-emb is-emb-g (pr1 u)

        a : fiber f b
        a = iterate n (g ∘ f) x₀ , q

        w : ¬ (is-perfect-image f g ((iterate n (g ∘ f)) x₀))
        w = λ s → pr2 u (s x₀ n refl)

      iii : ¬¬ (Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))))
      iii = λ t → i (λ s → t (ii s))

      iv : is-prop (Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))))
      iv =
        is-prop-Σ
          (is-prop-map-is-emb is-emb-f b)
          (λ s → is-prop-neg {A = is-perfect-image f g (pr1 s)})

      v : Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
      v = double-negation-elim-is-decidable (lem (_ , iv)) iii

Recent changes