comp_homOfVector — Mathlib

English

Composition distributes over the vector-to-affine-space construction: composing f with homOfVector g v equals homOfVector of the composed morphism and the vector f.appTop ∘ v.

Русский

Сведение композиции через конструирование вектора в афинном пространстве: композиция f с homOfVector g v равна homOfVector от композиции f и g и вектора f.appTop ∘ v.

LaTeX

$$$$f \circ \mathrm{homOfVector}(g,v) = \mathrm{homOfVector}(f\circ g, f.{\tt appTop} \circ v).$$$$

Lean4

@[reassoc]
theorem comp_homOfVector {X Y : Scheme} (v : n → Γ(Y, ⊤)) (f : X ⟶ Y) (g : Y ⟶ S) :
    f ≫ homOfVector g v = homOfVector (f ≫ g) (f.appTop ∘ v) := by ext1 <;> simp

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