Null maps
Content created by Fredrik Bakke.
Created on 2024-05-23.
Last modified on 2024-05-23.
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.local-maps open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.null-families-of-types open import orthogonal-factorization-systems.null-types open import orthogonal-factorization-systems.orthogonal-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
- 2024-05-23. Fredrik Bakke. Null maps, null types and null type families (#1088).