Mathlib.Topology.Bornology.Hom

LocallyBoundedMap structure

(α β : Type*) [Bornology α] [Bornology β]

Full source

/-- The type of bounded maps from `α` to `β`, the maps which send a bounded set to a bounded set. -/
structure LocallyBoundedMap (α β : Type*) [Bornology α] [Bornology β] where
  /-- 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' : (cobounded β).comap toFun ≤ cobounded α

Locally bounded map

Informal description

A locally bounded map between two types `α` and `β` equipped with bornologies is a function that sends every bounded subset of `α` to a bounded subset of `β`.

LocallyBoundedMapClass structure

(F : Type*) (α β : outParam Type*) [Bornology α] [Bornology β] [FunLike F α β]

Full source

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

You should extend this class when you extend `LocallyBoundedMap`. -/
class LocallyBoundedMapClass (F : Type*) (α β : outParam Type*) [Bornology α]
    [Bornology β] [FunLike F α β] : Prop where
  /-- 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) : (cobounded β).comap f ≤ cobounded α

Class of Locally Bounded Maps

Informal description

The class `LocallyBoundedMapClass F α β` states that terms of type `F` represent locally bounded maps between types `α` and `β` equipped with bornologies. A locally bounded map is a function that preserves boundedness, meaning it maps every bounded subset of `α` to a bounded subset of `β`. This class extends `FunLike F α β`, ensuring that terms of type `F` can be coerced to functions from `α` to `β`.

Bornology.IsBounded.image theorem

 [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (f : F) {s : Set α} (hs : IsBounded s) : IsBounded (f '' s)

Full source

theorem Bornology.IsBounded.image [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (f : F)
    {s : Set α} (hs : IsBounded s) : IsBounded (f '' s) :=
  comap_cobounded_le_iff.1 (comap_cobounded_le f) hs

Image of Bounded Set under Locally Bounded Map is Bounded

Informal description

Let $\alpha$ and $\beta$ be types equipped with bornologies, and let $F$ be a type representing locally bounded maps from $\alpha$ to $\beta$. For any locally bounded map $f \colon \alpha \to \beta$ and any bounded subset $s \subseteq \alpha$, the image $f(s) \subseteq \beta$ is also bounded.

LocallyBoundedMapClass.toLocallyBoundedMap definition

[Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (f : F) : LocallyBoundedMap α β

Full source

/-- 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 α β`. -/
@[coe]
def LocallyBoundedMapClass.toLocallyBoundedMap [Bornology α] [Bornology β]
    [LocallyBoundedMapClass F α β] (f : F) : LocallyBoundedMap α β where
  toFun := f
  comap_cobounded_le' := comap_cobounded_le f

Conversion from locally bounded map class to locally bounded map

Informal description

Given types $\alpha$ and $\beta$ equipped with bornologies, and a type $F$ representing locally bounded maps from $\alpha$ to $\beta$, the function `LocallyBoundedMapClass.toLocallyBoundedMap` converts an element $f$ of $F$ into an actual locally bounded map. This map preserves boundedness, meaning it sends every bounded subset of $\alpha$ to a bounded subset of $\beta$.

instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass instance

[Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] : CoeTC F (LocallyBoundedMap α β)

Full source

instance [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] :
    CoeTC F (LocallyBoundedMap α β) :=
  ⟨fun f => ⟨f, comap_cobounded_le f⟩⟩

Canonical Coercion from Locally Bounded Map Class to Locally Bounded Maps

Informal description

For any types $\alpha$ and $\beta$ equipped with bornologies, and any type $F$ representing locally bounded maps from $\alpha$ to $\beta$, there is a canonical coercion from $F$ to the type of locally bounded maps $\text{LocallyBoundedMap} \alpha \beta$.

LocallyBoundedMap.instFunLike instance

: FunLike (LocallyBoundedMap α β) α β

Full source

instance : FunLike (LocallyBoundedMap α β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr

Function-Like Structure of Locally Bounded Maps

Informal description

For any types $\alpha$ and $\beta$ equipped with bornologies, the type of locally bounded maps from $\alpha$ to $\beta$ has a function-like structure, meaning each locally bounded map can be treated as a function from $\alpha$ to $\beta$ with an injective coercion.

LocallyBoundedMap.instLocallyBoundedMapClass instance

: LocallyBoundedMapClass (LocallyBoundedMap α β) α β

Full source

instance : LocallyBoundedMapClass (LocallyBoundedMap α β) α β where
  comap_cobounded_le f := f.comap_cobounded_le'

Locally Bounded Maps as Locally Bounded Map Class

Informal description

For any types $\alpha$ and $\beta$ equipped with bornologies, the type of locally bounded maps from $\alpha$ to $\beta$ is an instance of the class `LocallyBoundedMapClass`. This means that every locally bounded map preserves boundedness, sending bounded subsets of $\alpha$ to bounded subsets of $\beta$.

LocallyBoundedMap.ext theorem

{f g : LocallyBoundedMap α β} (h : ∀ a, f a = g a) : f = g

Full source

@[ext]
theorem ext {f g : LocallyBoundedMap α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

Extensionality of Locally Bounded Maps

Informal description

For any two locally bounded maps $f, g$ between types $\alpha$ and $\beta$ equipped with bornologies, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.

LocallyBoundedMap.copy definition

(f : LocallyBoundedMap α β) (f' : α → β) (h : f' = f) : LocallyBoundedMap α β

Full source

/-- Copy of a `LocallyBoundedMap` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = f) : LocallyBoundedMap α β :=
  ⟨f', h.symm ▸ f.comap_cobounded_le'⟩

Copy of a locally bounded map with a new function

Informal description

Given a locally bounded map $f$ between types $\alpha$ and $\beta$ equipped with bornologies, and a function $f'$ equal to $f$, this constructs a new locally bounded map with the function $f'$ that preserves the property of sending bounded subsets to bounded subsets.

LocallyBoundedMap.coe_copy theorem

(f : LocallyBoundedMap α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Locally Bounded Map Equals Original Function

Informal description

Let $f$ be a locally bounded map between types $\alpha$ and $\beta$ equipped with bornologies, and let $f'$ be a function from $\alpha$ to $\beta$ such that $f' = f$. Then the underlying function of the copy of $f$ with $f'$ is equal to $f'$.

LocallyBoundedMap.copy_eq theorem

(f : LocallyBoundedMap α β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : LocallyBoundedMap α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Locally Bounded Map Equals Original

Informal description

Given a locally bounded map $f$ between types $\alpha$ and $\beta$ equipped with bornologies, and a function $f'$ equal to $f$, the copy of $f$ with $f'$ is equal to $f$ itself.

LocallyBoundedMap.ofMapBounded definition

(f : α → β) (h : ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)) : LocallyBoundedMap α β

Full source

/-- Construct a `LocallyBoundedMap` from the fact that the function maps bounded sets to bounded
sets. -/
def ofMapBounded (f : α → β) (h : ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)) :
    LocallyBoundedMap α β :=
  ⟨f, comap_cobounded_le_iff.2 h⟩

Locally bounded map from a boundedness-preserving function

Informal description

Given a function $f : \alpha \to \beta$ between types equipped with bornologies, if $f$ maps every bounded subset $s \subseteq \alpha$ to a bounded subset $f(s) \subseteq \beta$, then $f$ can be promoted to a locally bounded map from $\alpha$ to $\beta$.

LocallyBoundedMap.coe_ofMapBounded theorem

(f : α → β) {h} : ⇑(ofMapBounded f h) = f

Full source

@[simp]
theorem coe_ofMapBounded (f : α → β) {h} : ⇑(ofMapBounded f h) = f :=
  rfl

Coercion of Locally Bounded Map Construction Equals Original Function

Informal description

For any function $f \colon \alpha \to \beta$ between types equipped with bornologies, if $f$ satisfies the condition that it maps every bounded subset of $\alpha$ to a bounded subset of $\beta$, then the coercion of the locally bounded map constructed from $f$ (via `ofMapBounded`) is equal to $f$ itself.

LocallyBoundedMap.ofMapBounded_apply theorem

(f : α → β) {h} (a : α) : ofMapBounded f h a = f a

Full source

@[simp]
theorem ofMapBounded_apply (f : α → β) {h} (a : α) : ofMapBounded f h a = f a :=
  rfl

Pointwise Agreement of Locally Bounded Map Construction

Informal description

For any function $f \colon \alpha \to \beta$ between types equipped with bornologies, if $f$ preserves boundedness (i.e., maps bounded subsets of $\alpha$ to bounded subsets of $\beta$), then the locally bounded map constructed from $f$ via `ofMapBounded` agrees with $f$ pointwise. That is, for any $a \in \alpha$, we have $\text{ofMapBounded}\,f\,h\,a = f\,a$.

LocallyBoundedMap.id definition

: LocallyBoundedMap α α

Full source

/-- `id` as a `LocallyBoundedMap`. -/
protected def id : LocallyBoundedMap α α :=
  ⟨id, comap_id.le⟩

Identity as a locally bounded map

Informal description

The identity function on a type $\alpha$ equipped with a bornology is a locally bounded map, i.e., it preserves boundedness of subsets.

LocallyBoundedMap.instInhabited instance

: Inhabited (LocallyBoundedMap α α)

Full source

instance : Inhabited (LocallyBoundedMap α α) :=
  ⟨LocallyBoundedMap.id α⟩

Inhabitedness of Locally Bounded Maps on a Bornology

Informal description

For any type $\alpha$ equipped with a bornology, the type of locally bounded maps from $\alpha$ to itself is inhabited, meaning there exists at least one such map (specifically, the identity map).

LocallyBoundedMap.coe_id theorem

: ⇑(LocallyBoundedMap.id α) = id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(LocallyBoundedMap.id α) = id :=
  rfl

Identity Locally Bounded Map Coincides with Identity Function

Informal description

The canonical function associated with the identity locally bounded map on a type $\alpha$ equipped with a bornology is equal to the identity function on $\alpha$, i.e., $\text{id}_{\alpha} = \text{id}$.

LocallyBoundedMap.id_apply theorem

(a : α) : LocallyBoundedMap.id α a = a

Full source

@[simp]
theorem id_apply (a : α) : LocallyBoundedMap.id α a = a :=
  rfl

Identity Locally Bounded Map Evaluation

Informal description

For any element $a$ in a type $\alpha$ equipped with a bornology, the identity locally bounded map evaluated at $a$ equals $a$, i.e., $\text{id}(a) = a$.

LocallyBoundedMap.comp definition

(f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) : LocallyBoundedMap α γ

Full source

/-- Composition of `LocallyBoundedMap`s as a `LocallyBoundedMap`. -/
def comp (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) : LocallyBoundedMap α γ where
  toFun := f ∘ g
  comap_cobounded_le' :=
    comap_comap.ge.trans <| (comap_mono f.comap_cobounded_le').trans g.comap_cobounded_le'

Composition of locally bounded maps

Informal description

Given locally bounded maps $ f \colon \beta \to \gamma $ and $ g \colon \alpha \to \beta $, their composition $ f \circ g \colon \alpha \to \gamma $ is also a locally bounded map. This means that the composition preserves boundedness, i.e., if a subset $ S \subseteq \alpha $ is bounded, then $ f(g(S)) \subseteq \gamma $ is bounded.

LocallyBoundedMap.coe_comp theorem

(f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) : ⇑(f.comp g) = f ∘ g

Full source

@[simp]
theorem coe_comp (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) : ⇑(f.comp g) = f ∘ g :=
  rfl

Composition of Underlying Functions for Locally Bounded Maps

Informal description

For any locally bounded maps $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying function of their composition $f \circ g$ is equal to the composition of the underlying functions of $f$ and $g$.

LocallyBoundedMap.comp_apply theorem

(f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) (a : α) : f.comp g a = f (g a)

Full source

@[simp]
theorem comp_apply (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) (a : α) :
    f.comp g a = f (g a) :=
  rfl

Evaluation of Composition of Locally Bounded Maps

Informal description

For any locally bounded maps $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and any element $a \in \alpha$, the evaluation of the composition $f \circ g$ at $a$ equals the evaluation of $f$ at $g(a)$, i.e., $(f \circ g)(a) = f(g(a))$.

LocallyBoundedMap.comp_assoc theorem

 (f : LocallyBoundedMap γ δ) (g : LocallyBoundedMap β γ) (h : LocallyBoundedMap α β) :
  (f.comp g).comp h = f.comp (g.comp h)

Full source

@[simp]
theorem comp_assoc (f : LocallyBoundedMap γ δ) (g : LocallyBoundedMap β γ)
    (h : LocallyBoundedMap α β) : (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Locally Bounded Maps

Informal description

For any locally bounded maps $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of maps satisfies the associativity property $(f \circ g) \circ h = f \circ (g \circ h)$.

LocallyBoundedMap.comp_id theorem

(f : LocallyBoundedMap α β) : f.comp (LocallyBoundedMap.id α) = f

Full source

@[simp]
theorem comp_id (f : LocallyBoundedMap α β) : f.comp (LocallyBoundedMap.id α) = f :=
  ext fun _ => rfl

Right Identity Property of Locally Bounded Map Composition

Informal description

For any locally bounded map $f \colon \alpha \to \beta$ between types equipped with bornologies, the composition of $f$ with the identity locally bounded map on $\alpha$ equals $f$, i.e., $f \circ \text{id}_\alpha = f$.

LocallyBoundedMap.id_comp theorem

(f : LocallyBoundedMap α β) : (LocallyBoundedMap.id β).comp f = f

Full source

@[simp]
theorem id_comp (f : LocallyBoundedMap α β) : (LocallyBoundedMap.id β).comp f = f :=
  ext fun _ => rfl

Right Identity Property for Composition of Locally Bounded Maps

Informal description

For any locally bounded map $f \colon \alpha \to \beta$ between types equipped with bornologies, the composition of the identity map on $\beta$ with $f$ equals $f$, i.e., $\text{id}_\beta \circ f = f$.

LocallyBoundedMap.cancel_right theorem

 {g₁ g₂ : LocallyBoundedMap β γ} {f : LocallyBoundedMap α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : LocallyBoundedMap β γ} {f : LocallyBoundedMap α β}
    (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congrArg (comp · _)⟩

Right Cancellation Property for Composition of Locally Bounded Maps

Informal description

Let $f \colon \alpha \to \beta$ be a surjective locally bounded map between types equipped with bornologies, and let $g_1, g_2 \colon \beta \to \gamma$ be locally bounded maps. Then the composition $g_1 \circ f$ equals $g_2 \circ f$ if and only if $g_1 = g_2$.

LocallyBoundedMap.cancel_left theorem

 {g : LocallyBoundedMap β γ} {f₁ f₂ : LocallyBoundedMap α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : LocallyBoundedMap β γ} {f₁ f₂ : LocallyBoundedMap α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Left Cancellation Property for Composition of Locally Bounded Maps

Informal description

Let $g \colon \beta \to \gamma$ be an injective locally bounded map, and let $f_1, f_2 \colon \alpha \to \beta$ be locally bounded maps. Then the composition $g \circ f_1$ equals $g \circ f_2$ if and only if $f_1 = f_2$.

Mathlib.Topology.Bornology.Hom

Types of morphisms

Typeclasses