natTransOfLe — Mathlib

English

If S ≤ T between sieves on X, then there is a natural transformation from S.functor to T.functor given pointwise by the inclusion.

Русский

Если S ≤ T между сеиваями на X, тогда существует естественное преобразование из S.functor в T.functor, заданное точечно включением.

LaTeX

$$$\\text{natTransOfLe}_{S,T}(h): S.functor \\rightarrow T.functor$$$

Lean4

/-- If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced
presheaves.
-/
@[simps]
def natTransOfLe {S T : Sieve X} (h : S ≤ T) : S.functor ⟶ T.functor where app _ f := ⟨f.1, h _ f.2⟩

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