English
There exists a canonical instance that endows affine maps with function-like behavior, i.e., a FunLike structure, compatible with the affine space and module structures on the domain and codomain.
Русский
Существует канонический экземпляр, делающий аффинные отображения функциями; это структура типа FunLike, совместимая с аффинным пространством и модулями как в области определения, так и в области значения.
Lean4
instance instFunLike (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*) [Ring k] [AddCommGroup V1]
[Module k V1] [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2] [AffineSpace V2 P2] : FunLike (P1 →ᵃ[k] P2) P1 P2
where
coe := AffineMap.toFun
coe_injective' := fun ⟨f, f_linear, f_add⟩ ⟨g, g_linear, g_add⟩ => fun (h : f = g) =>
by
obtain ⟨p⟩ := (AddTorsor.nonempty : Nonempty P1)
congr with v
apply vadd_right_cancel (f p)
rw [← f_add, h, ← g_add]
