Binary Coproducts of Quasi-Borel Spaces

This file defines binary coproducts of quasi-borel spaces by giving a QuasiBorelSpace instance for the · ⊕ · type.

See [HKSY17], Proposition 17.

def QuasiBorelSpace.Sum.Encoding (A : Type u) (B : Type v) : Bool → Type (max u v)

We derive the QuasiBorelSpace instance for A ⊕ B via Sigma (Encoding A B).

Equations

• QuasiBorelSpace.Sum.Encoding A B true = ULift.{?u.78, ?u.79} A
• QuasiBorelSpace.Sum.Encoding A B false = ULift.{?u.86, ?u.85} B

def QuasiBorelSpace.Sum.Encoding.inl {A : Type u_1} {B : Type u_2} (x : A) : Sigma (Encoding A B)

The encoded version of Sum.inl.

Equations

• QuasiBorelSpace.Sum.Encoding.inl x = ⟨true, { down := x }⟩

def QuasiBorelSpace.Sum.Encoding.inr {A : Type u_1} {B : Type u_2} (x : B) : Sigma (Encoding A B)

The encoded version of Sum.inr.

Equations

• QuasiBorelSpace.Sum.Encoding.inr x = ⟨false, { down := x }⟩

def QuasiBorelSpace.Sum.Encoding.elim {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : A → C) (g : B → C) : Sigma (Encoding A B) → C

The encoded version of Sum.elim.

Equations

• QuasiBorelSpace.Sum.Encoding.elim f g ⟨true, x_1⟩ = f x_1.down
• QuasiBorelSpace.Sum.Encoding.elim f g ⟨false, x_1⟩ = g x_1.down

instance QuasiBorelSpace.Sum.Encoding.inst {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {b : Bool} : QuasiBorelSpace (Encoding A B b)

Equations

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

theorem QuasiBorelSpace.Sum.Encoding.isHom_inl {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom inl

theorem QuasiBorelSpace.Sum.Encoding.isHom_inr {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom inr

theorem QuasiBorelSpace.Sum.Encoding.isHom_elim {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → C} (hf : IsHom f) {g : B → C} (hg : IsHom g) : IsHom (elim f g)

def QuasiBorelSpace.Sum.encode {A : Type u_1} {B : Type u_2} : A ⊕ B → Sigma (Encoding A B)

Encodes an A ⊕ B as a Sigma (Encoding A B).

Equations

• QuasiBorelSpace.Sum.encode = Sum.elim QuasiBorelSpace.Sum.Encoding.inl QuasiBorelSpace.Sum.Encoding.inr

instance QuasiBorelSpace.Sum.instSum {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : QuasiBorelSpace (A ⊕ B)

Equations

• QuasiBorelSpace.Sum.instSum = QuasiBorelSpace.lift QuasiBorelSpace.Sum.encode

theorem QuasiBorelSpace.Sum.isHom_encode {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom encode

@[simp]

theorem QuasiBorelSpace.Sum.isHom_inl {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom Sum.inl

theorem QuasiBorelSpace.Sum.isHom_inl' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → B} (hf : IsHom f) : IsHom fun (x : A) => Sum.inl (f x)

@[simp]

theorem QuasiBorelSpace.Sum.isHom_inr {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom Sum.inr

theorem QuasiBorelSpace.Sum.isHom_inr' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → C} (hf : IsHom f) : IsHom fun (x : A) => Sum.inr (f x)

theorem QuasiBorelSpace.Sum.isHom_elim {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → C} (hf : IsHom f) {g : B → C} (hg : IsHom g) : IsHom (Sum.elim f g)

theorem QuasiBorelSpace.Sum.isHom_elim' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {D : Type u_4} [QuasiBorelSpace D] {f : A → B → D} (hf : IsHom fun (x : A × B) => f x.1 x.2) {g : A → C → D} (hg : IsHom fun (x : A × C) => g x.1 x.2) {h : A → B ⊕ C} (hh : IsHom h) : IsHom fun (x : A) => Sum.elim (f x) (g x) (h x)

theorem QuasiBorelSpace.Sum.isHom_map {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {D : Type u_4} [QuasiBorelSpace D] {E : Type u_5} [QuasiBorelSpace E] {f : A → B → D} (hf : IsHom fun (x : A × B) => f x.1 x.2) {g : A → C → E} (hg : IsHom fun (x : A × C) => g x.1 x.2) {h : A → B ⊕ C} (hh : IsHom h) : IsHom fun (x : A) => Sum.map (f x) (g x) (h x)

@[simp]

theorem QuasiBorelSpace.Sum.isHom_isLeft {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : IsHom Sum.isLeft

theorem OmegaQuasiBorelSpace.Sum.isHom_projl {A : Type u_1} {B : Type u_2} {C : Type u_3} [Preorder A] [QuasiBorelSpace A] [Preorder B] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : C → OmegaCompletePartialOrder.Chain (A ⊕ B)} (hf : QuasiBorelSpace.IsHom f) {g : C → A} (hg : QuasiBorelSpace.IsHom g) : QuasiBorelSpace.IsHom fun (x : C) => OmegaCompletePartialOrder.Chain.Sum.projl (f x)

theorem OmegaQuasiBorelSpace.Sum.isHom_projr {A : Type u_1} {B : Type u_2} {C : Type u_3} [Preorder A] [QuasiBorelSpace A] [Preorder B] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : C → OmegaCompletePartialOrder.Chain (A ⊕ B)} (hf : QuasiBorelSpace.IsHom f) {g : C → B} (hb : QuasiBorelSpace.IsHom g) : QuasiBorelSpace.IsHom fun (x : C) => OmegaCompletePartialOrder.Chain.Sum.projr (f x)

@[simp]

theorem OmegaQuasiBorelSpace.Sum.isHom_distrib {A : Type u_1} {B : Type u_2} [Preorder A] [QuasiBorelSpace A] [Preorder B] [QuasiBorelSpace B] : QuasiBorelSpace.IsHom OmegaCompletePartialOrder.Chain.Sum.distrib

noncomputable instance OmegaQuasiBorelSpace.Sum.instSum {A : Type u_1} {B : Type u_2} [OmegaQuasiBorelSpace A] [OmegaQuasiBorelSpace B] : OmegaQuasiBorelSpace (A ⊕ B)

Coproduct of omega quasi-borel spaces is again an omega quasi-borel space.

Equations

• OmegaQuasiBorelSpace.Sum.instSum = { toOmegaCompletePartialOrder := OmegaCompletePartialOrder.Sum.instSum_quasiBorelSpaces, toQuasiBorelSpace := QuasiBorelSpace.Sum.instSum, isHom_ωSup := ⋯ }