isContinuous_comp' — Mathlib

English

If a natural isomorphism e: F1 ⋙ F2 ≅ F12 exists and F1 ∘ F2 is continuous, then F12 is continuous.

Русский

Если существует естественный изоморфизм e: F1 ⋙ F2 ≅ F12 и F1 ⋙ F2 непрерывен, то F12 непрерывна.

LaTeX

$$$(F_1 \\circ F_2) \\cong F_{12} \\quad\\land\\quad (F_1 \\circ F_2).IsContinuous\\ J\\ L \\Rightarrow F_{12}.IsContinuous\\ J\\ L$$$

Lean4

theorem isContinuous_comp' {F₁ : C ⥤ D} {F₂ : D ⥤ E} {F₁₂ : C ⥤ E} (e : F₁ ⋙ F₂ ≅ F₁₂) (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₁₂ J L :=
  by
  have := Functor.isContinuous_comp F₁ F₂ J K L
  apply Functor.isContinuous_of_iso e

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