English
If M has a presentation and there is a linear equivalence e: M ≃_A N, then there is a corresponding presentation of N obtained by transporting along e.
Русский
Если у M есть презентация и имеется линейное эквивалентное отображение e: M ≃_A N, то существует презентация N, полученная перенесением по e.
LaTeX
$$$pres: \\text{Presentation } A M,\\ e: M \\simeq_A N \\quad\\Rightarrow\\quad \\text{pres.ofLinearEquiv}(e) : \\text{Presentation } A N$$$
Lean4
/-- The presentation of an `A`-module `N` that is deduced from a presentation of
a module `M` and a linear equivalence `e : M ≃ₗ[A] N`. -/
@[simps! toRelations toSolution]
def ofLinearEquiv (pres : Presentation.{w₀, w₁} A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) :
Presentation A N :=
ofIsPresentation (pres.toIsPresentation.of_linearEquiv e)
