Fixed Points of Functors

We construct fixed points of continuous (i.e., colimit-preserving) functors and provide a quasi-Borel space instance.

structure QuasiBorelSpace.Fix (F : Type u → Type u) [Functor F] : Type u

• val : QuasiBorelSpace.Colimit (QuasiBorelSpace.Sequence.Iterate F)

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Fix.inst {F : Type u_1 → Type u_1} [Functor F] : QuasiBorelSpace (Fix F)

Equations

• QuasiBorelSpace.Fix.inst = QuasiBorelSpace.lift QuasiBorelSpace.Fix.val✝

noncomputable def QuasiBorelSpace.Fix.unroll {F : Type u_1 → Type u_1} [Functor F] (x : Fix F) : F (Fix F)

Equations

• x.unroll = QuasiBorelSpace.Colimit.lift QuasiBorelSpace.Fix.unroll₀✝ ⋯ (QuasiBorelSpace.Fix.val✝ x)

@[simp]

theorem QuasiBorelSpace.Fix.isHom_unroll {F : Type u_1 → Type u_1} [Functor F] : IsHom unroll

noncomputable def QuasiBorelSpace.Fix.roll {F : Type u_1 → Type u_1} [Functor F] [Cocontinuous F] (x : F (Fix F)) : Fix F

Equations

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

@[simp]

theorem QuasiBorelSpace.Fix.isHom_roll {F : Type u_1 → Type u_1} [Functor F] [Cocontinuous F] : IsHom roll

@[simp]

theorem QuasiBorelSpace.Fix.unroll_roll {F : Type u_1 → Type u_1} [Functor F] [Cocontinuous F] (x : F (Fix F)) : (roll x).unroll = x

@[simp]

theorem QuasiBorelSpace.Fix.roll_unroll {F : Type u_1 → Type u_1} [Functor F] [Cocontinuous F] (x : Fix F) : roll x.unroll = x

noncomputable def QuasiBorelSpace.Fix.fold₀ {F : Type u_1 → Type u_1} {A : Type u_1} [Functor F] [QuasiBorelSpace A] (f : F A → A) (i : ℕ) : Sequence.Iterate F i → A

Equations

• QuasiBorelSpace.Fix.fold₀ f 0 x_2 = x_2.elim
• QuasiBorelSpace.Fix.fold₀ f n.succ x_2 = f (QuasiBorelSpace.Functor.map (QuasiBorelSpace.Fix.fold₀ f n) x_2.unroll)

@[simp]

theorem QuasiBorelSpace.Fix.isHom_fold₀ {A : Type u_1} [QuasiBorelSpace A] {i : ℕ} {F : Type u_1 → Type u_1} [Functor F] {f : F A → A} (hf : IsHom f) : IsHom (fold₀ f i)

@[simp]

theorem QuasiBorelSpace.Fix.fold₀_eq {A : Type u_1} [QuasiBorelSpace A] {F : Type u_1 → Type u_1} [Functor F] {f : F A → A} (hf : IsHom f) ⦃i j : ℕ⦄ (h : i ≤ j) (x : Sequence.Iterate F i) : fold₀ f j (Sequence.map h x) = fold₀ f i x

noncomputable def QuasiBorelSpace.Fix.fold {F : Type u_1 → Type u_1} {A : Type u_1} [Functor F] [QuasiBorelSpace A] (f : F A → A) (x : Fix F) : A

Equations

• QuasiBorelSpace.Fix.fold f x = QuasiBorelSpace.Colimit.lift (QuasiBorelSpace.Fix.fold₀ ⇑(QuasiBorelHom.mk' f)) ⋯ (QuasiBorelSpace.Fix.val✝ x)

@[simp]

theorem QuasiBorelSpace.Fix.isHom_fold {F : Type u_1 → Type u_1} {A : Type u_1} [Functor F] [QuasiBorelSpace A] (f : F A → A) : IsHom (fold f)

@[simp]

theorem QuasiBorelSpace.Fix.fold_roll {F : Type u_1 → Type u_1} {A : Type u_1} [Functor F] [QuasiBorelSpace A] [Cocontinuous F] (f : F A → A) (hf : IsHom f) (x : F (Fix F)) : fold f (roll x) = f (Functor.map (fold f) x)