sieveOfSection — Mathlib

English

For X, f: yoneda.obj X ⟶ F, we have range f = ofSection (yonedaEquiv f).

Русский

Для X и f: yoneda.obj X → F имеет место range f = ofSection (yonedaEquiv f).

LaTeX

$$$ range\\ f = ofSection (yonedaEquiv f) $$$

Lean4

/-- Given a subpresheaf `G` of `F`, an `F`-section `s` on `U`, we may define a sieve of `U`
consisting of all `f : V ⟶ U` such that the restriction of `s` along `f` is in `G`. -/
@[simps]
def sieveOfSection {U : Cᵒᵖ} (s : F.obj U) : Sieve (unop U)
    where
  arrows V f := F.map f.op s ∈ G.obj (op V)
  downward_closed :=
    @fun V W i hi j => by
      simp only [op_unop, op_comp, FunctorToTypes.map_comp_apply]
      exact G.map _ hi

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