map_ofArrows — Mathlib

English

The pushforward of an ofArrows presieve equals the presieve built from mapped arrows.

Русский

Перемещение стрелок presieve через F\xa0равно предсистеме, построенной из отображённых стрелок.

LaTeX

$$$\\mathrm{map} F (\\mathrm{ofArrows} Y f) = \\mathrm{ofArrows} (\\lambda i. F.map (f i))$$

Lean4

@[simp]
theorem map_ofArrows {X : C} {ι : Type*} {Y : ι → C} (f : ∀ i, Y i ⟶ X) :
    (ofArrows Y f).map F = ofArrows _ (fun i ↦ F.map (f i)) :=
  by
  refine le_antisymm (fun Z g hg ↦ ?_) fun _ _ ⟨i⟩ ↦ map_map ⟨i⟩
  obtain ⟨hu⟩ := hg
  obtain ⟨i, rfl, rfl⟩ := Presieve.ofArrows_surj _ _ hu
  simpa using ofArrows.mk i

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