coweightHom_toLinearMap — Mathlib

English

There is a canonical coweight representation on Aut P taking values in Monoid of linear equivalences on N in opposite order.

Русский

У Aut P есть каноническое представление по корневой каверной (coweight) через моноид линейных эквивалентностей на N в противоположном порядке.

LaTeX

$$$\\mathrm{coweightHom}(P): Aut(P) \\to^* (N \\simeq_R N)^{op}$$$

Lean4

theorem coweightHom_toLinearMap {P : RootPairing ι R M N} (g : Aut P) :
    (MulOpposite.unop (coweightHom P g)).toLinearMap = MulOpposite.unop (Hom.coweightHom P g.toHom) :=
  rfl

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