Cocompact continuous maps

The type of cocompact continuous maps are those which tend to the cocompact filter on the codomain along the cocompact filter on the domain. When the domain and codomain are Hausdorff, this is equivalent to many other conditions, including that preimages of compact sets are compact.

Cocompact continuous maps

structure CocompactMap (α : Type u) (β : Type v) [TopologicalSpace α] [TopologicalSpace β] extends C(α, β) : Type (max u v)

A cocompact continuous map is a continuous function between topological spaces which tends to the cocompact filter along the cocompact filter. Functions for which preimages of compact sets are compact always satisfy this property, and the converse holds for cocompact continuous maps when the codomain is Hausdorff (see CocompactMap.tendsto_of_forall_preimage and CocompactMap.isCompact_preimage).

Cocompact maps thus generalise proper maps, with which they correspond when the codomain is Hausdorff.

• toFun : α → β
• continuous_toFun : Continuous self.toFun
• cocompact_tendsto' : Filter.Tendsto self.toFun (Filter.cocompact α) (Filter.cocompact β)

  The cocompact filter on α tends to the cocompact filter on β under the function

class CocompactMapClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass F α β : Prop

CocompactMapClass F α β states that F is a type of cocompact continuous maps.

You should also extend this typeclass when you extend CocompactMap.

• map_continuous : ∀ (f : F), Continuous ⇑f
• cocompact_tendsto : ∀ (f : F), Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)

  The cocompact filter on α tends to the cocompact filter on β under the function

def CocompactMapClass.toCocompactMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [CocompactMapClass F α β] (f : F) : CocompactMap α β

Turn an element of a type F satisfying CocompactMapClass F α β into an actual CocompactMap. This is declared as the default coercion from F to CocompactMap α β.

Equations

• ↑f = { toContinuousMap := ↑f, cocompact_tendsto' := ⋯ }

instance CocompactMapClass.instCoeTCCocompactMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [CocompactMapClass F α β] : CoeTC F (CocompactMap α β)

Equations

• CocompactMapClass.instCoeTCCocompactMap = { coe := CocompactMapClass.toCocompactMap }

instance CocompactMap.instFunLike {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : FunLike (CocompactMap α β) α β

Equations

• CocompactMap.instFunLike = { coe := fun (f : CocompactMap α β) => f.toFun, coe_injective' := ⋯ }

instance CocompactMap.instCocompactMapClass {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : CocompactMapClass (CocompactMap α β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem CocompactMap.coe_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : CocompactMap α β} : ⇑f.toContinuousMap = ⇑f

theorem CocompactMap.ext {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : CocompactMap α β} (h : ∀ (x : α), f x = g x) : f = g

def CocompactMap.copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : CocompactMap α β) (f' : α → β) (h : f' = ⇑f) : CocompactMap α β

Copy of a CocompactMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toFun := f', continuous_toFun := ⋯, cocompact_tendsto' := ⋯ }

@[simp]

theorem CocompactMap.coe_copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : CocompactMap α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem CocompactMap.copy_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : CocompactMap α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

@[simp]

theorem CocompactMap.coe_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (h : Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)) : ⇑{ toContinuousMap := f, cocompact_tendsto' := h } = ⇑f

def CocompactMap.id (α : Type u_1) [TopologicalSpace α] : CocompactMap α α

The identity as a cocompact continuous map.

Equations

• CocompactMap.id α = { toContinuousMap := ContinuousMap.id α, cocompact_tendsto' := ⋯ }

@[simp]

theorem CocompactMap.coe_id (α : Type u_1) [TopologicalSpace α] : ⇑(CocompactMap.id α) = id

instance CocompactMap.instInhabited {α : Type u_1} [TopologicalSpace α] : Inhabited (CocompactMap α α)

Equations

• CocompactMap.instInhabited = { default := CocompactMap.id α }

def CocompactMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : CocompactMap β γ) (g : CocompactMap α β) : CocompactMap α γ

The composition of cocompact continuous maps, as a cocompact continuous map.

Equations

• f.comp g = { toContinuousMap := f.comp ↑g, cocompact_tendsto' := ⋯ }

@[simp]

theorem CocompactMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : CocompactMap β γ) (g : CocompactMap α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem CocompactMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : CocompactMap β γ) (g : CocompactMap α β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem CocompactMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (f : CocompactMap γ δ) (g : CocompactMap β γ) (h : CocompactMap α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem CocompactMap.id_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : CocompactMap α β) : (CocompactMap.id β).comp f = f

@[simp]

theorem CocompactMap.comp_id {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : CocompactMap α β) : f.comp (CocompactMap.id α) = f

theorem CocompactMap.tendsto_of_forall_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)) : Filter.Tendsto f (Filter.cocompact α) (Filter.cocompact β)

theorem CocompactMap.isCompact_preimage_of_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : CocompactMap α β) ⦃s : Set β⦄ (hs : IsCompact s) (h's : IsClosed s) : IsCompact (⇑f ⁻¹' s)

Preimages of compact closed sets are compact under a cocompact continuous map.

theorem CocompactMap.isCompact_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] (f : CocompactMap α β) ⦃s : Set β⦄ (hs : IsCompact s) : IsCompact (⇑f ⁻¹' s)

If the codomain is Hausdorff, preimages of compact sets are compact under a cocompact continuous map.

def Homeomorph.toCocompactMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : CocompactMap α β

A homeomorphism is a cocompact map.

Equations

• f.toCocompactMap = { toFun := ⇑f, continuous_toFun := ⋯, cocompact_tendsto' := ⋯ }

@[simp]

theorem Homeomorph.toCocompactMap_toFun {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) (a : α) : f.toCocompactMap a = f a