Theorems · Theorem · category theory

CategoryTheory.Functor.WellOrderInductionData.Extension.mk.injEq

∀ {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

0 results in Mathlib

Foundations

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

Assumes

LinearOrderSuccOrderOrderBot