mk_tensor — Mathlib

English

The Picard class is compatible with tensor products: Pic.mk R (M ⊗_R N) = Pic.mk R M · Pic.mk R N.

Русский

Класс Пикарда совместим с тензорным произведением: Pic.mk R (M ⊗_R N) = Pic.mk R M · Pic.mk R N.

LaTeX

$$$ \\mathrm{Pic.mk} R (M \\otimes_R N) = \\mathrm{Pic.mk} R M \\;.*\\; \\mathrm{Pic.mk} R N. $$$

Lean4

theorem mk_tensor : Pic.mk R (M ⊗[R] N) = Pic.mk R M * Pic.mk R N :=
  congr_arg (equivShrink _) <|
    Units.ext <| by
      simp_rw [Pic.mk, Equiv.symm_apply_apply]
      refine (Quotient.sound ?_).trans (Skeleton.toSkeleton_tensorObj ..)
      exact
        ⟨(Finite.reprEquiv R _ ≪≫ₗ
              TensorProduct.congr (Finite.reprEquiv R M).symm (Finite.reprEquiv R N).symm).toModuleIso⟩

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