mk_eq_mk_iff — Mathlib

English

For any R-modules M,N invertible, Pic.mk R M = Pic.mk R N iff there exists a linear equivalence M ≃ₗ[R] N.

Русский

Для инвертируемых R-модулей M,N: Pic.mk R M = Pic.mk R N тогда и только тогда, когда существует линейное эквивалентное отображение M ≃ₗ[R] N.

LaTeX

$$$ \\forall (R) [\\mathrm{CommRing} R] (M : Type*) (N : \\mathrm{Pic} R),\\; \\mathrm{Pic.mk} R M = \\mathrm{Pic.mk} R N \\iff \\mathrm{Nonempty}(M \\simeq_R N). $$$

Lean4

theorem mk_eq_mk_iff : Pic.mk R M = Pic.mk R N ↔ Nonempty (M ≃ₗ[R] N) :=
  let eN := mk.linearEquiv R N
  mk_eq_iff.trans ⟨fun ⟨e⟩ ↦ ⟨e ≪≫ₗ eN⟩, fun ⟨e⟩ ↦ ⟨e ≪≫ₗ eN.symm⟩⟩

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