The type-A graph automorphism on the general linear group scheme

This file transports signed reverse-inverse-transpose from general-linear matrix points to the coordinate Hopf algebra. Its characteristic theorem identifies precomposition by the recovered coordinate automorphism with TauCeti.typeAGraphAutomorphism under the standard point equivalence.

This is the ambient general-linear input for descending the graph automorphism to the type-A standard carrier.

noncomputable def TauCeti.GeneralLinear.typeAGraphCoordinateIso (r : ℕ) : coordinateHopfAlgebra ℤ (r + 1) ≅ coordinateHopfAlgebra ℤ (r + 1)

The coordinate Hopf-algebra automorphism corresponding to signed reverse-inverse-transpose on general-linear points.

Equations

• TauCeti.GeneralLinear.typeAGraphCoordinateIso r = (TauCeti.CommHopfAlgCat.pointsFunctor.preimageIso (TauCeti.GeneralLinear.typeAGraphPointsNatIso✝ r)).unop

theorem TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_typeAGraphCoordinateIso (r : ℕ) (A : CommAlgCat ℤ) (f : ↑(HopfAlgebra.points A)) : (pointsMulEquiv (r + 1)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (typeAGraphCoordinateIso r).hom).app A)) f) = (typeAGraphAutomorphism r ↑A) ((pointsMulEquiv (r + 1)) f)

Mapping a general-linear coordinate point along typeAGraphCoordinateIso realizes the matrix graph automorphism.

theorem TauCeti.GeneralLinear.pointsMulEquiv_comp_typeAGraphCoordinateIso (r : ℕ) (A : CommAlgCat ℤ) (f : ↑(HopfAlgebra.points A)) : (pointsMulEquiv (r + 1)) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (typeAGraphCoordinateIso r).hom))) = (typeAGraphAutomorphism r ↑A) ((pointsMulEquiv (r + 1)) f)

Explicit precomposition form of the action of typeAGraphCoordinateIso.