Theorems · Theorem · category theory

CategoryTheory.Functor.WellOrderInductionData.Extension.mk.inj

∀ {J : Type u} {inst : LinearOrder J} {inst_1 : SuccOrder J} {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} {inst_2 : OrderBot J} {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  {val : F.obj (Opposite.op j)}
  {map_zero : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = val₀}
  {map_succ :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val)}
  {map_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val,
            ⋯⟩}
  {val_1 : F.obj (Opposite.op j)}
  {map_zero_1 : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1 = val₀}
  {map_succ_1 :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1 =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1)}
  {map_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val_1 =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1,
            ⋯⟩},
  { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit } =
      { val := val_1, map_zero := map_zero_1, map_succ := map_succ_1, map_limit := map_limit_1 } →
    val = val_1

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound