mathlib3 documentation

topology.continuous_function.cocompact_map

Cocompact continuous maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
structure cocompact_map (α : Type u) (β : Type v) [topological_space α] [topological_space β] :
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 cocompact_map.tendsto_of_forall_preimage and cocompact_map.is_compact_preimage).

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

Instances for cocompact_map
source
@[class]
structure cocompact_map_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [topological_space α] [topological_space β] :
Type (max u_1 u_2 u_3)

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

You should also extend this typeclass when you extend cocompact_map.

Instances of this typeclass
Instances of other typeclasses for cocompact_map_class
  • cocompact_map_class.has_sizeof_inst
source
@[instance]
def cocompact_map_class.to_continuous_map_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [topological_space α] [topological_space β] [self : cocompact_map_class F α β] :
continuous_map_class F α β
source
@[protected, instance]
def cocompact_map_class.cocompact_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [cocompact_map_class F α β] :
has_coe_t F (cocompact_map α β)
Equations
source
@[protected, instance]
def cocompact_map.cocompact_map_class {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
cocompact_map_class (cocompact_map α β) α β
Equations
source
@[protected, instance]
def cocompact_map.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
has_coe_to_fun (cocompact_map α β) (λ (_x : cocompact_map α β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
@[simp]
theorem cocompact_map.coe_to_continuous_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : cocompact_map α β} :
⇑(f.to_continuous_map) = ⇑f
source
@[ext]
theorem cocompact_map.ext {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : cocompact_map α β} (h : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
source
@[protected]
def cocompact_map.copy {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : cocompact_map α β) (f' : α → β) (h : f' = ⇑f) :
cocompact_map α β

Copy of a cocompact_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[simp]
theorem cocompact_map.coe_copy {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : cocompact_map α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem cocompact_map.copy_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : cocompact_map α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[simp]
theorem cocompact_map.coe_mk {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) (h : filter.tendsto ⇑f (filter.cocompact α) (filter.cocompact β)) :
⇑{to_continuous_map := f, cocompact_tendsto' := h} = ⇑f
source
@[protected]
def cocompact_map.id (α : Type u_1) [topological_space α] :
cocompact_map α α

The identity as a cocompact continuous map.

Equations
source
@[simp]
theorem cocompact_map.coe_id (α : Type u_1) [topological_space α] :
⇑(cocompact_map.id α) = id
source
@[protected, instance]
def cocompact_map.inhabited {α : Type u_1} [topological_space α] :
inhabited (cocompact_map α α)
Equations
source
def cocompact_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : cocompact_map β γ) (g : cocompact_map α β) :
cocompact_map α γ

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

Equations
source
@[simp]
theorem cocompact_map.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : cocompact_map β γ) (g : cocompact_map α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem cocompact_map.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : cocompact_map β γ) (g : cocompact_map α β) (a : α) :
⇑(f.comp g) a = ⇑f (⇑g a)
source
@[simp]
theorem cocompact_map.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (f : cocompact_map γ δ) (g : cocompact_map β γ) (h : cocompact_map α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem cocompact_map.id_comp {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : cocompact_map α β) :
(cocompact_map.id β).comp f = f
source
@[simp]
theorem cocompact_map.comp_id {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : cocompact_map α β) :
f.comp (cocompact_map.id α) = f
source
theorem cocompact_map.tendsto_of_forall_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : ∀ (s : set β), is_compact s → is_compact (f ⁻¹' s)) :
filter.tendsto f (filter.cocompact α) (filter.cocompact β)
source
theorem cocompact_map.is_compact_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [t2_space β] (f : cocompact_map α β) ⦃s : set β⦄ (hs : is_compact s) :
is_compact (⇑f ⁻¹' s)

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

source
def homeomorph.to_cocompact_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
cocompact_map α β

A homemomorphism is a cocompact map.

Equations
source
@[simp]
theorem homeomorph.to_cocompact_map_to_continuous_map_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α ≃ₜ β) (ᾰ : α) :
⇑(f.to_cocompact_map.to_continuous_map) ᾰ = ⇑f ᾰ