liftHom — Mathlib

English

There is a canonical morphism liftHom: F.obj j ⟶ X, defined as the descents through the colimit induced by the isWellOrderContinuous structure, using a cocone built from the family s.

Русский

Существует каноническое отображение liftHom: F.obj j ⟶ X, определяемое как факторизация через колимит, индуцированный структурой IsWellOrderContinuous, используя кокон, построенный из семейства s.

LaTeX

$$$$ liftHom_j : F(obj\, j) \to X $$ defined by\ desc\; (F.isColimitOfIsWellOrderContinuous\ j\ hj)\ Cocone.mk\ { app := \lambda i, (s.1 ⟨i⟩).f' ... } $$$$

Lean4

/-- Auxiliary definition for `transfiniteComposition.wellOrderInductionData`. -/
noncomputable def liftHom : F.obj j ⟶ X :=
  (F.isColimitOfIsWellOrderContinuous j hj).desc
    (Cocone.mk _
      { app := fun i ↦ (s.1 ⟨i⟩).f'
        naturality i i'
          g := by
          have := congr_arg SqStruct.f' (s.2 g.op)
          dsimp at this ⊢
          rw [this, comp_id] })

Похожие утверждения