Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Kernel.Tensor

The kernel pair of an affine group homomorphism in coordinates #

For a coordinate morphism f : H ⟶ K, the kernel pair of Spec K → Spec H is isomorphic to Spec K × ker f. On points the isomorphism sends (g, n) to (g, g n); its inverse sends (g, h) to (g, g⁻¹ h). This file constructs the corresponding K-algebra equivalence K ⊗[H] K ≃ₐ[K] K ⊗[R] (K ⧸ kernelHopfIdeal f).

No flatness or surjectivity hypothesis is needed. The isomorphism supplies the kernel-pair calculation used to descend properties of affine-group morphisms from their kernels. The construction uses kernelHopfIdeal_toIdeal_le_ker_iff and the convolution functoriality of TauCeti.AlgHom.mapDomain and TauCeti.AlgHom.mapValue.

References #

source
noncomputable def TauCeti.CommHopfAlgCat.kernelPairTensorEquiv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
TensorProduct ↑H ↑K ↑K ≃ₐ[↑K] TensorProduct R (↑K) (↑K ⧸ (kernelHopfIdeal f).toIdeal)

The coordinate algebra of the kernel pair of an affine group homomorphism is the tensor product of the source coordinate algebra with that of its scheme-theoretic kernel. The map on points is (g,n) ↦ (g,gn).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.kernelPairTensorEquiv_tmul {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (x y : ↑K) :
    (kernelPairTensorEquiv f) (x ⊗ₜ[↑H] y) = x ⊗ₜ[R] 1 * (Algebra.TensorProduct.map (AlgHom.id R ↑K) (Ideal.Quotient.mkₐ R (kernelHopfIdeal f).toIdeal)) (CoalgebraStruct.comul y)

    On pure tensors, the kernel-pair equivalence multiplies the first factor by the comultiplication of the second, followed by projection onto the kernel coordinates.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.kernelPairTensorEquiv_symm_tmul_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (x y : ↑K) :
    (kernelPairTensorEquiv f).symm (x ⊗ₜ[R] (Ideal.Quotient.mk (kernelHopfIdeal f).toIdeal) y) = x ⊗ₜ[↑H] 1 * (Algebra.TensorProduct.mapOfCompatibleSMul (↑H) R ↑K ↑K ↑K) ((Algebra.TensorProduct.map (HopfAlgebra.antipodeAlgHom R ↑K) (AlgHom.id R ↑K)) (CoalgebraStruct.comul y))

    On a quotient representative, the inverse kernel-pair equivalence uses the antipode in the first leg of comultiplication and then balances the tensor product over H.