mk — Mathlib · SciLib

English

The class of an invertible R-module M in Pic(R) is the element Pic.mk R M.

Русский

Класс инвертируемого R-модуля M в группе Pic(R) задаётся элементом Pic.mk R M.

LaTeX

$$$ \\mathrm{Pic}(R) \\ni \\mathrm{Pic.mk} R M. $$$

Lean4

/-- The class of an invertible module in the Picard group. -/
protected noncomputable def mk : Pic R :=
  equivShrink _ <|
    letI M' := Finite.repr R M
    .mkOfMulEqOne ⟦.of R M'⟧ ⟦.of R (Dual R M')⟧ <|
      by
      rw [← toSkeleton, ← toSkeleton, mul_comm, ← Skeleton.toSkeleton_tensorObj]
      exact Quotient.sound ⟨(Invertible.linearEquiv R _).toModuleIso⟩

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