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 data 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.
TODO #
- Special types of morphisms: Isogenies, weight/coweight space embeddings
- Weyl group reimplementation?
theorem
RootPairing.Hom.ext
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
:
∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N}
{ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂}
{inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂} {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂}
{x y : P.Hom Q}, x.weightMap = y.weightMap → x.coweightMap = y.coweightMap → x.indexEquiv = y.indexEquiv → x = y
theorem
RootPairing.Hom.ext_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
:
∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N}
{ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂}
{inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂} {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂}
{x y : P.Hom Q}, x = y ↔ x.weightMap = y.weightMap ∧ x.coweightMap = y.coweightMap ∧ x.indexEquiv = y.indexEquiv
structure
RootPairing.Hom
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
:
Type (max (max (max (max (max u_1 u_3) u_4) u_5) u_6) u_7)
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
theorem
RootPairing.Hom.weight_coweight_transpose
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
(self : P.Hom Q)
:
self.weightMap.dualMap ∘ₗ ↑Q.toDualRight = ↑P.toDualRight ∘ₗ self.coweightMap
theorem
RootPairing.Hom.root_weightMap
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
(self : P.Hom Q)
:
theorem
RootPairing.Hom.coroot_coweightMap
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
(self : P.Hom Q)
:
@[simp]
theorem
RootPairing.Hom.id_indexEquiv_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(a : ι)
:
(RootPairing.Hom.id P).indexEquiv a = a
@[simp]
theorem
RootPairing.Hom.id_coweightMap_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(a : N)
:
(RootPairing.Hom.id P).coweightMap a = a
@[simp]
theorem
RootPairing.Hom.id_weightMap_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(a : M)
:
(RootPairing.Hom.id P).weightMap a = a
@[simp]
theorem
RootPairing.Hom.id_indexEquiv_symm_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(a : ι)
:
(RootPairing.Hom.id P).indexEquiv.symm a = a
def
RootPairing.Hom.id
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
:
P.Hom P
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
@[simp]
theorem
RootPairing.Hom.comp_coweightMap_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₁ : Type u_5}
{M₁ : Type u_6}
{N₁ : Type u_7}
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Hom P₂)
(f : P.Hom P₁)
:
∀ (a : N₂), (g.comp f).coweightMap a = f.coweightMap (g.coweightMap a)
@[simp]
theorem
RootPairing.Hom.comp_indexEquiv_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₁ : Type u_5}
{M₁ : Type u_6}
{N₁ : Type u_7}
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Hom P₂)
(f : P.Hom P₁)
:
∀ (a : ι), (g.comp f).indexEquiv a = g.indexEquiv (f.indexEquiv a)
@[simp]
theorem
RootPairing.Hom.comp_indexEquiv_symm_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₁ : Type u_5}
{M₁ : Type u_6}
{N₁ : Type u_7}
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Hom P₂)
(f : P.Hom P₁)
:
∀ (a : ι₂), (g.comp f).indexEquiv.symm a = f.indexEquiv.symm (g.indexEquiv.symm a)
@[simp]
theorem
RootPairing.Hom.comp_weightMap_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₁ : Type u_5}
{M₁ : Type u_6}
{N₁ : Type u_7}
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Hom P₂)
(f : P.Hom P₁)
:
∀ (a : M), (g.comp f).weightMap a = g.weightMap (f.weightMap a)
def
RootPairing.Hom.comp
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₁ : Type u_5}
{M₁ : Type u_6}
{N₁ : Type u_7}
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Hom P₂)
(f : P.Hom P₁)
:
P.Hom P₂
Composition of morphisms
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
RootPairing.Hom.id_comp
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Hom Q)
:
f.comp (RootPairing.Hom.id P) = f
@[simp]
theorem
RootPairing.Hom.comp_id
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Hom Q)
:
(RootPairing.Hom.id Q).comp f = f
@[simp]
theorem
RootPairing.Hom.comp_assoc
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{ι₁ : Type u_5}
{M₁ : Type u_6}
{N₁ : Type u_7}
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
{ι₃ : Type u_11}
{M₃ : Type u_12}
{N₃ : Type u_13}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₃]
[Module R N₃]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
{P₃ : RootPairing ι₃ R M₃ N₃}
(h : P₂.Hom P₃)
(g : P₁.Hom P₂)
(f : P.Hom P₁)
:
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
theorem
RootPairing.Hom.reflection_indexEquiv
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(i : ι)
:
(RootPairing.Hom.reflection P i).indexEquiv = P.reflection_perm i
@[simp]
theorem
RootPairing.Hom.reflection_coweightMap_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(i : ι)
(a : N)
:
(RootPairing.Hom.reflection P i).coweightMap a = a - (P.toPerfectPairing (P.root i)) a • P.coroot i
@[simp]
theorem
RootPairing.Hom.reflection_weightMap_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(i : ι)
(a : M)
:
(RootPairing.Hom.reflection P i).weightMap a = a - (P.flip.toPerfectPairing (P.flip.root i)) a • P.flip.coroot i
def
RootPairing.Hom.reflection
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(i : ι)
:
P.Hom P
The endomorphism of a root pairing given by a reflection.
Equations
- One or more equations did not get rendered due to their size.