Documentation

TauCeti.Algebra.Coalgebra.Comodule.Finite.ScalarExtension.Basic

Scalar extension of comodules #

Let C be a coalgebra over a commutative semiring R, and let A be an R-algebra. This file restricts scalar extension of the underlying-module functor to finitely generated comodules:

FGComoduleCat R C ⥤ SemimoduleCat A,    M ↦ A ⊗[R] M.

No finiteness or bialgebra structure is needed for the construction.

An automorphism of this functor is the same data as a family of A-linear automorphisms of the scalar extensions that is natural in the comodule, and autOfComponents assembles one from the other. Nothing beyond the coalgebra structure enters, and the value algebra need not be commutative.

Main declarations #

source
noncomputable def TauCeti.FGComoduleCat.scalarExtensionFunctor (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] :
CategoryTheory.Functor (FGComoduleCat R C) (SemimoduleCat A)

Scalar extension of the underlying-module functor on finitely generated comodules.

Equations
Instances For
    source
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_def (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] :
    scalarExtensionFunctor R C A = incl.comp (ComoduleCat.scalarExtensionFunctor R C A)

    Finite-comodule scalar extension is obtained by precomposing scalar extension on all comodules with the inclusion functor.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_obj (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (M : FGComoduleCat R C) :
    (scalarExtensionFunctor R C A).obj M = ↧(TensorProduct R A ↑M)

    Finite-comodule scalar extension sends M to the semimodule A ⊗[R] M.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.scalarExtensionFunctor_map (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] {M N : FGComoduleCat R C} (f : M ⟶ N) :
    (scalarExtensionFunctor R C A).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (SemimoduleCat.ofHom (LinearMap.baseChange A f.hom.toLinearMap)) (CategoryTheory.eqToHom ⋯))

    Scalar extension maps a finite-comodule morphism to base change of its underlying linear map.

    source
    noncomputable def TauCeti.FGComoduleCat.autOfComponents (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (F : (M : FGComoduleCat R C) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hnat : ∀ {M N : FGComoduleCat R C} (g : M ⟶ N), LinearMap.baseChange A g.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A g.hom.toLinearMap) :
    CategoryTheory.Aut (scalarExtensionFunctor R C A)

    A family of A-linear automorphisms of the scalar extensions of the finitely generated comodules, natural in the comodule, as an automorphism of the scalar-extension functor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.FGComoduleCat.autOfComponents_hom_app (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (F : (M : FGComoduleCat R C) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hnat : ∀ {M N : FGComoduleCat R C} (g : M ⟶ N), LinearMap.baseChange A g.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A g.hom.toLinearMap) (M : FGComoduleCat R C) :
      (autOfComponents R C A F ⋯).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F M).toLinearEquiv.toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))

      The component of the automorphism assembled from a natural family of linear automorphisms is that family, transported to the object chosen by the scalar-extension functor.

      source
      @[simp]
      theorem TauCeti.FGComoduleCat.autOfComponents_inv_app (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (F : (M : FGComoduleCat R C) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hnat : ∀ {M N : FGComoduleCat R C} (g : M ⟶ N), LinearMap.baseChange A g.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A g.hom.toLinearMap) (M : FGComoduleCat R C) :
      (autOfComponents R C A F ⋯).inv.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F M).toLinearEquiv.toModuleIsoₛ.inv (CategoryTheory.eqToHom ⋯))

      The inverse component of the automorphism assembled from a natural family of linear automorphisms is the inverse family, transported the same way.

      source
      theorem TauCeti.FGComoduleCat.autOfComponents_mul_natural (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (F G : (M : FGComoduleCat R C) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hF : ∀ {M N : FGComoduleCat R C} (f : M ⟶ N), LinearMap.baseChange A f.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap) (hG : ∀ {M N : FGComoduleCat R C} (f : M ⟶ N), LinearMap.baseChange A f.hom.toLinearMap ∘ₗ ↑(G M) = ↑(G N) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap) {M N : FGComoduleCat R C} (f : M ⟶ N) :
      LinearMap.baseChange A f.hom.toLinearMap ∘ₗ (↑(F M) * ↑(G M)) = (↑(F N) * ↑(G N)) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap

      The pointwise product of two natural families of automorphisms is natural.

      source
      theorem TauCeti.FGComoduleCat.autOfComponents_mul (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (F G : (M : FGComoduleCat R C) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hF : ∀ {M N : FGComoduleCat R C} (f : M ⟶ N), LinearMap.baseChange A f.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap) (hG : ∀ {M N : FGComoduleCat R C} (f : M ⟶ N), LinearMap.baseChange A f.hom.toLinearMap ∘ₗ ↑(G M) = ↑(G N) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap) :
      autOfComponents R C A F ⋯ * autOfComponents R C A G ⋯ = autOfComponents R C A (fun (M : FGComoduleCat R C) => F M * G M) ⋯

      Assembly by autOfComponents preserves pointwise multiplication.

      source
      theorem TauCeti.FGComoduleCat.autOfComponents_congr (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (F G : (M : FGComoduleCat R C) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hF : ∀ {M N : FGComoduleCat R C} (f : M ⟶ N), LinearMap.baseChange A f.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap) (hG : ∀ {M N : FGComoduleCat R C} (f : M ⟶ N), LinearMap.baseChange A f.hom.toLinearMap ∘ₗ ↑(G M) = ↑(G N) ∘ₗ LinearMap.baseChange A f.hom.toLinearMap) (h : ∀ (M : FGComoduleCat R C), F M = G M) :
      autOfComponents R C A F ⋯ = autOfComponents R C A G ⋯

      Pointwise equal natural families assemble to the same automorphism.