hasLift — Mathlib

English

The iterationFunctor is a functor from the opposite of J to C, sending j' to the SqStruct indexed by j'.unop, and on morphisms α: j' ⟶ j the map is given by α.unop via sq'.map.

Русский

Функтор итерации является функтором J^op → C, отправляющим j' в SqStruct c p f g j'.unop, а на морфизмах α: j' → j действует как α.unop через sq'.map.

LaTeX

$$$$ \text{iterationFunctor} : J^{op} \to C, \quad (\text{iterationFunctor}.obj j') = SqStruct(c,p,f,g,j'.unop) $$ $$ \text{on morphisms: } α \mapsto (\text{sq}.map(α.unop)) $$$$

Lean4

theorem hasLift : sq.HasLift :=
  by
  obtain ⟨s, hs⟩ := (wellOrderInductionData c f g hF).surjective { w₂ := sq.w, .. }
  replace hs := congr_arg SqStruct.f' hs
  dsimp at hs
  let t : Cocone F :=
    Cocone.mk X
      { app j := (s.1 ⟨j⟩).f'
        naturality j j' g := by simpa using congr_arg SqStruct.f' (s.2 g.op) }
  let l := hc.desc t
  have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j
  exact ⟨⟨{
          l := l
          fac_left := by rw [hl, hs]
          fac_right := hc.hom_ext (fun j ↦ by rw [reassoc_of% (hl j), SqStruct.w₂]) }⟩⟩

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