LeanPool.QuasiBorelSpaces.Functor

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Functor.

class QuasiBorelSpace.Functor (F : (A : Type u_2) → [QuasiBorelSpace A] → Type u_1) : Type (max u_1 (u_2 + 1))

A QuasiBorelSpace Functor is a function F : Type → Type such that:

• quasiBorelSpace {A : Type u_2} [QuasiBorelSpace A] : QuasiBorelSpace (F A)
  1. F maps QuasiBorelSpaces to QuasiBorelSpaces.
• map {A B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] : (A →𝒒 B) → F A →𝒒 F B
  2. There is a mapping from morphisms to morphisms.
• map_id {A : Type u_2} [QuasiBorelSpace A] : map QuasiBorelHom.id = QuasiBorelHom.id
  3. The mapping preserves the identity morphism.
• map_comp {A : Type u_2} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_2} [QuasiBorelSpace C] (f : B →𝒒 C) (g : A →𝒒 B) : (map f).comp (map g) = map (f.comp g)
  4. The mapping distributes over composition.

@[simp]

theorem QuasiBorelSpace.Functor.map_comp_coe {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] {A : Type u_1} [QuasiBorelSpace A] {B : Type u_1} [QuasiBorelSpace B] {C : Type u_1} [QuasiBorelSpace C] (f : B →𝒒 C) (g : A →𝒒 B) (x : F A) : (map f) ((map g) x) = (map (f.comp g)) x

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

A Sequence is a sequence of types S : ℕ → Type such that:

• quasiBorelSpace {n : ℕ} : QuasiBorelSpace (S n)
  1. Every S n is a QuasiBorelSpace.
• project (n : ℕ) : S (n + 1) →𝒒 S n
  2. There is a projection from each type to its predecessor.

structure QuasiBorelSpace.Comp (F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2) [Functor F] (S : ℕ → Type u_1) [Sequence S] (n : ℕ) : Type u_2

The composition of a Functor with a Sequence.

• get : F (S n)

  The underlying element of F (S n).

theorem QuasiBorelSpace.Comp.ext {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] {S : ℕ → Type u_1} [Sequence S] {n : ℕ} {x y : Comp F S n} (h : x.get = y.get) : x = y

theorem QuasiBorelSpace.Comp.ext_iff {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] {S : ℕ → Type u_1} [Sequence S] {n : ℕ} {x y : Comp F S n} : x = y ↔ x.get = y.get

@[instance_reducible]

instance QuasiBorelSpace.Comp.inst {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] {S : ℕ → Type u_1} [Sequence S] {n : ℕ} : QuasiBorelSpace (Comp F S n)

Equations

• QuasiBorelSpace.Comp.inst = QuasiBorelSpace.lift QuasiBorelSpace.Comp.get

theorem QuasiBorelSpace.Comp.isHom_mk {F : (A : Type u_2) → [QuasiBorelSpace A] → Type u_1} [Functor F] {S : ℕ → Type u_2} [Sequence S] {n : ℕ} : IsHom mk

theorem QuasiBorelSpace.Comp.isHom_get {F : (A : Type u_2) → [QuasiBorelSpace A] → Type u_1} [Functor F] {S : ℕ → Type u_2} [Sequence S] {n : ℕ} : IsHom get

@[instance_reducible]

instance QuasiBorelSpace.Comp.instSequence {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] {S : ℕ → Type u_1} [Sequence S] : Sequence (Comp F S)

Equations

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

@[simp]

theorem QuasiBorelSpace.Comp.project_def {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] {S : ℕ → Type u_1} [Sequence S] (n : ℕ) : Sequence.project n = { toFun := fun (x : Comp F S (n + 1)) => { get := (Functor.map (Sequence.project n)) x.get }, property := ⋯ }

structure QuasiBorelSpace.Limit (S : ℕ → Type u_1) [Sequence S] : Type u_1

The Limit of a Sequence S consists of:

• toFun (n : ℕ) : S n
  1. A sequence of elements, one from each S n.
• property (n : ℕ) : (Sequence.project n) (self.toFun (n + 1)) = self.toFun n
  2. A proof that every element is the projection of its successor.

@[instance_reducible]

instance QuasiBorelSpace.Limit.instDFunLikeNat {S : ℕ → Type u_1} [Sequence S] : DFunLike (Limit S) ℕ S

Equations

• QuasiBorelSpace.Limit.instDFunLikeNat = { coe := QuasiBorelSpace.Limit.toFun, coe_injective := ⋯ }

def QuasiBorelSpace.Limit.Simps.coe {S : ℕ → Type u_1} [Sequence S] (f : Limit S) (n : ℕ) : S n

A simps projection for function coercion.

Equations

• QuasiBorelSpace.Limit.Simps.coe f = ⇑f

theorem QuasiBorelSpace.Limit.ext {S : ℕ → Type u_1} [Sequence S] {f g : Limit S} (h : ∀ (x : ℕ), f x = g x) : f = g

theorem QuasiBorelSpace.Limit.ext_iff {S : ℕ → Type u_1} [Sequence S] {f g : Limit S} : f = g ↔ ∀ (x : ℕ), f x = g x

def QuasiBorelSpace.Limit.copy {S : ℕ → Type u_1} [Sequence S] (f : Limit S) (f' : (n : ℕ) → S n) (h : f' = ⇑f) : Limit S

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 QuasiBorelSpace.Limit.coe_mk {S : ℕ → Type u_1} [Sequence S] {f : (n : ℕ) → S n} (hf : ∀ (n : ℕ), (Sequence.project n) (f (n + 1)) = f n) : ⇑{ toFun := f, property := hf } = f

@[simp]

theorem QuasiBorelSpace.Limit.eta {S : ℕ → Type u_1} [Sequence S] (f : Limit S) : { toFun := ⇑f, property := ⋯ } = f

@[simp]

theorem QuasiBorelSpace.Limit.toFun_eq_coe {S : ℕ → Type u_1} [Sequence S] (f : Limit S) : f.toFun = ⇑f

@[simp]

theorem QuasiBorelSpace.Limit.project_coe {S : ℕ → Type u_1} [Sequence S] (n : ℕ) (f : Limit S) : (Sequence.project n) (f (n + 1)) = f n

def QuasiBorelSpace.Limit.toSubtype {S : ℕ → Type u_1} [Sequence S] (x : Limit S) : { f : (n : ℕ) → S n // ∀ (n : ℕ), (Sequence.project n) (f (n + 1)) = f n }

View a sequence limit as a compatible family of coordinates.

Equations

• x.toSubtype = ⟨x.toFun, ⋯⟩

@[instance_reducible]

instance QuasiBorelSpace.Limit.inst {S : ℕ → Type u_1} [Sequence S] : QuasiBorelSpace (Limit S)

Equations

• QuasiBorelSpace.Limit.inst = QuasiBorelSpace.lift QuasiBorelSpace.Limit.toSubtype

theorem QuasiBorelSpace.Limit.isHom_mk {A : Type u_2} [QuasiBorelSpace A] {S : ℕ → Type u_1} [Sequence S] {f : A → (n : ℕ) → S n} (hf₁ : IsHom f) (hf₂ : ∀ (x : A) (n : ℕ), (Sequence.project n) (f x (n + 1)) = f x n) : IsHom fun (x : A) => { toFun := f x, property := ⋯ }

theorem QuasiBorelSpace.Limit.isHom_coe {A : Type u_2} [QuasiBorelSpace A] {S : ℕ → Type u_1} [Sequence S] {f : A → Limit S} (hf : IsHom f) {n : ℕ} : IsHom fun (x : A) => (f x) n

structure QuasiBorelSpace.Bundle : Type (u + 1)

A type bundled with its quasi-Borel space structure.

• Carrier : Type u

  The underlying type of a bundled quasi-Borel space.

• quasiBorelSpace : QuasiBorelSpace self.Carrier

  The quasi-Borel structure on the bundled carrier.

def QuasiBorelSpace.Iter₀ (F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1) [Functor F] : ℕ → Bundle

Iterate the functor starting at the one-point quasi-Borel space.

Equations

• QuasiBorelSpace.Iter₀ F 0 = { Carrier := PUnit.{?u.1 + 1}, quasiBorelSpace := QuasiBorelSpace.PUnit.instPUnit }
• QuasiBorelSpace.Iter₀ F n.succ = { Carrier := F (QuasiBorelSpace.Iter₀ F n).Carrier, quasiBorelSpace := QuasiBorelSpace.Functor.quasiBorelSpace }

structure QuasiBorelSpace.Iter (F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1) [Functor F] (n : ℕ) : Type u_1

The Sequence obtained by iterating a Functor.

• get : (Iter₀ F n).Carrier

  The underlying element at the nth iterate.

@[instance_reducible]

instance QuasiBorelSpace.Iter.inst {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : QuasiBorelSpace (Iter F n)

Equations

• QuasiBorelSpace.Iter.inst = QuasiBorelSpace.lift QuasiBorelSpace.Iter.get

@[simp]

theorem QuasiBorelSpace.Iter.isHom_get {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : IsHom get

@[simp]

theorem QuasiBorelSpace.Iter.isHom_mk {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : IsHom mk

def QuasiBorelSpace.Iter.getHom {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : Iter F n →𝒒 (Iter₀ F n).Carrier

The underlying-value projection as a quasi-Borel homomorphism.

Equations

• QuasiBorelSpace.Iter.getHom = { toFun := QuasiBorelSpace.Iter.get, property := ⋯ }

def QuasiBorelSpace.Iter.mkHom {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : (Iter₀ F n).Carrier →𝒒 Iter F n

The wrapper constructor as a quasi-Borel homomorphism.

Equations

• QuasiBorelSpace.Iter.mkHom = { toFun := QuasiBorelSpace.Iter.mk, property := ⋯ }

def QuasiBorelSpace.Iter.zero {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : Iter F 0

Zero element constructor.

Equations

• QuasiBorelSpace.Iter.zero = { get := () }

instance QuasiBorelSpace.Iter.instSubsingletonOfNatNat {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] : Subsingleton (Iter F 0)

def QuasiBorelSpace.Iter.succ {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : F (Iter F n) →𝒒 Iter F (n + 1)

Successor element constructor.

Equations

• QuasiBorelSpace.Iter.succ = { toFun := fun (x : F (QuasiBorelSpace.Iter F n)) => { get := (QuasiBorelSpace.Functor.map QuasiBorelSpace.Iter.getHom) x }, property := ⋯ }

def QuasiBorelSpace.Iter.unsucc {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} : Iter F (n + 1) →𝒒 F (Iter F n)

Successor element destructor.

Equations

• QuasiBorelSpace.Iter.unsucc = { toFun := fun (x : QuasiBorelSpace.Iter F (n + 1)) => (QuasiBorelSpace.Functor.map QuasiBorelSpace.Iter.mkHom) x.get, property := ⋯ }

@[simp]

theorem QuasiBorelSpace.Iter.succ_unsucc {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} (x : Iter F (n + 1)) : succ (unsucc x) = x

@[simp]

theorem QuasiBorelSpace.Iter.unsucc_succ {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} (x : F (Iter F n)) : unsucc (succ x) = x

theorem QuasiBorelSpace.Iter.succ_injective {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_1} [Functor F] {n : ℕ} {x y : F (Iter F n)} (h : succ x = succ y) : x = y

def QuasiBorelSpace.Iter.project {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] (n : ℕ) : Iter F (n + 1) →𝒒 Iter F n

The projection between successive iterates of the functor.

Equations

• QuasiBorelSpace.Iter.project 0 = { toFun := fun (x : QuasiBorelSpace.Iter F (0 + 1)) => QuasiBorelSpace.Iter.zero, property := ⋯ }
• QuasiBorelSpace.Iter.project n.succ = QuasiBorelSpace.Iter.succ.comp ((QuasiBorelSpace.Functor.map (QuasiBorelSpace.Iter.project n)).comp QuasiBorelSpace.Iter.unsucc)

@[instance_reducible]

instance QuasiBorelSpace.Iter.instSequence {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : Sequence (Iter F)

Equations

• QuasiBorelSpace.Iter.instSequence = { quasiBorelSpace := @QuasiBorelSpace.Iter.inst F inst✝, project := fun {n : ℕ} => QuasiBorelSpace.Iter.project n }

@[simp]

theorem QuasiBorelSpace.Iter.project_zero {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : Sequence.project 0 = { toFun := fun (x : Iter F (0 + 1)) => zero, property := ⋯ }

@[simp]

theorem QuasiBorelSpace.Iter.project_succ {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] {n : ℕ} : Sequence.project (n + 1) = succ.comp ((Functor.map (Sequence.project n)).comp unsucc)

def QuasiBorelSpace.Iter.unfold {A : Type} [QuasiBorelSpace A] {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] (f : A →𝒒 F A) (n : ℕ) : A →𝒒 Iter F n

Constructs an Iterated sequence of a Functor from an unfolding function.

Equations

• QuasiBorelSpace.Iter.unfold f 0 = { toFun := fun (x : A) => QuasiBorelSpace.Iter.zero, property := ⋯ }
• QuasiBorelSpace.Iter.unfold f n.succ = { toFun := fun (x : A) => QuasiBorelSpace.Iter.succ ((QuasiBorelSpace.Functor.map (QuasiBorelSpace.Iter.unfold f n)) (f x)), property := ⋯ }

class QuasiBorelSpace.Continuous (F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2) [Functor F] : Type (max (u_1 + 1) u_2)

A functor F is continuous if it preserves Limits.

• seq {S : ℕ → Type u_1} [Sequence S] : F (Limit S) →𝒒 Limit (Comp F S)

  Folds a Functor into a Limit.

• unseq {S : ℕ → Type u_1} [Sequence S] : Limit (Comp F S) →𝒒 F (Limit S)

  Unfolds a Functor out of a Limit.

• seq_unseq {S : ℕ → Type u_1} [Sequence S] : seq.comp unseq = QuasiBorelHom.id

  seq and unseq are inverses.

• unseq_seq {S : ℕ → Type u_1} [Sequence S] : unseq.comp seq = QuasiBorelHom.id

  seq and unseq are inverses.

@[simp]

theorem QuasiBorelSpace.Continuous.seq_unseq_coe {F : (A : Type u_2) → [QuasiBorelSpace A] → Type u_1} [Functor F] [Continuous F] {S : ℕ → Type u_2} [Sequence S] (x : Limit (Comp F S)) : seq (unseq x) = x

@[simp]

theorem QuasiBorelSpace.Continuous.unseq_seq_coe {F : (A : Type u_1) → [QuasiBorelSpace A] → Type u_2} [Functor F] [Continuous F] {S : ℕ → Type u_1} [Sequence S] (x : F (Limit S)) : unseq (seq x) = x

structure QuasiBorelSpace.Nu (F : (A : Type) → [QuasiBorelSpace A] → Type) [Functor F] : Type

The greatest fixed point of a Functor.

• get : Limit (Iter F)

  The underlying compatible sequence of finite iterates.

@[instance_reducible]

instance QuasiBorelSpace.Nu.inst {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : QuasiBorelSpace (Nu F)

Equations

• QuasiBorelSpace.Nu.inst = QuasiBorelSpace.lift QuasiBorelSpace.Nu.get

@[simp]

theorem QuasiBorelSpace.Nu.isHom_get {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : IsHom get

@[simp]

theorem QuasiBorelSpace.Nu.isHom_mk {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : IsHom mk

def QuasiBorelSpace.Nu.shift {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : Limit (Iter F) →𝒒 Limit (Comp F (Iter F))

Shift a compatible family to a family in the functor-composed sequence.

Equations

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

@[simp]

theorem QuasiBorelSpace.Nu.shift_coe_coe_get {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] (x : Limit (Iter F)) (n : ℕ) : ((shift x) n).get = Iter.unsucc (x (n + 1))

def QuasiBorelSpace.Nu.unshift {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] : Limit (Comp F (Iter F)) →𝒒 Limit (Iter F)

Recover a compatible family from the functor-composed sequence.

Equations

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

@[simp]

theorem QuasiBorelSpace.Nu.unshift_coe_coe {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] (x : Limit (Comp F (Iter F))) : ⇑(unshift x) = fun (x_1 : ℕ) => match x_1 with | 0 => Iter.zero | n.succ => Iter.succ (x n).get

def QuasiBorelSpace.Nu.roll {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] [Continuous F] : F (Nu F) →𝒒 Nu F

Rolls a Functor into a Nu.

Equations

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

def QuasiBorelSpace.Nu.unroll {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] [Continuous F] : Nu F →𝒒 F (Nu F)

Unrolls a Functor out of a Nu.

Equations

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

@[simp]

theorem QuasiBorelSpace.Nu.roll_unroll {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] [Continuous F] (x : Nu F) : roll (unroll x) = x

@[simp]

theorem QuasiBorelSpace.Nu.unroll_roll {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] [Continuous F] (x : F (Nu F)) : unroll (roll x) = x

def QuasiBorelSpace.Nu.unfold {A : Type} [QuasiBorelSpace A] {F : (A : Type) → [QuasiBorelSpace A] → Type} [Functor F] (f : A →𝒒 F A) : A →𝒒 Nu F

Constructs a Nu from an unfolding.

Equations

• QuasiBorelSpace.Nu.unfold f = { toFun := fun (x : A) => { get := { toFun := fun (n : ℕ) => (QuasiBorelSpace.Iter.unfold f n) x, property := ⋯ } }, property := ⋯ }