wellOrderInductionData — Mathlib

English

There is a lemma stating that the liftHom constructed in the well-order induction data behaves compatibly with the maps F.map and the attaching cocone maps at succ steps.

Русский

Существует лемма, утверждающая, что построенное liftHom в рамках индукции по порядку согласуется с отображениями F.map и кокон-стрелами на шагах succ.

LaTeX

$$$$ \text{liftHom_fac}: F.map( homOfLE-hi ) \circ liftHom = (s.1) .f' $$$$

Lean4

/-- The projective system `sqFunctor c p f g` has a `WellOrderInductionData` structure. -/
noncomputable def wellOrderInductionData : (sqFunctor c p f g).WellOrderInductionData
    where
  succ j hj
    sq' :=
    have := hF j hj sq'.f'
    have := hF j hj
    { f' := sq'.sq.lift
      w₁ := by
        dsimp
        simp only [← sq'.w₁]
        conv_rhs => rw [← sq'.sq.fac_left, ← F.map_comp_assoc]
        rfl }
  map_succ j hj sq' := by cat_disch
  lift j hj s := lift hj s
  map_lift j hj s i hij := map_lift hj s hij

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