LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.MiscCat

Auxiliary declarations for the Borel determinacy formalization.

theorem inv_congr {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.IsIso f] (h : f = g) : CategoryTheory.inv f = CategoryTheory.inv g

theorem hom_inv_id_apply {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] {FC : C → C → Type u_4} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {c d : C} (f : c ≅ d) (x : CategoryTheory.ToType d) : (CategoryTheory.ConcreteCategory.hom f.hom) ((CategoryTheory.ConcreteCategory.hom f.inv) x) = x

theorem inv_hom_id_apply {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] {FC : C → C → Type u_4} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {c d : C} (f : c ≅ d) (x : CategoryTheory.ToType c) : (CategoryTheory.ConcreteCategory.hom f.inv) ((CategoryTheory.ConcreteCategory.hom f.hom) x) = x

theorem cancel_inv_left {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] {FC : C → C → Type u_4} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {c d : C} (f : c ⟶ d) [CategoryTheory.IsIso f] (x : CategoryTheory.ToType c) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) ((CategoryTheory.ConcreteCategory.hom f) x) = x

theorem cancel_inv_right {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] {FC : C → C → Type u_4} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {c d : C} (f : c ⟶ d) [CategoryTheory.IsIso f] (x : CategoryTheory.ToType d) : (CategoryTheory.ConcreteCategory.hom f) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) x) = x

theorem naturality_apply {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_6, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] {FD : D → D → Type u_4} {CD : D → Type w} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {c d : C} (f : c ⟶ d) (x : CategoryTheory.ToType (F.obj c)) : (CategoryTheory.ConcreteCategory.hom (α.app d)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (α.app c)) x)

theorem cancel_inv_left_types {c d : Type u} (f : c ⟶ d) [CategoryTheory.IsIso f] (x : c) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) ((CategoryTheory.ConcreteCategory.hom f) x) = x

theorem cancel_inv_right_types {c d : Type u} (f : c ⟶ d) [CategoryTheory.IsIso f] (x : d) : (CategoryTheory.ConcreteCategory.hom f) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) x) = x

theorem naturality_apply_types {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] {F G : CategoryTheory.Functor C (Type u)} (α : F ⟶ G) {c d : C} (f : c ⟶ d) (x : F.obj c) : (CategoryTheory.ConcreteCategory.hom (α.app d)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (α.app c)) x)

@[simp]

theorem cat_preimage_id {c : Type u} (x : Set c) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id c)) ⁻¹' x = x

@[simp]

theorem cat_preimage_comp {c d e : Type u} (f : c ⟶ d) (g : d ⟶ e) (x : Set e) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ⁻¹' x = ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' x

@[simp]

theorem cancel_inv_left'' {c d : Type u} (f : c ⟶ d) [CategoryTheory.IsIso f] : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f) = id

@[simp]

theorem cancel_inv_right'' {c d : Type u} (f : c ⟶ d) [CategoryTheory.IsIso f] : ⇑(CategoryTheory.ConcreteCategory.hom f) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) = id

theorem iso_cancel_comp {a b c : Type u} (f : a ⟶ b) (g : b ⟶ c) (h : a ⟶ c) (x : b) [CategoryTheory.IsIso f] [CategoryTheory.IsIso h] (hc : CategoryTheory.CategoryStruct.comp f g = h) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv h)) ((CategoryTheory.ConcreteCategory.hom g) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) x

instance instMonoOptionOfHomSome_leanPool {α : Type u_1} : CategoryTheory.Mono (TypeCat.ofHom some)

instance instNonemptyIsColimitColimitCocone_leanPool {J : Type} [CategoryTheory.Category.{u_4, 0} J] {F : CategoryTheory.Functor J Type} : Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.colimitCocone F))

def coproductColimitCocone {J : Type u1} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (Type (max u_4 u1))) : CategoryTheory.Limits.ColimitCocone F

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem isCoprod_type_iff {J : Type u1} {F : CategoryTheory.Functor (CategoryTheory.Discrete J) (Type (max u1 v1))} (t : CategoryTheory.Limits.Cocone F) : Nonempty (CategoryTheory.Limits.IsColimit t) ↔ (∀ (i : CategoryTheory.Discrete J), CategoryTheory.Mono (t.ι.app i)) ∧ (Set.univ.PairwiseDisjoint fun (i : CategoryTheory.Discrete J) => Set.range ⇑(CategoryTheory.ConcreteCategory.hom (t.ι.app i))) ∧ ∀ (y : t.1), ∃ (i : CategoryTheory.Discrete J) (x : (fun (X : Type (max u1 v1)) => X) (F.obj i)), (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = y

theorem colim_isIso {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] {F G : CategoryTheory.Functor C D} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G} (hs : CategoryTheory.Limits.IsColimit s) (ht : CategoryTheory.Limits.IsColimit t) (f : F ≅ G) : CategoryTheory.IsIso (hs.map t f.hom)

theorem coprod_type_isIso_iff {J : Type u1} {F G : CategoryTheory.Functor (CategoryTheory.Discrete J) (Type (max u1 v1))} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G} (hs : CategoryTheory.Limits.IsColimit s) (ht : CategoryTheory.Limits.IsColimit t) (f : (j : J) → F.obj { as := j } ⟶ G.obj { as := j }) : CategoryTheory.IsIso (hs.map t (CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete J) => match x with | { as := j } => f j)) ↔ ∀ (j : J), CategoryTheory.IsIso (f j)