Base changes among different families of neighbourhoods

This file builds base changes for .compactsInside, openNhds.

It also contains the evidences that openRcNhds_to_openNhdsand openRcNhds_to_compactNhds are initials functors.

def TopologicalSpace.Opens.baseChangeCompactsInside {α : Type u_1} [TopologicalSpace α] {U V : Opens α} (h : U ⟶ V) : ↑U.compactsInside → ↑V.compactsInside

For U an open subset included in a open subset V, there is a map sending compacts inside U to the ones inside V

Equations

• TopologicalSpace.Opens.baseChangeCompactsInside h ⟨K, hK⟩ = ⟨K, ⋯⟩

theorem TopologicalSpace.Opens.baseChangeCompactsInside_mono {α : Type u_1} [TopologicalSpace α] {U V : Opens α} (h : U ⟶ V) : Monotone (baseChangeCompactsInside h)

@[simp]

theorem TopologicalSpace.Opens.baseChangeCompactsInside_comp {α : Type u_1} [TopologicalSpace α] {U V W : Opens α} (h : U ⟶ V) (k : V ⟶ W) (K : ↑U.compactsInside) : baseChangeCompactsInside (CategoryTheory.CategoryStruct.comp h k) K = baseChangeCompactsInside k (baseChangeCompactsInside h K)

@[simp]

theorem TopologicalSpace.Opens.baseChangeOpenNhds_id {α : Type u_1} [TopologicalSpace α] {U : Opens α} (K : ↑U.compactsInside) : baseChangeCompactsInside (CategoryTheory.CategoryStruct.id U) K = K

def TopologicalSpace.Compacts.baseChangeOpenNhds {α : Type u_1} [TopologicalSpace α] {K L : Compacts α} (h : K ⟶ L) : ↑L.openNhds → ↑K.openNhds

For K a compact subset included in a compact subset L, there is a map sending open neighbourhoods of L to the ones of K

Equations

• TopologicalSpace.Compacts.baseChangeOpenNhds h ⟨U, hU⟩ = ⟨U, ⋯⟩

theorem TopologicalSpace.Compacts.baseChangeOpenNhds_mono {α : Type u_1} [TopologicalSpace α] {K L : Compacts α} (h : K ⟶ L) : Monotone (baseChangeOpenNhds h)

@[simp]

theorem TopologicalSpace.Compacts.baseChangeOpenNhds_comp {α : Type u_1} [TopologicalSpace α] {K L M : Compacts α} (h : K ⟶ L) (k : L ⟶ M) (U : ↑M.openNhds) : baseChangeOpenNhds (CategoryTheory.CategoryStruct.comp h k) U = baseChangeOpenNhds h (baseChangeOpenNhds k U)

@[simp]

theorem TopologicalSpace.Compacts.baseChangeOpenNhds_id {α : Type u_1} [TopologicalSpace α] {K : Compacts α} (U : ↑K.openNhds) : baseChangeOpenNhds (CategoryTheory.CategoryStruct.id K) U = U

def TopologicalSpace.Compacts.isInitialBotOpensOpenNhdsBot {α : Type u_1} [TopologicalSpace α] : CategoryTheory.Limits.IsInitial ⊥

The evidence that ⊥ is initial among the compact open neighbourhoods of ⊥

Equations

• TopologicalSpace.Compacts.isInitialBotOpensOpenNhdsBot = CategoryTheory.Limits.IsInitial.ofUniqueHom (fun (x : ↑⊥.openNhds) => CategoryTheory.homOfLE ⋯) ⋯

instance TopologicalSpace.Compacts.instInitialElemOpensOpenRcNhdsOpenNhdsFunctorOfT2SpaceOfLocallyCompactSpace {α : Type u_1} [TopologicalSpace α] {K : Compacts α} [T2Space α] [LocallyCompactSpace α] : ⋯.functor.Initial

instance TopologicalSpace.Compacts.instInitialElemOpensOpenRcNhdsCompactNhdsFunctorOfT2Space {α : Type u_1} [TopologicalSpace α] {K : Compacts α} [T2Space α] : ⋯.functor.Initial