homOfVector_over — Mathlib

English

Given a morphism f: X → S and a vector v of global coordinates, the map homOfVector f v gives a morphism X → 𝔸(n; S) with coordinate projections pulling back to v.

Русский

С гомоморфизмом f: X → S и вектором глобальных координат v, отображение homOfVector f v задаёт морфизм X → 𝔸(n; S) так, что координаты возвращаются в v.

LaTeX

$$$ \text{homOfVector } f v : X \to 𝔸(n; S) $ with appTop(coord S i) = v_i$$

Lean4

@[reassoc (attr := simp)]
theorem homOfVector_over : homOfVector f v ≫ 𝔸(n; S) ↘ S = f :=
  pullback.lift_fst _ _ _

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