lift — Mathlib

English

A noncomputable lift data structure liftHom is extended to produce a well-order induction framework for the SqFunctor, including the definition of lift and its compatibilities.

Русский

Непрерывная структура подъёма по хорошо упорядоченному порядку расширяется до рамок индукции по Well-Order для SqFunctor, включая определение lift и его совместимости.

LaTeX

$$$$ \text{liftHom} : F(j) \to X \quad\text{and}\quad \text{lift} : (sqFunctor\ c\ p\ f\ g).obj\ (Opposite\ op\ j) $$$$

Lean4

/-- Auxiliary definition for `transfiniteComposition.wellOrderInductionData`. -/
@[simps]
noncomputable def lift : (sqFunctor c p f g).obj (Opposite.op j)
    where
  f' := liftHom hj s
  w₁ :=
    by
    have h : ⊥ < j :=
      Ne.bot_lt'
        (by
          rintro rfl
          exact Order.not_isSuccLimit_bot hj)
    rw [liftHom_fac hj s ⊥ h]
    simpa using (s.1 ⟨⊥, h⟩).w₁
  w₂ :=
    (F.isColimitOfIsWellOrderContinuous j hj).hom_ext
      (fun ⟨i, hij⟩ ↦ by
        have := (s.1 ⟨i, hij⟩).w₂
        dsimp at this ⊢
        rw [liftHom_fac_assoc _ _ _ hij, this, Cocone.w_assoc])

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