LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.PointedTrees

Auxiliary declarations for the Borel determinacy formalization.

def Descriptive.Tree.PointedTrees : Type (u_1 + 1)

A tree with a chosen base node

Equations

• Descriptive.Tree.PointedTrees = ((T : Descriptive.Tree.Trees) × ↑↑T.snd)

structure Descriptive.Tree.PointedLenHom (S : PointedTrees) (T : PointedTrees) extends Descriptive.Tree.LenHom S.fst T.fst : Type (max u_1 u_2)

a base node preserving morphism of trees

• toFun : ↑↑S.fst.snd → ↑↑T.fst.snd
• monotone' : Monotone self.toFun
• h_length (x : ↥S.fst.snd) : (↑(self.toFun x)).length = (↑x).length
• hp : self.toFun S.snd = T.snd

theorem Descriptive.Tree.PointedLenHom.ext {S : PointedTrees} {T : PointedTrees} {x y : PointedLenHom S T} (toLenHom : x.toLenHom = y.toLenHom) : x = y

theorem Descriptive.Tree.PointedLenHom.ext_iff {S : PointedTrees} {T : PointedTrees} {x y : PointedLenHom S T} : x = y ↔ x.toLenHom = y.toLenHom

def Descriptive.Tree.PointedLenHom.toHom {S T : PointedTrees} (f : PointedLenHom S T) : S.fst ⟶ T.fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

• f.toHom = f.toLenHom

@[implicit_reducible]

instance Descriptive.Tree.PointedLenHom.instFunLikeElemListFstSubtypeSetMemCompleteSublatticeTreeTreesValSnd {S T : PointedTrees} : FunLike (PointedLenHom S T) ↑↑S.fst.snd ↑↑T.fst.snd

Equations

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

instance Descriptive.Tree.PointedLenHom.instOrderHomClassElemListFstSubtypeSetMemCompleteSublatticeTreeTreesValSnd {S T : PointedTrees} : OrderHomClass (PointedLenHom S T) ↑↑S.fst.snd ↑↑T.fst.snd

@[simp]

theorem Descriptive.Tree.PointedLenHom.add_toHom {S T : PointedTrees} (f : PointedLenHom S T) (x : ↑↑S.fst.snd) : f x = (CategoryTheory.ConcreteCategory.hom f.toHom) x

@[implicit_reducible]

instance Descriptive.Tree.PointedLenHom.instCategoryPointedTrees : CategoryTheory.Category.{u_1, u_1 + 1} PointedTrees

The category of trees with a chosen base node

Equations

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

theorem Descriptive.Tree.PointedLenHom.ext' {S T : PointedTrees} {f g : S ⟶ T} (h : f.toLenHom = g.toLenHom) : f = g

theorem Descriptive.Tree.PointedLenHom.ext'_iff {S T : PointedTrees} {f g : S ⟶ T} : f = g ↔ f.toLenHom = g.toLenHom

@[simp]

theorem Descriptive.Tree.PointedLenHom.rem_pointedLenHom {S T : PointedTrees} : PointedLenHom S T = (S ⟶ T)

@[simp]

theorem Descriptive.Tree.PointedLenHom.rem_toLenHom' {S T : PointedTrees} (f : S ⟶ T) (x : ↑↑S.fst.snd) : f.toLenHom x = (CategoryTheory.ConcreteCategory.hom (toHom f)) x

@[simp]

theorem Descriptive.Tree.PointedLenHom.pair_toHom {S T : PointedTrees} (f : S.fst ⟶ T.fst) (hf : f.toFun S.snd = T.snd) : { toLenHom := f, hp := hf }.toHom = f

@[simp]

theorem Descriptive.Tree.PointedLenHom.hp_simp {S T : PointedTrees} (f : S ⟶ T) : (CategoryTheory.ConcreteCategory.hom (toHom f)) S.snd = T.snd

@[simp]

theorem Descriptive.Tree.PointedLenHom.id_toLenHom (S : PointedTrees) : toHom (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.fst

@[simp]

theorem Descriptive.Tree.PointedLenHom.comp_toLenHom {S T U : PointedTrees} (f : S ⟶ T) (g : T ⟶ U) : toHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toHom f) (toHom g)

@[reducible, inline]

abbrev Descriptive.Tree.forgetPoint : CategoryTheory.Functor PointedTrees Trees

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

instance Descriptive.Tree.instReflectsIsomorphismsPointedTreesTreesForgetPoint : forgetPoint.ReflectsIsomorphisms

@[simp]

theorem Descriptive.Tree.pointed_isIso_iff {S T : PointedTrees} (f : S ⟶ T) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (forgetPoint.map f)

theorem Descriptive.Tree.apply_concat {S T : Trees} {x : List S.fst} {a : S.fst} (f : S ⟶ T) (hx : x ++ [a] ∈ S.snd) : ∃ (b : T.fst), ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x ++ [a], hx⟩) = ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x, ⋯⟩) ++ [b]

noncomputable def Descriptive.Tree.concat {S T : Trees} {x : List S.fst} {a : S.fst} (f : S ⟶ T) (hx : x ++ [a] ∈ S.snd) : T.fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.concat f hx = ⋯.choose

theorem Descriptive.Tree.concat_spec {S T : Trees} {x : List S.fst} {a : S.fst} (f : S ⟶ T) (hx : x ++ [a] ∈ S.snd) : ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x ++ [a], hx⟩) = ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x, ⋯⟩) ++ [concat f hx]

theorem Descriptive.Tree.concat_elem {S T : Trees} {x : List S.fst} {a : S.fst} (f : S ⟶ T) (hx : x ++ [a] ∈ S.snd) : ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x, ⋯⟩) ++ [concat f hx] ∈ T.snd

theorem Descriptive.Tree.concat_spec' {S T : Trees} {x : List S.fst} {a : S.fst} (f : S ⟶ T) (hx : x ++ [a] ∈ S.snd) : (CategoryTheory.ConcreteCategory.hom f) ⟨x ++ [a], hx⟩ = ⟨↑((CategoryTheory.ConcreteCategory.hom f) ⟨x, ⋯⟩) ++ [concat f hx], ⋯⟩

theorem Descriptive.Tree.concat_uniq {S T : Trees} {x : List S.fst} {a : S.fst} (f : S ⟶ T) (hx : x ++ [a] ∈ S.snd) (b : T.fst) (hb : ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x, ⋯⟩) ++ [b] = ↑((CategoryTheory.ConcreteCategory.hom f) ⟨x ++ [a], hx⟩)) : concat f hx = b

noncomputable def Descriptive.Tree.extensions : CategoryTheory.Functor PointedTrees (Type u_1)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def Descriptive.Tree.extensions.val' {T : PointedTrees} (a : extensions.obj T) : List T.fst.fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.extensions.val' a = ↑T.snd ++ [↑a]

def Descriptive.Tree.extensions.valT' {T : PointedTrees} (a : extensions.obj T) : ↑↑T.fst.snd

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.extensions.valT' a = ⟨Descriptive.Tree.extensions.val' a, ⋯⟩

@[simp]

theorem Descriptive.Tree.extensions.valT'_coe {T : PointedTrees} (a : extensions.obj T) : ↑(valT' a) = val' a

@[simp]

theorem Descriptive.Tree.extensions_map_val' {S T : PointedTrees} (f : S ⟶ T) (a : extensions.obj S) : extensions.val' ((CategoryTheory.ConcreteCategory.hom (extensions.map f)) a) = ↑((CategoryTheory.ConcreteCategory.hom (PointedLenHom.toHom f)) ⟨extensions.val' a, ⋯⟩)

@[simp]

theorem Descriptive.Tree.extensions_map_valT' {S T : PointedTrees} (f : S ⟶ T) (a : extensions.obj S) : extensions.valT' ((CategoryTheory.ConcreteCategory.hom (extensions.map f)) a) = (CategoryTheory.ConcreteCategory.hom (PointedLenHom.toHom f)) ⟨extensions.val' a, ⋯⟩

@[reducible, inline]

abbrev Descriptive.Tree.mkPointed {T : Trees} (x : ↑↑T.snd) : PointedTrees

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.mkPointed x = ⟨T, x⟩

def Descriptive.Tree.mkPointedMor {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) : mkPointed x ⟶ mkPointed ((CategoryTheory.ConcreteCategory.hom f) x)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.mkPointedMor f x = { toLenHom := f, hp := ⋯ }

theorem Descriptive.Tree.ExtensionsAt.eq_obj {T : Trees} (x : ↑↑T.snd) : ExtensionsAt x = extensions.obj (mkPointed x)

@[reducible, inline]

noncomputable abbrev Descriptive.Tree.ExtensionsAt.map {S T : Trees} (f : S ⟶ T) ⦃x : ↑↑S.snd⦄ ⦃y : ↑↑T.snd⦄ (h : (CategoryTheory.ConcreteCategory.hom f) x = y) (a : ExtensionsAt x) : ExtensionsAt y

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.ExtensionsAt.map f h a = (CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.extensions.map { toLenHom := f, hp := h })) a

@[simp]

theorem Descriptive.Tree.ExtensionsAt.map_val' {S T : Trees} (f : S ⟶ T) ⦃x : ↑↑S.snd⦄ ⦃y : ↑↑T.snd⦄ (h : (CategoryTheory.ConcreteCategory.hom f) x = y) (a : ExtensionsAt x) : (map f h a).val' = ↑((CategoryTheory.ConcreteCategory.hom f) a.valT')

@[simp]

theorem Descriptive.Tree.ExtensionsAt.map_valT' {S T : Trees} (f : S ⟶ T) ⦃x : ↑↑S.snd⦄ ⦃y : ↑↑T.snd⦄ (h : (CategoryTheory.ConcreteCategory.hom f) x = y) (a : ExtensionsAt x) : (map f h a).valT' = (CategoryTheory.ConcreteCategory.hom f) a.valT'