Null maps

Content created by Fredrik Bakke.

Created on 2024-05-23.
Last modified on 2024-11-19.

module orthogonal-factorization-systems.null-maps where
Imports 
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.diagonal-maps-of-types
open import foundation.equivalences
open import foundation.equivalences-arrows
open import foundation.families-of-equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-fibers-of-maps
open import foundation.homotopies
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.morphisms-arrows
open import foundation.postcomposition-functions
open import foundation.precomposition-functions
open import foundation.propositions
open import foundation.pullbacks
open import foundation.type-arithmetic-unit-type
open import foundation.type-theoretic-principle-of-choice
open import foundation.unit-type
open import foundation.universal-property-family-of-fibers-of-maps
open import foundation.universe-levels

open import orthogonal-factorization-systems.maps-local-at-maps
open import orthogonal-factorization-systems.null-families-of-types
open import orthogonal-factorization-systems.null-types
open import orthogonal-factorization-systems.orthogonal-maps
open import orthogonal-factorization-systems.types-local-at-maps

Idea

A map f : A → B is said to be null at Y, or Y-null if its fibers are Y-null, or equivalently, if the square

         Δ
    A ------> (Y → A)
    |            |
  f |            | f ∘ -
    ∨            ∨
    B ------> (Y → B)
         Δ

is a pullback.

Definitions

The fiber condition for Y-null maps

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

  is-null-map : UU (l1 ⊔ l2 ⊔ l3)
  is-null-map = is-null-family Y (fiber f)

  is-property-is-null-map : is-prop is-null-map
  is-property-is-null-map = is-property-is-null-family Y (fiber f)

  is-null-map-Prop : Prop (l1 ⊔ l2 ⊔ l3)
  is-null-map-Prop = (is-null-map , is-property-is-null-map)

The pullback condition for Y-null maps

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

  cone-is-null-map-pullback-condition :
    cone (diagonal-exponential B Y) (postcomp Y f) A
  cone-is-null-map-pullback-condition =
    (f , diagonal-exponential A Y , refl-htpy)

  is-null-map-pullback-condition : UU (l1 ⊔ l2 ⊔ l3)
  is-null-map-pullback-condition =
    is-pullback
      ( diagonal-exponential B Y)
      ( postcomp Y f)
      ( cone-is-null-map-pullback-condition)

  is-prop-is-null-map-pullback-condition :
    is-prop is-null-map-pullback-condition
  is-prop-is-null-map-pullback-condition =
    is-prop-is-pullback
      ( diagonal-exponential B Y)
      ( postcomp Y f)
      ( cone-is-null-map-pullback-condition)

Properties

A type family is Y-null if and only if its total space projection is

module _
  {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} (B : A → UU l3)
  where

  is-null-family-is-null-map-pr1 :
    is-null-map Y (pr1 {B = B}) → is-null-family Y B
  is-null-family-is-null-map-pr1 =
    is-null-family-equiv-family (inv-equiv-fiber-pr1 B)

  is-null-map-pr1-is-null-family :
    is-null-family Y B → is-null-map Y (pr1 {B = B})
  is-null-map-pr1-is-null-family =
    is-null-family-equiv-family (equiv-fiber-pr1 B)

The pullback and fiber condition for Y-null maps are equivalent

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

  abstract
    compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition :
      (b : B) →
      equiv-arrow
        ( map-fiber-vertical-map-cone
          ( diagonal-exponential B Y)
          ( postcomp Y f)
          ( cone-is-null-map-pullback-condition Y f)
          ( b))
        ( diagonal-exponential (fiber f b) Y)
    compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition b =
      ( id-equiv ,
        inv-compute-Π-fiber-postcomp Y f (diagonal-exponential B Y b) ,
        ( λ where (x , refl) → refl))

  is-null-map-pullback-condition-is-null-map :
    is-null-map Y f → is-null-map-pullback-condition Y f
  is-null-map-pullback-condition-is-null-map H =
    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
      ( diagonal-exponential B Y)
      ( postcomp Y f)
      ( cone-is-null-map-pullback-condition Y f)
      ( λ b →
        is-equiv-source-is-equiv-target-equiv-arrow
          ( map-fiber-vertical-map-cone
            ( diagonal-exponential B Y)
            ( postcomp Y f)
            ( cone-is-null-map-pullback-condition Y f)
            ( b))
          ( diagonal-exponential (fiber f b) Y)
          ( compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition
            ( b))
          ( H b))

  is-null-map-is-null-map-pullback-condition :
    is-null-map-pullback-condition Y f → is-null-map Y f
  is-null-map-is-null-map-pullback-condition H b =
    is-equiv-target-is-equiv-source-equiv-arrow
      ( map-fiber-vertical-map-cone
        ( diagonal-exponential B Y)
        ( postcomp Y f)
        ( cone-is-null-map-pullback-condition Y f)
        ( b))
      ( diagonal-exponential (fiber f b) Y)
      ( compute-map-fiber-vertical-map-cone-is-null-map-pullback-condition b)
      ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
        ( diagonal-exponential B Y)
        ( postcomp Y f)
        ( cone-is-null-map-pullback-condition Y f)
        ( H)
        ( b))

A map is Y-null if and only if it is local at the terminal projection Y → unit

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

  is-local-terminal-map-is-null-map :
    is-null-map Y f → is-local-map (terminal-map Y) f
  is-local-terminal-map-is-null-map H x =
    is-local-terminal-map-is-null Y (fiber f x) (H x)

  is-null-map-is-local-terminal-map :
    is-local-map (terminal-map Y) f → is-null-map Y f
  is-null-map-is-local-terminal-map H x =
    is-null-is-local-terminal-map Y (fiber f x) (H x)

  equiv-is-local-terminal-map-is-null-map :
    is-null-map Y f ≃ is-local-map (terminal-map Y) f
  equiv-is-local-terminal-map-is-null-map =
    equiv-iff-is-prop
      ( is-property-is-null-map Y f)
      ( is-property-is-local-map (terminal-map Y) f)
      ( is-local-terminal-map-is-null-map)
      ( is-null-map-is-local-terminal-map)

  equiv-is-null-map-is-local-terminal-map :
    is-local-map (terminal-map Y) f ≃ is-null-map Y f
  equiv-is-null-map-is-local-terminal-map =
    inv-equiv equiv-is-local-terminal-map-is-null-map

A map is Y-null if and only if the terminal projection of Y is orthogonal to f

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

  is-null-map-is-orthogonal-fiber-condition-terminal-map :
    is-orthogonal-fiber-condition-right-map (terminal-map Y) f →
    is-null-map Y f
  is-null-map-is-orthogonal-fiber-condition-terminal-map H b =
    is-equiv-target-is-equiv-source-equiv-arrow
      ( precomp (terminal-map Y) (fiber f b))
      ( diagonal-exponential (fiber f b) Y)
      ( left-unit-law-function-type (fiber f b) , id-equiv , refl-htpy)
      ( H (point b))

  is-orthogonal-fiber-condition-terminal-map-is-null-map :
    is-null-map Y f →
    is-orthogonal-fiber-condition-right-map (terminal-map Y) f
  is-orthogonal-fiber-condition-terminal-map-is-null-map H b =
    is-equiv-source-is-equiv-target-equiv-arrow
      ( precomp (terminal-map Y) (fiber f (b star)))
      ( diagonal-exponential (fiber f (b star)) Y)
      ( left-unit-law-function-type (fiber f (b star)) , id-equiv , refl-htpy)
      ( H (b star))

  is-null-map-is-orthogonal-pullback-condition-terminal-map :
    is-orthogonal-pullback-condition (terminal-map Y) f → is-null-map Y f
  is-null-map-is-orthogonal-pullback-condition-terminal-map H =
    is-null-map-is-orthogonal-fiber-condition-terminal-map
      ( is-orthogonal-fiber-condition-right-map-is-orthogonal-pullback-condition
        ( terminal-map Y)
        ( f)
        ( H))

  is-orthogonal-pullback-condition-terminal-map-is-null-map :
    is-null-map Y f → is-orthogonal-pullback-condition (terminal-map Y) f
  is-orthogonal-pullback-condition-terminal-map-is-null-map H =
    is-orthogonal-pullback-condition-is-orthogonal-fiber-condition-right-map
      ( terminal-map Y)
      ( f)
      ( is-orthogonal-fiber-condition-terminal-map-is-null-map H)

  is-null-map-is-orthogonal-terminal-map :
    is-orthogonal (terminal-map Y) f → is-null-map Y f
  is-null-map-is-orthogonal-terminal-map H =
    is-null-map-is-orthogonal-fiber-condition-terminal-map
      ( is-orthogonal-fiber-condition-right-map-is-orthogonal
        ( terminal-map Y)
        ( f)
        ( H))

  is-orthogonal-terminal-map-is-null-map :
    is-null-map Y f → is-orthogonal (terminal-map Y) f
  is-orthogonal-terminal-map-is-null-map H =
    is-orthogonal-is-orthogonal-fiber-condition-right-map (terminal-map Y) f
      ( is-orthogonal-fiber-condition-terminal-map-is-null-map H)

Recent changes