functorPushforward_union — Mathlib

English

Let F: C → D be a functor and S, R be sieves on an object X ∈ C. Then pushing forward along F preserves joins: F_*(S ∨ R) = F_*(S) ∨ F_*(R).

Русский

Пусть F: C → D — функтор и S, R — сеивая на X ∈ C. Тогда перенос по F сохраняет объединение: F_*(S ∪ R) = F_*(S) ∪ F_*(R).

LaTeX

$$$F_*(S \\lor R) = F_*(S) \\lor F_*(R)$$$

Lean4

theorem functorPushforward_union (S R : Sieve X) :
    (S ⊔ R).functorPushforward F = S.functorPushforward F ⊔ R.functorPushforward F :=
  (functor_galoisConnection F X).l_sup

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