Isogenies of root pairings

A morphism of root pairings carries each root to a root. An isogeny is allowed to rescale: it carries each root to a positive integer multiple of a root, with the multiple depending on the root. This is the notion of SGA III, Exposé XXI, 6.8, and it is what an isogeny of reductive group schemes induces on root data; the special isogenies in characteristics two and three, which are not isomorphisms, are the reason the notion is needed at all.

TauCeti.RootPairingIsogeny P Q carries a linear map of weight spaces, its transpose on coweight spaces, and a bijection of index sets, together with a family exponent : ι → ℤ of positive integers, and it asks

weightMap (P.root i) = exponent i • Q.root (indexEquiv i),
coweightMap (Q.coroot (indexEquiv i)) = exponent i • P.coroot i.

Both lattice maps are required to be injective with finite-index image. At exponent = 1 the root and coroot equations are those of a RootPairing.Hom, TauCeti.RootPairingIsogeny.toHom performs that conversion, and TauCeti.RootPairingIsogeny.ofEquiv turns a RootPairing.Equiv into an isogeny. The transpose condition is stated as the bilinear identity Q.toLinearMap (weightMap x) y = P.toLinearMap x (coweightMap y), which is the unfolded form of the corresponding RootPairing.Hom field.

The two conditions are not independent of the pairings: they force TauCeti.RootPairingIsogeny.exponent_mul_pairing,

exponent i * Q.pairing (indexEquiv i) (indexEquiv j) = exponent j * P.pairing i j,

so an isogeny with a nonconstant exponent transforms the Cartan matrix rather than preserving it. That is exactly what a length-exchanging map of a non-simply-laced diagram does, and it is why RootPairing.Hom, whose index bijection preserves all Cartan integers, cannot express one.

Isogenies compose, with exponents multiplying along the composite, and for each positive integer c the scaling TauCeti.RootPairingIsogeny.smulId P c is an isogeny of a finite free ℤ-root pairing P with itself with constant exponent c. At c a prime p the latter is the root-datum shadow of the p-power Frobenius isogeny, which is what makes f.comp f = smulId P p the root-datum form of the relation τ ^ 2 = Frob_p satisfied by a special isogeny.

Main definitions

• TauCeti.RootPairingIsogeny: an isogeny of root pairings.
• TauCeti.RootPairingIsogeny.comp: the composite of two isogenies.
• TauCeti.RootPairingIsogeny.smulId: multiplication by a scalar, as an isogeny.
• TauCeti.RootPairingIsogeny.ofMatrix: an isogeny between root data on coordinate lattices, presented by an integer matrix.
• TauCeti.RootPairingIsogeny.toHom: an isogeny with constant exponent 1 as a root-pairing morphism.
• TauCeti.RootPairingIsogeny.ofEquiv: an equivalence of root pairings is an isogeny with all exponents 1.

Main results

• TauCeti.RootPairingIsogeny.exponent_mul_pairing: the exponents intertwine the two Cartan matrices.
• TauCeti.RootPairingIsogeny.comp_smulId: every isogeny intertwines scaling on its source with scaling on its target, so scaling is central among the endo-isogenies of one pairing.
• TauCeti.RootPairingIsogeny.comp_ofEquiv_smulId_eq_iff: an automorphism composed with a scaling is that scaling exactly when the automorphism is trivial.

References

• Schémas en groupes (SGA 3), Exposé XXI, 6.8.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.

This is a prerequisite for the target "Special isogenies in characteristics two and three" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

structure TauCeti.RootPairingIsogeny {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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) (Q : RootPairing ι₂ R M₂ N₂) : Type (max (max (max (max (max u_1 u_2) u_5) u_6) u_7) u_8)

An isogeny of root pairings: a pair of mutually transposed maps of weight and coweight spaces and a bijection of index sets, carrying each root to a prescribed scalar multiple of a root and each coroot to the same multiple of a coroot.

With all exponents equal to 1 this is a RootPairing.Hom; the extra generality is what an isogeny of reductive group schemes that is not an isomorphism induces on root data.

• weightMap : M →ₗ[R] M₂

  A linear map on weight space.

• coweightMap : N₂ →ₗ[R] N

  A contravariant linear map on coweight space.

• indexEquiv : ι ≃ ι₂

  A bijection on index sets.

• exponent : ι → ℤ

  The positive integer by which the root at each index is rescaled.

• exponent_pos (i : ι) : 0 < self.exponent i

  Every root-rescaling exponent is positive.

• weightMap_injective : Function.Injective ⇑self.weightMap

  The map on the weight lattice is injective.

• coweightMap_injective : Function.Injective ⇑self.coweightMap

  The contravariant map on the coweight lattice is injective.

• weightMap_finiteIndex : self.weightMap.range.toAddSubgroup.FiniteIndex

  The image in the target weight lattice has finite index.

• coweightMap_finiteIndex : self.coweightMap.range.toAddSubgroup.FiniteIndex

  The image in the source coweight lattice has finite index.

• weight_coweight_transpose (x : M) (y : N₂) : (Q.toLinearMap (self.weightMap x)) y = (P.toLinearMap x) (self.coweightMap y)

  The weight and coweight maps are transposes with respect to the two root pairings.

• root_weightMap (i : ι) : self.weightMap (P.root i) = ↑(self.exponent i) • Q.root (self.indexEquiv i)

  The weight map sends each root to its prescribed positive integral multiple.

• coroot_coweightMap (i : ι) : self.coweightMap (Q.coroot (self.indexEquiv i)) = ↑(self.exponent i) • P.coroot i

  The coweight map sends each corresponding coroot to the same integral multiple.

theorem TauCeti.RootPairingIsogeny.ext {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {inst✝ : CommRing R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {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 : RootPairingIsogeny P Q} (weightMap : x.weightMap = y.weightMap) (coweightMap : x.coweightMap = y.coweightMap) (indexEquiv : x.indexEquiv = y.indexEquiv) (exponent : x.exponent = y.exponent) : x = y

theorem TauCeti.RootPairingIsogeny.ext_iff {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {inst✝ : CommRing R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {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 : RootPairingIsogeny P Q} : x = y ↔ x.weightMap = y.weightMap ∧ x.coweightMap = y.coweightMap ∧ x.indexEquiv = y.indexEquiv ∧ x.exponent = y.exponent

def TauCeti.RootPairingIsogeny.toHom {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) (h : ∀ (i : ι), f.exponent i = 1) : P.Hom Q

An isogeny whose exponents are all 1, as a morphism of root pairings.

Equations

• f.toHom h = { weightMap := f.weightMap, coweightMap := f.coweightMap, indexEquiv := f.indexEquiv, weight_coweight_transpose := ⋯, root_weightMap := ⋯, coroot_coweightMap := ⋯ }

@[simp]

theorem TauCeti.RootPairingIsogeny.toHom_weightMap {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) (h : ∀ (i : ι), f.exponent i = 1) : (f.toHom h).weightMap = f.weightMap

@[simp]

theorem TauCeti.RootPairingIsogeny.toHom_coweightMap {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) (h : ∀ (i : ι), f.exponent i = 1) : (f.toHom h).coweightMap = f.coweightMap

@[simp]

theorem TauCeti.RootPairingIsogeny.toHom_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) (h : ∀ (i : ι), f.exponent i = 1) : (f.toHom h).indexEquiv = f.indexEquiv

theorem TauCeti.RootPairingIsogeny.exponent_mul_pairing {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) (i j : ι) : ↑(f.exponent i) * Q.pairing (f.indexEquiv i) (f.indexEquiv j) = ↑(f.exponent j) * P.pairing i j

The exponents of an isogeny intertwine the Cartan matrices of its source and target.

def TauCeti.RootPairingIsogeny.smulId {ι : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] (P : RootPairing ι ℤ M N) (c : ℕ+) : RootPairingIsogeny P P

Multiplication by a positive integer, as an isogeny of a finite free ℤ-root pairing with itself. At a prime p this is the isogeny of root data underlying the p-power Frobenius.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.RootPairingIsogeny.smulId_weightMap {ι : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] (P : RootPairing ι ℤ M N) (c : ℕ+) : (smulId P c).weightMap = ↑c • LinearMap.id

@[simp]

theorem TauCeti.RootPairingIsogeny.smulId_coweightMap {ι : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] (P : RootPairing ι ℤ M N) (c : ℕ+) : (smulId P c).coweightMap = ↑c • LinearMap.id

@[simp]

theorem TauCeti.RootPairingIsogeny.smulId_indexEquiv {ι : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] (P : RootPairing ι ℤ M N) (c : ℕ+) : (smulId P c).indexEquiv = Equiv.refl ι

@[simp]

theorem TauCeti.RootPairingIsogeny.smulId_exponent {ι : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] (P : RootPairing ι ℤ M N) (c : ℕ+) (i : ι) : (smulId P c).exponent i = ↑↑c

def TauCeti.RootPairingIsogeny.comp {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (g : RootPairingIsogeny Q S) (f : RootPairingIsogeny P Q) : RootPairingIsogeny P S

The composite of two isogenies, whose exponent at an index is the product of the exponent of the first at that index and the exponent of the second at its image.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.RootPairingIsogeny.comp_weightMap {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (g : RootPairingIsogeny Q S) (f : RootPairingIsogeny P Q) : (g.comp f).weightMap = g.weightMap ∘ₗ f.weightMap

@[simp]

theorem TauCeti.RootPairingIsogeny.comp_coweightMap {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (g : RootPairingIsogeny Q S) (f : RootPairingIsogeny P Q) : (g.comp f).coweightMap = f.coweightMap ∘ₗ g.coweightMap

@[simp]

theorem TauCeti.RootPairingIsogeny.comp_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (g : RootPairingIsogeny Q S) (f : RootPairingIsogeny P Q) : (g.comp f).indexEquiv = f.indexEquiv.trans g.indexEquiv

@[simp]

theorem TauCeti.RootPairingIsogeny.comp_exponent {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (g : RootPairingIsogeny Q S) (f : RootPairingIsogeny P Q) (i : ι) : (g.comp f).exponent i = f.exponent i * g.exponent (f.indexEquiv i)

def TauCeti.RootPairingIsogeny.ofMatrix {ι : Type u_1} {ι₂ : Type u_2} {n : ℕ} (P : RootDatum ι (Fin n → ℤ) (Fin n → ℤ)) (Q : RootDatum ι₂ (Fin n → ℤ) (Fin n → ℤ)) (hP : ∀ (x y : Fin n → ℤ), (P.toLinearMap x) y = x ⬝ᵥ y) (hQ : ∀ (x y : Fin n → ℤ), (Q.toLinearMap x) y = x ⬝ᵥ y) (A : Matrix (Fin n) (Fin n) ℤ) (e : ι ≃ ι₂) (c : ι → ℤ) (hc : ∀ (i : ι), 0 < c i) (hA : A.det ≠ 0) (hroot : ∀ (i : ι), A.mulVec (P.root i) = c i • Q.root (e i)) (hcoroot : ∀ (i : ι), A.transpose.mulVec (Q.coroot (e i)) = c i • P.coroot i) : RootPairingIsogeny P Q

An isogeny between root data on the coordinate lattices Fin n → ℤ with the dot-product pairing, presented by the integer matrix acting on the character lattice. The map on the cocharacter lattice is the transposed matrix, which is what the transpose condition forces. Nonvanishing of the determinant supplies injectivity and finite-index image for both maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.RootPairingIsogeny.ofMatrix_weightMap {ι : Type u_1} {ι₂ : Type u_2} {n : ℕ} (P : RootDatum ι (Fin n → ℤ) (Fin n → ℤ)) (Q : RootDatum ι₂ (Fin n → ℤ) (Fin n → ℤ)) (hP : ∀ (x y : Fin n → ℤ), (P.toLinearMap x) y = x ⬝ᵥ y) (hQ : ∀ (x y : Fin n → ℤ), (Q.toLinearMap x) y = x ⬝ᵥ y) (A : Matrix (Fin n) (Fin n) ℤ) (e : ι ≃ ι₂) (c : ι → ℤ) (hc : ∀ (i : ι), 0 < c i) (hA : A.det ≠ 0) (hroot : ∀ (i : ι), A.mulVec (P.root i) = c i • Q.root (e i)) (hcoroot : ∀ (i : ι), A.transpose.mulVec (Q.coroot (e i)) = c i • P.coroot i) : (ofMatrix P Q hP hQ A e c hc hA hroot hcoroot).weightMap = A.mulVecLin

@[simp]

theorem TauCeti.RootPairingIsogeny.ofMatrix_coweightMap {ι : Type u_1} {ι₂ : Type u_2} {n : ℕ} (P : RootDatum ι (Fin n → ℤ) (Fin n → ℤ)) (Q : RootDatum ι₂ (Fin n → ℤ) (Fin n → ℤ)) (hP : ∀ (x y : Fin n → ℤ), (P.toLinearMap x) y = x ⬝ᵥ y) (hQ : ∀ (x y : Fin n → ℤ), (Q.toLinearMap x) y = x ⬝ᵥ y) (A : Matrix (Fin n) (Fin n) ℤ) (e : ι ≃ ι₂) (c : ι → ℤ) (hc : ∀ (i : ι), 0 < c i) (hA : A.det ≠ 0) (hroot : ∀ (i : ι), A.mulVec (P.root i) = c i • Q.root (e i)) (hcoroot : ∀ (i : ι), A.transpose.mulVec (Q.coroot (e i)) = c i • P.coroot i) : (ofMatrix P Q hP hQ A e c hc hA hroot hcoroot).coweightMap = A.transpose.mulVecLin

@[simp]

theorem TauCeti.RootPairingIsogeny.ofMatrix_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {n : ℕ} (P : RootDatum ι (Fin n → ℤ) (Fin n → ℤ)) (Q : RootDatum ι₂ (Fin n → ℤ) (Fin n → ℤ)) (hP : ∀ (x y : Fin n → ℤ), (P.toLinearMap x) y = x ⬝ᵥ y) (hQ : ∀ (x y : Fin n → ℤ), (Q.toLinearMap x) y = x ⬝ᵥ y) (A : Matrix (Fin n) (Fin n) ℤ) (e : ι ≃ ι₂) (c : ι → ℤ) (hc : ∀ (i : ι), 0 < c i) (hA : A.det ≠ 0) (hroot : ∀ (i : ι), A.mulVec (P.root i) = c i • Q.root (e i)) (hcoroot : ∀ (i : ι), A.transpose.mulVec (Q.coroot (e i)) = c i • P.coroot i) : (ofMatrix P Q hP hQ A e c hc hA hroot hcoroot).indexEquiv = e

@[simp]

theorem TauCeti.RootPairingIsogeny.ofMatrix_exponent {ι : Type u_1} {ι₂ : Type u_2} {n : ℕ} (P : RootDatum ι (Fin n → ℤ) (Fin n → ℤ)) (Q : RootDatum ι₂ (Fin n → ℤ) (Fin n → ℤ)) (hP : ∀ (x y : Fin n → ℤ), (P.toLinearMap x) y = x ⬝ᵥ y) (hQ : ∀ (x y : Fin n → ℤ), (Q.toLinearMap x) y = x ⬝ᵥ y) (A : Matrix (Fin n) (Fin n) ℤ) (e : ι ≃ ι₂) (c : ι → ℤ) (hc : ∀ (i : ι), 0 < c i) (hA : A.det ≠ 0) (hroot : ∀ (i : ι), A.mulVec (P.root i) = c i • Q.root (e i)) (hcoroot : ∀ (i : ι), A.transpose.mulVec (Q.coroot (e i)) = c i • P.coroot i) (i : ι) : (ofMatrix P Q hP hQ A e c hc hA hroot hcoroot).exponent i = c i

def TauCeti.RootPairingIsogeny.ofEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : P.Equiv Q) : RootPairingIsogeny P Q

An equivalence of root pairings is an isogeny all of whose exponents are 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.RootPairingIsogeny.ofEquiv_weightMap {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : P.Equiv Q) : (ofEquiv f).weightMap = (↑f).weightMap

@[simp]

theorem TauCeti.RootPairingIsogeny.ofEquiv_coweightMap {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : P.Equiv Q) : (ofEquiv f).coweightMap = (↑f).coweightMap

@[simp]

theorem TauCeti.RootPairingIsogeny.ofEquiv_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : P.Equiv Q) : (ofEquiv f).indexEquiv = (↑f).indexEquiv

@[simp]

theorem TauCeti.RootPairingIsogeny.ofEquiv_exponent {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : P.Equiv Q) (i : ι) : (ofEquiv f).exponent i = 1

def TauCeti.RootPairingIsogeny.id {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : RootPairingIsogeny P P

The identity isogeny of a root pairing.

Equations

• TauCeti.RootPairingIsogeny.id P = TauCeti.RootPairingIsogeny.ofEquiv (RootPairing.Equiv.id P)

@[simp]

theorem TauCeti.RootPairingIsogeny.id_weightMap {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : (id P).weightMap = LinearMap.id

@[simp]

theorem TauCeti.RootPairingIsogeny.id_coweightMap {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : (id P).coweightMap = LinearMap.id

@[simp]

theorem TauCeti.RootPairingIsogeny.id_indexEquiv {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : (id P).indexEquiv = Equiv.refl ι

@[simp]

theorem TauCeti.RootPairingIsogeny.id_exponent {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) : (id P).exponent i = 1

@[simp]

theorem TauCeti.RootPairingIsogeny.ofEquiv_one {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} : ofEquiv 1 = id P

The identity automorphism becomes the identity isogeny.

@[simp]

theorem TauCeti.RootPairingIsogeny.comp_id {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) : (id Q).comp f = f

Composing an isogeny on the left with the identity isogeny does not change it.

@[simp]

theorem TauCeti.RootPairingIsogeny.id_comp {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} (f : RootPairingIsogeny P Q) : f.comp (id P) = f

Composing an isogeny on the right with the identity isogeny does not change it.

@[simp]

theorem TauCeti.RootPairingIsogeny.comp_assoc {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [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} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} {ι₄ : Type u_11} {M₄ : Type u_12} {N₄ : Type u_13} [AddCommGroup M₄] [Module R M₄] [AddCommGroup N₄] [Module R N₄] {T : RootPairing ι₄ R M₄ N₄} (h : RootPairingIsogeny S T) (g : RootPairingIsogeny Q S) (f : RootPairingIsogeny P Q) : (h.comp g).comp f = h.comp (g.comp f)

Composition of root-pairing isogenies is associative.

theorem TauCeti.RootPairingIsogeny.comp_smulId {ι : Type u_1} {ι₂ : Type u_2} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [AddCommGroup M] [AddCommGroup N] [AddCommGroup M₂] [AddCommGroup N₂] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] [Module.Free ℤ M₂] [Module.Finite ℤ M₂] [Module.Free ℤ N₂] [Module.Finite ℤ N₂] {P : RootPairing ι ℤ M N} {Q : RootPairing ι₂ ℤ M₂ N₂} (f : RootPairingIsogeny P Q) (c : ℕ+) : f.comp (smulId P c) = (smulId Q c).comp f

Scaling is natural: an isogeny f : P ⟶ Q intertwines multiplication by a positive integer on P with multiplication by the same integer on Q. At P = Q this says that scaling is central in the monoid of endo-isogenies, and since TauCeti.RootPairingIsogeny.smulId at a prime power q is the root-datum shadow of the q-power Frobenius, that specialization is the root-datum form of the fact that a Frobenius commutes with every endo-isogeny of the datum.

theorem TauCeti.RootPairingIsogeny.comp_ofEquiv_smulId_eq_iff {ι : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] [Module.Free ℤ M] [Module.Finite ℤ M] [Module.Free ℤ N] [Module.Finite ℤ N] {P : RootPairing ι ℤ M N} (f : P.Equiv P) (c : ℕ+) : (ofEquiv f).comp (smulId P c) = smulId P c ↔ f = 1

Scaling cancels an automorphism factor: composing an automorphism of a finite free ℤ-root pairing with multiplication by a positive integer returns that multiplication exactly when the automorphism is trivial. Multiplication by c is injective on a torsion-free weight lattice, so it cancels, and an automorphism of a root pairing is determined by its weight map.