LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeLim

Auxiliary declarations for the Borel determinacy formalization.

def Descriptive.Tree.constTreeObj (k : ℕ) (A : Type u_3) : ↥(tree A)

Object function of adjoint of res k

Equations

• Descriptive.Tree.constTreeObj k A = ⟨{x : List A | ∃ m ≤ k, x ∈ Set.range (List.replicate m)}, ⋯⟩

@[simp]

theorem Descriptive.Tree.mem_constTree {A : Type u_1} {m k : ℕ} (a : A) (h : m ≤ k) : List.replicate m a ∈ constTreeObj k A

noncomputable def Descriptive.Tree.headD {A : Type u_1} {k : ℕ} (x : ↥(constTreeObj k A)) : A

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.headD x = Exists.choose ⋯

@[simp]

theorem Descriptive.Tree.eq_replicate_headD {A : Type u_1} {k : ℕ} (x : ↥(constTreeObj k A)) : List.replicate (↑x).length (headD x) = ↑x

theorem Descriptive.Tree.headD_nonempty {A : Type u_1} {k : ℕ} (x : ↥(constTreeObj k A)) (h : ↑x ≠ []) : headD x = (↑x).head h

@[simp]

theorem Descriptive.Tree.constTree_length {A : Type u_1} {k : ℕ} (x : ↥(constTreeObj k A)) : (↑x).length ≤ k

@[simp]

theorem Descriptive.Tree.constTree_zero {A : Type u_1} (x : ↥(constTreeObj 0 A)) : ↑x = []

def Descriptive.Tree.constTree (k : ℕ) : CategoryTheory.Functor (Type u_3) Trees

Adjoint of res k

Equations

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

@[simp]

theorem Descriptive.Tree.head_constTree_map {A B : Type u_1} (k : ℕ) (f : A ⟶ B) {x : ↥(constTreeObj k A)} (h : ↑x ≠ []) : (↑((CategoryTheory.ConcreteCategory.hom ((constTree k).map f)) x)).head ⋯ = (CategoryTheory.ConcreteCategory.hom f) ((↑x).head h)

def Descriptive.Tree.resEqUnit (k : ℕ) : CategoryTheory.Functor.id (Type u_3) ⟶ (constTree k).comp (resEq k)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.resEqUnit k = { app := fun (x : Type ?u.1) => TypeCat.ofHom fun (a : (CategoryTheory.Functor.id (Type ?u.1)).obj x) => ⟨List.replicate k a, ⋯⟩, naturality := ⋯ }

noncomputable def Descriptive.Tree.resEqCounitComp (k : ℕ) (T : Trees) : (constTree k).obj ((resEq k).obj T) ⟶ T

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

noncomputable def Descriptive.Tree.resEqCounit (k : ℕ) : (resEq k).comp (constTree k) ⟶ CategoryTheory.Functor.id Trees

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.resEqCounit k = { app := Descriptive.Tree.resEqCounitComp k, naturality := ⋯ }

noncomputable def Descriptive.Tree.resEqAdj (k : ℕ) : constTree k ⊣ resEq k

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

instance Descriptive.Tree.instIsRightAdjointTreesResEq (k : ℕ) : (resEq k).IsRightAdjoint

instance Descriptive.Tree.instPreservesLimitsOfSizeTreesResEq (k : ℕ) : CategoryTheory.Limits.PreservesLimitsOfSize.{u_3, u_4, u_5, u_5, u_5 + 1, u_5 + 1} (resEq k)

def Descriptive.Tree.limObj {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) : ↥(tree ((j : J) → (F.obj j).fst))

Object function of limit functor in Trees

Equations

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

def Descriptive.Tree.limCone {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) : CategoryTheory.Limits.Cone F

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def Descriptive.Tree.coneZip {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) (s : CategoryTheory.Limits.Cone F) (x : ↑↑s.pt.snd) : List ((j : J) → (F.obj j).fst)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.coneZip F s x = List.zipFun (fun (j : J) => ↑((CategoryTheory.ConcreteCategory.hom (s.π.app j)) x)) ⋯

@[simp]

theorem Descriptive.Tree.coneZip_mapEval {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) (s : CategoryTheory.Limits.Cone F) (x : ↑↑s.pt.snd) (j : J) : List.mapEval j (coneZip F s x) = ↑((CategoryTheory.ConcreteCategory.hom (s.π.app j)) x)

@[simp]

theorem Descriptive.Tree.coneZip_length {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) (s : CategoryTheory.Limits.Cone F) (x : ↑↑s.pt.snd) : (coneZip F s x).length = (↑x).length

def Descriptive.Tree.isLimitLift {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) (s : CategoryTheory.Limits.Cone F) : s.pt ⟶ (limCone F).pt

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.isLimitLift F s = { toFun := fun (x : ↑↑s.pt.snd) => ⟨Descriptive.Tree.coneZip F s x, ⋯⟩, monotone' := ⋯, h_length := ⋯ }

def Descriptive.Tree.isLimit {J : Type} [CategoryTheory.Category.{u_3, 0} J] (F : CategoryTheory.Functor J Trees) : CategoryTheory.Limits.IsLimit (limCone F)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.isLimit F = { lift := Descriptive.Tree.isLimitLift F, fac := ⋯, uniq := ⋯ }

theorem Descriptive.Tree.proj_fixing (F : CategoryTheory.Functor ℕᵒᵖ Trees) (k : ℕ) (hF : ∀ (n : ℕ), Fixing (k + n) (F.map (CategoryTheory.homOfLE ⋯).op)) (n : ℕ) : Fixing (k + n) ((limCone F).π.app (Opposite.op n))