# Images of subtypes

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

Created on 2022-09-15.

module foundation.images-subtypes where

Imports
open import foundation.dependent-pair-types
open import foundation.full-subtypes
open import foundation.functoriality-propositional-truncation
open import foundation.images
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.pullbacks-subtypes
open import foundation.subtypes
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.identity-types

open import order-theory.galois-connections-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders
open import order-theory.similarity-of-order-preserving-maps-large-posets


## Idea

Consider a map f : A → B and a subtype S ⊆ A, then the image of S under f is the subtype of B consisting of the values of the composite S ⊆ A → B. In other words, the image im f S of a subtype S under f satisfies the universal property that

  (im f S ⊆ U) ↔ (S ⊆ U ∘ f).


The image operation on subtypes is an order preserving map from the powerset of A to the powerset of B. Thus we obtain a Galois connection between the powersets of A and B: the image-pullback Galois connection

  image-subtype f ⊣ pullback-subtype f.


## Definitions

### The predicate of being the image of a subtype under a map

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

is-image-map-subtype : {l4 : Level} (T : subtype l4 B) → UUω
is-image-map-subtype T =
{l : Level} (U : subtype l B) → (T ⊆ U) ↔ (S ⊆ U ∘ f)


### The image of a subtype under a map

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

im-subtype : subtype (l1 ⊔ l2 ⊔ l3) B
im-subtype y = subtype-im (f ∘ inclusion-subtype S) y

is-in-im-subtype : B → UU (l1 ⊔ l2 ⊔ l3)
is-in-im-subtype = is-in-subtype im-subtype


### The order preserving operation taking the image of a subtype under a map

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

preserves-order-im-subtype :
{l3 l4 : Level} (S : subtype l3 A) (T : subtype l4 A) →
S ⊆ T → im-subtype f S ⊆ im-subtype f T
preserves-order-im-subtype S T H y p =
apply-universal-property-trunc-Prop p
( im-subtype f T y)
( λ ((x , s) , q) → unit-trunc-Prop ((x , H x s) , q))

im-subtype-hom-Large-Poset :
hom-Large-Poset
( λ l → l1 ⊔ l2 ⊔ l)
( powerset-Large-Poset A)
( powerset-Large-Poset B)
map-hom-Large-Preorder im-subtype-hom-Large-Poset =
im-subtype f
preserves-order-hom-Large-Preorder im-subtype-hom-Large-Poset =
preserves-order-im-subtype


### The image-pullback Galois connection on powersets

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

{l3 l4 : Level} (S : subtype l3 A) (T : subtype l4 B) →
(im-subtype f S ⊆ T) → (S ⊆ pullback-subtype f T)
forward-implication-adjoint-relation-image-pullback-subtype S T H x p =
H (f x) (unit-trunc-Prop ((x , p) , refl))

{l3 l4 : Level} (S : subtype l3 A) (T : subtype l4 B) →
(S ⊆ pullback-subtype f T) → (im-subtype f S ⊆ T)
backward-implication-adjoint-relation-image-pullback-subtype S T H y p =
apply-universal-property-trunc-Prop p
( T y)
( λ where ((x , s) , refl) → H x s)

{l3 l4 : Level} (S : subtype l3 A) (T : subtype l4 B) →
(im-subtype f S ⊆ T) ↔ (S ⊆ pullback-subtype f T)
pr1 (adjoint-relation-image-pullback-subtype S T) =
pr2 (adjoint-relation-image-pullback-subtype S T) =

image-pullback-subtype-galois-connection-Large-Poset :
galois-connection-Large-Poset
( λ l → l1 ⊔ l2 ⊔ l)
( λ l → l)
( powerset-Large-Poset A)
( powerset-Large-Poset B)
image-pullback-subtype-galois-connection-Large-Poset =
im-subtype-hom-Large-Poset f
image-pullback-subtype-galois-connection-Large-Poset =
pullback-subtype-hom-Large-Poset f
image-pullback-subtype-galois-connection-Large-Poset =


## Properties

### If S and T have the same elements, then im-subtype f S and im-subtype f T have the same elements

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f : A → B)
(S : subtype l3 A) (T : subtype l4 A)
where

has-same-elements-im-has-same-elements-subtype :
has-same-elements-subtype S T →
has-same-elements-subtype (im-subtype f S) (im-subtype f T)
has-same-elements-im-has-same-elements-subtype s =
has-same-elements-sim-subtype
( im-subtype f S)
( im-subtype f T)
( preserves-sim-hom-Large-Poset
( powerset-Large-Poset A)
( powerset-Large-Poset B)
( im-subtype-hom-Large-Poset f)
( S)
( T)
( sim-has-same-elements-subtype S T s))


### The image subtype im f (full-subtype A) has the same elements as the subtype im f

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

compute-im-full-subtype :
has-same-elements-subtype
( im-subtype f (full-subtype lzero A))
( subtype-im f)
compute-im-full-subtype y =
iff-equiv
( equiv-trunc-Prop
( ( right-unit-law-Σ-is-contr
( λ a →
is-contr-map-is-equiv is-equiv-inclusion-full-subtype (pr1 a))) ∘e
( compute-fiber-comp f inclusion-full-subtype y)))


### The image subtype im (g ∘ f) S has the same elements as the image subtype im g (im f S)

Proof: The asserted similarity follows at once from the similarity

  pullback-subtype (g ∘ f) ≈ pullback-subtype g ∘ pullback-subtype f


via the image-pullback Galois connection.

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
(g : B → C) (f : A → B) (S : subtype l4 A)
where

compute-im-subtype-comp :
has-same-elements-subtype
( im-subtype (g ∘ f) S)
( im-subtype g (im-subtype f S))
compute-im-subtype-comp =
has-same-elements-sim-subtype
( im-subtype (g ∘ f) S)
( im-subtype g (im-subtype f S))
( lower-sim-upper-sim-galois-connection-Large-Poset
( powerset-Large-Poset A)
( powerset-Large-Poset C)
( image-pullback-subtype-galois-connection-Large-Poset (g ∘ f))
( comp-galois-connection-Large-Poset
( powerset-Large-Poset A)
( powerset-Large-Poset B)
( powerset-Large-Poset C)
( image-pullback-subtype-galois-connection-Large-Poset g)
( image-pullback-subtype-galois-connection-Large-Poset f))
( refl-sim-hom-Large-Poset
( powerset-Large-Poset C)
( powerset-Large-Poset A)
( pullback-subtype-hom-Large-Poset (g ∘ f)))
( S))


### The image im (g ∘ f) has the same elements as the image subtype im g (im f)

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

compute-subtype-im-comp :
has-same-elements-subtype (subtype-im (g ∘ f)) (im-subtype g (subtype-im f))
compute-subtype-im-comp x =
logical-equivalence-reasoning
is-in-subtype-im (g ∘ f) x
↔ is-in-im-subtype (g ∘ f) (full-subtype lzero A) x
by
inv-iff (compute-im-full-subtype (g ∘ f) x)
↔ is-in-im-subtype g (im-subtype f (full-subtype lzero A)) x
by
compute-im-subtype-comp g f (full-subtype lzero A) x
↔ is-in-im-subtype g (subtype-im f) x
by
has-same-elements-im-has-same-elements-subtype g
( im-subtype f (full-subtype lzero A))
( subtype-im f)
( compute-im-full-subtype f)
( x)