LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InvLimitNat

Auxiliary declarations for the Borel determinacy formalization.

theorem eq_homOfLE {X : Type u} [Preorder X] {x y : X} (f : x ⟶ y) : f = CategoryTheory.homOfLE ⋯

@[simp]

theorem map_eq_homOfLE {X Y : Type u} [Preorder X] [Preorder Y] {x y : X} (F : CategoryTheory.Functor X Y) (f : x ⟶ y) : F.map f = CategoryTheory.homOfLE ⋯

theorem heq_eqToHom {C : Type u2} [CategoryTheory.Category.{u1, u2} C] {a b c d : C} (ab : a = b) (bc : b = c) (cd : c = d) : CategoryTheory.eqToHom ab ≍ CategoryTheory.eqToHom cd

theorem left_eqToHom_iff_heq {C : Type u2} [CategoryTheory.Category.{u1, u2} C] {W X Y : C} (f : W ⟶ X) (g : Y ⟶ X) (h : W = Y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) g ↔ f ≍ g

theorem congr_comp {C : Type u2} [CategoryTheory.Category.{u1, u2} C] {a b b' c d : C} (f : c ⟶ d) {g : b ⟶ c} {g' : b' ⟶ c} {h : a ⟶ b} {h' : a ⟶ b'} (H : CategoryTheory.CategoryStruct.comp h g = CategoryTheory.CategoryStruct.comp h' g') : CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp h' (CategoryTheory.CategoryStruct.comp g' f)

def recComp {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) : F (m + n) ⟶ F m

Auxiliary declaration for the Borel determinacy formalization.

Equations

• recComp m n f = Nat.recAux (CategoryTheory.CategoryStruct.id (F m)) (fun (n : ℕ) (ih : F (m + n) ⟶ F m) => CategoryTheory.CategoryStruct.comp (f (m + n)) ih) n

theorem recComp_induction {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (p : ⦃c d : C⦄ → (c ⟶ d) → Prop) (pid : ∀ (c : C), p (CategoryTheory.CategoryStruct.id c)) (pcomp : ∀ {c d e : C} (f : c ⟶ d) (g : d ⟶ e), p f → p g → p (CategoryTheory.CategoryStruct.comp f g)) (m n : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) (h : ∀ (n : ℕ), p (f (m + n))) : p (recComp m n f)

theorem recComp_iso {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) (h : ∀ (n : ℕ), CategoryTheory.IsIso (f (m + n))) : CategoryTheory.IsIso (recComp m n f)

def recCompOfLE {C : Type u2} [CategoryTheory.Category.{u1, u2} C] {m n : ℕ} (h : m ≤ n) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) : F n ⟶ F m

Auxiliary declaration for the Borel determinacy formalization.

Equations

• recCompOfLE h f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (recComp m (n - m) f)

@[simp]

theorem recComp.eq_zero {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) (h : n = 0) : recComp m n f = CategoryTheory.eqToHom ⋯

@[simp]

theorem recCompOfLE.refl {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (n : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) : recCompOfLE ⋯ f = CategoryTheory.CategoryStruct.id (F n)

@[simp]

theorem recComp.sum {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n p : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) : CategoryTheory.CategoryStruct.comp (recComp (m + n) p f) (recComp m n f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (recComp m (n + p) f)

@[simp]

theorem recComp.eq_sum {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n p q : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) (h : p = m + n) : CategoryTheory.CategoryStruct.comp (recComp p q f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (recComp m n f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (recComp m (n + q) f)

@[simp]

theorem recCompOfLE.trans {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n p : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) (h1 : m ≤ n) (h2 : n ≤ p) : CategoryTheory.CategoryStruct.comp (recCompOfLE h2 f) (recCompOfLE h1 f) = recCompOfLE ⋯ f

@[simp]

theorem recComp.eq_one {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n : ℕ) {F : ℕ → C} (f : (n : ℕ) → F (n + 1) ⟶ F n) (h : n = 1) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (recComp m n f) = f m

@[simp]

theorem recComp.functor {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (m n : ℕ) (F : CategoryTheory.Functor ℕᵒᵖ C) : (recComp m n fun (n : ℕ) => F.map (CategoryTheory.homOfLE ⋯).op) = F.map (CategoryTheory.homOfLE ⋯).op

noncomputable def natFreeCat {C : Type u2} [CategoryTheory.Category.{u1, u2} C] : CategoryTheory.Functor ℕᵒᵖ C ≃ (O : ℕ → C) × ((n : ℕ) → O (n + 1) ⟶ O n)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem natFreeCat_apply_symm_apply {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (x : (O : ℕ → C) × ((n : ℕ) → O (n + 1) ⟶ O n)) : (natFreeCat (natFreeCat.symm x)).snd = x.snd

theorem isIso_map_nat {C : Type u2} [CategoryTheory.Category.{u1, u2} C] (F : CategoryTheory.Functor ℕᵒᵖ C) {m : ℕ} (hF : ∀ n ≥ m, CategoryTheory.IsIso (F.map (CategoryTheory.homOfLE ⋯).op)) {c d : ℕᵒᵖ} (f : c ⟶ d) : Opposite.unop d ≥ m → CategoryTheory.IsIso (F.map f)

theorem nat_add_initial {C : Type u2} [CategoryTheory.Category.{u1, u2} C] {F : CategoryTheory.Functor ℕᵒᵖ C} {s : CategoryTheory.Limits.Cone F} (hs : CategoryTheory.Limits.IsLimit s) (n : ℕ) (hn : ∀ k ≥ n, CategoryTheory.IsIso (F.map (CategoryTheory.homOfLE ⋯).op)) (k : ℕ) (hk : n ≤ k) : CategoryTheory.IsIso (s.π.app (Opposite.op k))