Mathlib.Topology.Category.TopCat.Opens

TopologicalSpace.Opens.opensHom.instFunLike instance

: FunLike (U ⟶ V) U V

Full source

instance opensHom.instFunLike : FunLike (U ⟶ V) U V where
  coe f := Set.inclusion f.le
  coe_injective' := by rintro ⟨⟨_⟩⟩ _ _; congr!

Function-Like Structure on Morphisms of Open Sets

Informal description

For any open sets $U$ and $V$ in a topological space $X$, the morphisms $U \to V$ in the category of open sets can be treated as functions from $U$ to $V$. Specifically, any morphism $f : U \to V$ can be coerced to a function that maps each point $x \in U$ to a point in $V$, preserving the inclusion $U \subseteq V$.

TopologicalSpace.Opens.apply_def theorem

(f : U ⟶ V) (x : U) : f x = ⟨x, f.le x.2⟩

Full source

lemma apply_def (f : U ⟶ V) (x : U) : f x = ⟨x, f.le x.2⟩ := rfl

Definition of Morphism Application in Open Sets Category

Informal description

For any morphism $f \colon U \to V$ between open sets $U$ and $V$ in a topological space $X$, and for any point $x \in U$, the application of $f$ to $x$ yields the point $\langle x, f.le\ x.2\rangle \in V$, where $x.2$ is the proof that $x \in U$ and $f.le$ is the proof that $U \subseteq V$.

TopologicalSpace.Opens.apply_mk theorem

(f : U ⟶ V) (x : X) (hx) : f ⟨x, hx⟩ = ⟨x, f.le hx⟩

Full source

@[simp] lemma apply_mk (f : U ⟶ V) (x : X) (hx) : f ⟨x, hx⟩ = ⟨x, f.le hx⟩ := rfl

Application of Morphism to Constructed Point in Open Sets

Informal description

For any morphism $f \colon U \to V$ between open sets $U$ and $V$ in a topological space $X$, and for any point $x \in X$ with proof $hx$ that $x \in U$, the application of $f$ to the point $\langle x, hx\rangle \in U$ equals $\langle x, f.le\ hx\rangle \in V$, where $f.le$ is the proof that $U \subseteq V$.

TopologicalSpace.Opens.val_apply theorem

(f : U ⟶ V) (x : U) : (f x : X) = x

Full source

@[simp] lemma val_apply (f : U ⟶ V) (x : U) : (f x : X) = x := rfl

Underlying Point Preservation by Open Set Morphisms

Informal description

For any morphism $f \colon U \to V$ between open sets $U$ and $V$ in a topological space $X$, and for any point $x \in U$, the underlying point in $X$ of $f(x)$ is equal to $x$.

TopologicalSpace.Opens.coe_id theorem

(f : U ⟶ U) : ⇑f = id

Full source

@[simp, norm_cast] lemma coe_id (f : U ⟶ U) : ⇑f = id := rfl

Identity Morphism in Opens Category Acts as Identity Function

Informal description

For any morphism $f \colon U \to U$ in the category of open sets of a topological space $X$, the underlying function of $f$ is equal to the identity function on $U$.

TopologicalSpace.Opens.id_apply theorem

(f : U ⟶ U) (x : U) : f x = x

Full source

lemma id_apply (f : U ⟶ U) (x : U) : f x = x := rfl

Identity Morphism Acts as Identity Function on Points in Open Sets

Informal description

For any morphism $f \colon U \to U$ in the category of open sets of a topological space $X$, and for any point $x \in U$, the evaluation of $f$ at $x$ equals $x$.

TopologicalSpace.Opens.comp_apply theorem

(f : U ⟶ V) (g : V ⟶ W) (x : U) : (f ≫ g) x = g (f x)

Full source

@[simp] lemma comp_apply (f : U ⟶ V) (g : V ⟶ W) (x : U) : (f ≫ g) x = g (f x) := rfl

Composition of Open Set Inclusions Acts as Function Composition

Informal description

For any morphisms $f \colon U \to V$ and $g \colon V \to W$ in the category of open sets of a topological space $X$, and for any point $x \in U$, the composition $(f \gg g)(x)$ is equal to $g(f(x))$.

TopologicalSpace.Opens.infLELeft definition

(U V : Opens X) : U ⊓ V ⟶ U

Full source

/-- The inclusion `U ⊓ V ⟶ U` as a morphism in the category of open sets.
-/
noncomputable def infLELeft (U V : Opens X) : U ⊓ VU ⊓ V ⟶ U :=
  inf_le_left.hom

Inclusion of intersection into first open set

Informal description

For any two open sets $U$ and $V$ in a topological space $X$, the inclusion map $U \cap V \hookrightarrow U$ is a morphism in the category of open sets of $X$.

TopologicalSpace.Opens.infLERight definition

(U V : Opens X) : U ⊓ V ⟶ V

Full source

/-- The inclusion `U ⊓ V ⟶ V` as a morphism in the category of open sets.
-/
noncomputable def infLERight (U V : Opens X) : U ⊓ VU ⊓ V ⟶ V :=
  inf_le_right.hom

Inclusion of intersection into second open set

Informal description

For any two open sets $U$ and $V$ in a topological space $X$, the inclusion map $U \cap V \hookrightarrow V$ is a morphism in the category of open sets of $X$.

TopologicalSpace.Opens.leSupr definition

{ι : Type*} (U : ι → Opens X) (i : ι) : U i ⟶ iSup U

Full source

/-- The inclusion `U i ⟶ iSup U` as a morphism in the category of open sets.
-/
noncomputable def leSupr {ι : Type*} (U : ι → Opens X) (i : ι) : U i ⟶ iSup U :=
  (le_iSup U i).hom

Inclusion of an open set into the union of a family of open sets

Informal description

For any family of open sets $U : \iota \to \text{Opens}(X)$ indexed by a type $\iota$ in a topological space $X$, and for any index $i \in \iota$, the inclusion map $U_i \hookrightarrow \bigsqcup_{j \in \iota} U_j$ is a morphism in the category of open sets of $X$. Here, $\bigsqcup_{j \in \iota} U_j$ denotes the supremum (union) of the family of open sets $U$.

TopologicalSpace.Opens.botLE definition

(U : Opens X) : ⊥ ⟶ U

Full source

/-- The inclusion `⊥ ⟶ U` as a morphism in the category of open sets.
-/
noncomputable def botLE (U : Opens X) : ⊥⊥ ⟶ U :=
  bot_le.hom

Inclusion of empty open set into any open set

Informal description

The morphism representing the inclusion of the empty open set $\bot$ into any open set $U$ in the category of open sets of a topological space $X$.

TopologicalSpace.Opens.leTop definition

(U : Opens X) : U ⟶ ⊤

Full source

/-- The inclusion `U ⟶ ⊤` as a morphism in the category of open sets.
-/
noncomputable def leTop (U : Opens X) : U ⟶ ⊤ :=
  le_top.hom

Inclusion of an open set into the entire space

Informal description

The morphism representing the inclusion of an open set $ U $ into the entire topological space $ X $ (denoted as $ \top $) in the category of open sets of $ X $.

TopologicalSpace.Opens.infLELeft_apply theorem

(U V : Opens X) (x) : (infLELeft U V) x = ⟨x.1, (@inf_le_left _ _ U V : _ ≤ _) x.2⟩

Full source

theorem infLELeft_apply (U V : Opens X) (x) :
    (infLELeft U V) x = ⟨x.1, (@inf_le_left _ _ U V : _ ≤ _) x.2⟩ :=
  rfl

Pointwise Action of Intersection Inclusion Morphism

Informal description

For any open sets $U$ and $V$ in a topological space $X$ and any point $x \in U \cap V$, the morphism $\text{infLELeft}\, U\, V$ maps $x$ to the point $\langle x.1, (\text{inf\_le\_left}\, U\, V)\, x.2 \rangle$ in $U$, where $x.1$ is the underlying point of $x$ and $x.2$ is the proof that $x.1 \in U \cap V$.

TopologicalSpace.Opens.infLELeft_apply_mk theorem

(U V : Opens X) (x) (m) : (infLELeft U V) ⟨x, m⟩ = ⟨x, (@inf_le_left _ _ U V : _ ≤ _) m⟩

Full source

@[simp]
theorem infLELeft_apply_mk (U V : Opens X) (x) (m) :
    (infLELeft U V) ⟨x, m⟩ = ⟨x, (@inf_le_left _ _ U V : _ ≤ _) m⟩ :=
  rfl

Inclusion of Intersection into First Open Set at Point Level

Informal description

For any open sets $U$ and $V$ in a topological space $X$, any point $x \in X$, and any proof $m$ that $x$ belongs to $U \cap V$, the morphism $\text{infLELeft}\, U\, V$ maps the point $\langle x, m \rangle$ in $U \cap V$ to the point $\langle x, (\text{inf\_le\_left}\, U\, V)\, m \rangle$ in $U$.

TopologicalSpace.Opens.leSupr_apply_mk theorem

{ι : Type*} (U : ι → Opens X) (i : ι) (x) (m) : (leSupr U i) ⟨x, m⟩ = ⟨x, (le_iSup U i :) m⟩

Full source

@[simp]
theorem leSupr_apply_mk {ι : Type*} (U : ι → Opens X) (i : ι) (x) (m) :
    (leSupr U i) ⟨x, m⟩ = ⟨x, (le_iSup U i :) m⟩ :=
  rfl

Inclusion of a Point in an Open Set into the Union of Open Sets

Informal description

For any family of open sets $U : \iota \to \text{Opens}(X)$ indexed by a type $\iota$ in a topological space $X$, any index $i \in \iota$, any point $x \in X$, and any proof $m$ that $x$ is in $U_i$, the morphism $\text{leSupr}\, U\, i$ maps the point $\langle x, m \rangle$ in $U_i$ to the point $\langle x, (\text{le\_iSup}\, U\, i)\, m \rangle$ in the union $\bigsqcup_{j \in \iota} U_j$.

TopologicalSpace.Opens.toTopCat definition

(X : TopCat.{u}) : Opens X ⥤ TopCat

Full source

/-- The functor from open sets in `X` to `TopCat`,
realising each open set as a topological space itself.
-/
def toTopCat (X : TopCatTopCat.{u}) : OpensOpens X ⥤ TopCat where
  obj U := TopCat.of U
  map i := TopCat.ofHom ⟨fun x ↦ ⟨x.1, i.le x.2⟩,
    IsEmbedding.subtypeVal.continuous_iff.2 continuous_induced_dom⟩

Functor from open sets to topological spaces

Informal description

The functor $\text{toTopCat}$ from the category of open sets $\text{Opens}(X)$ in a topological space $X$ to the category of topological spaces $\text{TopCat}$, which realizes each open set $U$ as a topological space itself (with the subspace topology inherited from $X$). For a morphism $i : U \to V$ in $\text{Opens}(X)$ (which represents an inclusion $U \subseteq V$), the functor maps it to the continuous inclusion map $U \hookrightarrow V$.

TopologicalSpace.Opens.toTopCat_map theorem

(X : TopCat.{u}) {U V : Opens X} {f : U ⟶ V} {x} {h} : ((toTopCat X).map f) ⟨x, h⟩ = ⟨x, f.le h⟩

Full source

@[simp]
theorem toTopCat_map (X : TopCatTopCat.{u}) {U V : Opens X} {f : U ⟶ V} {x} {h} :
    ((toTopCat X).map f) ⟨x, h⟩ = ⟨x, f.le h⟩ :=
  rfl

Action of Open Set Inclusion Functor on Points

Informal description

For any topological space $X$ and open sets $U, V \subseteq X$, given a morphism $f : U \to V$ in the category of open sets of $X$ (which corresponds to an inclusion $U \subseteq V$), and any point $x \in U$ with proof $h$ that $x \in U$, the image of $\langle x, h \rangle$ under the continuous map $(toTopCat\, X).map\, f$ is $\langle x, f.le\, h \rangle$, where $f.le$ is the proof that $x \in V$.

TopologicalSpace.Opens.inclusion' definition

{X : TopCat.{u}} (U : Opens X) : (toTopCat X).obj U ⟶ X

Full source

/-- The inclusion map from an open subset to the whole space, as a morphism in `TopCat`.
-/
@[simps! -fullyApplied]
def inclusion' {X : TopCatTopCat.{u}} (U : Opens X) : (toTopCat X).obj U ⟶ X :=
  TopCat.ofHom
  { toFun := _
    continuous_toFun := continuous_subtype_val }

Inclusion of an open subset into a topological space

Informal description

For a topological space $X$ and an open subset $U \subseteq X$, the function `inclusion' U` is the continuous inclusion map from the subspace $U$ (with the subspace topology) to the whole space $X$. More precisely, given an open set $U$ in $X$, `inclusion' U` is a morphism in the category of topological spaces from the topological space associated to $U$ (via the functor `toTopCat X`) to the topological space $X$ itself. The underlying function is the natural inclusion of $U$ into $X$, and this function is continuous with respect to the subspace topology on $U$.

TopologicalSpace.Opens.coe_inclusion' theorem

{X : TopCat} {U : Opens X} : (inclusion' U : U → X) = Subtype.val

Full source

@[simp]
theorem coe_inclusion' {X : TopCat} {U : Opens X} :
    (inclusion' U : U → X) = Subtype.val := rfl

Inclusion Map as Subtype Projection

Informal description

For a topological space $X$ and an open subset $U \subseteq X$, the underlying function of the inclusion map $U \hookrightarrow X$ is equal to the canonical projection from the subtype $U$ to $X$.

TopologicalSpace.Opens.isOpenEmbedding theorem

{X : TopCat.{u}} (U : Opens X) : IsOpenEmbedding (inclusion' U)

Full source

theorem isOpenEmbedding {X : TopCatTopCat.{u}} (U : Opens X) : IsOpenEmbedding (inclusion' U) :=
  U.2.isOpenEmbedding_subtypeVal

Inclusion of Open Subset is Open Embedding

Informal description

For any topological space $X$ and any open subset $U$ of $X$, the inclusion map $U \hookrightarrow X$ is an open embedding.

TopologicalSpace.Opens.inclusionTopIso definition

(X : TopCat.{u}) : (toTopCat X).obj ⊤ ≅ X

Full source

/-- The inclusion of the top open subset (i.e. the whole space) is an isomorphism.
-/
def inclusionTopIso (X : TopCatTopCat.{u}) : (toTopCat X).obj ⊤ ≅ X where
  hom := inclusion' ⊤
  inv := TopCat.ofHom ⟨fun x => ⟨x, trivial⟩, continuous_def.2 fun _ ⟨_, hS, hSU⟩ => hSU ▸ hS⟩

Isomorphism of the whole space as an open subset

Informal description

For a topological space $ X $, the inclusion of the entire space $ X $ (considered as an open subset) into itself is an isomorphism in the category of topological spaces. More precisely, the isomorphism consists of: - A continuous map $ \text{hom} $ which is the inclusion $ X \hookrightarrow X $. - A continuous map $ \text{inv} $ which is the identity map $ X \to X $, realized as a continuous map from $ X $ to the subspace $ X $ (with the subspace topology). This isomorphism establishes that the topological space $ X $ and the open subset $ X $ (as a subspace) are isomorphic in the category of topological spaces.

TopologicalSpace.Opens.map definition

(f : X ⟶ Y) : Opens Y ⥤ Opens X

Full source

/-- `Opens.map f` gives the functor from open sets in Y to open set in X,
    given by taking preimages under f. -/
def map (f : X ⟶ Y) : OpensOpens Y ⥤ Opens X where
  obj U := ⟨f ⁻¹' (U : Set Y), U.isOpen.preimage f.hom.continuous⟩
  map i := ⟨⟨fun _ h => i.le h⟩⟩

Preimage functor for open sets under a continuous map

Informal description

Given a continuous map $ f : X \to Y $ between topological spaces, the functor $\text{Opens.map}\, f$ maps an open set $ U $ in $ Y $ to its preimage $ f^{-1}(U) $ in $ X $, which is open due to the continuity of $ f $. On morphisms, it maps an inclusion $ U \subseteq V $ in $ Y $ to the corresponding inclusion $ f^{-1}(U) \subseteq f^{-1}(V) $ in $ X $.

TopologicalSpace.Opens.map_coe theorem

(f : X ⟶ Y) (U : Opens Y) : ((map f).obj U : Set X) = f ⁻¹' (U : Set Y)

Full source

@[simp]
theorem map_coe (f : X ⟶ Y) (U : Opens Y) : ((map f).obj U : Set X) = f ⁻¹' (U : Set Y) :=
  rfl

Preimage of Open Set Under Continuous Map

Informal description

For any continuous map $f \colon X \to Y$ between topological spaces and any open set $U$ in $Y$, the underlying set of the preimage of $U$ under $f$ is equal to the set-theoretic preimage $f^{-1}(U)$.

TopologicalSpace.Opens.map_obj theorem

(f : X ⟶ Y) (U) (p) : (map f).obj ⟨U, p⟩ = ⟨f ⁻¹' U, p.preimage f.hom.continuous⟩

Full source

@[simp]
theorem map_obj (f : X ⟶ Y) (U) (p) : (map f).obj ⟨U, p⟩ = ⟨f ⁻¹' U, p.preimage f.hom.continuous⟩ :=
  rfl

Object part of preimage functor for open sets under continuous maps

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous map, and $U \subseteq Y$ an open subset with proof $p$ that $U$ is open. Then the object part of the preimage functor $\mathrm{map}\,f$ applied to $\langle U, p\rangle$ is $\langle f^{-1}(U), q\rangle$, where $q$ is the proof that $f^{-1}(U)$ is open obtained by applying the continuity of $f$ to $p$.

TopologicalSpace.Opens.map_homOfLE theorem

 (f : X ⟶ Y) {U V : Opens Y} (e : U ≤ V) :
  (TopologicalSpace.Opens.map f).map (homOfLE e) =
    homOfLE (show (Opens.map f).obj U ≤ (Opens.map f).obj V from fun _ hx ↦ e hx)

Full source

@[simp]
lemma map_homOfLE (f : X ⟶ Y) {U V : Opens Y} (e : U ≤ V) :
    (TopologicalSpace.Opens.map f).map (homOfLE e) =
      homOfLE (show (Opens.map f).obj U ≤ (Opens.map f).obj V from fun _ hx ↦ e hx) :=
  rfl

Functoriality of Open Set Preimages on Inclusion Morphisms

Informal description

Given a continuous map $f \colon X \to Y$ between topological spaces and open sets $U, V \subseteq Y$ such that $U \subseteq V$, the functor $\mathrm{Opens.map}\, f$ maps the inclusion morphism $\mathrm{homOfLE}\, e \colon U \to V$ (where $e$ is the proof that $U \subseteq V$) to the inclusion morphism $\mathrm{homOfLE}\, e' \colon f^{-1}(U) \to f^{-1}(V)$, where $e'$ is the proof that $f^{-1}(U) \subseteq f^{-1}(V)$.

TopologicalSpace.Opens.map_id_obj theorem

(U : Opens X) : (map (𝟙 X)).obj U = U

Full source

@[simp]
theorem map_id_obj (U : Opens X) : (map (𝟙 X)).obj U = U :=
  let ⟨_, _⟩ := U
  rfl

Identity Map Preserves Open Sets

Informal description

For any open set $U$ in a topological space $X$, the preimage of $U$ under the identity map $\mathrm{id}_X$ is equal to $U$ itself, i.e., $(\mathrm{map}\, \mathrm{id}_X).U = U$.

TopologicalSpace.Opens.map_id_obj' theorem

(U) (p) : (map (𝟙 X)).obj ⟨U, p⟩ = ⟨U, p⟩

Full source

@[simp]
theorem map_id_obj' (U) (p) : (map (𝟙 X)).obj ⟨U, p⟩ = ⟨U, p⟩ :=
  rfl

Identity Map Preserves Open Set Representation

Informal description

For any open set $U$ in a topological space $X$ with proof $p$ that $U$ is open, the preimage of $\langle U, p \rangle$ under the identity map $\mathrm{id}_X$ is equal to $\langle U, p \rangle$ itself.

TopologicalSpace.Opens.map_id_obj_unop theorem

(U : (Opens X)ᵒᵖ) : (map (𝟙 X)).obj (unop U) = unop U

Full source

theorem map_id_obj_unop (U : (Opens X)ᵒᵖ) : (map (𝟙 X)).obj (unop U) = unop U := by
  simp

Identity Map Preserves Open Sets in Opposite Category

Informal description

For any open set $U$ in the opposite category of open sets of a topological space $X$, the preimage of $U$ under the identity map $\mathrm{id}_X$ is equal to $U$ itself, i.e., $(\mathrm{map}\, \mathrm{id}_X).U = U$.

TopologicalSpace.Opens.op_map_id_obj theorem

(U : (Opens X)ᵒᵖ) : (map (𝟙 X)).op.obj U = U

Full source

theorem op_map_id_obj (U : (Opens X)ᵒᵖ) : (map (𝟙 X)).op.obj U = U := by simp

Opposite Identity Map Preserves Open Sets

Informal description

For any open set $U$ in the opposite category of open sets of a topological space $X$, the preimage of $U$ under the opposite of the identity map functor $\mathrm{map}\, \mathrm{id}_X$ is equal to $U$ itself.

TopologicalSpace.Opens.map_top theorem

(f : X ⟶ Y) : (Opens.map f).obj ⊤ = ⊤

Full source

@[simp]
lemma map_top (f : X ⟶ Y) : (Opens.map f).obj ⊤ = ⊤ := rfl

Preimage of Entire Space under Continuous Map is Entire Space

Informal description

For any continuous map $f \colon X \to Y$ between topological spaces, the preimage of the entire space $Y$ under $f$ is the entire space $X$, i.e., $f^{-1}(Y) = X$.

TopologicalSpace.Opens.leMapTop definition

(f : X ⟶ Y) (U : Opens X) : U ⟶ (map f).obj ⊤

Full source

/-- The inclusion `U ⟶ (map f).obj ⊤` as a morphism in the category of open sets.
-/
noncomputable def leMapTop (f : X ⟶ Y) (U : Opens X) : U ⟶ (map f).obj ⊤ :=
  leTop U

Inclusion into the preimage of the entire space under a continuous map

Informal description

The morphism representing the inclusion of an open set $ U $ in $ X $ into the preimage of the entire space $ Y $ under a continuous map $ f : X \to Y $. In other words, it is the inclusion $ U \subseteq f^{-1}(Y) $, which holds since $ f^{-1}(Y) = X $.

TopologicalSpace.Opens.map_comp_obj theorem

(f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).obj U = (map f).obj ((map g).obj U)

Full source

@[simp]
theorem map_comp_obj (f : X ⟶ Y) (g : Y ⟶ Z) (U) :
    (map (f ≫ g)).obj U = (map f).obj ((map g).obj U) :=
  rfl

Preimage of Composition of Continuous Maps

Informal description

For any continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$ between topological spaces, and any open set $U$ in $Z$, the preimage of $U$ under the composition $f \circ g$ is equal to the preimage under $f$ of the preimage of $U$ under $g$. In other words, $(f \circ g)^{-1}(U) = f^{-1}(g^{-1}(U))$.

TopologicalSpace.Opens.map_comp_obj' theorem

(f : X ⟶ Y) (g : Y ⟶ Z) (U) (p) : (map (f ≫ g)).obj ⟨U, p⟩ = (map f).obj ((map g).obj ⟨U, p⟩)

Full source

@[simp]
theorem map_comp_obj' (f : X ⟶ Y) (g : Y ⟶ Z) (U) (p) :
    (map (f ≫ g)).obj ⟨U, p⟩ = (map f).obj ((map g).obj ⟨U, p⟩) :=
  rfl

Preimage of Composition of Continuous Maps on Open Sets

Informal description

For continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$ between topological spaces, and an open set $U \subseteq Z$ with proof $p$ that $U$ is open, the preimage of $U$ under the composition $f \circ g$ is equal to the preimage under $f$ of the preimage of $U$ under $g$. That is, $(f \circ g)^{-1}(U) = f^{-1}(g^{-1}(U))$.

TopologicalSpace.Opens.map_comp_map theorem

(f : X ⟶ Y) (g : Y ⟶ Z) {U V} (i : U ⟶ V) : (map (f ≫ g)).map i = (map f).map ((map g).map i)

Full source

@[simp]
theorem map_comp_map (f : X ⟶ Y) (g : Y ⟶ Z) {U V} (i : U ⟶ V) :
    (map (f ≫ g)).map i = (map f).map ((map g).map i) :=
  rfl

Functoriality of Preimage Maps for Composition of Continuous Functions

Informal description

Let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps between topological spaces. For any open sets $U, V$ in $Z$ and any inclusion morphism $i \colon U \to V$, the following equality holds for the preimage functors: $$(\mathrm{map}(f \circ g)).\mathrm{map}(i) = (\mathrm{map}\, f).\mathrm{map}((\mathrm{map}\, g).\mathrm{map}(i))$$ where $\mathrm{map}(-)$ denotes the preimage functor on open sets induced by a continuous map.

TopologicalSpace.Opens.map_comp_obj_unop theorem

(f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).obj (unop U) = (map f).obj ((map g).obj (unop U))

Full source

@[simp]
theorem map_comp_obj_unop (f : X ⟶ Y) (g : Y ⟶ Z) (U) :
    (map (f ≫ g)).obj (unop U) = (map f).obj ((map g).obj (unop U)) :=
  rfl

Preimage of Composition of Continuous Maps on Open Sets

Informal description

For any continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$ between topological spaces, and any open set $U$ in $Z$ (given as an unopposed object), the preimage of $U$ under the composition $f \circ g$ is equal to the preimage under $f$ of the preimage of $U$ under $g$. In other words, $(f \circ g)^{-1}(U) = f^{-1}(g^{-1}(U))$.

TopologicalSpace.Opens.op_map_comp_obj theorem

(f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U)

Full source

@[simp]
theorem op_map_comp_obj (f : X ⟶ Y) (g : Y ⟶ Z) (U) :
    (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U) :=
  rfl

Functoriality of Preimage for Open Sets under Composition of Continuous Maps

Informal description

For continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$ between topological spaces, and for any open set $U$ in $Z$, the preimage functor satisfies $(f \circ g)^{-1}(U) = f^{-1}(g^{-1}(U))$ at the level of open sets.

TopologicalSpace.Opens.map_iSup theorem

(f : X ⟶ Y) {ι : Type*} (U : ι → Opens Y) : (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Full source

theorem map_iSup (f : X ⟶ Y) {ι : Type*} (U : ι → Opens Y) :
    (map f).obj (iSup U) = iSup ((map f).obj ∘ U) := by
  ext1; rw [iSup_def, iSup_def, map_obj]
  dsimp; rw [Set.preimage_iUnion]

Preimage Preserves Union of Open Sets under Continuous Maps

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous map, and $\{U_i\}_{i \in \iota}$ a family of open sets in $Y$. Then the preimage of the union $\bigcup_{i \in \iota} U_i$ under $f$ is equal to the union of the preimages of each $U_i$ under $f$, i.e., \[ f^{-1}\left(\bigcup_{i \in \iota} U_i\right) = \bigcup_{i \in \iota} f^{-1}(U_i). \]

TopologicalSpace.Opens.mapId definition

: map (𝟙 X) ≅ 𝟭 (Opens X)

Full source

/-- The functor `Opens X ⥤ Opens X` given by taking preimages under the identity function
is naturally isomorphic to the identity functor.
-/
@[simps]
def mapId : mapmap (𝟙 X) ≅ 𝟭 (Opens X) where
  hom := { app := fun U => eqToHom (map_id_obj U) }
  inv := { app := fun U => eqToHom (map_id_obj U).symm }

Natural isomorphism between identity preimage functor and identity functor on open sets

Informal description

The functor that takes preimages of open sets under the identity map on a topological space $ X $ is naturally isomorphic to the identity functor on the category of open sets of $ X $. Specifically, for any open set $ U $ in $ X $, the preimage $ (\mathrm{map}\, \mathrm{id}_X).U $ is equal to $ U $ itself, and this equality induces the natural isomorphism.

TopologicalSpace.Opens.map_id_eq theorem

: map (𝟙 X) = 𝟭 (Opens X)

Full source

theorem map_id_eq : map (𝟙 X) = 𝟭 (Opens X) := by
  rfl

Identity Functor Property of Preimage Functor: $\mathrm{map}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{Opens}(X)}$

Informal description

The preimage functor $\mathrm{map}$ applied to the identity morphism $\mathrm{id}_X$ is equal to the identity functor on the category of open sets of $X$, i.e., $\mathrm{map}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{Opens}(X)}$.

TopologicalSpace.Opens.mapComp definition

(f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) ≅ map g ⋙ map f

Full source

/-- The natural isomorphism between taking preimages under `f ≫ g`, and the composite
of taking preimages under `g`, then preimages under `f`.
-/
@[simps]
def mapComp (f : X ⟶ Y) (g : Y ⟶ Z) : mapmap (f ≫ g) ≅ map g ⋙ map f where
  hom := { app := fun U => eqToHom (map_comp_obj f g U) }
  inv := { app := fun U => eqToHom (map_comp_obj f g U).symm }

Natural isomorphism for preimage functors under composition of continuous maps

Informal description

For any continuous maps $ f \colon X \to Y $ and $ g \colon Y \to Z $ between topological spaces, there is a natural isomorphism between the functor $\text{map}(f \circ g)$ and the composition of functors $\text{map}\, g \circ \text{map}\, f$. This isomorphism is given by the identity morphism at each open set $U$ in $Z$, viewed as a morphism $(f \circ g)^{-1}(U) \to f^{-1}(g^{-1}(U))$ and its inverse, both of which are constructed using the equality $(f \circ g)^{-1}(U) = f^{-1}(g^{-1}(U))$.

TopologicalSpace.Opens.map_comp_eq theorem

(f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) = map g ⋙ map f

Full source

theorem map_comp_eq (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) = mapmap g ⋙ map f :=
  rfl

Functoriality of Preimage Functor under Composition of Continuous Maps

Informal description

For any continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$ between topological spaces, the functor obtained by mapping open sets through the composition $f \circ g$ is equal to the composition of the functors obtained by mapping open sets through $g$ followed by $f$. That is, $\text{map}(f \circ g) = \text{map}\, g \circ \text{map}\, f$.

TopologicalSpace.Opens.mapIso definition

(f g : X ⟶ Y) (h : f = g) : map f ≅ map g

Full source

/-- If two continuous maps `f g : X ⟶ Y` are equal,
then the functors `Opens Y ⥤ Opens X` they induce are isomorphic.
-/
def mapIso (f g : X ⟶ Y) (h : f = g) : mapmap f ≅ map g :=
  NatIso.ofComponents fun U => eqToIso (by rw [congr_arg map h])

Natural isomorphism of preimage functors for equal continuous maps

Informal description

Given two continuous maps $ f, g : X \to Y $ between topological spaces that are equal (i.e., $ f = g $), the functors $\text{Opens.map}\, f$ and $\text{Opens.map}\, g$ induced by $ f $ and $ g $ are naturally isomorphic. The natural isomorphism is constructed using the equality $ f = g $, which ensures that the preimage functors $ \text{Opens.map}\, f $ and $ \text{Opens.map}\, g $ coincide on objects and morphisms.

TopologicalSpace.Opens.map_eq theorem

(f g : X ⟶ Y) (h : f = g) : map f = map g

Full source

theorem map_eq (f g : X ⟶ Y) (h : f = g) : map f = map g := by
  subst h
  rfl

Equality of Preimage Functors for Equal Continuous Maps

Informal description

For any two continuous maps $f, g : X \to Y$ between topological spaces, if $f = g$, then the preimage functors $\text{map}\, f$ and $\text{map}\, g$ are equal.

TopologicalSpace.Opens.mapIso_refl theorem

(f : X ⟶ Y) (h) : mapIso f f h = Iso.refl (map _)

Full source

@[simp]
theorem mapIso_refl (f : X ⟶ Y) (h) : mapIso f f h = Iso.refl (map _) :=
  rfl

Identity Natural Isomorphism for Preimage Functors of Equal Continuous Maps

Informal description

For any continuous map $f : X \to Y$ between topological spaces, the natural isomorphism $\text{mapIso}\, f\, f\, h$ between the preimage functors (induced by the equality $f = f$) is equal to the identity isomorphism on $\text{map}\, f$.

TopologicalSpace.Opens.mapIso_hom_app theorem

(f g : X ⟶ Y) (h : f = g) (U : Opens Y) : (mapIso f g h).hom.app U = eqToHom (by rw [h])

Full source

@[simp]
theorem mapIso_hom_app (f g : X ⟶ Y) (h : f = g) (U : Opens Y) :
    (mapIso f g h).hom.app U = eqToHom (by rw [h]) :=
  rfl

Component of Natural Isomorphism for Equal Continuous Maps on Open Sets

Informal description

For any two continuous maps $f, g : X \to Y$ between topological spaces such that $f = g$, and for any open set $U$ in $Y$, the component of the natural isomorphism $\text{mapIso}\, f\, g\, h$ at $U$ is equal to the morphism $\text{eqToHom}$ constructed from the equality obtained by rewriting with $h$.

TopologicalSpace.Opens.mapIso_inv_app theorem

(f g : X ⟶ Y) (h : f = g) (U : Opens Y) : (mapIso f g h).inv.app U = eqToHom (by rw [h])

Full source

@[simp]
theorem mapIso_inv_app (f g : X ⟶ Y) (h : f = g) (U : Opens Y) :
    (mapIso f g h).inv.app U = eqToHom (by rw [h]) :=
  rfl

Inverse Component of Natural Isomorphism for Equal Continuous Maps on Open Sets

Informal description

For any continuous maps $f, g \colon X \to Y$ between topological spaces with $f = g$, and for any open set $U$ in $Y$, the inverse component of the natural isomorphism $\text{mapIso}\, f\, g\, h$ at $U$ is equal to the morphism $\text{eqToHom}$ constructed from the equality obtained by rewriting with $h$.

TopologicalSpace.Opens.mapMapIso definition

{X Y : TopCat.{u}} (H : X ≅ Y) : Opens Y ≌ Opens X

Full source

/-- A homeomorphism of spaces gives an equivalence of categories of open sets.

TODO: define `OrderIso.equivalence`, use it.
-/
@[simps]
def mapMapIso {X Y : TopCatTopCat.{u}} (H : X ≅ Y) : OpensOpens Y ≌ Opens X where
  functor := map H.hom
  inverse := map H.inv
  unitIso := NatIso.ofComponents fun U => eqToIso (by simp [map, Set.preimage_preimage])
  counitIso := NatIso.ofComponents fun U => eqToIso (by simp [map, Set.preimage_preimage])

Equivalence of open set categories induced by a homeomorphism

Informal description

Given a homeomorphism $H \colon X \cong Y$ between topological spaces $X$ and $Y$, the function `mapMapIso` constructs an equivalence of categories $\text{Opens}(Y) \simeq \text{Opens}(X)$ between their categories of open sets. The equivalence is given by: - The functor $\text{Opens}(Y) \to \text{Opens}(X)$ that sends an open set $U \subseteq Y$ to its preimage $H^{-1}(U) \subseteq X$. - The inverse functor $\text{Opens}(X) \to \text{Opens}(Y)$ that sends an open set $V \subseteq X$ to its preimage $H(V) \subseteq Y$. - Natural isomorphisms witnessing the equivalence, constructed using the homeomorphism properties of $H$.

IsOpenMap.functor definition

{X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) : Opens X ⥤ Opens Y

Full source

/-- An open map `f : X ⟶ Y` induces a functor `Opens X ⥤ Opens Y`.
-/
@[simps obj_coe]
def IsOpenMap.functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) : OpensOpens X ⥤ Opens Y where
  obj U := ⟨f '' (U : Set X), hf (U : Set X) U.2⟩
  map h := ⟨⟨Set.image_subset _ h.down.down⟩⟩

Functor induced by an open map on open sets

Informal description

Given a continuous map $f \colon X \to Y$ between topological spaces that is an open map (i.e., the image of every open set in $X$ is open in $Y$), this defines a functor from the category of open sets of $X$ to the category of open sets of $Y$. The functor maps an open set $U \subseteq X$ to its image $f(U) \subseteq Y$, and a morphism (inclusion) $U \subseteq V$ to the inclusion $f(U) \subseteq f(V)$.

IsOpenMap.adjunction definition

{X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) : hf.functor ⊣ Opens.map f

Full source

/-- An open map `f : X ⟶ Y` induces an adjunction between `Opens X` and `Opens Y`.
-/
def IsOpenMap.adjunction {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) :
    hf.functor ⊣ Opens.map f where
  unit := { app := fun _ => homOfLE fun x hxU => ⟨x, hxU, rfl⟩ }
  counit := { app := fun _ => homOfLE fun _ ⟨_, hfxV, hxy⟩ => hxy ▸ hfxV }

Adjunction induced by an open map between categories of open sets

Informal description

Given a continuous map $ f \colon X \to Y $ between topological spaces that is an open map, there is an adjunction between the functor $ hf.\text{functor} \colon \text{Opens}\, X \to \text{Opens}\, Y $ (which sends an open set $ U \subseteq X $ to its image $ f(U) \subseteq Y $) and the preimage functor $ \text{Opens.map}\, f \colon \text{Opens}\, Y \to \text{Opens}\, X $ (which sends an open set $ V \subseteq Y $ to its preimage $ f^{-1}(V) \subseteq X $). The unit of the adjunction is given by the inclusion $ U \subseteq f^{-1}(f(U)) $ for each open set $ U \subseteq X $, and the counit is given by the inclusion $ f(f^{-1}(V)) \subseteq V $ for each open set $ V \subseteq Y $.

IsOpenMap.functorFullOfMono instance

{X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) [H : Mono f] : hf.functor.Full

Full source

instance IsOpenMap.functorFullOfMono {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) [H : Mono f] :
    hf.functor.Full where
  map_surjective i :=
    ⟨homOfLE fun x hx => by
      obtain ⟨y, hy, eq⟩ := i.le ⟨x, hx, rfl⟩
      exact (TopCat.mono_iff_injective f).mp H eq ▸ hy, rfl⟩

Fullness of the Open Map Functor for Monomorphisms

Informal description

For any continuous open map $f \colon X \to Y$ between topological spaces that is a monomorphism, the induced functor from the category of open sets of $X$ to the category of open sets of $Y$ is full. That is, for any open sets $U, V \subseteq X$, every inclusion $f(U) \subseteq f(V)$ in $Y$ comes from an inclusion $U \subseteq V$ in $X$.

IsOpenMap.functor_faithful instance

{X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) : hf.functor.Faithful

Full source

instance IsOpenMap.functor_faithful {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) :
    hf.functor.Faithful where

Faithfulness of the Functor Induced by an Open Map

Informal description

For any continuous map $f \colon X \to Y$ between topological spaces that is an open map, the induced functor from the category of open sets of $X$ to the category of open sets of $Y$ is faithful. This means that for any two open sets $U, V \subseteq X$, the functor maps distinct inclusions $U \subseteq V$ to distinct inclusions $f(U) \subseteq f(V)$.

Topology.IsOpenEmbedding.functor_obj_injective theorem

{X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding f) : Function.Injective hf.isOpenMap.functor.obj

Full source

lemma Topology.IsOpenEmbedding.functor_obj_injective {X Y : TopCat} {f : X ⟶ Y}
    (hf : IsOpenEmbedding f) : Function.Injective hf.isOpenMap.functor.obj :=
  fun _ _ e ↦ Opens.ext (Set.image_injective.mpr hf.injective (congr_arg (↑· : Opens Y → Set Y) e))

Injectivity of Open Embedding's Induced Functor on Objects

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be an open embedding. Then the object mapping of the functor induced by $f$ on open sets is injective, i.e., for any open sets $U, V \subseteq X$, if $f(U) = f(V)$ as open sets in $Y$, then $U = V$.

Topology.IsInducing.functorObj definition

{X Y : TopCat} {f : X ⟶ Y} (_ : IsInducing f) (U : Opens X) : Opens Y

Full source

/-- Given an inducing map `X ⟶ Y` and some `U : Opens X`, this is the union of all open sets
whose preimage is `U`. This is right adjoint to `Opens.map`. -/
@[nolint unusedArguments]
def functorObj {X Y : TopCat} {f : X ⟶ Y} (_ : IsInducing f) (U : Opens X) : Opens Y :=
  sSup { s : Opens Y | (Opens.map f).obj s = U }

Maximal open set with given preimage under an inducing map

Informal description

Given an inducing continuous map $f \colon X \to Y$ between topological spaces and an open set $U$ in $X$, this constructs the largest open set $V$ in $Y$ such that the preimage $f^{-1}(V)$ equals $U$. Formally, it is defined as the supremum of all open sets $V$ in $Y$ satisfying $f^{-1}(V) = U$.

Topology.IsInducing.map_functorObj theorem

{X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) (U : Opens X) : (Opens.map f).obj (hf.functorObj U) = U

Full source

lemma map_functorObj {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f)
    (U : Opens X) :
    (Opens.map f).obj (hf.functorObj U) = U := by
  apply le_antisymm
  · rintro x ⟨_, ⟨s, rfl⟩, _, ⟨rfl : _ = U, rfl⟩, hx : f x ∈ s⟩; exact hx
  · intros x hx
    obtain ⟨U, hU⟩ := U
    obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU
    exact Opens.mem_sSup.mpr ⟨⟨_, ht⟩, rfl, hx⟩

Preimage of Maximal Open Set Under Inducing Map Equals Original Open Set

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be an inducing continuous map. For any open set $U$ in $X$, the preimage of the maximal open set $V$ in $Y$ satisfying $f^{-1}(V) = U$ under $f$ is equal to $U$, i.e., $f^{-1}(V) = U$.

Topology.IsInducing.mem_functorObj_iff theorem

{X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) (U : Opens X) {x : X} : f x ∈ hf.functorObj U ↔ x ∈ U

Full source

lemma mem_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) (U : Opens X)
    {x : X} : f x ∈ hf.functorObj Uf x ∈ hf.functorObj U ↔ x ∈ U := by
  conv_rhs => rw [← hf.map_functorObj U]
  rfl

Characterization of Membership in Maximal Open Set Under Inducing Map

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be an inducing continuous map. For any open set $U$ in $X$ and any point $x \in X$, the image $f(x)$ belongs to the maximal open set $V$ in $Y$ satisfying $f^{-1}(V) = U$ if and only if $x$ belongs to $U$. In other words, $f(x) \in V \leftrightarrow x \in U$.

Topology.IsInducing.le_functorObj_iff theorem

 {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) {U : Opens X} {V : Opens Y} :
  V ≤ hf.functorObj U ↔ (Opens.map f).obj V ≤ U

Full source

lemma le_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) {U : Opens X}
    {V : Opens Y} : V ≤ hf.functorObj U ↔ (Opens.map f).obj V ≤ U := by
  obtain ⟨U, hU⟩ := U
  obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU
  constructor
  · exact fun i x hx ↦ (hf.mem_functorObj_iff ((Opens.map f).obj ⟨t, ht⟩)).mp (i hx)
  · intros h x hx
    refine Opens.mem_sSup.mpr ⟨⟨_, V.2.union ht⟩, Opens.ext ?_, Set.mem_union_left t hx⟩
    dsimp
    rwa [Set.union_eq_right]

Characterization of Open Set Inclusion Under Inducing Map via Preimages

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be an inducing continuous map. For any open set $U$ in $X$ and any open set $V$ in $Y$, the inclusion $V \subseteq hf.functorObj(U)$ holds if and only if the preimage $f^{-1}(V)$ is contained in $U$.

Topology.IsInducing.opensGI definition

{X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) : GaloisInsertion (Opens.map f).obj hf.functorObj

Full source

/-- An inducing map `f : X ⟶ Y` induces a Galois insertion between `Opens Y` and `Opens X`. -/
def opensGI {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) :
    GaloisInsertion (Opens.map f).obj hf.functorObj :=
  ⟨_, fun _ _ ↦ hf.le_functorObj_iff.symm, fun U ↦ (hf.map_functorObj U).ge, fun _ _ ↦ rfl⟩

Galois insertion between open set functors for an inducing map

Informal description

Given an inducing continuous map $ f \colon X \to Y $ between topological spaces, there is a Galois insertion between the preimage functor $\text{Opens.map}\, f$ (which maps open sets in $ Y $ to their preimages in $ X $) and the functor $\text{functorObj}$ (which maps open sets in $ X $ to the largest open sets in $ Y $ with the same preimage under $ f $).

Topology.IsInducing.functor definition

{X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) : Opens X ⥤ Opens Y

Full source

/-- An inducing map `f : X ⟶ Y` induces a functor `Opens X ⥤ Opens Y`. -/
@[simps]
def functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) :
    OpensOpens X ⥤ Opens Y where
  obj := hf.functorObj
  map {U V} h := homOfLE (hf.le_functorObj_iff.mpr ((hf.map_functorObj U).trans_le h.le))

Functor on open sets induced by an inducing map

Informal description

Given an inducing continuous map $f \colon X \to Y$ between topological spaces, this defines a functor from the category of open sets of $X$ to the category of open sets of $Y$. The functor maps an open set $U$ in $X$ to the largest open set $V$ in $Y$ such that $f^{-1}(V) = U$, and it maps inclusions of open sets $U \subseteq V$ in $X$ to the corresponding inclusions in $Y$.

Topology.IsInducing.adjunction definition

{X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) : Opens.map f ⊣ hf.functor

Full source

/-- An inducing map `f : X ⟶ Y` induces an adjunction between `Opens Y` and `Opens X`. -/
def adjunction {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) :
    Opens.mapOpens.map f ⊣ hf.functor :=
  hf.opensGI.gc.adjunction

Adjunction between open set functors for an inducing map

Informal description

Given an inducing continuous map $ f \colon X \to Y $ between topological spaces, the preimage functor $\text{Opens.map}\, f$ (which maps open sets in $ Y $ to their preimages in $ X $) is left adjoint to the functor $\text{functor}$ (which maps open sets in $ X $ to the largest open sets in $ Y $ with the same preimage under $ f $).

TopologicalSpace.Opens.isOpenEmbedding_obj_top theorem

{X : TopCat} (U : Opens X) : U.isOpenEmbedding.isOpenMap.functor.obj ⊤ = U

Full source

@[simp]
theorem isOpenEmbedding_obj_top {X : TopCat} (U : Opens X) :
    U.isOpenEmbedding.isOpenMap.functor.obj ⊤ = U := by
  ext1
  exact Set.image_univ.trans Subtype.range_coe

Image of Entire Space Under Open Embedding Functor is Original Open Set

Informal description

For any topological space $X$ and any open subset $U \subseteq X$, the image of the entire space $U$ (considered as a topological space with the subspace topology) under the functor induced by the open embedding $U \hookrightarrow X$ is equal to $U$ itself. In other words, if we apply the open map functor to the top element of the lattice of open sets of $U$, we recover $U$ as an open set in $X$.

TopologicalSpace.Opens.inclusion'_map_eq_top theorem

{X : TopCat} (U : Opens X) : (Opens.map U.inclusion').obj U = ⊤

Full source

@[simp]
theorem inclusion'_map_eq_top {X : TopCat} (U : Opens X) : (Opens.map U.inclusion').obj U = ⊤ := by
  ext1
  exact Subtype.coe_preimage_self _

Preimage of Open Set Under Inclusion is Entire Space

Informal description

For any topological space $X$ and any open subset $U \subseteq X$, the preimage of $U$ under the inclusion map $U \hookrightarrow X$ is equal to the entire space of $U$ (i.e., the top element in the lattice of open subsets of $U$). In other words, $(U \hookrightarrow X)^{-1}(U) = U$ as open subsets of $U$.

TopologicalSpace.Opens.adjunction_counit_app_self theorem

{X : TopCat} (U : Opens X) : U.isOpenEmbedding.isOpenMap.adjunction.counit.app U = eqToHom (by simp)

Full source

@[simp]
theorem adjunction_counit_app_self {X : TopCat} (U : Opens X) :
    U.isOpenEmbedding.isOpenMap.adjunction.counit.app U = eqToHom (by simp) := Subsingleton.elim _ _

Counit of Open Embedding Adjunction is Identity at Self

Informal description

For any topological space $X$ and any open subset $U \subseteq X$, the counit of the adjunction between the functor induced by the open embedding $U \hookrightarrow X$ and the preimage functor, evaluated at $U$, is equal to the identity morphism (constructed via `eqToHom` from a trivial equality).

TopologicalSpace.Opens.inclusion'_top_functor theorem

(X : TopCat) : (@Opens.isOpenEmbedding X ⊤).isOpenMap.functor = map (inclusionTopIso X).inv

Full source

theorem inclusion'_top_functor (X : TopCat) :
    (@Opens.isOpenEmbedding X ⊤).isOpenMap.functor = map (inclusionTopIso X).inv := by
  refine CategoryTheory.Functor.ext ?_ ?_
  · intro U
    ext x
    exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
  · subsingleton

Functor Equality for Whole Space Inclusion and Preimage Functor

Informal description

For a topological space $X$, the functor induced by the open embedding of the entire space $X$ (considered as an open subset) is equal to the preimage functor along the inverse of the isomorphism $X \cong \text{toTopCat}(X).obj(\top)$.

TopologicalSpace.Opens.functor_obj_map_obj theorem

 {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) (U : Opens Y) :
  hf.functor.obj ((Opens.map f).obj U) = hf.functor.obj ⊤ ⊓ U

Full source

theorem functor_obj_map_obj {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) (U : Opens Y) :
    hf.functor.obj ((Opens.map f).obj U) = hf.functor.obj ⊤ ⊓ U := by
  ext
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨⟨x, trivial, rfl⟩, hx⟩
  · rintro ⟨⟨x, -, rfl⟩, hx⟩
    exact ⟨x, hx, rfl⟩

Image-Preimage Intersection Identity for Open Maps

Informal description

Let $X$ and $Y$ be topological spaces, and let $f \colon X \to Y$ be a continuous open map. For any open set $U \subseteq Y$, the image under $f$ of the preimage of $U$ equals the intersection of the image of $X$ under $f$ with $U$, i.e., \[ f(f^{-1}(U)) = f(X) \cap U. \]

TopologicalSpace.Opens.set_range_inclusion' theorem

{X : TopCat} (U : Opens X) : Set.range (inclusion' U) = (U : Set X)

Full source

lemma set_range_inclusion' {X : TopCat} (U : Opens X) :
    Set.range (inclusion' U) = (U : Set X) := by
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    exact x.2
  · intro h
    exact ⟨⟨x, h⟩, rfl⟩

Range of Open Subset Inclusion Equals Subset Itself

Informal description

For a topological space $X$ and an open subset $U \subseteq X$, the range of the inclusion map $U \hookrightarrow X$ is equal to $U$ as a subset of $X$.

TopologicalSpace.Opens.functor_map_eq_inf theorem

{X : TopCat} (U V : Opens X) : U.isOpenEmbedding.isOpenMap.functor.obj ((Opens.map U.inclusion').obj V) = V ⊓ U

Full source

@[simp]
theorem functor_map_eq_inf {X : TopCat} (U V : Opens X) :
    U.isOpenEmbedding.isOpenMap.functor.obj ((Opens.map U.inclusion').obj V) = V ⊓ U := by
  ext1
  simp only [IsOpenMap.coe_functor_obj, map_coe, coe_inf,
    Set.image_preimage_eq_inter_range, set_range_inclusion' U]

Image-Preimage Intersection Identity for Open Subset Inclusions

Informal description

For any topological space $X$ and open subsets $U, V \subseteq X$, the image of the preimage of $V$ under the inclusion map $U \hookrightarrow X$ is equal to the intersection $V \cap U$.

TopologicalSpace.Opens.map_functor_eq' theorem

{X U : TopCat} (f : U ⟶ X) (hf : IsOpenEmbedding f) (V) : ((Opens.map f).obj <| hf.isOpenMap.functor.obj V) = V

Full source

theorem map_functor_eq' {X U : TopCat} (f : U ⟶ X) (hf : IsOpenEmbedding f) (V) :
    ((Opens.map f).obj <| hf.isOpenMap.functor.obj V) = V :=
  Opens.ext <| Set.preimage_image_eq _ hf.injective

Preimage of Image under Open Embedding Equals Original Set

Informal description

Let $X$ and $U$ be topological spaces, and let $f \colon U \to X$ be a continuous map that is an open embedding. Then for any open set $V$ in $U$, the preimage of the image of $V$ under $f$ is equal to $V$ itself, i.e., $f^{-1}(f(V)) = V$.

TopologicalSpace.Opens.map_functor_eq theorem

 {X : TopCat} {U : Opens X} (V : Opens U) :
  ((Opens.map U.inclusion').obj <| U.isOpenEmbedding.isOpenMap.functor.obj V) = V

Full source

@[simp]
theorem map_functor_eq {X : TopCat} {U : Opens X} (V : Opens U) :
    ((Opens.map U.inclusion').obj <| U.isOpenEmbedding.isOpenMap.functor.obj V) = V :=
  TopologicalSpace.Opens.map_functor_eq' _ U.isOpenEmbedding V

Preimage of Image under Open Inclusion Equals Original Set

Informal description

Let $X$ be a topological space and $U$ an open subset of $X$. For any open subset $V$ of $U$ (with the subspace topology), the preimage under the inclusion map $U \hookrightarrow X$ of the image of $V$ under this inclusion equals $V$ itself. In other words, $i^{-1}(i(V)) = V$ where $i : U \hookrightarrow X$ is the inclusion map.

TopologicalSpace.Opens.adjunction_counit_map_functor theorem

 {X : TopCat} {U : Opens X} (V : Opens U) :
  U.isOpenEmbedding.isOpenMap.adjunction.counit.app (U.isOpenEmbedding.isOpenMap.functor.obj V) =
    eqToHom (by dsimp; rw [map_functor_eq V])

Full source

@[simp]
theorem adjunction_counit_map_functor {X : TopCat} {U : Opens X} (V : Opens U) :
    U.isOpenEmbedding.isOpenMap.adjunction.counit.app (U.isOpenEmbedding.isOpenMap.functor.obj V) =
      eqToHom (by dsimp; rw [map_functor_eq V]) := by
  subsingleton

Counit of Adjunction for Open Embedding Equals Equality Morphism

Informal description

Let $X$ be a topological space and $U$ an open subset of $X$. For any open subset $V$ of $U$ (with the subspace topology), the counit of the adjunction between the functor induced by the open embedding $U \hookrightarrow X$ and the preimage functor, evaluated at the image of $V$ under this functor, is equal to the morphism induced by the equality $f^{-1}(f(V)) = V$, where $f$ is the inclusion map.