English
Given a root pairing P on index set ι and linear equivalences e, f, g, one can transport P to a new root pairing on ι₂ with M₂, N₂, defined by the data (e, f, g). This transported object preserves the root and coroot structure in the sense described by the pushforward construction, including the induced permutation of roots and coroots.
Русский
Пусть задано парирование корней P на индексном множестве ι и линейные эквивалентности e, f, g. Тогда существует перенесение P на новое парирование на ι₂ с M₂, N₂, заданное данными e, f, g, сохраняющее структуру корней и корнетов и индуцирующее отображение корней и корнетов.
LaTeX
$$$ \\exists P' = RootPairing.map(e,f,g) : RootPairing_{\\iota_2} \\\\ R \\\\ M_2 \\\\ N_2 \\;\\land\\; span\\_root(P') = top \\land\\ span\\_coroot(P') = top$$$
Lean4
/-- Push forward a root pairing along linear equivalences, also reindexing the (co)roots. -/
protected def map (e : ι ≃ ι₂) (f : M ≃ₗ[R] M₂) (g : N ≃ₗ[R] N₂) : RootPairing ι₂ R M₂ N₂
where
__ := (f.symm.trans P.toPerfPair).trans g.symm.dualMap
isPerfPair_toLinearMap := by
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
have : IsReflexive R N₂ := equiv g
infer_instance
root := (e.symm.toEmbedding.trans P.root).trans f.toEmbedding
coroot := (e.symm.toEmbedding.trans P.coroot).trans g.toEmbedding
root_coroot_two i := by simp
reflectionPerm i := e.symm.trans <| (P.reflectionPerm (e.symm i)).trans e
reflectionPerm_root i j := by simp [reflection_apply]
reflectionPerm_coroot i j := by simp [coreflection_apply]
