LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeExtensions

Auxiliary declarations for the Borel determinacy formalization.

@[reducible, inline]

abbrev Descriptive.Tree.mkPointedMor' {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (h : Fixing (↑y).length f := by all_goals as_aux_lemma => synthFixing) : mkPointed (pInv f y ⋯) ⟶ mkPointed y

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.mkPointedMor' f y h = { toLenHom := f, hp := ⋯ }

@[reducible, inline]

abbrev Descriptive.Tree.pointedResObj (k : ℕ) (T : PointedTrees) : PointedTrees

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.pointedResObj k T = ⟨(Descriptive.Tree.res k).obj T.fst, ⟨List.take k ↑T.snd, ⋯⟩⟩

def Descriptive.Tree.pointedRes (k : ℕ) : CategoryTheory.Functor PointedTrees PointedTrees

restriction of a pointed tree, obtained by replacing the base node by an ancestor if necessary

Equations

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

theorem Descriptive.Tree.pointedRes_isIso_iff_fixing (k : ℕ) {S T : PointedTrees} (f : S ⟶ T) : CategoryTheory.IsIso ((pointedRes k).map f) ↔ Fixing k (PointedLenHom.toHom f)

def Descriptive.Tree.extensionsRes (T : PointedTrees) : extensions.obj T ≃ extensions.obj ((pointedRes ((↑T.snd).length + 1)).obj T)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem Descriptive.Tree.extensionsRes_val' {T : Trees} {x : ↑↑T.snd} (a : ExtensionsAt x) : extensions.val' ((extensionsRes (mkPointed x)) a) = a.val'

@[simp]

theorem Descriptive.Tree.extensionsRes_res_valT' {T : Trees} {x : ↑↑T.snd} (a : ExtensionsAt x) : res.val' (extensions.valT' ((extensionsRes (mkPointed x)) a)) = a.valT'

@[simp]

theorem Descriptive.Tree.extensionsRes_symm_val' {T : Trees} {x : ↑↑T.snd} (a : extensions.obj ((pointedRes ((↑(mkPointed x).snd).length + 1)).obj (mkPointed x))) : ExtensionsAt.val' ((extensionsRes (mkPointed x)).symm a) = extensions.val' a

@[simp]

theorem Descriptive.Tree.cast_val' {k m : ℕ} {S : PointedTrees} (h : k = m) (a : extensions.obj ((pointedRes k).obj S)) : extensions.val' (cast ⋯ a) = extensions.val' a

noncomputable def Descriptive.Tree.pointedResIso {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) (hx : Fixing ((↑x).length + 1) f := by as_aux_lemma => synthFixing) : (pointedRes ((↑x).length + 1)).obj (mkPointed x) ≅ (pointedRes ((↑x).length + 1)).obj (mkPointed ((CategoryTheory.ConcreteCategory.hom f) x))

if f is (|x|+1)-fixing, then it induces a bijection on extensions of x

Equations

• Descriptive.Tree.pointedResIso f x hx = CategoryTheory.asIso ((Descriptive.Tree.pointedRes ((↑x).length + 1)).map (Descriptive.Tree.mkPointedMor f x))

noncomputable def Descriptive.Tree.extensionsEquiv {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) (hx : Fixing ((↑x).length + 1) f := by as_aux_lemma => synthFixing) : ExtensionsAt x ≃ ExtensionsAt ((CategoryTheory.ConcreteCategory.hom f) x)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem Descriptive.Tree.extensionsEquiv_val' {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) (a : ExtensionsAt x) (hx : Fixing ((↑x).length + 1) f) : ((extensionsEquiv f x hx) a).valT' = (CategoryTheory.ConcreteCategory.hom f) a.valT'

@[simp]

theorem Descriptive.Tree.extensionsEquiv_symm_val' {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) (hx : Fixing ((↑x).length + 1) f) (a : ExtensionsAt ((CategoryTheory.ConcreteCategory.hom f) x)) : ((extensionsEquiv f x hx).symm a).valT' = pInv f a.valT' ⋯

@[simp]

theorem Descriptive.Tree.ExtensionsAt.cast_valT' {A : Type u_1} {T : ↥(tree A)} {x y : ↥T} (h : x = y) (a : ExtensionsAt x) : (cast ⋯ a).valT' = a.valT'

noncomputable def Descriptive.Tree.pointedResIso' {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (hy : Fixing ((↑y).length + 1) f := by as_aux_lemma => synthFixing) : (pointedRes ((↑y).length + 1)).obj (mkPointed y) ≅ (pointedRes ((↑y).length + 1)).obj (mkPointed (pInv f y ⋯))

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.pointedResIso' f y hy = (CategoryTheory.asIso ((Descriptive.Tree.pointedRes ((↑y).length + 1)).map (Descriptive.Tree.mkPointedMor' f y ⋯))).symm

noncomputable def Descriptive.Tree.extensionsEquiv' {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (hy : Fixing ((↑y).length + 1) f := by as_aux_lemma => synthFixing) : ExtensionsAt y ≃ ExtensionsAt (pInv f y ⋯)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.extensionsEquiv' f y hy = ((Descriptive.Tree.extensionsEquiv f (Descriptive.Tree.pInv f y ⋯) ⋯).trans (Equiv.cast ⋯)).symm

@[simp]

theorem Descriptive.Tree.extensionsEquiv'_symm_val' {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (hy : Fixing ((↑y).length + 1) f) (a : ExtensionsAt (pInv f y ⋯)) : ((extensionsEquiv' f y hy).symm a).valT' = (CategoryTheory.ConcreteCategory.hom f) a.valT'

@[simp]

theorem Descriptive.Tree.extensionsEquiv'_val' {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (a : ExtensionsAt y) (hy : Fixing ((↑y).length + 1) f) : ((extensionsEquiv' f y hy) a).valT' = pInv f a.valT' ⋯

@[simp]

theorem Descriptive.Tree.val_res_zero {S : Trees} (x : ↑↑((res 0).obj S).snd) : ↑x = []

theorem Descriptive.Tree.zero_fixing {S T : Trees} (f : S ⟶ T) : Fixing 0 f ↔ ([] ∈ S.snd ↔ [] ∈ T.snd)

theorem Descriptive.Tree.lim_isPruned (F : CategoryTheory.Functor ℕᵒᵖ Trees) (hF : ∀ (n : ℕ), Fixing n (F.map (CategoryTheory.homOfLE ⋯).op)) (h : ∀ (n : ℕ), IsPruned (F.obj (Opposite.op n)).snd) : IsPruned (limCone F).pt.snd

theorem Descriptive.Tree.lim_ne (F : CategoryTheory.Functor ℕᵒᵖ Trees) (hF : ∀ (n : ℕ), Fixing n (F.map (CategoryTheory.homOfLE ⋯).op)) (h : ∀ (n : ℕ), [] ∈ (F.obj (Opposite.op n)).snd) : [] ∈ (limCone F).pt.snd