LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.RestrictTree

Auxiliary declarations for the Borel determinacy formalization.

def Descriptive.Tree.res (k : ℕ) : CategoryTheory.Functor Trees Trees

Remove all nodes of a tree beyond level k

Equations

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

@[simp]

theorem Descriptive.Tree.res_obj_fst (k : ℕ) (S : Trees) : ((res k).obj S).fst = S.fst

theorem Descriptive.Tree.res_ext {S : Trees} {k : ℕ} (x y : ↑↑((res k).obj S).snd) (h : ↑x = ↑y) : x = y

theorem Descriptive.Tree.res_ext_iff {S : Trees} {k : ℕ} {x y : ↑↑((res k).obj S).snd} : x = y ↔ ↑x = ↑y

@[simp]

theorem Descriptive.Tree.mem_res_obj {T : Trees} {k : ℕ} (x : List T.fst) : x ∈ ((res k).obj T).snd ↔ x ∈ T.snd ∧ x.length ≤ k

def Descriptive.Tree.resEq (k : ℕ) : CategoryTheory.Functor Trees (Type u_1)

Remove all nodes of a tree not on level exactly k

Equations

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

@[simp]

theorem Descriptive.Tree.resEq_map (k : ℕ) {X✝ Y✝ : Trees} (f : X✝ ⟶ Y✝) : (resEq k).map f = TypeCat.ofHom fun (x : ↑{x : List X✝.fst | x ∈ X✝.snd ∧ x.length = k}) => ⟨↑((CategoryTheory.ConcreteCategory.hom f) ⟨↑x, ⋯⟩), ⋯⟩

theorem Descriptive.Tree.resEq_ext {S : Trees} {k : ℕ} (x y : (resEq k).obj S) (h : ↑x = ↑y) : x = y

theorem Descriptive.Tree.resEq_ext_iff {S : Trees} {k : ℕ} {x y : (resEq k).obj S} : x = y ↔ ↑x = ↑y

theorem Descriptive.Tree.resEq_ext_hEq {T : Trees} {k m : ℕ} (x : (resEq k).obj T) (y : (resEq m).obj T) (h' : ↑x = ↑y) : x ≍ y

@[simp]

theorem Descriptive.Tree.res_mem {S : Trees} {k : ℕ} (x : ↑↑((res k).obj S).snd) : ↑x ∈ S.snd

Auxiliary declaration for the Borel determinacy formalization.

def Descriptive.Tree.res.val' {S : Trees} {k : ℕ} (x : ↑↑((res k).obj S).snd) : ↑↑S.snd

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.res.val' x = ⟨↑x, ⋯⟩

@[simp]

theorem Descriptive.Tree.res.val'_coe {S : Trees} {k : ℕ} (x : ↑↑((res k).obj S).snd) : ↑(val' x) = ↑x

theorem Descriptive.Tree.res.ext_val' {S : Trees} {k : ℕ} {x y : ↑↑((res k).obj S).snd} (h : val' x = val' y) : x = y

@[simp]

theorem Descriptive.Tree.res_val {S T : Trees} (f : S ⟶ T) (k : ℕ) (x : (fun (S : Trees) => ↑↑S.snd) ((res k).obj S)) : ↑((CategoryTheory.ConcreteCategory.hom ((res k).map f)) x) = ↑((CategoryTheory.ConcreteCategory.hom f) (res.val' x))

@[simp]

theorem Descriptive.Tree.res_val'_val {S : Trees} {k : ℕ} (x : ↑↑S.snd) (h : ↑x ∈ ↑((res k).obj S).snd) : res.val' ⟨↑x, h⟩ = x

@[simp]

theorem Descriptive.Tree.res_len_le {S : Trees} {k : ℕ} (x : ↑↑((res k).obj S).snd) : (↑x).length ≤ k

@[simp]

theorem Descriptive.Tree.resEq_mem {S : Trees} {k : ℕ} (x : (resEq k).obj S) : ↑x ∈ S.snd

Auxiliary declaration for the Borel determinacy formalization.

def Descriptive.Tree.resEq.val' {S : Trees} {k : ℕ} (x : (resEq k).obj S) : ↑↑S.snd

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.resEq.val' x = ⟨↑x, ⋯⟩

@[simp]

theorem Descriptive.Tree.resEq.val'_coe {S : Trees} {k : ℕ} (x : (resEq k).obj S) : ↑(val' x) = ↑x

theorem Descriptive.Tree.resEq.ext_val' {S : Trees} {k : ℕ} {x y : (resEq k).obj S} (h : val' x = val' y) : x = y

theorem Descriptive.Tree.resEq_val {S T : Trees} (f : S ⟶ T) (k : ℕ) (x : (fun (X : Type u_1) => X) ((resEq k).obj S)) : ↑((CategoryTheory.ConcreteCategory.hom ((resEq k).map f)) x) = ↑((CategoryTheory.ConcreteCategory.hom f) (resEq.val' x))

@[simp]

theorem Descriptive.Tree.resEq_val'_val {S : Trees} {k : ℕ} (x : ↑↑S.snd) (h : ↑x ∈ {x : List S.fst | x ∈ S.snd ∧ x.length = k}) : resEq.val' ⟨↑x, h⟩ = x

@[simp]

theorem Descriptive.Tree.resEq_len {T : Trees} (k : ℕ) (x : (resEq k).obj T) : (↑x).length = k

def Descriptive.Tree.resIncl {k m : ℕ} (h : k ≤ m) : resEq k ⟶ (res m).comp (CategoryTheory.forget Trees)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.resIncl h = { app := fun (x : Descriptive.Tree.Trees) => TypeCat.ofHom fun (x_1 : (Descriptive.Tree.resEq k).obj x) => ⟨↑x_1, ⋯⟩, naturality := ⋯ }

theorem Descriptive.Tree.resIncl_len {S : Trees} {k m : ℕ} (h : k ≤ m) (x : (fun (X : Type u_1) => X) ((resEq k).obj S)) : (↑((CategoryTheory.ConcreteCategory.hom ((resIncl h).app S)) x)).length = k

def Descriptive.Tree.resCocone (k : ℕ) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor fun (i : Fin (k + 1)) => resEq ↑i)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

noncomputable def Descriptive.Tree.resIsColimit (k : ℕ) : CategoryTheory.Limits.IsColimit (resCocone k)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def Descriptive.Tree.evResCocone (k : ℕ) (S : Trees) : CategoryTheory.Limits.Cocone ((CategoryTheory.Discrete.functor fun (i : Fin (k + 1)) => resEq ↑i).comp ((CategoryTheory.evaluation Trees (Type u_1)).obj S))

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

noncomputable def Descriptive.Tree.evResIsColimit (k : ℕ) (S : Trees) : CategoryTheory.Limits.IsColimit (evResCocone k S)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.evResIsColimit k S = CategoryTheory.Limits.isColimitOfPreserves ((CategoryTheory.evaluation Descriptive.Tree.Trees (Type ?u.1)).obj S) (Descriptive.Tree.resIsColimit k)

class Descriptive.Tree.Fixing {S T : Trees} (k : outParam ℕ) (f : S ⟶ T) : Prop

A morphism is k-fixing if it is a bijection on the first k levels

• prop : CategoryTheory.IsIso ((res k).map f)

instance Descriptive.Tree.instIsIsoTreesMapResOfFixing {S T : Trees} {k : ℕ} (f : S ⟶ T) [h : Fixing k f] : CategoryTheory.IsIso ((res k).map f)

class Descriptive.Tree.FixingEq {S T : Trees} (k : outParam ℕ) (f : S ⟶ T) : Prop

Whether a morphism is a bijection on level k

• prop : CategoryTheory.IsIso ((resEq k).map f)

instance Descriptive.Tree.instIsIsoObjTreesResEqMapOfFixingEq {S T : Trees} {k : ℕ} (f : S ⟶ T) [h : FixingEq k f] : CategoryTheory.IsIso ((resEq k).map f)

theorem Descriptive.Tree.fixing_iff_forget_isIso {S T : Trees} (k : ℕ) (f : S ⟶ T) : Fixing k f ↔ CategoryTheory.IsIso (((res k).comp (CategoryTheory.forget Trees)).map f)

theorem Descriptive.Tree.Fixing.bijective {S T : Trees} {k : ℕ} {f : S ⟶ T} (h : Fixing k f) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((res k).map f))

theorem Descriptive.Tree.fixing_iff_fixingEq {S T : Trees} (k : ℕ) (f : S ⟶ T) : Fixing k f ↔ ∀ n ≤ k, FixingEq n f

theorem Descriptive.Tree.Fixing.mon {S T : Trees} {k n : ℕ} {f : S ⟶ T} (h : Fixing k f) (hn : n ≤ k) : Fixing n f

theorem Descriptive.Tree.fixing_iso {S T : Trees} {f : S ⟶ T} [CategoryTheory.IsIso f] {k : ℕ} : Fixing k f

instance Descriptive.Tree.fixing_comp {S T U : Trees} {k : ℕ} {f : S ⟶ T} {g : T ⟶ U} [h : Fixing k f] [h' : Fixing k g] : Fixing k (CategoryTheory.CategoryStruct.comp f g)

def Descriptive.Tree.tacticSynthFixing : Lean.ParserDescr

Tactic support used by the Borel determinacy formalization.

Equations

• Descriptive.Tree.tacticSynthFixing = Lean.ParserDescr.node `Descriptive.Tree.tacticSynthFixing 1024 (Lean.ParserDescr.nonReservedSymbol "synthFixing" false)

instance Descriptive.Tree.fixingEq_of_fixing {S T : Trees} {k : ℕ} {f : S ⟶ T} [h : Fixing k f] : FixingEq k f

theorem Descriptive.Tree.Fixing.inj {S T : Trees} (f : S ⟶ T) (x y : ↑↑S.snd) (ht : Fixing (↑x).length f := by as_aux_lemma => synthFixing) (he : (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) y) : x = y

noncomputable def Descriptive.Tree.pInv {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (h : Fixing (↑y).length f := by as_aux_lemma => synthFixing) : ↑↑S.snd

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.pInv f y h = Descriptive.Tree.res.val' ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((Descriptive.Tree.res (↑y).length).map f))) ⟨↑y, ⋯⟩)

@[simp]

theorem Descriptive.Tree.h_length_pInv {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (h : Fixing (↑y).length f) : (↑(pInv f y h)).length = (↑y).length

@[simp]

theorem Descriptive.Tree.cancel_pInv_left {S T : Trees} (f : S ⟶ T) (x : ↑↑S.snd) (h : Fixing (↑((CategoryTheory.ConcreteCategory.hom f) x)).length f) : pInv f ((CategoryTheory.ConcreteCategory.hom f) x) h = x

@[simp]

theorem Descriptive.Tree.cancel_pInv_right {S T : Trees} (f : S ⟶ T) (y : ↑↑T.snd) (h : Fixing (↑y).length f) : (CategoryTheory.ConcreteCategory.hom f) (pInv f y h) = y

@[simp]

theorem Descriptive.Tree.pInv_id {S : Trees} (x : ↑↑S.snd) : pInv (CategoryTheory.CategoryStruct.id S) x ⋯ = x

@[simp]

theorem Descriptive.Tree.pInv_comp {S T U : Trees} (f : S ⟶ T) (g : T ⟶ U) (y : ↑↑U.snd) (hg : Fixing (↑y).length g := by as_aux_lemma => synthFixing) (hf : Fixing (↑y).length f := by as_aux_lemma => synthFixing) : pInv (CategoryTheory.CategoryStruct.comp f g) y ⋯ = pInv f (pInv g y hg) ⋯

theorem Descriptive.Tree.pInv_comp' {S T U : Trees} (f : S ⟶ T) (g : T ⟶ U) (y : ↑↑U.snd) (hg : Fixing (↑y).length g) (hf : Fixing (↑(pInv g y hg)).length f) : pInv (CategoryTheory.CategoryStruct.comp f g) y ⋯ = pInv f (pInv g y hg) hf

theorem Descriptive.Tree.take_apply_pInv {n : ℕ} {S T : Trees} (f : S ⟶ T) (x : ↥T.snd) (h : Fixing (↑x).length f) : pInv f (take n x) ⋯ = take n (pInv f x h)

theorem Descriptive.Tree.take_apply_pInv_val {n : ℕ} {S T : Trees} (f : S ⟶ T) (x : ↥T.snd) (h : Fixing (↑x).length f) : ↑(pInv f (take n x) ⋯) = List.take n ↑(pInv f x h)

@[simp]

theorem Descriptive.Tree.inv_val'_eq_pInv {k : ℕ} {S T : Trees} (f : S ⟶ T) (x : (fun (S : Trees) => ↑↑S.snd) ((res k).obj T)) (h : Fixing k f := by as_aux_lemma => synthFixing) : res.val' ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((res k).map f))) x) = pInv f (res.val' x) ⋯

theorem Descriptive.Tree.inv_val'_eq_pInv' {k : ℕ} {S T : Trees} (f : S ⟶ T) (x : (fun (X : Type u_1) => X) ((resEq k).obj T)) (h : Fixing k f := by as_aux_lemma => synthFixing) : resEq.val' ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((resEq k).map f))) x) = pInv f (resEq.val' x) ⋯

@[simp]

theorem Descriptive.Tree.inv_val_eq_pInv_val {k : ℕ} {S T : Trees} (f : S ⟶ T) (x : (fun (S : Trees) => ↑↑S.snd) ((res k).obj T)) (h : Fixing k f := by as_aux_lemma => synthFixing) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((res k).map f))) x) = ↑(pInv f (res.val' x) ⋯)

theorem Descriptive.Tree.inv_val_eq_pInv_val' {k : ℕ} {S T : Trees} (f : S ⟶ T) (x : (fun (X : Type u_1) => X) ((resEq k).obj T)) (h : Fixing k f := by as_aux_lemma => synthFixing) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((resEq k).map f))) x) = ↑(pInv f (resEq.val' x) ⋯)