Mathlib.Topology.Category.TopCat.Basic

TopCat structure

Full source

/-- The category of topological spaces. -/
structure TopCat where
  private mk ::
  /-- The underlying type. -/
  carrier : Type u
  [str : TopologicalSpace carrier]

Category of Topological Spaces

Informal description

The category `TopCat` consists of topological spaces as objects, where each object is a type equipped with a topology. Morphisms in this category are continuous maps between these topological spaces.

TopCat.instCoeSortType instance

: CoeSort (TopCat) (Type u)

Full source

instance : CoeSort (TopCat) (Type u) :=
  ⟨TopCat.carrier⟩

Topological Spaces as Types

Informal description

Every object in the category of topological spaces can be viewed as a type.

TopCat.of abbrev

(X : Type u) [TopologicalSpace X] : TopCat

Full source

/-- The object in `TopCat` associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `TopCat`. -/
abbrev of (X : Type u) [TopologicalSpace X] : TopCat :=
  ⟨X⟩

Construction of Topological Space Object from Type

Informal description

Given a type $X$ equipped with a topological space structure, the abbreviation `TopCat.of X` constructs an object in the category `TopCat` of topological spaces.

TopCat.coe_of theorem

(X : Type u) [TopologicalSpace X] : (of X : Type u) = X

Full source

lemma coe_of (X : Type u) [TopologicalSpace X] : (of X : Type u) = X :=
  rfl

Underlying Type of Topological Space Construction Equals Original Type

Informal description

For any type $X$ equipped with a topological space structure, the underlying type of the topological space object `TopCat.of X` is equal to $X$ itself, i.e., $(\text{TopCat.of } X : \text{Type } u) = X$.

TopCat.of_carrier theorem

(X : TopCat.{u}) : of X = X

Full source

lemma of_carrier (X : TopCatTopCat.{u}) : of X = X := rfl

Equality of Topological Space Construction and Original Space

Informal description

For any topological space $X$ in the category `TopCat`, the construction `TopCat.of X` is equal to $X$ itself, i.e., $\text{TopCat.of } X = X$.

TopCat.Hom structure

(X Y : TopCat.{u})

Full source

/-- The type of morphisms in `TopCat`. -/
@[ext]
structure Hom (X Y : TopCatTopCat.{u}) where
  private mk ::
  /-- The underlying `ContinuousMap`. -/
  hom' : C(X, Y)

Continuous maps between topological spaces

Informal description

The type of morphisms between two topological spaces $ X $ and $ Y $ in the category `TopCat`, consisting of continuous maps from $ X $ to $ Y $.

TopCat.instCategory instance

: Category TopCat

Full source

instance : Category TopCat where
  Hom X Y := Hom X Y
  id X := ⟨ContinuousMap.id X⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

The Category of Topological Spaces

Informal description

The category $\mathrm{TopCat}$ of topological spaces, where objects are topological spaces and morphisms are continuous maps, forms a category.

TopCat.instConcreteCategoryContinuousMapCarrier instance

: ConcreteCategory.{u} TopCat (fun X Y => C(X, Y))

Full source

instance : ConcreteCategory.{u} TopCat (fun X Y => C(X, Y)) where
  hom := Hom.hom'
  ofHom f := ⟨f⟩

Topological Spaces as a Concrete Category

Informal description

The category of topological spaces $\mathrm{TopCat}$ is a concrete category, where the objects are topological spaces and the morphisms between objects $X$ and $Y$ are the continuous maps $C(X, Y)$.

TopCat.Hom.hom abbrev

{X Y : TopCat.{u}} (f : Hom X Y)

Full source

/-- Turn a morphism in `TopCat` back into a `ContinuousMap`. -/
abbrev Hom.hom {X Y : TopCatTopCat.{u}} (f : Hom X Y) :=
  ConcreteCategory.hom (C := TopCat) f

Underlying Continuous Map of a Topological Morphism

Informal description

Given two topological spaces $X$ and $Y$ in the category $\mathrm{TopCat}$, and a morphism $f$ in $\mathrm{Hom}(X, Y)$, this function extracts the underlying continuous map $f \colon X \to Y$.

TopCat.ofHom abbrev

{X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : of X ⟶ of Y

Full source

/-- Typecheck a `ContinuousMap` as a morphism in `TopCat`. -/
abbrev ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : ofof X ⟶ of Y :=
  ConcreteCategory.ofHom (C := TopCat) f

Construction of Continuous Map as Morphism in Category of Topological Spaces

Informal description

Given two types $X$ and $Y$ equipped with topological space structures, and a continuous map $f : C(X, Y)$, the abbreviation `TopCat.ofHom f` constructs a morphism from `TopCat.of X` to `TopCat.of Y$ in the category of topological spaces.

TopCat.Hom.Simps.hom definition

(X Y : TopCat) (f : Hom X Y)

Full source

/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
def Hom.Simps.hom (X Y : TopCat) (f : Hom X Y) :=
  f.hom

Underlying continuous map of a topological morphism

Informal description

Given two topological spaces $ X $ and $ Y $ in the category $\mathrm{TopCat}$, and a morphism $ f $ in $\mathrm{Hom}(X, Y)$, this function extracts the underlying continuous map $ f \colon X \to Y $.

TopCat.hom_id theorem

{X : TopCat.{u}} : (𝟙 X : X ⟶ X).hom = ContinuousMap.id X

Full source

@[simp]
lemma hom_id {X : TopCatTopCat.{u}} : (𝟙 X : X ⟶ X).hom = ContinuousMap.id X := rfl

Identity Morphism's Underlying Map is Identity in $\mathrm{TopCat}$

Informal description

For any topological space $X$ in the category $\mathrm{TopCat}$, the underlying continuous map of the identity morphism $\mathrm{id}_X \colon X \to X$ is equal to the identity continuous map $\mathrm{id}_X$ on $X$.

TopCat.id_app theorem

(X : TopCat.{u}) (x : ↑X) : (𝟙 X : X ⟶ X) x = x

Full source

@[simp]
theorem id_app (X : TopCatTopCat.{u}) (x : ↑X) : (𝟙 X : X ⟶ X) x = x := rfl

Identity Morphism Acts as Identity on Points in Topological Spaces

Informal description

For any topological space $X$ in the category $\mathrm{TopCat}$ and any point $x \in X$, the identity morphism $\mathrm{id}_X$ evaluated at $x$ equals $x$, i.e., $\mathrm{id}_X(x) = x$.

TopCat.coe_id theorem

(X : TopCat.{u}) : (𝟙 X : X → X) = id

Full source

@[simp] theorem coe_id (X : TopCatTopCat.{u}) : (𝟙 X : X → X) = id := rfl

Identity Morphism as Identity Function in $\mathrm{TopCat}$

Informal description

For any topological space $X$ in the category $\mathrm{TopCat}$, the identity morphism $𝟙 X$ (as a function from $X$ to $X$) is equal to the identity function $\mathrm{id}$.

TopCat.hom_comp theorem

{X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).hom = g.hom.comp f.hom

Full source

@[simp]
lemma hom_comp {X Y Z : TopCatTopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).hom = g.hom.comp f.hom := rfl

Composition of Continuous Maps Preserves Underlying Functions

Informal description

For any topological spaces $X$, $Y$, and $Z$, and for any continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, the underlying continuous map of the composition $f \gg g$ is equal to the composition of the underlying continuous maps $g \circ f$.

TopCat.comp_app theorem

{X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g : X → Z) x = g (f x)

Full source

@[simp]
theorem comp_app {X Y Z : TopCatTopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g : X → Z) x = g (f x) := rfl

Evaluation of Composition of Continuous Maps

Informal description

For any topological spaces $X$, $Y$, and $Z$, and for any continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, the evaluation of the composition $f \gg g$ at a point $x \in X$ is equal to $g(f(x))$.

TopCat.coe_comp theorem

{X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : X → Z) = g ∘ f

Full source

@[simp] theorem coe_comp {X Y Z : TopCatTopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g : X → Z) = g ∘ f := rfl

Composition of Continuous Maps as Function Composition

Informal description

For any topological spaces $X$, $Y$, and $Z$ in the category $\mathrm{TopCat}$, and for any continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, the composition of $f$ and $g$ in the category $\mathrm{TopCat}$ (denoted $f \gg g$) is equal to the usual function composition $g \circ f$ when viewed as functions between the underlying sets.

TopCat.hom_ext theorem

{X Y : TopCat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g

Full source

@[ext]
lemma hom_ext {X Y : TopCat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g :=
  Hom.ext hf

Extensionality of Continuous Maps via Underlying Functions

Informal description

For any topological spaces $X$ and $Y$ in the category $\mathrm{TopCat}$, and for any continuous maps $f, g \colon X \to Y$, if the underlying functions of $f$ and $g$ are equal (i.e., $f.\mathrm{hom} = g.\mathrm{hom}$), then $f = g$ as morphisms in $\mathrm{TopCat}$.

TopCat.ext theorem

{X Y : TopCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g

Full source

@[ext]
lemma ext {X Y : TopCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
  ConcreteCategory.hom_ext _ _ w

Extensionality of Continuous Maps in Topological Spaces

Informal description

For any topological spaces $X$ and $Y$ in the category $\mathrm{TopCat}$, and for any continuous maps $f, g \colon X \to Y$, if $f(x) = g(x)$ for all $x \in X$, then $f = g$.

TopCat.hom_ofHom theorem

{X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : (ofHom f).hom = f

Full source

@[simp]
lemma hom_ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
  (ofHom f).hom = f := rfl

Underlying Map of Constructed Morphism in Topological Spaces

Informal description

For any types $X$ and $Y$ equipped with topological space structures, and any continuous map $f \colon C(X, Y)$, the underlying continuous map of the morphism `TopCat.ofHom f` in the category of topological spaces is equal to $f$.

TopCat.ofHom_hom theorem

{X Y : TopCat} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

Full source

@[simp]
lemma ofHom_hom {X Y : TopCat} (f : X ⟶ Y) :
    ofHom (Hom.hom f) = f := rfl

Equality of Continuous Map Construction and Original Morphism in $\mathrm{TopCat}$

Informal description

For any topological spaces $X$ and $Y$ in the category $\mathrm{TopCat}$ and any continuous map $f \colon X \to Y$, the construction of the morphism from the underlying continuous map of $f$ is equal to $f$ itself. That is, $\mathrm{ofHom}(\mathrm{Hom.hom}(f)) = f$.

TopCat.ofHom_id theorem

{X : Type u} [TopologicalSpace X] : ofHom (ContinuousMap.id X) = 𝟙 (of X)

Full source

@[simp]
lemma ofHom_id {X : Type u} [TopologicalSpace X] : ofHom (ContinuousMap.id X) = 𝟙 (of X) := rfl

Identity Continuous Map Corresponds to Identity Morphism in TopCat

Informal description

For any type $X$ equipped with a topological space structure, the continuous identity map on $X$ corresponds to the identity morphism in the category of topological spaces, i.e., $\mathrm{ofHom}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{TopCat.of}(X)}$.

TopCat.ofHom_comp theorem

 {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) :
  ofHom (g.comp f) = ofHom f ≫ ofHom g

Full source

@[simp]
lemma ofHom_comp {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    (f : C(X, Y)) (g : C(Y, Z)) :
    ofHom (g.comp f) = ofHomofHom f ≫ ofHom g :=
  rfl

Composition of Continuous Maps Corresponds to Composition of Morphisms in $\mathrm{TopCat}$

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y$ and $g \colon Y \to Z$ be continuous maps. Then the morphism in $\mathrm{TopCat}$ corresponding to the composition $g \circ f$ is equal to the composition of the morphisms corresponding to $f$ and $g$, i.e., $\mathrm{ofHom}(g \circ f) = \mathrm{ofHom}(f) \circ \mathrm{ofHom}(g)$.

TopCat.ofHom_apply theorem

{X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) : (ofHom f) x = f x

Full source

lemma ofHom_apply {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) :
    (ofHom f) x = f x := rfl

Morphism Application in Topological Category: $\mathrm{ofHom}\, f(x) = f(x)$

Informal description

For any topological spaces $X$ and $Y$ (as types with topological structures) and any continuous map $f \colon X \to Y$, the application of the morphism $\mathrm{ofHom}\, f$ (in the category of topological spaces) to a point $x \in X$ equals the application of $f$ to $x$, i.e., $(\mathrm{ofHom}\, f)(x) = f(x)$.

TopCat.hom_inv_id_apply theorem

{X Y : TopCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x

Full source

lemma hom_inv_id_apply {X Y : TopCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x := by
  simp

Inverse-Homomorphism Identity for Topological Space Isomorphisms

Informal description

For any isomorphism $f \colon X \to Y$ in the category of topological spaces and any point $x \in X$, the composition of the inverse morphism $f^{-1}$ with $f$ evaluated at $x$ returns $x$, i.e., $f^{-1}(f(x)) = x$.

TopCat.inv_hom_id_apply theorem

{X Y : TopCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y

Full source

lemma inv_hom_id_apply {X Y : TopCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y := by
  simp

Inverse-Homomorphism Identity for Topological Space Isomorphisms

Informal description

For any isomorphism $f \colon X \cong Y$ in the category of topological spaces and any point $y \in Y$, the composition of the morphisms $f$ and its inverse satisfies $f_{\text{hom}}(f_{\text{inv}}(y)) = y$.

TopCat.coe_of_of theorem

 {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {x} :
  @DFunLike.coe (TopCat.of X ⟶ TopCat.of Y) ((CategoryTheory.forget TopCat).obj (TopCat.of X))
      (fun _ ↦ (CategoryTheory.forget TopCat).obj (TopCat.of Y)) HasForget.instFunLike (ofHom f) x =
    @DFunLike.coe C(X, Y) X (fun _ ↦ Y) _ f x

Full source

/--
Replace a function coercion for a morphism `TopCat.of X ⟶ TopCat.of Y` with the definitionally
equal function coercion for a continuous map `C(X, Y)`.
-/
@[simp] theorem coe_of_of {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    {f : C(X, Y)} {x} :
    @DFunLike.coe (TopCat.ofTopCat.of X ⟶ TopCat.of Y) ((CategoryTheory.forget TopCat).obj (TopCat.of X))
      (fun _ ↦ (CategoryTheory.forget TopCat).obj (TopCat.of Y)) HasForget.instFunLike
      (ofHom f) x =
    @DFunLike.coe C(X, Y) X
      (fun _ ↦ Y) _
      f x :=
  rfl

Equality of Function Coercions for Continuous Maps in $\mathrm{TopCat}$

Informal description

For any types $X$ and $Y$ equipped with topological space structures, and any continuous map $f \colon C(X, Y)$, the evaluation of the morphism $\mathrm{TopCat.ofHom}\, f$ at a point $x \in X$ is equal to the evaluation of $f$ at $x$. In other words, the coercion of the morphism $\mathrm{TopCat.ofHom}\, f$ to a function coincides with the coercion of $f$ itself.

TopCat.inhabited instance

: Inhabited TopCat

Full source

instance inhabited : Inhabited TopCat :=
  ⟨TopCat.of Empty⟩

The Category of Topological Spaces is Inhabited

Informal description

The category of topological spaces `TopCat` is inhabited.

TopCat.hom_apply theorem

{X Y : TopCat} (f : X ⟶ Y) (x : X) : f x = ContinuousMap.toFun f.hom x

Full source

@[deprecated
  "Simply remove this from the `simp`/`rw` set: the LHS and RHS are now identical."
  (since := "2025-01-30")]
lemma hom_apply {X Y : TopCat} (f : X ⟶ Y) (x : X) : f x = ContinuousMap.toFun f.hom x := rfl

Evaluation of Morphisms in the Category of Topological Spaces

Informal description

For any topological spaces $X$ and $Y$ in the category $\mathrm{TopCat}$, given a morphism $f \colon X \to Y$ and a point $x \in X$, the evaluation of $f$ at $x$ equals the evaluation of the underlying continuous map of $f$ at $x$. That is, $f(x) = f_{\text{hom}}(x)$, where $f_{\text{hom}}$ is the continuous map associated with $f$.

TopCat.discrete definition

: Type u ⥤ TopCat.{u}

Full source

/-- The discrete topology on any type. -/
def discrete : Type u ⥤ TopCat.{u} where
  obj X := @of X ⊥
  map f := @ofHom _ _ ⊥ ⊥ <| @ContinuousMap.mk _ _ ⊥ ⊥ f continuous_bot

Discrete topology functor

Informal description

The functor that equips any type $X$ with the discrete topology, where every subset of $X$ is open, and maps any function $f$ between types to the corresponding continuous map between the discrete topological spaces.

TopCat.instDiscreteTopologyCarrierObjDiscrete instance

{X : Type u} : DiscreteTopology (discrete.obj X)

Full source

instance {X : Type u} : DiscreteTopology (discrete.obj X) :=
  ⟨rfl⟩

Discrete Topology on Types via the Discrete Functor

Informal description

For any type $X$, the topological space obtained by equipping $X$ with the discrete topology (where every subset is open) is indeed a discrete topological space.

TopCat.trivial definition

: Type u ⥤ TopCat.{u}

Full source

/-- The trivial topology on any type. -/
def trivial : Type u ⥤ TopCat.{u} where
  obj X := @of X ⊤
  map f := @ofHom _ _ ⊤ ⊤ <| @ContinuousMap.mk _ _ ⊤ ⊤ f continuous_top

Trivial topology functor

Informal description

The functor that equips any type $X$ with the trivial topology (where only the empty set and $X$ itself are open), and maps any function $f$ between types to the corresponding continuous map between the trivially topologized spaces.

TopCat.isoOfHomeo definition

{X Y : TopCat.{u}} (f : X ≃ₜ Y) : X ≅ Y

Full source

/-- Any homeomorphisms induces an isomorphism in `Top`. -/
@[simps]
def isoOfHomeo {X Y : TopCatTopCat.{u}} (f : X ≃ₜ Y) : X ≅ Y where
  hom := ofHom f
  inv := ofHom f.symm

Isomorphism from homeomorphism in topological spaces

Informal description

Given a homeomorphism $f : X \simeq Y$ between topological spaces $X$ and $Y$, this function constructs an isomorphism $X \cong Y$ in the category of topological spaces, where: - The forward morphism is the continuous map $f$ - The inverse morphism is the continuous inverse map $f^{-1}$

TopCat.homeoOfIso definition

{X Y : TopCat.{u}} (f : X ≅ Y) : X ≃ₜ Y

Full source

/-- Any isomorphism in `Top` induces a homeomorphism. -/
@[simps]
def homeoOfIso {X Y : TopCatTopCat.{u}} (f : X ≅ Y) : X ≃ₜ Y where
  toFun := f.hom
  invFun := f.inv
  left_inv x := by simp
  right_inv x := by simp
  continuous_toFun := f.hom.hom.continuous
  continuous_invFun := f.inv.hom.continuous

Homeomorphism from topological space isomorphism

Informal description

Given an isomorphism $f : X \cong Y$ in the category of topological spaces, this function constructs a homeomorphism $X \simeq Y$ where: - The forward map is the morphism component of $f$ - The inverse map is the inverse morphism component of $f$ - Both maps are continuous (as required by the topological space category structure)

TopCat.of_isoOfHomeo theorem

{X Y : TopCat.{u}} (f : X ≃ₜ Y) : homeoOfIso (isoOfHomeo f) = f

Full source

@[simp]
theorem of_isoOfHomeo {X Y : TopCatTopCat.{u}} (f : X ≃ₜ Y) : homeoOfIso (isoOfHomeo f) = f := by
  ext
  rfl

Identity of Homeomorphism Construction via Isomorphism

Informal description

For any homeomorphism $f \colon X \simeq Y$ between topological spaces $X$ and $Y$, the composition of the functors `isoOfHomeo` and `homeoOfIso` applied to $f$ yields $f$ itself, i.e., $\text{homeoOfIso}(\text{isoOfHomeo}(f)) = f$.

TopCat.of_homeoOfIso theorem

{X Y : TopCat.{u}} (f : X ≅ Y) : isoOfHomeo (homeoOfIso f) = f

Full source

@[simp]
theorem of_homeoOfIso {X Y : TopCatTopCat.{u}} (f : X ≅ Y) : isoOfHomeo (homeoOfIso f) = f := by
  ext
  rfl

Isomorphism-Homeomorphism Roundtrip Identity in Topological Spaces

Informal description

For any isomorphism $f \colon X \cong Y$ in the category of topological spaces, the composition of the functors `isoOfHomeo` and `homeoOfIso` applied to $f$ yields $f$ itself, i.e., $\text{isoOfHomeo}(\text{homeoOfIso}(f)) = f$.

TopCat.isIso_of_bijective_of_isOpenMap theorem

{X Y : TopCat.{u}} (f : X ⟶ Y) (hfbij : Function.Bijective f) (hfcl : IsOpenMap f) : IsIso f

Full source

lemma isIso_of_bijective_of_isOpenMap {X Y : TopCatTopCat.{u}} (f : X ⟶ Y)
    (hfbij : Function.Bijective f) (hfcl : IsOpenMap f) : IsIso f :=
  let e : X ≃ₜ Y :=
    (Equiv.ofBijective f hfbij).toHomeomorphOfContinuousOpen f.hom.continuous hfcl
  inferInstanceAs <| IsIso (TopCat.isoOfHomeo e).hom

Bijective Open Continuous Maps are Isomorphisms in TopCat

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be a continuous map. If $f$ is bijective and an open map, then $f$ is an isomorphism in the category of topological spaces.

TopCat.isIso_of_bijective_of_isClosedMap theorem

{X Y : TopCat.{u}} (f : X ⟶ Y) (hfbij : Function.Bijective f) (hfcl : IsClosedMap f) : IsIso f

Full source

lemma isIso_of_bijective_of_isClosedMap {X Y : TopCatTopCat.{u}} (f : X ⟶ Y)
    (hfbij : Function.Bijective f) (hfcl : IsClosedMap f) : IsIso f :=
  let e : X ≃ₜ Y :=
    (Equiv.ofBijective f hfbij).toHomeomorphOfContinuousClosed f.hom.continuous hfcl
  inferInstanceAs <| IsIso (TopCat.isoOfHomeo e).hom

Bijective Closed Continuous Maps are Isomorphisms in TopCat

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be a continuous map. If $f$ is bijective and a closed map, then $f$ is an isomorphism in the category of topological spaces.

TopCat.isOpenEmbedding_iff_comp_isIso theorem

{X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : IsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding f

Full source

theorem isOpenEmbedding_iff_comp_isIso {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] :
    IsOpenEmbeddingIsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding f :=
  (TopCat.homeoOfIso (asIso g)).isOpenEmbedding.of_comp_iff f

Open embedding property under composition with isomorphism in topological spaces

Informal description

For topological spaces $X$, $Y$, and $Z$, a continuous map $f \colon X \to Y$, and an isomorphism $g \colon Y \to Z$ in the category of topological spaces, the composition $f \circ g$ is an open embedding if and only if $f$ is an open embedding.

TopCat.isOpenEmbedding_iff_comp_isIso' theorem

{X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Full source

@[simp]
theorem isOpenEmbedding_iff_comp_isIso' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] :
    IsOpenEmbeddingIsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f := by
  simp only [← Functor.map_comp]
  exact isOpenEmbedding_iff_comp_isIso f g

Open Embedding Property under Precomposition with Isomorphism in Topological Spaces

Informal description

For topological spaces $X$, $Y$, and $Z$, a continuous map $f \colon X \to Y$, and an isomorphism $g \colon Y \to Z$ in the category of topological spaces, the composition $g \circ f$ is an open embedding if and only if $f$ is an open embedding.

TopCat.isOpenEmbedding_iff_isIso_comp theorem

{X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : IsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding g

Full source

theorem isOpenEmbedding_iff_isIso_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
    IsOpenEmbeddingIsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding g := by
  constructor
  · intro h
    convert h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding
    exact congr_arg (DFunLike.coeDFunLike.coe ∘ ConcreteCategory.hom) (IsIso.inv_hom_id_assoc f g).symm
  · exact fun h => h.comp (TopCat.homeoOfIso (asIso f)).isOpenEmbedding

Open Embedding of Composition with Isomorphism

Informal description

For topological spaces $X, Y, Z$ and continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, if $f$ is an isomorphism, then the composition $f \circ g$ is an open embedding if and only if $g$ is an open embedding.

TopCat.isOpenEmbedding_iff_isIso_comp' theorem

{X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding g

Full source

@[simp]
theorem isOpenEmbedding_iff_isIso_comp' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
    IsOpenEmbeddingIsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding g := by
  simp only [← Functor.map_comp]
  exact isOpenEmbedding_iff_isIso_comp f g

Open Embedding of Composition with Isomorphism (Variant)

Informal description

For topological spaces $X, Y, Z$ and continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, if $f$ is an isomorphism, then the composition $g \circ f$ is an open embedding if and only if $g$ is an open embedding.