comp_base_apply — Mathlib

English

Let f: X → Y and g: Y → Z be morphisms of schemes and x ∈ X. Then the base map of the composed morphism satisfies (f ≫ g).base x = g.base (f.base x).

Русский

Пусть f: X → Y и g: Y → Z — морфизмы схем, и x ∈ X. Тогда базовое отображение композиции равно композиции базовых отображений: (f ≫ g).base x = g.base (f.base x).

LaTeX

$$$ (f \\circ g).base(x) = g.base(f.base(x)) $$$

Lean4

theorem comp_base_apply {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g).base x = g.base (f.base x) := by simp

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