freeLocus_congr — Mathlib

English

The free locus is invariant under linear equivalences: if M ≅ M', then freeLocus(R,M) = freeLocus(R,M').

Русский

Свободный локус инвариантен относительно линейных эквивалентностей модулей.

LaTeX

$$$\text{freeLocus}(R,M) = \text{freeLocus}(R,M')$ для всякого изоморфизма $M \cong M'$.$$

Lean4

theorem freeLocus_congr {M'} [AddCommGroup M'] [Module R M'] (e : M ≃ₗ[R] M') : freeLocus R M = freeLocus R M' :=
  by
  ext p
  exact mem_freeLocus_of_isLocalization _ _ _ (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M' ∘ₗ e.toLinearMap)

Похожие утверждения