Scalar-extended coordinate spans of the represented modular F4 flag

This file identifies the first two blocks of the adapted represented basis with the concrete matrix-coordinate scalar extensions preserved by the F4 generators. The statements work over an arbitrary value algebra over ZMod 2; no injectivity or flatness hypothesis is used.

@[reducible, inline]

abbrev TauCeti.DynkinType.f4ShortRootCotangentDual : Type

The cotangent-dual adjoint module of GL₂₆ over ZMod 2.

Equations

• TauCeti.DynkinType.f4ShortRootCotangentDual = Module.Dual (ZMod 2) (TauCeti.Bialgebra.CotangentSpace (ZMod 2) ↑(TauCeti.GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26))

noncomputable def TauCeti.DynkinType.f4ShortRootCotangentFlagIdeal {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Submodule A (TensorProduct (ZMod 2) A f4ShortRootCotangentDual)

The scalar-extended represented-ideal term of the cotangent flag.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootCotangentFlagBasis_mem_ideal {A : Type} [CommRing A] [Algebra (ZMod 2) A] (i : Fin f4ShortRootRepresentedIdealRank) : (Module.Basis.baseChange A f4ShortRootCotangentFlagBasis) (Fin.castAdd f4ShortRootRepresentedComplementRank (Fin.castAdd 26 i)) ∈ f4ShortRootCotangentFlagIdeal

Each basis vector in the first adapted block belongs to the ideal term.

noncomputable def TauCeti.DynkinType.f4ShortRootCotangentFlagRange {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Submodule A (TensorProduct (ZMod 2) A f4ShortRootCotangentDual)

The scalar-extended represented-range term of the cotangent flag.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootCotangentFlagBasis_mem_range {A : Type} [CommRing A] [Algebra (ZMod 2) A] (i : Fin (f4ShortRootRepresentedIdealRank + 26)) : (Module.Basis.baseChange A f4ShortRootCotangentFlagBasis) (Fin.castAdd f4ShortRootRepresentedComplementRank i) ∈ f4ShortRootCotangentFlagRange

Each basis vector in the first two adapted blocks belongs to the range term.

Stability of the represented flag

The following two submodules are the matrix-coordinate scalar extensions of the represented range M and its represented ideal J. We give them by the images of their distinguished bases. This form makes the torus stability argument valid over an arbitrary value algebra, without any flatness or injectivity hypothesis on its structure map from ZMod 2.

noncomputable def TauCeti.DynkinType.f4ShortRootRepresentedRangeMatrixBaseChange {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Submodule A (Matrix (Fin 26) (Fin 26) A)

The base-changed matrix-coordinate range of the short-root adjoint representation.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootRepresentedRangeMatrixBaseChange_eq_span_basis {A : Type} [CommRing A] [Algebra (ZMod 2) A] : f4ShortRootRepresentedRangeMatrixBaseChange = Submodule.span A (Set.range fun (k : f4ChevalleyIndex) => f4ShortRootAdjointMatrixBaseChange (f4ModularChevalleyBasis k))

The represented range written as the span of its distinguished Chevalley basis matrices.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootAdjointMatrixBaseChange_chevalleyBasis_mem_range {A : Type} [CommRing A] [Algebra (ZMod 2) A] (k : f4ChevalleyIndex) : f4ShortRootAdjointMatrixBaseChange (f4ModularChevalleyBasis k) ∈ f4ShortRootRepresentedRangeMatrixBaseChange

Each Chevalley adjoint matrix is in the scalar-extended represented range.

noncomputable def TauCeti.DynkinType.f4ShortRootRepresentedIdealMatrixBaseChange {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Submodule A (Matrix (Fin 26) (Fin 26) A)

The base-changed matrix-coordinate image of the short-root ideal.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootRepresentedIdealMatrixBaseChange_eq_span_basis {A : Type} [CommRing A] [Algebra (ZMod 2) A] : f4ShortRootRepresentedIdealMatrixBaseChange = Submodule.span A (Set.range fun (i : Fin 26) => f4ShortRootAdjointMatrixBaseChange ↑(f4ShortRootLieIdealBasis i))

The represented ideal written as the span of its distinguished short-root basis matrices.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootAdjointMatrixBaseChange_idealBasis_mem_ideal {A : Type} [CommRing A] [Algebra (ZMod 2) A] (i : Fin 26) : f4ShortRootAdjointMatrixBaseChange (f4ModularChevalleyBasis (f4ShortRootBasisCoordinate i)) ∈ f4ShortRootRepresentedIdealMatrixBaseChange

Each ideal-basis adjoint matrix is in the scalar-extended represented ideal.

theorem TauCeti.DynkinType.f4ShortRootRepresentedRangeMatrixBaseChange_eq_span {A : Type} [CommRing A] [Algebra (ZMod 2) A] : f4ShortRootRepresentedRangeMatrixBaseChange = Submodule.span A (Set.range fun (X : f4ModularChevalleyLieAlgebra) => f4ShortRootAdjointMatrixBaseChange X)

The distinguished-basis definition of the base-changed represented range agrees with the A-span of every entrywise base-changed matrix in M.

theorem TauCeti.DynkinType.f4ShortRootRepresentedIdealMatrixBaseChange_eq_span {A : Type} [CommRing A] [Algebra (ZMod 2) A] : f4ShortRootRepresentedIdealMatrixBaseChange = Submodule.span A (Set.range fun (y : ↥f4ShortRootLieIdeal) => f4ShortRootAdjointMatrixBaseChange ↑y)

The distinguished-basis definition of the base-changed represented ideal agrees with the A-span of every entrywise base-changed matrix in J.

theorem TauCeti.DynkinType.f4ShortRootRepresentedIdealMatrixBaseChange_le_range {A : Type} [CommRing A] [Algebra (ZMod 2) A] : f4ShortRootRepresentedIdealMatrixBaseChange ≤ f4ShortRootRepresentedRangeMatrixBaseChange

The base-changed represented ideal is contained in the base-changed represented range.

noncomputable def TauCeti.DynkinType.f4ShortRootEndMatrixBaseChangeLinearMap {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Module.End (ZMod 2) ↥f4ShortRootLieIdeal →ₗ[ZMod 2] Matrix (Fin 26) (Fin 26) A

Entrywise scalar extension of an endomorphism of the modular short-root ideal, in its distinguished matrix coordinates.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootEndMatrixBaseChangeLinearMap_adjoint {A : Type} [CommRing A] [Algebra (ZMod 2) A] (X : f4ModularChevalleyLieAlgebra) : f4ShortRootEndMatrixBaseChangeLinearMap (f4ShortRootAdjoint X) = f4ShortRootAdjointMatrixBaseChange X

Scalar extension of the adjoint endomorphism agrees with its named matrix.

noncomputable def TauCeti.DynkinType.f4ShortRootCotangentBaseChangeMatrixEquiv {A : Type} [CommRing A] [Algebra (ZMod 2) A] : TensorProduct (ZMod 2) A (Module.Dual (ZMod 2) (Bialgebra.CotangentSpace (ZMod 2) ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26))) ≃ₗ[A] Matrix (Fin 26) (Fin 26) A

Scalar extension of the cotangent-dual matrix coordinates used by the adjoint comodule.

Equations

• TauCeti.DynkinType.f4ShortRootCotangentBaseChangeMatrixEquiv = Derivation.tangentScalarExtensionEquiv.trans (TauCeti.GeneralLinear.tangentLinearEquivMatrix 26)

theorem TauCeti.DynkinType.f4ShortRootCotangentBaseChangeMatrixEquiv_apply {A : Type} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct (ZMod 2) A (Module.Dual (ZMod 2) (Bialgebra.CotangentSpace (ZMod 2) ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26)))) : f4ShortRootCotangentBaseChangeMatrixEquiv x = (GeneralLinear.tangentMatrix 26) (Derivation.tangentScalarExtensionEquiv x)

Evaluation of the scalar-extended cotangent matrix equivalence.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootCotangentBaseChangeMatrixEquiv_basis {A : Type} [CommRing A] [Algebra (ZMod 2) A] (i : Fin (f4ShortRootRepresentedIdealRank + 26 + f4ShortRootRepresentedComplementRank)) : f4ShortRootCotangentBaseChangeMatrixEquiv (1 ⊗ₜ[ZMod 2] f4ShortRootEndEquivCotangentDual (f4ShortRootEndBasis i)) = f4ShortRootEndMatrixBaseChangeLinearMap (f4ShortRootEndBasis i)

The transported adapted cotangent basis is the entrywise scalar extension of the adapted endomorphism basis.

theorem TauCeti.DynkinType.f4ShortRootCotangentFlagIdeal_map {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Submodule.map (↑f4ShortRootCotangentBaseChangeMatrixEquiv) f4ShortRootCotangentFlagIdeal = f4ShortRootRepresentedIdealMatrixBaseChange

Under cotangent-dual matrix coordinates, the first adapted basis block is exactly the scalar-extended represented ideal.

theorem TauCeti.DynkinType.f4ShortRootCotangentFlagRange_map {A : Type} [CommRing A] [Algebra (ZMod 2) A] : Submodule.map (↑f4ShortRootCotangentBaseChangeMatrixEquiv) f4ShortRootCotangentFlagRange = f4ShortRootRepresentedRangeMatrixBaseChange

Under cotangent-dual matrix coordinates, the first two adapted basis blocks are exactly the scalar-extended represented range.

@[simp]

theorem TauCeti.DynkinType.mem_f4ShortRootCotangentFlagIdeal_iff {A : Type} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct (ZMod 2) A f4ShortRootCotangentDual) : x ∈ f4ShortRootCotangentFlagIdeal ↔ f4ShortRootCotangentBaseChangeMatrixEquiv x ∈ f4ShortRootRepresentedIdealMatrixBaseChange

A cotangent vector belongs to the ideal flag term exactly when its matrix coordinates belong to the base-changed represented ideal.

@[simp]

theorem TauCeti.DynkinType.mem_f4ShortRootCotangentFlagRange_iff {A : Type} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct (ZMod 2) A f4ShortRootCotangentDual) : x ∈ f4ShortRootCotangentFlagRange ↔ f4ShortRootCotangentBaseChangeMatrixEquiv x ∈ f4ShortRootRepresentedRangeMatrixBaseChange

A cotangent vector belongs to the range flag term exactly when its matrix coordinates belong to the base-changed represented range.

theorem TauCeti.DynkinType.f4ShortRootCotangentFlagIdeal_le_range {A : Type} [CommRing A] [Algebra (ZMod 2) A] : f4ShortRootCotangentFlagIdeal ≤ f4ShortRootCotangentFlagRange

The represented ideal is the first step of the represented range flag.

@[instance_reducible]

noncomputable def TauCeti.DynkinType.f4ShortRootCotangentAdjointComodule : Comodule (ZMod 2) (↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26)) f4ShortRootCotangentDual

The adjoint comodule structure used for the represented cotangent flag.

Equations

• TauCeti.DynkinType.f4ShortRootCotangentAdjointComodule = Derivation.adjointComodule

theorem TauCeti.DynkinType.f4ShortRoot_adjoint_blockTriangular_of_preserves_flag {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑(HopfAlgebra.points ↧A)) (hIdeal : ∀ {x : TensorProduct (ZMod 2) A f4ShortRootCotangentDual}, x ∈ f4ShortRootCotangentFlagIdeal → (Comodule.endOfPoint f4ShortRootCotangentDual g.ofConv) x ∈ f4ShortRootCotangentFlagIdeal) (hRange : ∀ {x : TensorProduct (ZMod 2) A f4ShortRootCotangentDual}, x ∈ f4ShortRootCotangentFlagRange → (Comodule.endOfPoint f4ShortRootCotangentDual g.ofConv) x ∈ f4ShortRootCotangentFlagRange) : ((Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).map ⇑g.ofConv).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

A point acts block triangularly on the adapted flag if it preserves its two nontrivial steps.