Documentation

TauCeti.Algebra.AlgebraicGroup.Representation.Tannaka.BaseChange

Base change of tensor automorphisms of scalar extension #

Let H be a bialgebra over a commutative semiring R, and let f : A →ₐ[R] B be a morphism of commutative R-algebras. A tensor automorphism of scalar extension on the finite H-comodules has, at each comodule M, an A-linear automorphism of A ⊗[R] M. Base changing those components along f produces a tensor automorphism over B, and this is functorial in the value algebra. No antipode is needed for the assembly or base change: these use only the monoidal structure on finite comodules. Compatibility with the point action additionally assumes a Hopf algebra, whose antipode makes each point action invertible.

The base-changed family is natural in the comodule, is the identity at the tensor unit, and is compatible with the tensor comparison, because base change of endomorphisms (Module.End.mapValue) preserves each of those. Feeding it to TauCeti.Tannaka.monoidalAutOfComponents produces the base-changed tensor automorphism.

Compatibility with the point action is tensorAutMapValue_fgPointTensorIso: pushing a point forward along f and acting agrees with acting and then base changing the tensor automorphism. Together with reconstruction this makes the Tannakian equivalence natural in the value algebra; see TauCeti.Algebra.AlgebraicGroup.Representation.Tannaka.GroupFunctor.

Main declarations #

References #

source
noncomputable def TauCeti.Tannaka.tensorAutMapValue (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) :
CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H B)

Base change of a tensor automorphism of finite-comodule scalar extension along a morphism of value algebras: base change each transported component.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Tannaka.scalarExtensionComponent_tensorAutMapValue (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) :
    scalarExtensionComponent R H B (tensorAutMapValue R H A B f η) M = Module.End.mapValue f (scalarExtensionComponent R H A η M)

    The transported component of a base-changed tensor automorphism is the base change of the transported component.

    source
    noncomputable def TauCeti.Tannaka.tensorAutMapValueHom (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) :
    CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A) →* CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H B)

    Base change of tensor automorphisms along a morphism of value algebras, as a group homomorphism.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Tannaka.tensorAutMapValueHom_apply (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) :
      (tensorAutMapValueHom R H A B f) η = tensorAutMapValue R H A B f η

      The bundled base-change homomorphism acts by tensorAutMapValue.

      source
      theorem TauCeti.Tannaka.scalarExtensionComponent_tensorAutMapValue_comp_rTensor (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) :
      ↑R (scalarExtensionComponent R H B (tensorAutMapValue R H A B f η) M) ∘ₗ LinearMap.rTensor (↑M) f.toLinearMap = LinearMap.rTensor (↑M) f.toLinearMap ∘ₗ ↑R (scalarExtensionComponent R H A η M)

      The transport square characterizing the components of a base-changed tensor automorphism: they are compatible with the original components along the comparison of scalar extensions.

      source
      @[simp]
      theorem TauCeti.Tannaka.tensorAutMapValue_id (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) :
      tensorAutMapValue R H A A (AlgHom.id R A) η = η

      Base change along the identity morphism of value algebras is the identity.

      source
      @[simp]
      theorem TauCeti.Tannaka.tensorAutMapValue_comp (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (C : Type u) [CommSemiring C] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) :
      tensorAutMapValue R H A C (g.comp f) η = tensorAutMapValue R H B C g (tensorAutMapValue R H A B f η)

      Base change along a composite of morphisms of value algebras is the composite of base changes.

      source
      @[simp]
      theorem TauCeti.Tannaka.tensorAutMapValue_fgPointTensorIso (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (g : WithConv (H →ₐ[R] A)) :
      tensorAutMapValue R H A B f (fgPointTensorIso R H A g) = fgPointTensorIso R H B ((AlgHom.mapValue f) g)

      Base change of tensor automorphisms is compatible with the point action: pushing an algebra-valued point forward along f and acting agrees with acting and then base changing.