English
The composition of two continuous functors is continuous: if F1: C ⥤ D is J–K continuous and F2: D ⥤ E is K–L continuous, then F1 ⋙ F2: C ⥤ E is J–L continuous.
Русский
Составной функтор двух непрерывных функторов по топологиям сохраняет непрерывность: если F1 неприменим по J→K и F2 по K→L, то F1 ⋙ F2 неприменим по J→L.
LaTeX
$$$(F_1.IsContinuous\\ J\\ K) \\land (F_2.IsContinuous\\ K\\ L) \\Rightarrow ((F_1 \\circ F_2).IsContinuous\\ J\\ L)$$$
Lean4
theorem isContinuous_comp (F₁ : C ⥤ D) (F₂ : D ⥤ E) (J : GrothendieckTopology C) (K : GrothendieckTopology D)
(L : GrothendieckTopology E) [Functor.IsContinuous.{t} F₁ J K] [Functor.IsContinuous.{t} F₂ K L] :
Functor.IsContinuous.{t} (F₁ ⋙ F₂) J L where
op_comp_isSheaf_of_types
G := F₁.op_comp_isSheaf_of_types J K ⟨_, (isSheaf_iff_isSheaf_of_type _ _).2 (F₂.op_comp_isSheaf_of_types K L G)⟩
