map — Mathlib

English

Under a functor F, the zeroth presieve of the image equals the image of the zeroth presieve: (E.map F).presieve₀ = E.presieve₀.map F.

Русский

Под действием отображения F нулевое презивное переходится в образ так, что (E.map F).presieve₀ = E.presieve₀.map F.

LaTeX

$$(E.map F).presieve₀ = E.presieve₀.map F$$

Lean4

/-- The image of a `0`-hypercover under a functor. -/
@[simps toPreZeroHypercover]
def map (F : C ⥤ D) (E : ZeroHypercover.{w} J S) (h : J ≤ K.comap F) : ZeroHypercover.{w} K (F.obj S)
    where
  __ := E.toPreZeroHypercover.map F
  mem₀ := by
    rw [PreZeroHypercover.presieve₀_map, ← mem_comap_iff]
    exact h _ E.mem₀

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