Colimits

This file defines colimits of Sequences.

@[instance_reducible]

def QuasiBorelSpace.Colimit.setoid (S : ℕ → Type u_1) [Sequence S] : Setoid ((i : ℕ) × S i)

Equations

• QuasiBorelSpace.Colimit.setoid S = { r := Relation.EqvGen fun (x y : (i : ℕ) × S i) => ∃ (h : x.fst ≤ y.fst), QuasiBorelSpace.Sequence.map h x.snd = y.snd, iseqv := ⋯ }

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

• mk₀ :: (
• val : Quotient (QuasiBorelSpace.Colimit.setoid S)
• )

def QuasiBorelSpace.Colimit.mk {S : ℕ → Type u_1} [Sequence S] (i : ℕ) (x : S i) : Colimit S

Equations

• QuasiBorelSpace.Colimit.mk i x = { val := ⟦⟨i, x⟩⟧ }

def QuasiBorelSpace.Colimit.lift {S : ℕ → Type u_1} [Sequence S] {A : Sort u_2} (f : (i : ℕ) → S i → A) (hf : ∀ ⦃i j : ℕ⦄ (h : i ≤ j) (x : S i), f j (Sequence.map h x) = f i x) (x : Colimit S) : A

Equations

• QuasiBorelSpace.Colimit.lift f hf x = Quotient.lift (fun (x : (i : ℕ) × S i) => f x.fst x.snd) ⋯ (QuasiBorelSpace.Colimit.val✝ x)

@[instance_reducible]

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

Equations

• QuasiBorelSpace.Colimit.instQuasiBorelSpace = QuasiBorelSpace.lift QuasiBorelSpace.Colimit.val✝

def QuasiBorelSpace.Colimit.map {S : ℕ → Type u_1} {S' : ℕ → Type u_2} [Sequence S] [Sequence S'] (f : {i : ℕ} → S i → S' i) (hf : ∀ {i j : ℕ} (h : i ≤ j) (x : S i), Sequence.map h (f x) = f (Sequence.map h x)) : Colimit S → Colimit S'

Equations

• QuasiBorelSpace.Colimit.map f hf = QuasiBorelSpace.Colimit.lift (fun (i : ℕ) (x : S i) => QuasiBorelSpace.Colimit.mk i (f x)) ⋯

noncomputable def QuasiBorelSpace.Colimit.unroll {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] : Colimit (Sequence.Compose F S) → F (Colimit S)

Equations

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

class QuasiBorelSpace.Cocontinuous (F : Type u → Type u) [Functor F] : Type (u + 1)

• roll {S : ℕ → Type u} [Sequence S] : F (Colimit S) →𝒒 Colimit (Sequence.Compose F S)
• roll_unroll {S : ℕ → Type u} [Sequence S] (x : Colimit (Sequence.Compose F S)) : roll x.unroll = x
• unroll_roll {S : ℕ → Type u} [Sequence S] (x : F (Colimit S)) : (roll x).unroll = x