Documentation

TauCeti.Algebra.Coalgebra.Comodule.Finite.ScalarExtension.Monoidal

Monoidal scalar extension of finite comodules #

For a commutative R-algebra A, scalar extension from finitely generated comodules to A-semimodules is a strong monoidal functor. Its tensorator is inverse base-change distributivity and its unit comparison is A ≃ A ⊗[R] R.

The construction follows Mathlib's monoidal structure on ModuleCat.extendScalars in Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction, adapted to semimodules and the finite comodule source category.

Main declarations #

source
@[instance_reducible]
noncomputable instance TauCeti.FGComoduleCat.instMonoidalScalarExtensionFunctor (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] :
(scalarExtensionFunctor R H A).Monoidal

Scalar extension from finitely generated comodules to semimodules is strong monoidal.

Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable def TauCeti.FGComoduleCat.scalarExtensionMonoidalFunctor (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] :
CategoryTheory.LaxMonoidalFunctor (FGComoduleCat R H) (SemimoduleCat A)

The scalar-extension functor on finite comodules, bundled as a lax monoidal functor.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FGComoduleCat.scalarExtensionMonoidalFunctor_toFunctor (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] :
    (scalarExtensionMonoidalFunctor R H A).toFunctor = scalarExtensionFunctor R H A

    The underlying functor of bundled monoidal scalar extension is scalar extension.

    source
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_μ (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (M N : FGComoduleCat R H) :
    CategoryTheory.Functor.LaxMonoidal.μ (scalarExtensionFunctor R H A) M N = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (SemimoduleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm) (CategoryTheory.eqToHom ⋯))

    Formula for the tensorator of finite-comodule scalar extension.

    source
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_ε (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] :
    CategoryTheory.Functor.LaxMonoidal.ε (scalarExtensionFunctor R H A) = CategoryTheory.CategoryStruct.comp (SemimoduleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.rid R A A).symm) (CategoryTheory.eqToHom ⋯)

    Formula for the unit comparison of finite-comodule scalar extension.

    source
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_δ (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (M N : FGComoduleCat R H) :
    CategoryTheory.Functor.OplaxMonoidal.δ (scalarExtensionFunctor R H A) M N = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (SemimoduleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)))

    Formula for the inverse tensorator of finite-comodule scalar extension.

    source
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_η (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] :
    CategoryTheory.Functor.OplaxMonoidal.η (scalarExtensionFunctor R H A) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (SemimoduleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.rid R A A))

    Formula for the inverse unit comparison of finite-comodule scalar extension.