English
There is a pushforward of a root system along linear equivalences, yielding a RootSystem on ι₂ with spaces M₂, N₂ equal to the pushforward of P via the map described in RootPairing.map, and whose span conditions are preserved.
Русский
Существуют перенос корневой системы вдоль линейных эквивалентностей, дающий RootSystem на ι₂ с пространствами M₂, N₂, являющийся переносом данных P через отображение RootPairing.map и сохраняющий условия порожденности пространства корней и косых корней.
LaTeX
$$$ RootSystem.map \\; e \\; f \\; g : RootSystem_{\\iota_2} \\; R \\; M_2 \\; N_2$ with \\; span\\_root = top, \\; span\\_coroot = top$$$
Lean4
/-- Push forward a root system along linear equivalences, also reindexing the (co)roots. -/
protected def _root_.RootSystem.map {P : RootSystem ι R M N} (e : ι ≃ ι₂) (f : M ≃ₗ[R] M₂) (g : N ≃ₗ[R] N₂) :
RootSystem ι₂ R M₂ N₂ where
__ := P.toRootPairing.map e f g
span_root_eq_top := by simp [Embedding.coe_trans, range_comp, span_image, RootPairing.map]
span_coroot_eq_top := by simp [Embedding.coe_trans, range_comp, span_image, RootPairing.map]
