Documentation

Mathlib.Topology.Bornology.Hom

Locally bounded maps #

This file defines locally bounded maps between bornologies.

We use the DFunLike 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 #

Typeclasses #

structure LocallyBoundedMap (α : Type u_6) (β : Type u_7) [Bornology α] [Bornology β] :
Type (max u_6 u_7)

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

Instances For

    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.

    class LocallyBoundedMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Bornology α] [Bornology β] [FunLike F α β] :

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

    You should extend this class when you extend LocallyBoundedMap.

    Instances
      theorem LocallyBoundedMapClass.comap_cobounded_le {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} :
      ∀ {inst : Bornology α} {inst_1 : Bornology β} {inst_2 : FunLike F α β} [self : LocallyBoundedMapClass F α β] (f : F), Filter.comap (⇑f) (Bornology.cobounded β) Bornology.cobounded α

      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.

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

      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' := }
      Instances For
        instance instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] :
        Equations
        • instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass = { coe := fun (f : F) => { toFun := f, comap_cobounded_le' := } }
        instance LocallyBoundedMap.instFunLike {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] :
        Equations
        • LocallyBoundedMap.instFunLike = { coe := fun (f : LocallyBoundedMap α β) => f.toFun, coe_injective' := }
        Equations
        • =
        theorem LocallyBoundedMap.ext_iff {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] {f : LocallyBoundedMap α β} {g : LocallyBoundedMap α β} :
        f = g ∀ (a : α), f a = g a
        theorem LocallyBoundedMap.ext {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] {f : LocallyBoundedMap α β} {g : LocallyBoundedMap α β} (h : ∀ (a : α), f a = g a) :
        f = g
        def LocallyBoundedMap.copy {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) (f' : αβ) (h : f' = f) :

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

        Equations
        • f.copy f' h = { toFun := f', comap_cobounded_le' := }
        Instances For
          @[simp]
          theorem LocallyBoundedMap.coe_copy {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) (f' : αβ) (h : f' = f) :
          (f.copy f' h) = f'
          theorem LocallyBoundedMap.copy_eq {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) (f' : αβ) (h : f' = f) :
          f.copy f' h = f
          def LocallyBoundedMap.ofMapBounded {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : αβ) (h : ∀ ⦃s : Set α⦄, Bornology.IsBounded sBornology.IsBounded (f '' s)) :

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

          Equations
          Instances For
            @[simp]
            theorem LocallyBoundedMap.coe_ofMapBounded {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : αβ) {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded sBornology.IsBounded (f '' s)} :
            @[simp]
            theorem LocallyBoundedMap.ofMapBounded_apply {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : αβ) {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded sBornology.IsBounded (f '' s)} (a : α) :

            id as a LocallyBoundedMap.

            Equations
            Instances For
              @[simp]
              theorem LocallyBoundedMap.coe_id (α : Type u_2) [Bornology α] :
              @[simp]
              theorem LocallyBoundedMap.id_apply {α : Type u_2} [Bornology α] (a : α) :
              def LocallyBoundedMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) :

              Composition of LocallyBoundedMaps as a LocallyBoundedMap.

              Equations
              • f.comp g = { toFun := f g, comap_cobounded_le' := }
              Instances For
                @[simp]
                theorem LocallyBoundedMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) :
                (f.comp g) = f g
                @[simp]
                theorem LocallyBoundedMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β) (a : α) :
                (f.comp g) a = f (g a)
                @[simp]
                theorem LocallyBoundedMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Bornology α] [Bornology β] [Bornology γ] [Bornology δ] (f : LocallyBoundedMap γ δ) (g : LocallyBoundedMap β γ) (h : LocallyBoundedMap α β) :
                (f.comp g).comp h = f.comp (g.comp h)
                @[simp]
                theorem LocallyBoundedMap.comp_id {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) :
                f.comp (LocallyBoundedMap.id α) = f
                @[simp]
                theorem LocallyBoundedMap.id_comp {α : Type u_2} {β : Type u_3} [Bornology α] [Bornology β] (f : LocallyBoundedMap α β) :
                (LocallyBoundedMap.id β).comp f = f
                @[simp]
                theorem LocallyBoundedMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] {g₁ : LocallyBoundedMap β γ} {g₂ : LocallyBoundedMap β γ} {f : LocallyBoundedMap α β} (hf : Function.Surjective f) :
                g₁.comp f = g₂.comp f g₁ = g₂
                @[simp]
                theorem LocallyBoundedMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bornology α] [Bornology β] [Bornology γ] {g : LocallyBoundedMap β γ} {f₁ : LocallyBoundedMap α β} {f₂ : LocallyBoundedMap α β} (hg : Function.Injective g) :
                g.comp f₁ = g.comp f₂ f₁ = f₂