English
Given a map e, a linear equivalence e' matching the affine translation at a base point p, mk' constructs an affine equivalence with the required properties.
Русский
Задавая отображение e, линейное эквивалентное e' и базовую точку p, mk' строит аффинное эквивалентное отображение с нужными свойствами.
LaTeX
$$$\text{mk'}(e,e',p,h) \in P_1 \overset{\mathrm{Affine}}{\to} P_2$$$
Lean4
/-- Construct an affine equivalence by verifying the relation between the map and its linear part at
one base point. Namely, this function takes a map `e : P₁ → P₂`, a linear equivalence
`e' : V₁ ≃ₗ[k] V₂`, and a point `p` such that for any other point `p'` we have
`e p' = e' (p' -ᵥ p) +ᵥ e p`. -/
def mk' (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ p' : P₁, e p' = e' (p' -ᵥ p) +ᵥ e p) : P₁ ≃ᵃ[k] P₂
where
toFun := e
invFun := fun q' : P₂ => e'.symm (q' -ᵥ e p) +ᵥ p
left_inv p' := by simp [h p', vadd_vsub, vsub_vadd]
right_inv q' := by simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), vadd_vsub, vsub_vadd]
linear := e'
map_vadd' p' v := by simp [h p', h (v +ᵥ p'), vadd_vsub_assoc, vadd_vadd]
