comp_c_app — Mathlib

English

The composition of two LocallyRingedSpace morphisms respects the corresponding composition of their c-app components.

Русский

Состав гомоморфизмов LocallyRingedSpace согласуется с композицией соответствующих компонентов c.app.

LaTeX

$$$ (f \\gg g).c.app U = g.c.app U \\circ f.c.app (op (Opens.map g.base).obj U.unop) $$$

Lean4

theorem comp_c_app {X Y Z : LocallyRingedSpace.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (Opens Z)ᵒᵖ) :
    (f ≫ g).c.app U = g.c.app U ≫ f.c.app (op <| (Opens.map g.base).obj U.unop) :=
  rfl

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