English
Two affine maps f,g : (ι → φv i) →ᵃ[k] P2 are equal if they agree on all Pi.single evaluations and on the origin, i.e., f(Pi.single i x) = g(Pi.single i x) for all i and x, and f(0) = g(0) implies f = g.
Русский
Два аффинных отображения f,g : (ι → φv i) →ᵃ[k] P2 равны, если они совпадают на всех значениях Pi.single и в нуле: f(Pi.single i x) = g(Pi.single i x) для всех i, x, и f(0) = g(0) тогда f = g.
LaTeX
$$$\left(\forall i\forall x\; f(\Pi.single i x) = g(\Pi.single i x)\right) \land (f 0 = g 0) \Rightarrow f = g$$$
Lean4
/-- Two affine maps from a Pi-type of modules `(i : ι) → φv i` are equal if they are equal in their
operation on `Pi.single` and at zero. Analogous to `LinearMap.pi_ext`. See also `pi_ext_nonempty`,
which instead of agreement at zero requires `Nonempty ι`. -/
theorem pi_ext_zero (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) (h₂ : f 0 = g 0) : f = g :=
by
apply ext_linear
· apply LinearMap.pi_ext
intro i x
have s₁ := h i x
have s₂ := f.map_vadd 0 (Pi.single i x)
have s₃ := g.map_vadd 0 (Pi.single i x)
rw [vadd_eq_add, add_zero] at s₂ s₃
replace h₂ := h i 0
simp only [Pi.single_zero] at h₂
rwa [s₂, s₃, h₂, vadd_right_cancel_iff] at s₁
· exact h₂
