Exponentials of Quasi-Borel Spaces

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

See [HKSY17], Proposition 18.

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.

• toFun : A → B

  The underlying function.

• property : QuasiBorelSpace.IsHom self.toFun

  The underlying function is a morphism.

def QuasiBorelHom.«term_→𝒒_» : Lean.TrailingParserDescr

The type of morphisms between QuasiBorelSpaces.

Equations

• QuasiBorelHom.«term_→𝒒_» = Lean.ParserDescr.trailingNode `QuasiBorelHom.«term_→𝒒_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →𝒒 ") (Lean.ParserDescr.cat `term 25))

instance QuasiBorelHom.instFunLike {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] : FunLike (A →𝒒 B) A B

Equations

• QuasiBorelHom.instFunLike = { coe := QuasiBorelHom.toFun, coe_injective' := ⋯ }

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

• QuasiBorelHom.Simps.coe f = ⇑f

theorem QuasiBorelHom.ext {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f g : A →𝒒 B} (h : ∀ (x : A), f x = g x) : f = g

theorem QuasiBorelHom.ext_iff {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f g : A →𝒒 B} : f = g ↔ ∀ (x : A), f x = g x

def QuasiBorelHom.copy {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : 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 := ⋯ }

@[simp]

theorem QuasiBorelHom.coe_mk {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f : A → B} (hf : QuasiBorelSpace.IsHom f) : ⇑{ toFun := f, property := hf } = f

@[simp]

theorem QuasiBorelHom.eta {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (f : A →𝒒 B) : { toFun := ⇑f, property := ⋯ } = f

@[simp]

theorem QuasiBorelHom.toFun_eq_coe {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (f : A →𝒒 B) : f.toFun = ⇑f

@[simp]

theorem QuasiBorelHom.isHom_coe {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (f : A →𝒒 B) : QuasiBorelSpace.IsHom ⇑f

instance QuasiBorelHom.instQuasiBorelSpace {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] : QuasiBorelSpace (A →𝒒 B)

Equations

• QuasiBorelHom.instQuasiBorelSpace = { IsVar := fun (φ : ℝ → A →𝒒 B) => QuasiBorelSpace.IsHom fun (x : ℝ × A) => (φ x.1) x.2, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

instance QuasiBorelHom.instMeasurableSpaceOfQuasiBorelSpace {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace B} [QuasiBorelSpace A] [QuasiBorelSpace A] : MeasurableSpace (A →𝒒 B)

Equations

• QuasiBorelHom.instMeasurableSpaceOfQuasiBorelSpace = QuasiBorelSpace.toMeasurableSpace

theorem QuasiBorelHom.isHom_def {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (φ : ℝ → A →𝒒 B) : QuasiBorelSpace.IsHom φ ↔ QuasiBorelSpace.IsHom fun (x : ℝ × A) => (φ x.1) x.2

@[simp]

theorem QuasiBorelHom.isHom_eval {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : QuasiBorelSpace.IsHom fun (p : (A →𝒒 B) × A) => p.1 p.2

theorem QuasiBorelHom.isHom_eval' {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : 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)

theorem QuasiBorelHom.isHom_mk {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : 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 := ⋯ }

@[simp]

theorem QuasiBorelHom.isHom_iff {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : A → B →𝒒 C) : QuasiBorelSpace.IsHom f ↔ QuasiBorelSpace.IsHom fun (x : A × B) => (f x.1) x.2

def QuasiBorelHom.curry {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : 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 := ⋯ }

@[simp]

theorem QuasiBorelHom.curry_coe_coe {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : A × B →𝒒 C) (x : A) : ⇑(f.curry x) = fun (y : B) => f (x, y)

def QuasiBorelHom.uncurry {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : 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 := ⋯ }

@[simp]

theorem QuasiBorelHom.uncurry_coe {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : A →𝒒 B →𝒒 C) : ⇑f.uncurry = fun (x : A × B) => (f x.1) x.2

@[simp]

theorem QuasiBorelHom.curry_uncurry {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : A →𝒒 B →𝒒 C) : f.uncurry.curry = f

@[simp]

theorem QuasiBorelHom.uncurry_curry {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : A × B →𝒒 C) : f.curry.uncurry = f

def QuasiBorelHom.id {A : Type u_1} {x✝ : QuasiBorelSpace A} : A →𝒒 A

The identity morphism.

Equations

• QuasiBorelHom.id = { toFun := fun (x : A) => x, property := ⋯ }

@[simp]

theorem QuasiBorelHom.id_coe {A : Type u_1} {x✝ : QuasiBorelSpace A} : ⇑id = fun (x : A) => x

@[simp]

theorem QuasiBorelHom.eq_id {A : Type u_1} {x✝ : QuasiBorelSpace A} : { toFun := fun (x : A) => x, property := ⋯ } = id

def QuasiBorelHom.comp {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : B →𝒒 C) (g : A →𝒒 B) : A →𝒒 C

Morphism composition.

Equations

• f.comp g = { toFun := fun (x : A) => f (g x), property := ⋯ }

@[simp]

theorem QuasiBorelHom.comp_coe {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} (f : B →𝒒 C) (g : A →𝒒 B) : ⇑(f.comp g) = fun (x : A) => f (g x)

@[simp]

theorem QuasiBorelHom.eq_comp {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} {f : B → C} (hf : QuasiBorelSpace.IsHom f) {g : A → B} (hg : QuasiBorelSpace.IsHom g) : { toFun := f, property := hf }.comp { toFun := g, property := hg } = { toFun := fun (x : A) => f (g x), property := ⋯ }