Functors

This file defines two classes of functors:

• Functor: endofunctors over the category of quasi-Borel spaces.
• Sequences: functors from the poset category on ℕ to the category of quasi-Borel spaces.

class QuasiBorelSpace.Functor (F : Type u → Type v) : Type (max (u + 1) v)

• quasiBorelSpace {A : Type u} [QuasiBorelSpace A] : QuasiBorelSpace (F A)
• map₀ {A B : Type u} [QuasiBorelSpace A] [QuasiBorelSpace B] : (A →𝒒 B) → F A →𝒒 F B
• map₀_id {A : Type u} {x✝ : QuasiBorelSpace A} : map₀ QuasiBorelHom.id = QuasiBorelHom.id
• map₀_comp {A : Type u} {x✝ : QuasiBorelSpace A} {B : Type u} {x✝¹ : QuasiBorelSpace B} {C : Type u} {x✝² : QuasiBorelSpace C} (f : B →𝒒 C) (g : A →𝒒 B) (x : F A) : (map₀ f) ((map₀ g) x) = (map₀ (f.comp g)) x

noncomputable def QuasiBorelSpace.Functor.map {F : Type u_1 → Type u_2} {A B : Type u_1} [Functor F] [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A → B) : F A → F B

Equations

• QuasiBorelSpace.Functor.map f = ⇑(QuasiBorelSpace.Functor.map₀ (QuasiBorelHom.mk' f))

class QuasiBorelSpace.Sequence (S : ℕ → Type u_1) : Type u_1

• quasiBorelSpace {n : ℕ} : QuasiBorelSpace (S n)
• map₀ {m n : ℕ} : m ≤ n → S m →𝒒 S n
• map₀_id {n : ℕ} : map₀ ⋯ = QuasiBorelHom.id
• map₀_comp {m n o : ℕ} (h₁ : n ≤ o) (h₂ : m ≤ n) (x : S m) : (map₀ h₁) ((map₀ h₂) x) = (map₀ ⋯) x

def QuasiBorelSpace.Sequence.map {S : ℕ → Type u_1} [Sequence S] {m n : ℕ} (h : m ≤ n) : S m → S n

Equations

• QuasiBorelSpace.Sequence.map h = ⇑(QuasiBorelSpace.Sequence.map₀ h)

noncomputable def QuasiBorelSpace.Sequence.Internal.step {S : ℕ → Type u_1} [(n : ℕ) → QuasiBorelSpace (S n)] (f : (n : ℕ) → S n → S (n + 1)) {m n : ℕ} (h : m ≤ n) : S m →𝒒 S n

Equations

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

@[instance_reducible]

noncomputable def QuasiBorelSpace.Sequence.fromStep {S : ℕ → Type u_1} [(n : ℕ) → QuasiBorelSpace (S n)] (f : (n : ℕ) → S n → S (n + 1)) : Sequence S

Equations

• QuasiBorelSpace.Sequence.fromStep f = { quasiBorelSpace := inst✝, map₀ := fun {m n : ℕ} => QuasiBorelSpace.Sequence.Internal.step f, map₀_id := ⋯, map₀_comp := ⋯ }