English
The identity equivalence on P is a RootPairing.Equiv P P with the trivial Hom, weight, and coweight components; it acts as the identity on all associated structures.
Русский
Идентичное эквивалентности на P имеет тривиальные отображения, действующие как тождественные на всех сопутствующих структурах.
LaTeX
$$$\mathrm{id}_P : \text{RootPairing.Equiv } P P$ is the identity equivalence, i.e., the left and right unit constraints hold.$$
Lean4
/-- The identity equivalence of a root pairing. -/
@[simps!]
def id (P : RootPairing ι R M N) : RootPairing.Equiv P P :=
{ Hom.id P with
bijective_weightMap := _root_.id bijective_id
bijective_coweightMap := _root_.id bijective_id }
