Factorizations of maps into function classes

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-24.
Last modified on 2024-04-25.

module orthogonal-factorization-systems.factorizations-of-maps-function-classes where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.structure-identity-principle
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import orthogonal-factorization-systems.factorizations-of-maps
open import orthogonal-factorization-systems.function-classes
open import orthogonal-factorization-systems.global-function-classes

Idea

A function class factorization of a map f : A → B into function classes L and R is a pair of maps l : A → X and r : X → B, where l ∈ L and r ∈ R, such that their composite r ∘ l is f.

         X
        ∧ \
 L ∋ l /   \ r ∈ R
      /     ∨
    A -----> B
        f

Definitions

The predicate of being a function class factorization

module _
  {l1 l2 l3 lL lR : Level}
  (L : function-class l1 l3 lL)
  (R : function-class l3 l2 lR)
  {A : UU l1} {B : UU l2} {f : A → B}
  (F : factorization l3 f)
  where

  is-function-class-factorization-Prop : Prop (lL ⊔ lR)
  is-function-class-factorization-Prop =
    product-Prop
      ( L (left-map-factorization F))
      ( R (right-map-factorization F))

  is-function-class-factorization : UU (lL ⊔ lR)
  is-function-class-factorization =
    type-Prop is-function-class-factorization-Prop

  is-prop-is-function-class-factorization :
    is-prop is-function-class-factorization
  is-prop-is-function-class-factorization =
    is-prop-type-Prop is-function-class-factorization-Prop

  is-in-left-class-left-map-is-function-class-factorization :
    is-function-class-factorization →
    is-in-function-class L (left-map-factorization F)
  is-in-left-class-left-map-is-function-class-factorization = pr1

  is-in-right-class-right-map-is-function-class-factorization :
    is-function-class-factorization →
    is-in-function-class R (right-map-factorization F)
  is-in-right-class-right-map-is-function-class-factorization = pr2

  left-class-map-is-function-class-factorization :
    is-function-class-factorization →
    type-function-class L A (image-factorization F)
  pr1 (left-class-map-is-function-class-factorization x) =
    left-map-factorization F
  pr2 (left-class-map-is-function-class-factorization x) =
    is-in-left-class-left-map-is-function-class-factorization x

  right-class-map-is-function-class-factorization :
    is-function-class-factorization →
    type-function-class R (image-factorization F) B
  pr1 (right-class-map-is-function-class-factorization x) =
    right-map-factorization F
  pr2 (right-class-map-is-function-class-factorization x) =
    is-in-right-class-right-map-is-function-class-factorization x

The type of factorizations into function classes

function-class-factorization :
  {l1 l2 l3 lL lR : Level}
  (L : function-class l1 l3 lL)
  (R : function-class l3 l2 lR)
  {A : UU l1} {B : UU l2} (f : A → B) → UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lL ⊔ lR)
function-class-factorization {l3 = l3} L R f =
  Σ (factorization l3 f) (is-function-class-factorization L R)

module _
  {l1 l2 l3 lL lR : Level}
  (L : function-class l1 l3 lL)
  (R : function-class l3 l2 lR)
  {A : UU l1} {B : UU l2} {f : A → B}
  (F : function-class-factorization L R f)
  where

  factorization-function-class-factorization : factorization l3 f
  factorization-function-class-factorization = pr1 F

  is-function-class-factorization-function-class-factorization :
    is-function-class-factorization L R
      ( factorization-function-class-factorization)
  is-function-class-factorization-function-class-factorization = pr2 F

  image-function-class-factorization : UU l3
  image-function-class-factorization =
    image-factorization factorization-function-class-factorization

  left-map-function-class-factorization :
    A → image-function-class-factorization
  left-map-function-class-factorization =
    left-map-factorization factorization-function-class-factorization

  right-map-function-class-factorization :
    image-function-class-factorization → B
  right-map-function-class-factorization =
    right-map-factorization factorization-function-class-factorization

  is-factorization-function-class-factorization :
    is-factorization f
      ( right-map-function-class-factorization)
      ( left-map-function-class-factorization)
  is-factorization-function-class-factorization =
    is-factorization-factorization factorization-function-class-factorization

  is-in-left-class-left-map-function-class-factorization :
    is-in-function-class L left-map-function-class-factorization
  is-in-left-class-left-map-function-class-factorization =
    is-in-left-class-left-map-is-function-class-factorization L R
      ( factorization-function-class-factorization)
      ( is-function-class-factorization-function-class-factorization)

  is-in-right-class-right-map-function-class-factorization :
    is-in-function-class R right-map-function-class-factorization
  is-in-right-class-right-map-function-class-factorization =
    is-in-right-class-right-map-is-function-class-factorization L R
      ( factorization-function-class-factorization)
      ( is-function-class-factorization-function-class-factorization)

  left-class-map-function-class-factorization :
    type-function-class L A image-function-class-factorization
  left-class-map-function-class-factorization =
    left-class-map-is-function-class-factorization L R
      ( factorization-function-class-factorization)
      ( is-function-class-factorization-function-class-factorization)

  right-class-map-function-class-factorization :
    type-function-class R image-function-class-factorization B
  right-class-map-function-class-factorization =
    right-class-map-is-function-class-factorization L R
      ( factorization-function-class-factorization)
      ( is-function-class-factorization-function-class-factorization)

Properties

Characterization of identifications of factorizations of a map into function classes

Proof: This follows immediately from the characterization of identifications of factorizations using the subtype identity principle.

What follows is a long list of auxillary definitions.

module _
  {l1 l2 l3 lL lR : Level}
  (L : function-class l1 l3 lL)
  (R : function-class l3 l2 lR)
  {A : UU l1} {B : UU l2} (f : A → B)
  where

  equiv-function-class-factorization :
    (F E : function-class-factorization L R f) → UU (l1 ⊔ l2 ⊔ l3)
  equiv-function-class-factorization F E =
    equiv-factorization f
      ( factorization-function-class-factorization L R F)
      ( factorization-function-class-factorization L R E)

  id-equiv-function-class-factorization :
    (F : function-class-factorization L R f) →
    equiv-function-class-factorization F F
  id-equiv-function-class-factorization F =
    id-equiv-factorization f
      ( factorization-function-class-factorization L R F)

  equiv-eq-function-class-factorization :
    (F E : function-class-factorization L R f) →
    F ＝ E → equiv-function-class-factorization F E
  equiv-eq-function-class-factorization F E p =
    equiv-eq-factorization f
      ( factorization-function-class-factorization L R F)
      ( factorization-function-class-factorization L R E)
      ( ap pr1 p)

  is-torsorial-equiv-function-class-factorization :
    (F : function-class-factorization L R f) →
    is-torsorial (equiv-function-class-factorization F)
  is-torsorial-equiv-function-class-factorization F =
    is-torsorial-Eq-subtype
      ( is-torsorial-equiv-factorization f
        ( factorization-function-class-factorization L R F))
      ( is-prop-is-function-class-factorization L R)
      ( factorization-function-class-factorization L R F)
      ( id-equiv-function-class-factorization F)
      ( is-function-class-factorization-function-class-factorization L R F)

  is-equiv-equiv-eq-function-class-factorization :
    (F E : function-class-factorization L R f) →
    is-equiv (equiv-eq-function-class-factorization F E)
  is-equiv-equiv-eq-function-class-factorization F =
    fundamental-theorem-id
      ( is-torsorial-equiv-function-class-factorization F)
      ( equiv-eq-function-class-factorization F)

  extensionality-function-class-factorization :
    (F E : function-class-factorization L R f) →
    (F ＝ E) ≃ (equiv-function-class-factorization F E)
  pr1 (extensionality-function-class-factorization F E) =
    equiv-eq-function-class-factorization F E
  pr2 (extensionality-function-class-factorization F E) =
    is-equiv-equiv-eq-function-class-factorization F E

  eq-equiv-function-class-factorization :
    (F E : function-class-factorization L R f) →
    equiv-function-class-factorization F E → F ＝ E
  eq-equiv-function-class-factorization F E =
    map-inv-equiv (extensionality-function-class-factorization F E)

See also

Recent changes