mem_functorPushforward_iff_of_full

English

A variant stating that for full F, the pushforward condition for f in the image reduces to injectivity of the mapping of F on arrows.

Русский

Вариант: для полного F условие переноса для f в образе сводится к инъективности отображения F на стрелы.

LaTeX

$$$(R.arrows.functorPushforward F)(F.map f) \\leftrightarrow R f$$$

Lean4

theorem mem_functorPushforward_iff_of_full [F.Full] {X Y : C} (R : Sieve X) (f : F.obj Y ⟶ F.obj X) :
    (R.arrows.functorPushforward F) f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R g :=
  by
  refine ⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, hg⟩ ↦ ?_⟩
  · obtain ⟨h', hh'⟩ := F.map_surjective h
    use h' ≫ g
    simp only [Functor.map_comp, hh', hcomp, true_and]
    apply R.downward_closed hg
  · use Y, g, 𝟙 _, hg
    simp [hcomp]

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