imageSieve — Mathlib

English

Same as earlier isLocallyInjective_iff_injective for presheaves.

Русский

То же самое, что ранее isLocallyInjective_iff_injective для предшев.

LaTeX

$$IsLocallyInjective φ ⇔ ∀ X, Injective (φ.app X)$$

Lean4

/-- Given `f : F ⟶ G`, a morphism between presieves, and `s : G.obj (op U)`, this is the sieve
of `U` consisting of the `i : V ⟶ U` such that `s` restricted along `i` is in the image of `f`. -/
@[simps -isSimp]
def imageSieve {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : ToType (G.obj (op U))) : Sieve U
    where
  arrows V i := ∃ t : ToType (F.obj (op V)), f.app _ t = G.map i.op s
  downward_closed := by
    rintro V W i ⟨t, ht⟩ j
    refine ⟨F.map j.op t, ?_⟩
    rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]

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