dual_projective — Mathlib

English

Canonical application of the dual product equivalence gives the expected evaluation: dualProdDualEquivDual (φ, ψ) = φ.coprod ψ.

Русский

Каноническое применение эквивалентности двойного дуала к паре дуалов даёт сопряжение к копродукту.

LaTeX

$$$ (Module.Dual\\, R\\, M \\times Module.Dual\\, R\\, M') \\cong_{R} Module.Dual\\, R\\, (M \\times M') $$$

Lean4

instance dual_projective [Projective R M] : Projective R (Dual R M) :=
  have ⟨_, f, g, _, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
  .of_split f.dualMap g.dualMap (congr_arg dualMap hfg)

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