English
Solutions of tautological relations in an A-module correspond to linear maps M → N; i.e., there is a canonical equivalence between Solution and LinearMap.
Русский
Решения тавталогических отношений в A-модуле соответствуют линейным отображениям M → N; есть каноническое эквивалентное соответствие между Solution и LinearMap.
LaTeX
$${A} → (tautologicalRelations A M).Solution N ≃ (M →_A N)$$
Lean4
/-- Solutions of `tautologicalRelations A M` in an `A`-module `N` identify to `M →ₗ[A] N`. -/
noncomputable def tautologicalRelationsSolutionEquiv {N : Type w} [AddCommGroup N] [Module A N] :
(tautologicalRelations A M).Solution N ≃ (M →ₗ[A] N)
where
toFun
s :=
{ toFun := s.var
map_add' := fun m₁ m₂ ↦ by
symm
rw [← sub_eq_zero]
simpa using s.linearCombination_var_relation (.add m₁ m₂)
map_smul' := fun a m ↦ by
symm
rw [← sub_eq_zero]
simpa using s.linearCombination_var_relation (.smul a m) }
invFun
f :=
{ var := f
linearCombination_var_relation := by rintro (_ | _) <;> simp }
