Colimits

This file provides basic lemmas about colimits of Sequences.

@[simp]

theorem QuasiBorelSpace.Colimit.isHom_mk {S : ℕ → Type u_1} [Sequence S] {i : ℕ} : IsHom (mk i)

theorem QuasiBorelSpace.Colimit.isHom_lift {S : ℕ → Type u_3} [Sequence S] {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → (i : ℕ) → S i → B} {g : A → Colimit S} (hf₁ : ∀ (z : A) ⦃i j : ℕ⦄ (h : i ≤ j) (x : S i), f z j (Sequence.map h x) = f z i x) (hf₂ : ∀ (i : ℕ), IsHom fun (x : A × S i) => f x.1 i x.2) (hg : IsHom g) : IsHom fun (x : A) => lift (f x) ⋯ (g x)

theorem QuasiBorelSpace.Colimit.induction {S : ℕ → Type u_1} [Sequence S] {P : Colimit S → Prop} (mk : ∀ (i : ℕ) (x : S i), P (mk i x)) (x : Colimit S) : P x

theorem QuasiBorelSpace.Colimit.sound {S : ℕ → Type u_1} [Sequence S] {i j : ℕ} (h₀ : i ≤ j) {x : S i} {y : S j} (h₁ : Sequence.map h₀ x = y) : mk i x = mk j y

@[simp]

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

@[simp]

theorem QuasiBorelSpace.Colimit.map_mk {S : ℕ → Type u_2} {S' : ℕ → Type u_1} [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)) (i : ℕ) (x : S i) : map (fun {i : ℕ} => f) ⋯ (mk i x) = mk i (f x)

@[simp]

theorem QuasiBorelSpace.Colimit.mk_lift {S : ℕ → Type u_1} [Sequence S] : lift mk ⋯ = id

@[simp]

theorem QuasiBorelSpace.Colimit.mk_map {S : ℕ → Type u_1} [Sequence S] {j i : ℕ} {h : j ≤ i} (x : S j) : mk i (Sequence.map h x) = mk j x

@[simp]

theorem QuasiBorelSpace.Colimit.isHom_map {S : ℕ → Type u_1} {S' : ℕ → Type u_2} [Sequence S] [Sequence S'] (f : {i : ℕ} → S i → S' i) (hf₁ : ∀ {i : ℕ}, IsHom f) (hf₂ : ∀ {i j : ℕ} (h : i ≤ j) (x : S i), Sequence.map h (f x) = f (Sequence.map h x)) : IsHom (map (fun {i : ℕ} => f) ⋯)

theorem QuasiBorelSpace.Colimit.apply_lift {S : ℕ → Type u_3} [Sequence S] {B : Sort u_1} {C : Sort u_2} {x : Colimit S} {k : B → C} {f : (i : ℕ) → S i → B} (hf : ∀ ⦃i j : ℕ⦄ (h : i ≤ j) (x : S i), f j (Sequence.map h x) = f i x) : k (lift f hf x) = lift (fun (i : ℕ) (x : S i) => k (f i x)) ⋯ x

@[simp]

theorem QuasiBorelSpace.Colimit.isHom_unroll {S : ℕ → Type u_1} [Sequence S] {F : Type u_1 → Type u_1} [Functor F] : IsHom unroll

@[simp]

theorem QuasiBorelSpace.Colimit.unroll_mk {S : ℕ → Type u_1} [Sequence S] {F : Type u_1 → Type u_1} {i : ℕ} [Functor F] (x : Sequence.Compose F S i) : (mk i x).unroll = Functor.map (mk i) x.val

theorem QuasiBorelSpace.Cocontinuous.unroll_inj {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Cocontinuous F] [Sequence S] {x y : Colimit (Sequence.Compose F S)} (h : x.unroll = y.unroll) : x = y

theorem QuasiBorelSpace.Cocontinuous.roll_inj {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Cocontinuous F] [Sequence S] {x y : F (Colimit S)} (h : roll x = roll y) : x = y

theorem QuasiBorelSpace.Cocontinuous.map_unroll {F : Type u_1 → Type u_1} {S S' : ℕ → Type u_1} [Functor F] [Sequence S] [Sequence S'] (f : {i : ℕ} → S i → S' i) (hf₁ : ∀ {i : ℕ}, IsHom f) (hf₂ : ∀ {i j : ℕ} (h : i ≤ j) (x : S i), Sequence.map h (f x) = f (Sequence.map h x)) (x : Colimit (Sequence.Compose F S)) : (Colimit.map (fun {i : ℕ} => Sequence.Compose.map fun {i : ℕ} => f) ⋯ x).unroll = Functor.map (Colimit.map (fun {i : ℕ} => f) ⋯) x.unroll

theorem QuasiBorelSpace.Cocontinuous.map_roll {F : Type u_1 → Type u_1} {S S' : ℕ → Type u_1} [Functor F] [Cocontinuous F] [Sequence S] [Sequence S'] (f : {i : ℕ} → S i → S' i) (hf₁ : ∀ {i : ℕ}, IsHom f) (hf₂ : ∀ {i j : ℕ} (h : i ≤ j) (x : S i), Sequence.map h (f x) = f (Sequence.map h x)) (x : F (Colimit S)) : Colimit.map (fun {i : ℕ} => Sequence.Compose.map fun {i : ℕ} => f) ⋯ (roll x) = roll (Functor.map (Colimit.map (fun {i : ℕ} => f) ⋯) x)

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Cocontinuous.instIdentity : Cocontinuous Functor.Identity

Equations

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

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Cocontinuous.instConst {A : Type u_1} [QuasiBorelSpace A] : Cocontinuous (Functor.Const A)

Equations

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

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Cocontinuous.instProd {F G : Type u_1 → Type u_1} [Functor F] [Cocontinuous F] [Functor G] [Cocontinuous G] : Cocontinuous (Functor.Prod F G)

Equations

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

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Cocontinuous.instSum {F G : Type u_1 → Type u_1} [Functor F] [Cocontinuous F] [Functor G] [Cocontinuous G] : Cocontinuous (Functor.Sum F G)

Equations

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