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.
- indexEquiv : ι ≃ ι₂
A bijection on index sets.
- weight_coweight_transpose : self.weightMap.dualMap ∘ₗ ↑Q.toDualRight = ↑P.toDualRight ∘ₗ self.coweightMap
Instances For
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)
:
x = y
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)
:
f.weightMap.dualMap (Q.toDualRight x) = P.toDualRight (f.coweightMap x)
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)
:
f.weightMap (P.root i) = Q.root (f.indexEquiv i)
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)
:
f.coweightMap (Q.coroot i) = P.coroot (f.indexEquiv.symm i)
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.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
@[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_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
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.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✝)
@[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)
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)
:
Monoid (P.Hom P)
The endomorphism monoid of a root pairing.
Equations
- RootPairing.Hom.instMonoid P = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯
@[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)
:
RootPairing.Hom.weightMap 1 = LinearMap.id
@[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)
:
RootPairing.Hom.coweightMap 1 = LinearMap.id
@[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.
Equations
- P.End = P.Hom P
Instances For
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)
:
P.End →* Module.End R M
The weight space representation of endomorphisms
Equations
- RootPairing.Hom.weightHom P = { toFun := fun (g : P.End) => g.weightMap, map_one' := ⋯, map_mul' := ⋯ }
Instances For
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
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.
- 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
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)
:
x = y
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 ⋯
Instances For
@[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)
:
(RootPairing.Equiv.weightEquiv P Q e) m = (↑e).weightMap 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)
:
(RootPairing.Equiv.weightEquiv P Q e).symm ((↑e).weightMap 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₂)
:
(↑e).weightMap ((RootPairing.Equiv.weightEquiv P Q e).symm 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
- RootPairing.Equiv.coweightEquiv P Q e = LinearEquiv.ofBijective (↑e).coweightMap ⋯
Instances For
@[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₂)
:
(RootPairing.Equiv.coweightEquiv P Q e) n = (↑e).coweightMap 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₂)
:
(RootPairing.Equiv.coweightEquiv P Q e).symm ((↑e).coweightMap 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)
:
(↑e).coweightMap ((RootPairing.Equiv.coweightEquiv P Q e).symm 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 := ⋯ }
Instances For
@[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 : ι)
:
(↑(RootPairing.Equiv.id P)).indexEquiv.symm a = a
@[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 : ι)
:
(↑(RootPairing.Equiv.id P)).indexEquiv a = a
@[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)
:
(↑(RootPairing.Equiv.id P)).coweightMap a = a
@[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)
:
(↑(RootPairing.Equiv.id P)).weightMap a = 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
Equations
- g.comp f = { toHom := (↑g).comp ↑f, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ }
Instances For
@[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✝ : ι)
:
(↑(g.comp f)).indexEquiv a✝ = (↑g).indexEquiv ((↑f).indexEquiv a✝)
@[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₂)
:
(↑(g.comp f)).coweightMap a✝ = (↑f).coweightMap ((↑g).coweightMap a✝)
@[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✝ : ι₂)
:
(↑(g.comp f)).indexEquiv.symm a✝ = (↑f).indexEquiv.symm ((↑g).indexEquiv.symm 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)
:
(↑(g.comp f)).weightMap a✝ = (↑g).weightMap ((↑f).weightMap 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₁)
:
↑(g.comp f) = (↑g).comp ↑f
@[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)
:
f.comp (RootPairing.Equiv.id P) = f
@[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)
:
(RootPairing.Equiv.id Q).comp f = f
@[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₁)
:
(h.comp g).comp f = h.comp (g.comp f)
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)
:
Monoid (P.Equiv P)
Equivalences form a monoid.
Equations
- RootPairing.Equiv.instMonoid P = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯
@[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)
:
↑(RootPairing.Equiv.weightEquiv P P 1) = LinearMap.id
@[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)
:
↑(RootPairing.Equiv.coweightEquiv P P 1) = LinearMap.id
@[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)
:
↑1 = 1
@[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)
:
RootPairing.Equiv.weightEquiv P P (x.comp y) = RootPairing.Equiv.weightEquiv P P y ≪≫ₗ RootPairing.Equiv.weightEquiv P P x
@[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)
:
RootPairing.Equiv.weightEquiv P P x * RootPairing.Equiv.weightEquiv P P y = RootPairing.Equiv.weightEquiv P P y ≪≫ₗ RootPairing.Equiv.weightEquiv P P x
@[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)
:
RootPairing.Equiv.coweightEquiv P P (x.comp y) = RootPairing.Equiv.coweightEquiv P P x ≪≫ₗ RootPairing.Equiv.coweightEquiv P P y
@[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)
:
RootPairing.Equiv.coweightEquiv P P x * RootPairing.Equiv.coweightEquiv P P y = RootPairing.Equiv.coweightEquiv P P y ≪≫ₗ RootPairing.Equiv.coweightEquiv P P x
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.
Instances For
@[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)
:
(↑(RootPairing.Equiv.symm P Q f)).weightMap = ↑(RootPairing.Equiv.weightEquiv P Q f).symm
@[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)
:
(↑(RootPairing.Equiv.symm P Q f)).coweightMap = ↑(RootPairing.Equiv.coweightEquiv P Q f).symm
@[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)
:
(↑(RootPairing.Equiv.symm P Q f)).indexEquiv = (↑f).indexEquiv.symm
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)
:
Group (P.Equiv P)
Equivalences form a group.
Equations
@[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.
Equations
- P.Aut = P.Equiv P
Instances For
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.
Instances For
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)
:
↑((RootPairing.Equiv.toEndUnit P) g) = ↑g
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)
:
((RootPairing.Equiv.toEndUnit P) g).inv = ↑(RootPairing.Equiv.symm P P g)
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' := ⋯ }
Instances For
@[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)
:
↑((RootPairing.Equiv.weightHom P) g) = (RootPairing.Hom.weightHom P) ↑g
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)
:
RootPairing.Equiv.weightEquiv P P g⁻¹ = (RootPairing.Equiv.weightEquiv P P g)⁻¹
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' := ⋯ }
Instances For
@[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)
:
↑(MulOpposite.unop ((RootPairing.Equiv.coweightHom P) g)) = MulOpposite.unop ((RootPairing.Hom.coweightHom P) ↑g)
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' := ⋯ }
Instances For
@[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)
:
(RootPairing.Equiv.indexHom P) g = (↑g).indexEquiv
@[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)
:
(↑g⁻¹).indexEquiv = ((RootPairing.Equiv.indexHom P) g)⁻¹
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.
Instances For
@[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 : ι)
:
RootPairing.Equiv.weightEquiv P P (RootPairing.Equiv.reflection P i) = P.reflection 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 : ι)
:
RootPairing.Equiv.coweightEquiv P P (RootPairing.Equiv.reflection P i) = P.coreflection 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 : ι)
:
(↑(RootPairing.Equiv.reflection P i)).indexEquiv = P.reflection_perm 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.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)
:
MulAction P.Aut M
Equations
instance
RootPairing.Equiv.instMulActionMulOppositeAut
{ι : 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
instance
RootPairing.Equiv.instMulActionAut_1
{ι : 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)
:
MulAction P.Aut ι