topologically_isStableUnderComposition

English

If P is stable under composition for maps of topological spaces, then topologically P is stable under composition for scheme morphisms.

Русский

Если P стабильно по композиции для отображений топологических пространств, то topologically P стабильно по композиции для гомоморфизмов схем.

LaTeX

$$(topologically P).IsStableUnderComposition$$

Lean4

/-- If a property of maps of topological spaces is stable under composition, the induced
morphism property of schemes is stable under composition. -/
theorem topologically_isStableUnderComposition
    (hP :
      ∀ {α β γ : Type u} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α → β) (g : β → γ)
        (_ : P f) (_ : P g), P (g ∘ f)) :
    (topologically P).IsStableUnderComposition where
  comp_mem {X Y Z} f g hf
    hg := by
    simp only [topologically, Scheme.comp_coeBase, TopCat.coe_comp]
    exact hP _ _ hf hg

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