Morphisms of root pairings #
This file defines morphisms of root pairings, following the definition of morphisms of root data given in SGA III Exp. 21 Section 6.
Main definitions: #
Hom
: A morphism of root pairings is a linear map of weight spaces, its transverse on coweight spaces, and a bijection on the set that indexes roots and coroots.Hom.id
: The identity morphism.Hom.comp
: The composite of two morphisms.End
: The endomorphism monoid of a root pairing.Hom.weightHom
: The homomorphism from the endomorphism monoid to linear endomorphisms on the weight space.Hom.coweightHom
: The homomorphism from the endomorphism monoid to the opposite monoid of linear endomorphisms on the coweight space.Equiv
: An equivalence of root pairings is a morphism for which the maps on weight spaces and coweight spaces are bijective.Equiv.toHom
: The morphism underlying an equivalence.Equiv.weightEquiv
: The linear isomorphism on weight spaces given by an equivalence.Equiv.coweightEquiv
: The linear isomorphism on coweight spaces given by an equivalence.Equiv.id
: The identity equivalence.Equiv.comp
: The composite of two equivalences.Equiv.symm
: The inverse of an equivalence.Aut
: The automorphism group of a root pairing.Equiv.toEndUnit
: The group isomorphism between the automorphism group of a root pairing and the group of invertible endomorphisms.Equiv.weightHom
: The homomorphism from the automorphism group to linear automorphisms on the weight space.Equiv.coweightHom
: The homomorphism from the automorphism group to the opposite group of linear automorphisms on the coweight space.Equiv.reflection
: The automorphism of a root pairing given by reflection in a root and coreflection in the corresponding coroot.
TODO #
- Special types of morphisms: Isogenies, weight/coweight space embeddings
- Weyl group reimplementation?
A morphism of root pairings is a pair of mutually transposed maps of weight and coweight spaces that preserves roots and coroots. We make the map of indexing sets explicit.
A linear map on weight space.
A contravariant linear map on coweight space.
- indexEquiv : ι ≃ ι₂
A bijection on index sets.
- weight_coweight_transpose : self.weightMap.dualMap ∘ₗ ↑Q.toDualRight = ↑P.toDualRight ∘ₗ self.coweightMap
Instances For
The identity morphism of a root pairing.
Equations
- RootPairing.Hom.id P = { weightMap := LinearMap.id, coweightMap := LinearMap.id, indexEquiv := Equiv.refl ι, weight_coweight_transpose := ⋯, root_weightMap := ⋯, coroot_coweightMap := ⋯ }
Instances For
Composition of morphisms
Equations
- One or more equations did not get rendered due to their size.
Instances For
The endomorphism monoid of a root pairing.
Equations
- RootPairing.Hom.instMonoid P = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯
The endomorphism monoid of a root pairing.
Equations
- P.End = P.Hom P
Instances For
The weight space representation of endomorphisms
Equations
- RootPairing.Hom.weightHom P = { toFun := fun (g : P.End) => g.weightMap, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The coweight space representation of endomorphisms
Equations
- RootPairing.Hom.coweightHom P = { toFun := fun (g : P.End) => MulOpposite.op g.coweightMap, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The permutation representation of the endomorphism monoid on the root index set
Equations
- RootPairing.Hom.indexHom P = { toFun := fun (f : P.End) => f.indexEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
An equivalence of root pairings is a morphism where the maps of weight and coweight spaces are bijective.
See also RootPairing.Equiv.toEndUnit
.
- coweightMap : N₂ →ₗ[R] N
- indexEquiv : ι ≃ ι₂
- weight_coweight_transpose : (↑self).weightMap.dualMap ∘ₗ ↑Q.toDualRight = ↑P.toDualRight ∘ₗ (↑self).coweightMap
- root_weightMap : ⇑(↑self).weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑(↑self).indexEquiv
- coroot_coweightMap : ⇑(↑self).coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑(↑self).indexEquiv.symm
- bijective_weightMap : Function.Bijective ⇑(↑self).weightMap
- bijective_coweightMap : Function.Bijective ⇑(↑self).coweightMap
Instances For
The linear equivalence of weight spaces given by an equivalence of root pairings.
Equations
- RootPairing.Equiv.weightEquiv P Q e = LinearEquiv.ofBijective (↑e).weightMap ⋯
Instances For
The contravariant equivalence of coweight spaces given by an equivalence of root pairings.
Equations
- RootPairing.Equiv.coweightEquiv P Q e = LinearEquiv.ofBijective (↑e).coweightMap ⋯
Instances For
The identity equivalence of a root pairing.
Equations
- RootPairing.Equiv.id P = { toHom := RootPairing.Hom.id P, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ }
Instances For
Composition of equivalences
Equations
- g.comp f = { toHom := (↑g).comp ↑f, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ }
Instances For
Equivalences form a monoid.
Equations
- RootPairing.Equiv.instMonoid P = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯
The inverse of a root pairing equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equivalences form a group.
Equations
The automorphism group of a root pairing.
Equations
- P.Aut = P.Equiv P
Instances For
The isomorphism between the automorphism group of a root pairing and the group of invertible endomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weight space representation of automorphisms
Equations
- RootPairing.Equiv.weightHom P = { toFun := RootPairing.Equiv.weightEquiv P P, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The coweight space representation of automorphisms
Equations
- RootPairing.Equiv.coweightHom P = { toFun := fun (g : P.Aut) => MulOpposite.op (RootPairing.Equiv.coweightEquiv P P g), map_one' := ⋯, map_mul' := ⋯ }
Instances For
The permutation representation of the automorphism group on the root index set
Equations
- RootPairing.Equiv.indexHom P = { toFun := fun (g : P.Aut) => (↑g).indexEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The automorphism of a root pairing given by a reflection.
Equations
- One or more equations did not get rendered due to their size.