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?
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.
A bijection on index sets.
- weight_coweight_transpose : self.weightMap.dualMap ∘ₗ ↑Q.toDualRight = ↑P.toDualRight ∘ₗ self.coweightMap
theorem
RootPairing.Hom.ext_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{inst✝ : CommRing R}
{inst✝¹ : AddCommGroup M}
{inst✝² : Module R M}
{inst✝³ : AddCommGroup N}
{inst✝⁴ : Module R N}
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
{inst✝⁵ : AddCommGroup M₂}
{inst✝⁶ : Module R M₂}
{inst✝⁷ : AddCommGroup N₂}
{inst✝⁸ : Module R N₂}
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
{x y : P.Hom Q}
:
theorem
RootPairing.Hom.ext
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{inst✝ : CommRing R}
{inst✝¹ : AddCommGroup M}
{inst✝² : Module R M}
{inst✝³ : AddCommGroup N}
{inst✝⁴ : Module R N}
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
{inst✝⁵ : AddCommGroup M₂}
{inst✝⁶ : Module R M₂}
{inst✝⁷ : AddCommGroup N₂}
{inst✝⁸ : Module R N₂}
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
{x y : P.Hom Q}
(weightMap : x.weightMap = y.weightMap)
(coweightMap : x.coweightMap = y.coweightMap)
(indexEquiv : x.indexEquiv = y.indexEquiv)
:
theorem
RootPairing.Hom.weight_coweight_transpose_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}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(x : N₂)
(f : P.Hom Q)
:
theorem
RootPairing.Hom.root_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}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(i : ι)
(f : P.Hom Q)
:
theorem
RootPairing.Hom.coroot_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}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(i : ι₂)
(f : P.Hom Q)
:
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 := ⋯ }
@[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 : ι)
:
@[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)
:
@[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)
:
@[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 : ι)
:
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.
@[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)
:
@[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✝ : ι)
:
@[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✝ : ι₂)
:
@[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₂)
:
@[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)
:
@[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)
:
@[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₁)
:
instance
RootPairing.Hom.instMonoid
{ι : 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)
:
The endomorphism monoid of a root pairing.
Equations
- RootPairing.Hom.instMonoid P = { mul := RootPairing.Hom.comp, mul_assoc := ⋯, one := RootPairing.Hom.id P, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }
@[simp]
theorem
RootPairing.Hom.weightMap_one
{ι : 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)
:
@[simp]
theorem
RootPairing.Hom.coweightMap_one
{ι : 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)
:
@[simp]
theorem
RootPairing.Hom.indexEquiv_one
{ι : 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)
:
@[simp]
theorem
RootPairing.Hom.weightMap_mul
{ι : 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)
(x y : P.Hom P)
:
@[simp]
theorem
RootPairing.Hom.coweightMap_mul
{ι : 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)
(x y : P.Hom P)
:
@[simp]
theorem
RootPairing.Hom.indexEquiv_mul
{ι : 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)
(x y : P.Hom P)
:
@[reducible, inline]
abbrev
RootPairing.End
{ι : 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)
:
Type (max (max (max (max (max u_1 u_3) u_4) u_1) u_3) u_4)
The endomorphism monoid of a root pairing.
def
RootPairing.Hom.weightHom
{ι : 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)
:
The weight space representation of endomorphisms
theorem
RootPairing.Hom.weightHom_injective
{ι : 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)
:
def
RootPairing.Hom.coweightHom
{ι : 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)
:
The coweight space representation of endomorphisms
Equations
- RootPairing.Hom.coweightHom P = { toFun := fun (g : P.End) => MulOpposite.op g.coweightMap, map_one' := ⋯, map_mul' := ⋯ }
theorem
RootPairing.Hom.coweightHom_injective
{ι : 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)
:
def
RootPairing.Hom.indexHom
{ι : 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)
:
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' := ⋯ }
structure
RootPairing.Equiv
{ι : 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₂)
extends P.Hom Q :
Type (max (max (max (max (max u_1 u_3) u_4) u_5) u_6) u_7)
An equivalence of root pairings is a morphism where the maps of weight and coweight spaces are bijective.
See also RootPairing.Equiv.toEndUnit.
- weight_coweight_transpose : (↑self).weightMap.dualMap ∘ₗ ↑Q.toDualRight = ↑P.toDualRight ∘ₗ (↑self).coweightMap
- bijective_weightMap : Function.Bijective ⇑(↑self).weightMap
- bijective_coweightMap : Function.Bijective ⇑(↑self).coweightMap
theorem
RootPairing.Equiv.ext
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{inst✝ : CommRing R}
{inst✝¹ : AddCommGroup M}
{inst✝² : Module R M}
{inst✝³ : AddCommGroup N}
{inst✝⁴ : Module R N}
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
{inst✝⁵ : AddCommGroup M₂}
{inst✝⁶ : Module R M₂}
{inst✝⁷ : AddCommGroup N₂}
{inst✝⁸ : Module R N₂}
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
{x y : P.Equiv Q}
(weightMap : (↑x).weightMap = (↑y).weightMap)
(coweightMap : (↑x).coweightMap = (↑y).coweightMap)
(indexEquiv : (↑x).indexEquiv = (↑y).indexEquiv)
:
theorem
RootPairing.Equiv.ext_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
{inst✝ : CommRing R}
{inst✝¹ : AddCommGroup M}
{inst✝² : Module R M}
{inst✝³ : AddCommGroup N}
{inst✝⁴ : Module R N}
{ι₂ : Type u_5}
{M₂ : Type u_6}
{N₂ : Type u_7}
{inst✝⁵ : AddCommGroup M₂}
{inst✝⁶ : Module R M₂}
{inst✝⁷ : AddCommGroup N₂}
{inst✝⁸ : Module R N₂}
{P : RootPairing ι R M N}
{Q : RootPairing ι₂ R M₂ N₂}
{x y : P.Equiv Q}
:
x = y ↔ (↑x).weightMap = (↑y).weightMap ∧ (↑x).coweightMap = (↑y).coweightMap ∧ (↑x).indexEquiv = (↑y).indexEquiv
def
RootPairing.Equiv.weightEquiv
{ι : 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₂)
(e : P.Equiv Q)
:
The linear equivalence of weight spaces given by an equivalence of root pairings.
Equations
- RootPairing.Equiv.weightEquiv P Q e = LinearEquiv.ofBijective (↑e).weightMap ⋯
@[simp]
theorem
RootPairing.Equiv.weightEquiv_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}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(e : P.Equiv Q)
(m : M)
:
@[simp]
theorem
RootPairing.Equiv.weightEquiv_symm_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₂)
(e : P.Equiv Q)
(m : M)
:
@[simp]
theorem
RootPairing.Equiv.weightMap_weightEquiv_symm
{ι : 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₂)
(e : P.Equiv Q)
(m : M₂)
:
def
RootPairing.Equiv.coweightEquiv
{ι : 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₂)
(e : P.Equiv Q)
:
The contravariant equivalence of coweight spaces given by an equivalence of root pairings.
Equations
@[simp]
theorem
RootPairing.Equiv.coweightEquiv_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}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(e : P.Equiv Q)
(n : N₂)
:
@[simp]
theorem
RootPairing.Equiv.coweightEquiv_symm_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₂)
(e : P.Equiv Q)
(n : N₂)
:
@[simp]
theorem
RootPairing.Equiv.coweightMap_coweightEquiv_symm
{ι : 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₂)
(e : P.Equiv Q)
(n : N)
:
def
RootPairing.Equiv.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.Equiv P
The identity equivalence of a root pairing.
Equations
- RootPairing.Equiv.id P = { toHom := RootPairing.Hom.id P, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ }
@[simp]
theorem
RootPairing.Equiv.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)
:
@[simp]
theorem
RootPairing.Equiv.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)
:
@[simp]
theorem
RootPairing.Equiv.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 : ι)
:
@[simp]
theorem
RootPairing.Equiv.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 : ι)
:
def
RootPairing.Equiv.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_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₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
:
P.Equiv P₂
Composition of equivalences
@[simp]
theorem
RootPairing.Equiv.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_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₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
(a✝ : N₂)
:
@[simp]
theorem
RootPairing.Equiv.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_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₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
(a✝ : ι)
:
@[simp]
theorem
RootPairing.Equiv.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_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₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
(a✝ : M)
:
@[simp]
theorem
RootPairing.Equiv.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_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₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
(a✝ : ι₂)
:
@[simp]
theorem
RootPairing.Equiv.toHom_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_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₂]
{P : RootPairing ι R M N}
{P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂}
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
:
@[simp]
theorem
RootPairing.Equiv.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_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Equiv Q)
:
@[simp]
theorem
RootPairing.Equiv.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_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Equiv Q)
:
@[simp]
theorem
RootPairing.Equiv.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_8}
{M₁ : Type u_9}
{N₁ : Type u_10}
{ι₂ : Type u_11}
{M₂ : Type u_12}
{N₂ : Type u_13}
{ι₃ : Type u_14}
{M₃ : Type u_15}
{N₃ : Type u_16}
[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₂.Equiv P₃)
(g : P₁.Equiv P₂)
(f : P.Equiv P₁)
:
instance
RootPairing.Equiv.instMonoid
{ι : 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)
:
Equivalences form a monoid.
Equations
- RootPairing.Equiv.instMonoid P = { mul := RootPairing.Equiv.comp, mul_assoc := ⋯, one := RootPairing.Equiv.id P, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }
@[simp]
theorem
RootPairing.Equiv.weightEquiv_one
{ι : 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)
:
@[simp]
theorem
RootPairing.Equiv.coweightEquiv_one
{ι : 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)
:
@[simp]
theorem
RootPairing.Equiv.toHom_one
{ι : 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)
:
@[simp]
theorem
RootPairing.Equiv.mul_eq_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]
{P : RootPairing ι R M N}
(x y : P.Equiv P)
:
@[simp]
theorem
RootPairing.Equiv.weightEquiv_comp_toLin
{ι : 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}
(x y : P.Equiv P)
:
@[simp]
theorem
RootPairing.Equiv.weightEquiv_mul
{ι : 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}
(x y : P.Equiv P)
:
@[simp]
theorem
RootPairing.Equiv.coweightEquiv_comp_toLin
{ι : 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}
(x y : P.Equiv P)
:
@[simp]
theorem
RootPairing.Equiv.coweightEquiv_mul
{ι : 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}
(x y : P.Equiv P)
:
def
RootPairing.Equiv.symm
{ι : 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_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Equiv Q)
:
Q.Equiv P
The inverse of a root pairing equivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
RootPairing.Equiv.inv_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_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Equiv Q)
:
@[simp]
theorem
RootPairing.Equiv.inv_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_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Equiv Q)
:
@[simp]
theorem
RootPairing.Equiv.inv_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]
{ι₂ : Type u_8}
{M₂ : Type u_9}
{N₂ : Type u_10}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
(P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂)
(f : P.Equiv Q)
:
instance
RootPairing.Equiv.instGroup
{ι : 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)
:
Equivalences form a group.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
RootPairing.Aut
{ι : 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)
:
Type (max (max (max (max (max u_1 u_3) u_4) u_1) u_3) u_4)
The automorphism group of a root pairing.
def
RootPairing.Equiv.toEndUnit
{ι : 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)
:
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.
theorem
RootPairing.Equiv.toEndUnit_val
{ι : 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)
(g : P.Aut)
:
theorem
RootPairing.Equiv.toEndUnit_inv
{ι : 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)
(g : P.Aut)
:
def
RootPairing.Equiv.weightHom
{ι : 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)
:
The weight space representation of automorphisms
Equations
- RootPairing.Equiv.weightHom P = { toFun := RootPairing.Equiv.weightEquiv P P, map_one' := ⋯, map_mul' := ⋯ }
@[simp]
theorem
RootPairing.Equiv.weightHom_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)
(e : P.Equiv P)
:
theorem
RootPairing.Equiv.weightHom_toLinearMap
{ι : 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}
(g : P.Aut)
:
theorem
RootPairing.Equiv.weightHom_injective
{ι : 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)
:
@[simp]
theorem
RootPairing.Equiv.weightEquiv_inv
{ι : 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}
(g : P.Aut)
:
def
RootPairing.Equiv.coweightHom
{ι : 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)
:
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' := ⋯ }
@[simp]
theorem
RootPairing.Equiv.coweightHom_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)
(g : P.Aut)
:
theorem
RootPairing.Equiv.coweightHom_toLinearMap
{ι : 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}
(g : P.Aut)
:
theorem
RootPairing.Equiv.coweightHom_injective
{ι : 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)
:
theorem
RootPairing.Equiv.coweightHom_op
{ι : 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}
(g : P.Aut)
:
@[simp]
theorem
RootPairing.Equiv.coweightEquiv_inv
{ι : 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}
(g : P.Aut)
:
def
RootPairing.Equiv.indexHom
{ι : 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)
:
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' := ⋯ }
@[simp]
theorem
RootPairing.Equiv.indexHom_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)
(g : P.Aut)
:
@[simp]
theorem
RootPairing.Equiv.indexEquiv_inv
{ι : 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}
(g : P.Aut)
:
def
RootPairing.Equiv.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.Aut
The automorphism of a root pairing given by a reflection.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
RootPairing.Equiv.reflection_weightEquiv
{ι : 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 : ι)
:
@[simp]
theorem
RootPairing.Equiv.reflection_coweightEquiv
{ι : 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 : ι)
:
@[simp]
theorem
RootPairing.Equiv.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 : ι)
:
@[simp]
theorem
RootPairing.Equiv.reflection_inv
{ι : 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 : ι)
:
instance
RootPairing.Equiv.instDistribMulActionAut
{ι : 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)
:
DistribMulAction P.Aut M
Equations
- RootPairing.Equiv.instDistribMulActionAut P = { smul := fun (w : P.Aut) (x : M) => ((RootPairing.Equiv.weightHom P) w) x, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
@[simp]
theorem
RootPairing.Equiv.reflection_smul
{ι : 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 : ι)
(x : M)
:
@[simp]
theorem
RootPairing.Equiv.root_indexEquiv_eq_smul
{ι : 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 : ι)
(g : P.Aut)
:
instance
RootPairing.Equiv.instDistribMulActionMulOppositeAut
{ι : 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)
:
Equations
- One or more equations did not get rendered due to their size.
instance
RootPairing.Equiv.instSMulCommClassAut
{ι : 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)
:
SMulCommClass P.Aut R M
instance
RootPairing.Equiv.instSMulCommClassMulOppositeAut
{ι : 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)
:
SMulCommClass P.Autᵐᵒᵖ R N
instance
RootPairing.Equiv.instMulActionAut
{ι : 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)
:
Equations
- RootPairing.Equiv.instMulActionAut P = { smul := fun (w : P.Aut) (i : ι) => ((RootPairing.Equiv.indexHom P) w) i, one_smul := ⋯, mul_smul := ⋯ }