English
Repeatedly applying π to generators yields the same span description as before; range π remains the same.
Русский
Повторное применение π к генераторам даёт прежнее описание оболочки.
LaTeX
$$Eq (LinearMap.range solution.π) (Submodule.span A (Set.range solution.var))$$
Lean4
/-- Given `relations : Relations A` and an `A`-module `M`, this is a constructor
for `relations.Solution M` for which the data is given as
a linear map `π : (relations.G →₀ A) →ₗ[A] M`. (See also `ofπ'` for an alternate
vanishing criterion.) -/
@[simps -isSimp]
noncomputable def ofπ : relations.Solution M
where
var g := π (Finsupp.single g 1)
linearCombination_var_relation
r := by
have : π = Finsupp.linearCombination _ (fun g ↦ π (Finsupp.single g 1)) := by ext; simp
rw [← this]
exact hπ r
