Locally bounded maps

This file defines locally bounded maps between bornologies.

We use the FunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms

• LocallyBoundedMap: Locally bounded maps. Maps which preserve boundedness.

Typeclasses

• LocallyBoundedMapClass

ink

structure LocallyBoundedMap (α : Type u_1) (β : Type u_2) [inst : Bornology α] [inst : Bornology β] : Type (maxu_1u_2)

• The function underlying a locally bounded map

  toFun : α → β

• The pullback of the Bornology.cobounded filter under the function is contained in the cobounded filter. Equivalently, the function maps bounded sets to bounded sets.

  comap_cobounded_le' : Filter.comap toFun (Bornology.cobounded β) ≤ Bornology.cobounded α

The type of bounded maps from α to β, the maps which send a bounded set to a bounded set.

ink

class LocallyBoundedMapClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Bornology α] [inst : Bornology β] extends FunLike : Type (max(maxu_1u_2)u_3)

• The pullback of the Bornology.cobounded filter under the function is contained in the cobounded filter. Equivalently, the function maps bounded sets to bounded sets.

  comap_cobounded_le : ∀ (f : F), Filter.comap (↑f) (Bornology.cobounded β) ≤ Bornology.cobounded α

LocallyBoundedMapClass F α β states that F is a type of bounded maps.

You should extend this class when you extend LocallyBoundedMap.

ink

theorem IsBounded.image {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] [inst : LocallyBoundedMapClass F α β] {f : F} {s : Set α} (hs : Bornology.IsBounded s) : Bornology.IsBounded (↑f '' s)

ink

def LocallyBoundedMapClass.toLocallyBoundedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst : Bornology β] [inst : LocallyBoundedMapClass F α β] (f : F) : LocallyBoundedMap α β

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

Equations

• ↑f = { toFun := ↑f, comap_cobounded_le' := (_ : Filter.comap (↑f) (Bornology.cobounded β) ≤ Bornology.cobounded α) }

ink

instance instCoeTCLocallyBoundedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst : Bornology β] [inst : LocallyBoundedMapClass F α β] : CoeTC F (LocallyBoundedMap α β)

Equations

• instCoeTCLocallyBoundedMap = { coe := fun f => { toFun := ↑f, comap_cobounded_le' := (_ : Filter.comap (↑f) (Bornology.cobounded β) ≤ Bornology.cobounded α) } }

ink

instance LocallyBoundedMap.instLocallyBoundedMapClassLocallyBoundedMap {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] : LocallyBoundedMapClass (LocallyBoundedMap α β) α β

Equations

• One or more equations did not get rendered due to their size.

ink

theorem LocallyBoundedMap.ext {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] {f : LocallyBoundedMap α β} {g : LocallyBoundedMap α β} (h : ∀ (a : α), ↑f a = ↑g a) : f = g

ink

def LocallyBoundedMap.copy {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = ↑f) : LocallyBoundedMap α β

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

Equations

• LocallyBoundedMap.copy f f' h = { toFun := f', comap_cobounded_le' := (_ : Filter.comap f' (Bornology.cobounded β) ≤ Bornology.cobounded α) }

ink

@[simp]

theorem LocallyBoundedMap.coe_copy {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = ↑f) : ↑(LocallyBoundedMap.copy f f' h) = f'

ink

theorem LocallyBoundedMap.copy_eq {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = ↑f) : LocallyBoundedMap.copy f f' h = f

ink

def LocallyBoundedMap.ofMapBounded {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : α → β) (h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)) : LocallyBoundedMap α β

Construct a LocallyBoundedMap from the fact that the function maps bounded sets to bounded sets.

Equations

• LocallyBoundedMap.ofMapBounded f h = { toFun := f, comap_cobounded_le' := (_ : Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α) }

ink

@[simp]

theorem LocallyBoundedMap.coe_ofMapBounded {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : α → β) {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)} : ↑(LocallyBoundedMap.ofMapBounded f h) = f

ink

@[simp]

theorem LocallyBoundedMap.ofMapBounded_apply {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : α → β) {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)} (a : α) : ↑(LocallyBoundedMap.ofMapBounded f h) a = f a

ink

def LocallyBoundedMap.id (α : Type u_1) [inst : Bornology α] : LocallyBoundedMap α α

id as a LocallyBoundedMap.

Equations

• LocallyBoundedMap.id α = { toFun := id, comap_cobounded_le' := (_ : Filter.comap id (Bornology.cobounded α) ≤ Bornology.cobounded α) }

ink

instance LocallyBoundedMap.instInhabitedLocallyBoundedMap (α : Type u_1) [inst : Bornology α] : Inhabited (LocallyBoundedMap α α)

Equations

• LocallyBoundedMap.instInhabitedLocallyBoundedMap α = { default := LocallyBoundedMap.id α }

ink

@[simp]

theorem LocallyBoundedMap.coe_id (α : Type u_1) [inst : Bornology α] : ↑(LocallyBoundedMap.id α) = id

ink

@[simp]

theorem LocallyBoundedMap.id_apply {α : Type u_1} [inst : Bornology α] (a : α) : ↑(LocallyBoundedMap.id α) a = a

ink

def LocallyBoundedMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Bornology α] [inst : Bornology β] [inst : Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) : LocallyBoundedMap α γ

Composition of LocallyBoundedMaps as a LocallyBoundedMap.

Equations

• LocallyBoundedMap.comp f g = { toFun := ↑f ∘ ↑g, comap_cobounded_le' := (_ : Filter.comap (↑f ∘ ↑g) (Bornology.cobounded γ) ≤ Bornology.cobounded α) }

ink

@[simp]

theorem LocallyBoundedMap.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bornology α] [inst : Bornology β] [inst : Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) : ↑(LocallyBoundedMap.comp f g) = ↑f ∘ ↑g

ink

@[simp]

theorem LocallyBoundedMap.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bornology α] [inst : Bornology β] [inst : Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) (a : α) : ↑(LocallyBoundedMap.comp f g) a = ↑f (↑g a)

ink

@[simp]

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

ink

@[simp]

theorem LocallyBoundedMap.comp_id {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : LocallyBoundedMap α β) : LocallyBoundedMap.comp f (LocallyBoundedMap.id α) = f

ink

@[simp]

theorem LocallyBoundedMap.id_comp {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst : Bornology β] (f : LocallyBoundedMap α β) : LocallyBoundedMap.comp (LocallyBoundedMap.id β) f = f

ink

theorem LocallyBoundedMap.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bornology α] [inst : Bornology β] [inst : Bornology γ] {g₁ : LocallyBoundedMap β γ} {g₂ : LocallyBoundedMap β γ} {f : LocallyBoundedMap α β} (hf : Function.Surjective ↑f) : LocallyBoundedMap.comp g₁ f = LocallyBoundedMap.comp g₂ f ↔ g₁ = g₂

ink

theorem LocallyBoundedMap.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bornology α] [inst : Bornology β] [inst : Bornology γ] {g : LocallyBoundedMap β γ} {f₁ : LocallyBoundedMap α β} {f₂ : LocallyBoundedMap α β} (hg : Function.Injective ↑g) : LocallyBoundedMap.comp g f₁ = LocallyBoundedMap.comp g f₂ ↔ f₁ = f₂