LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.LenTreeHom

Auxiliary declarations for the Borel determinacy formalization.

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

The objects of the category of trees

Equations

• Descriptive.Tree.Trees = ((A : Type ?u.1) × ↥(Descriptive.tree A))

@[implicit_reducible]

instance Descriptive.Tree.instCoeSortTreesType : CoeSort Trees (Type u_1)

Equations

• Descriptive.Tree.instCoeSortTreesType = { coe := fun (S : Descriptive.Tree.Trees) => ↑↑S.snd }

structure Descriptive.Tree.LenHom (S : Trees) (T : Trees) extends ↑↑S.snd →o ↑↑T.snd : Type (max u_1 u_2)

The morphisms in the category of trees, length-preserving order-preserving maps

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

theorem Descriptive.Tree.LenHom.ext {S : Trees} {T : Trees} {x y : LenHom S T} (toFun : x.toFun = y.toFun) : x = y

theorem Descriptive.Tree.LenHom.ext_iff {S : Trees} {T : Trees} {x y : LenHom S T} : x = y ↔ x.toFun = y.toFun

@[implicit_reducible]

instance Descriptive.Tree.instCategoryTrees : CategoryTheory.Category.{u_1, u_1 + 1} Trees

The category of trees has as objects trees in some set of nodes and as morphisms length-preserving order-preserving maps. It is a topos (although this fact is not proved here). Namely, the map to Presheaves on ℕ such that evaluation becomes resEq and the transition maps are given by List.take induces an equivalence

Equations

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

def Descriptive.Tree.forgetPO : CategoryTheory.Functor Trees PartOrd

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

instance Descriptive.Tree.instFaithfulTreesPartOrdForgetPO : forgetPO.Faithful

@[implicit_reducible]

instance Descriptive.Tree.instFunLikeHomTreesElemListFstSubtypeSetMemCompleteSublatticeTreeValSnd {S T : Trees} : FunLike (S ⟶ T) ↑↑S.snd ↑↑T.snd

Equations

• Descriptive.Tree.instFunLikeHomTreesElemListFstSubtypeSetMemCompleteSublatticeTreeValSnd = { coe := fun (f : S ⟶ T) => f.toFun, coe_injective := ⋯ }

instance Descriptive.Tree.instOrderHomClassHomTreesElemListFstSubtypeSetMemCompleteSublatticeTreeValSnd {S T : Trees} : OrderHomClass (S ⟶ T) ↑↑S.snd ↑↑T.snd

@[implicit_reducible]

instance Descriptive.Tree.instConcreteCategoryTreesHomElemListFstSubtypeSetMemCompleteSublatticeTreeValSnd : CategoryTheory.ConcreteCategory Trees fun (S T : Trees) => S ⟶ T

Equations

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

@[simp]

theorem Descriptive.Tree.rem_lenHom {S T : Trees} : LenHom S T = (S ⟶ T)

theorem Descriptive.Tree.tree_ext {S : Trees} {x y : ↑↑S.snd} (h : ↑x = ↑y) : x = y

theorem Descriptive.Tree.tree_ext_iff {S : Trees} {x y : ↑↑S.snd} : x = y ↔ ↑x = ↑y

@[implicit_reducible]

instance Descriptive.Tree.instPartialOrderTreeElement {S : Trees} : PartialOrder ↑↑S.snd

Equations

• Descriptive.Tree.instPartialOrderTreeElement = inferInstance

@[simp]

theorem Descriptive.Tree.le_def_trees {T : Trees} (x y : ↑↑T.snd) : x ≤ y ↔ ↑x <+: ↑y

@[simp]

theorem Descriptive.Tree.rem_toOrderHom {S T : Trees} (f : S ⟶ T) : ⇑f.toOrderHom = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem Descriptive.Tree.rem_toFun {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) : f.toFun x = (CategoryTheory.ConcreteCategory.hom f) x

@[simp]

theorem Descriptive.Tree.forget_map {S T : Trees} (f : S ⟶ T) : (CategoryTheory.forget Trees).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem Descriptive.Tree.LenHom.id_toFun (S : Trees) : (CategoryTheory.CategoryStruct.id S).toFun = id

theorem Descriptive.Tree.LenHom.comp_toFun {S T U : Trees} (f : S ⟶ T) (g : T ⟶ U) : (CategoryTheory.CategoryStruct.comp f g).toFun = g.toFun ∘ f.toFun

instance Descriptive.Tree.LenHom.instIsIsoElemListFstSubtypeSetMemCompleteSublatticeTreeValSndOfHomToFunOfTrees {S T : Trees} (f : S ⟶ T) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (TypeCat.ofHom f.toFun)

theorem Descriptive.Tree.LenHom.inv_toFun {S T : Trees} (f : S ⟶ T) [CategoryTheory.IsIso f] : (CategoryTheory.inv f).toFun = ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv (TypeCat.ofHom f.toFun)))

@[simp]

theorem Descriptive.Tree.LenHom.h_length_simp {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) : (↑((CategoryTheory.ConcreteCategory.hom f) x)).length = (↑x).length

theorem Descriptive.Tree.LenHom.h_length_inv {S T : Trees} (f : S ⟶ T) [CategoryTheory.IsIso (TypeCat.ofHom f.toFun)] (x : ↑↑T.snd) : (↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv (TypeCat.ofHom f.toFun))) x)).length = (↑x).length

@[simp]

theorem Descriptive.Tree.LenHom.map_nil {S T : Trees} (f : S ⟶ T) (h : [] ∈ S.snd) : ↑((CategoryTheory.ConcreteCategory.hom f) ⟨[], h⟩) = []

theorem Descriptive.Tree.LenHom.map_ne_nil {S T : Trees} (f : S ⟶ T) {x : ↑↑S.snd} (h : ↑x ≠ []) : ↑((CategoryTheory.ConcreteCategory.hom f) x) ≠ []

theorem Descriptive.Tree.LenHom.mk_eval (S T : Trees) (f : ↑↑S.snd → ↑↑T.snd) (hf1 : Monotone f) (hf2 : ∀ (x : ↥S.snd), (↑({ toFun := f, monotone' := hf1 }.toFun x)).length = (↑x).length) (x : ↑↑S.snd) : { toFun := f, monotone' := hf1, h_length := hf2 } x = f x

theorem Descriptive.Tree.take_apply {S T : Trees} (f : S ⟶ T) (n : ℕ) (x : ↑↑S.snd) : (CategoryTheory.ConcreteCategory.hom f) (take n x) = take n ((CategoryTheory.ConcreteCategory.hom f) x)

theorem Descriptive.Tree.take_apply_val {S T : Trees} (f : S ⟶ T) (n : ℕ) (x : ↑↑S.snd) : ↑((CategoryTheory.ConcreteCategory.hom f) (take n x)) = List.take n ↑((CategoryTheory.ConcreteCategory.hom f) x)

theorem Descriptive.Tree.prefix_iff {S T : Trees} (f : S ⟶ T) (x y : (fun (S : Trees) => ↑↑S.snd) S) (hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)) : (CategoryTheory.ConcreteCategory.hom f) x ≤ (CategoryTheory.ConcreteCategory.hom f) y ↔ x ≤ y

instance Descriptive.Tree.instReflectsIsomorphismsTreesForgetHomElemListFstSubtypeSetMemCompleteSublatticeTreeValSnd : (CategoryTheory.forget Trees).ReflectsIsomorphisms