Documentation

QuasiBorelSpaces.Hom

Exponentials of Quasi-Borel Spaces #

This file defines the exponential object in the category of quasi-borel spaces.

See [HKSY17], Proposition 18.

source
structure QuasiBorelHom (A : Type u_1) (B : Type u_2) [QuasiBorelSpace A] [QuasiBorelSpace B] :
Type (max u_1 u_2)

The type of morphisms between QuasiBorelSpaces.

Instances For
    source
    def QuasiBorelHom.Β«term_→𝒒_Β» :
    Lean.TrailingParserDescr

    The type of morphisms between QuasiBorelSpaces.

    Equations
    Instances For
      source
      instance QuasiBorelHom.instFunLike {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] :
      FunLike (A →𝒒 B) A B
      Equations
      source
      def QuasiBorelHom.Simps.coe {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A →𝒒 B) :
      A β†’ B

      A simps projection for function coercion.

      Equations
      Instances For
        source
        theorem QuasiBorelHom.ext {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f g : A →𝒒 B} (h : βˆ€ (x : A), f x = g x) :
        f = g
        source
        theorem QuasiBorelHom.ext_iff {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f g : A →𝒒 B} :
        f = g ↔ βˆ€ (x : A), f x = g x
        source
        def QuasiBorelHom.copy {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A →𝒒 B) (f' : A β†’ B) (h : f' = ⇑f) :
        A →𝒒 B

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

        Equations
        • f.copy f' h = { toFun := f', property := β‹― }
        Instances For
          source
          @[simp]
          theorem QuasiBorelHom.coe_mk {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A β†’ B} (hf : QuasiBorelSpace.IsHom f) :
          ⇑{ toFun := f, property := hf } = f
          source
          @[simp]
          theorem QuasiBorelHom.eta {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A →𝒒 B) :
          { toFun := ⇑f, property := β‹― } = f
          source
          @[simp]
          theorem QuasiBorelHom.toFun_eq_coe {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A →𝒒 B) :
          f.toFun = ⇑f
          source
          @[simp]
          theorem QuasiBorelHom.isHom_coe {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A →𝒒 B) :
          QuasiBorelSpace.IsHom ⇑f
          source
          instance QuasiBorelHom.instQuasiBorelSpace {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] :
          QuasiBorelSpace (A →𝒒 B)
          Equations
          source
          theorem QuasiBorelHom.isHom_def {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (Ο† : ℝ β†’ A →𝒒 B) :
          QuasiBorelSpace.IsHom Ο† ↔ QuasiBorelSpace.IsHom fun (x : ℝ Γ— A) => (Ο† x.1) x.2
          source
          @[simp]
          theorem QuasiBorelHom.isHom_eval {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] :
          QuasiBorelSpace.IsHom fun (p : (A →𝒒 B) Γ— A) => p.1 p.2
          source
          theorem QuasiBorelHom.isHom_eval' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A β†’ B →𝒒 C} (hf : QuasiBorelSpace.IsHom f) {g : A β†’ B} (hg : QuasiBorelSpace.IsHom g) :
          QuasiBorelSpace.IsHom fun (x : A) => (f x) (g x)
          source
          @[simp]
          theorem QuasiBorelHom.isHom_iff {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A β†’ B →𝒒 C) :
          QuasiBorelSpace.IsHom f ↔ QuasiBorelSpace.IsHom fun (x : A Γ— B) => (f x.1) x.2
          source
          theorem QuasiBorelHom.isHom_mk {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A β†’ B β†’ C} (hf : QuasiBorelSpace.IsHom fun (x : A Γ— B) => f x.1 x.2) :
          QuasiBorelSpace.IsHom fun (x : A) => { toFun := f x, property := β‹― }
          source
          def QuasiBorelHom.curry {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A Γ— B →𝒒 C) :
          A →𝒒 B →𝒒 C

          Currying for QuasiBorelHoms.

          Equations
          • f.curry = { toFun := fun (x : A) => { toFun := fun (y : B) => f (x, y), property := β‹― }, property := β‹― }
          Instances For
            source
            @[simp]
            theorem QuasiBorelHom.curry_coe {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A Γ— B →𝒒 C) (x : A) :
            f.curry x = { toFun := fun (y : B) => f (x, y), property := β‹― }
            source
            def QuasiBorelHom.uncurry {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A →𝒒 B →𝒒 C) :
            A Γ— B →𝒒 C

            Uncurrying for QuasiBorelHoms.

            Equations
            • f.uncurry = { toFun := fun (x : A Γ— B) => (f x.1) x.2, property := β‹― }
            Instances For
              source
              @[simp]
              theorem QuasiBorelHom.uncurry_coe {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A →𝒒 B →𝒒 C) (x : A Γ— B) :
              f.uncurry x = (f x.1) x.2
              source
              @[simp]
              theorem QuasiBorelHom.curry_uncurry {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A →𝒒 B →𝒒 C) :
              f.uncurry.curry = f
              source
              @[simp]
              theorem QuasiBorelHom.uncurry_curry {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] (f : A Γ— B →𝒒 C) :
              f.curry.uncurry = f