surjective_π_app_zero_of_surjective_map_aux

English

Auxiliary surjectivity result for the π_0 component of a limit cone.

Русский

Вспомогательный результат сюръективности компонента π_0 предельного конуса.

LaTeX

$$$\\text{surjective }((\\text{limitCone } F).\\pi.app\\langle 0\\rangle)$$$

Lean4

/-- Auxiliary lemma. Use `limit_of_surjections_surjective` instead. -/
theorem surjective_π_app_zero_of_surjective_map_aux : Function.Surjective ((limitCone F).π.app ⟨0⟩) :=
  by
  intro a
  refine ⟨⟨fun ⟨n⟩ ↦ preimage hF a n, ?_⟩, rfl⟩
  intro ⟨n⟩ ⟨m⟩ ⟨⟨⟨(h : m ≤ n)⟩⟩⟩
  induction h with
  | refl => erw [CategoryTheory.Functor.map_id, types_id_apply]
  | @step p h ih =>
    rw [← ih]
    have h' : m ≤ p := h
    erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op), types_comp_apply,
      (hF p _).choose_spec]
    rfl

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