The category of comodules over a coalgebra

This file bundles the right comodules defined in TauCeti.Algebra.Coalgebra.Comodule.Basic into a category. For a fixed coalgebra C over a commutative semiring R, objects are R-semimodules with a right C-coaction and morphisms are the comodule morphisms already defined by Comodule.Hom.

The reductive-groups roadmap asks for the category of finite-dimensional comodules over a Hopf algebra as the representation category of an affine group scheme. This file supplies the underlying bundled category and its forgetful functor to SemimoduleCat; finiteness, tensor products, duals, and the Hopf-algebra specialization can be added on top.

Main definitions

• TauCeti.ComoduleCat: bundled right comodules over a fixed coalgebra.
• TauCeti.ComoduleCat.of: build a bundled comodule from an unbundled one.
• TauCeti.ComoduleCat.ofHom: view an unbundled comodule morphism as a categorical morphism.
• forget₂ (ComoduleCat R C) (SemimoduleCat R): the forgetful functor to semimodules.

References

This is the categorical packaging of the standard right-comodule definition, added for Layer 1 of the Tau Ceti reductive-groups roadmap: "Comodules over a coalgebra/Hopf algebra". The bundled-category API follows the pattern of Mathlib.Algebra.Category.CoalgCat.Basic and Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

structure TauCeti.ComoduleCat (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] extends SemimoduleCat R : Type (max (max u v) (w + 1))

The category of right comodules over a fixed R-coalgebra C.

• carrier : Type w
• isAddCommMonoid : AddCommMonoid ↑self.toSemimoduleCat
• isModule : Module R ↑self.toSemimoduleCat
• instComodule : Comodule R C ↑self.toSemimoduleCat

  The right C-comodule structure on the underlying module.

@[instance_reducible]

instance TauCeti.ComoduleCat.instCoeSortType (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] : CoeSort (ComoduleCat R C) (Type w)

Equations

• TauCeti.ComoduleCat.instCoeSortType R C = { coe := fun (M : TauCeti.ComoduleCat R C) => ↑M.toSemimoduleCat }

@[instance_reducible]

instance TauCeti.ComoduleCat.instAddCommMonoidCarrier (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) : AddCommMonoid ↑M.toSemimoduleCat

Equations

• TauCeti.ComoduleCat.instAddCommMonoidCarrier R C M = M.isAddCommMonoid

@[instance_reducible]

instance TauCeti.ComoduleCat.instModuleCarrier (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) : Module R ↑M.toSemimoduleCat

Equations

• TauCeti.ComoduleCat.instModuleCarrier R C M = M.isModule

@[reducible, inline]

abbrev TauCeti.ComoduleCat.of (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R C M] : ComoduleCat R C

Build a bundled comodule from a type carrying the usual unbundled typeclasses.

Equations

• TauCeti.ComoduleCat.of R C M = { carrier := M, isAddCommMonoid := inst✝², isModule := inst✝¹, instComodule := inferInstance }

@[simp]

theorem TauCeti.ComoduleCat.of_coact (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] : Comodule.coact = Comodule.coact

The coaction on ComoduleCat.of is the original unbundled coaction.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.Hom (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : Type w

Morphisms in ComoduleCat are morphisms of the underlying right comodules.

Equations

• TauCeti.ComoduleCat.Hom R C M N = TauCeti.Comodule.Hom R C ↑M.toSemimoduleCat ↑N.toSemimoduleCat

@[instance_reducible]

instance TauCeti.ComoduleCat.category (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Category.{w, max (max u v) (w + 1)} (ComoduleCat R C)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.ComoduleCat.homZero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : Zero (M ⟶ N)

The zero structure on categorical morphisms is the zero comodule morphism.

Equations

• TauCeti.ComoduleCat.homZero R C M N = { zero := let __LinearMap := 0; { toLinearMap := __LinearMap, map_coact := ⋯ } }

@[instance_reducible]

instance TauCeti.ComoduleCat.homAdd (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : Add (M ⟶ N)

Addition of categorical morphisms is pointwise addition of comodule morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.ComoduleCat.homAddCommMonoid (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : AddCommMonoid (M ⟶ N)

Categorical morphisms form an additive commutative monoid under pointwise operations.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.ComoduleCat.homSMul (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : SMul R (M ⟶ N)

Scalar multiplication of categorical morphisms is pointwise scalar multiplication of comodule morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.ComoduleCat.homModule (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : Module R (M ⟶ N)

Categorical morphisms form an R-module under pointwise operations.

Equations

• TauCeti.ComoduleCat.homModule R C M N = { toSMul := TauCeti.ComoduleCat.homSMul R C M N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance TauCeti.ComoduleCat.concreteCategory (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.ConcreteCategory (ComoduleCat R C) fun (M N : ComoduleCat R C) => Comodule.Hom R C ↑M.toSemimoduleCat ↑N.toSemimoduleCat

ComoduleCat is concrete, with concrete morphisms the bundled comodule morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.hom (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : Comodule.Hom R C ↑M.toSemimoduleCat ↑N.toSemimoduleCat

Turn a morphism in ComoduleCat back into its underlying comodule morphism.

Equations

• TauCeti.ComoduleCat.hom R C f = f

@[reducible, inline]

abbrev TauCeti.ComoduleCat.ofHom (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Comodule.Hom R C M N) : of R C M ⟶ of R C N

Typecheck an unbundled comodule morphism as a morphism in ComoduleCat.

Equations

• TauCeti.ComoduleCat.ofHom R C f = f

@[simp]

theorem TauCeti.ComoduleCat.hom_ofHom (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Comodule.Hom R C M N) : CategoryTheory.ConcreteCategory.hom (ofHom R C f) = f

Turning an unbundled comodule morphism into a categorical morphism and back is the identity.

@[simp]

theorem TauCeti.ComoduleCat.ofHom_hom (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : ofHom R C (CategoryTheory.ConcreteCategory.hom f) = f

Turning a categorical morphism into an unbundled comodule morphism and back is the identity.

@[simp]

theorem TauCeti.ComoduleCat.ofHom_id (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] : ofHom R C (Comodule.Hom.id R C M) = CategoryTheory.CategoryStruct.id (of R C M)

The categorical identity is the bundled form of the identity comodule morphism.

@[simp]

theorem TauCeti.ComoduleCat.ofHom_comp (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Comodule.Hom R C M N) (g : Comodule.Hom R C N P) : ofHom R C (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom R C f) (ofHom R C g)

Categorical composition is the bundled form of composition of comodule morphisms.

@[simp]

theorem TauCeti.ComoduleCat.ofHom_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Comodule.Hom R C M N) (m : M) : (CategoryTheory.ConcreteCategory.hom (ofHom R C f)) m = f m

The bundled form of a comodule morphism applies as the original morphism.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.homLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : ↑M.toSemimoduleCat →ₗ[R] ↑N.toSemimoduleCat

The underlying linear map of a ComoduleCat morphism.

Equations

• TauCeti.ComoduleCat.homLinearMap R C f = f.toLinearMap

theorem TauCeti.ComoduleCat.hom_ext (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} {f g : M ⟶ N} (h : ∀ (m : (fun (X : ComoduleCat R C) => ↑X.toSemimoduleCat) M), (CategoryTheory.ConcreteCategory.hom f) m = (CategoryTheory.ConcreteCategory.hom g) m) : f = g

Two morphisms of bundled comodules are equal when their underlying functions are equal.

theorem TauCeti.ComoduleCat.hom_ext_iff {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} {f g : M ⟶ N} : f = g ↔ ∀ (m : (fun (X : ComoduleCat R C) => ↑X.toSemimoduleCat) M), (CategoryTheory.ConcreteCategory.hom f) m = (CategoryTheory.ConcreteCategory.hom g) m

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_id (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) : (CategoryTheory.CategoryStruct.id M).toLinearMap = LinearMap.id

The identity morphism has the identity linear map underneath.

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_comp (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ N) (g : N ⟶ P) : (CategoryTheory.CategoryStruct.comp f g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Composition in ComoduleCat is composition of the underlying linear maps.

@[simp]

theorem TauCeti.ComoduleCat.id_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) m = m

The identity morphism acts as the identity function.

@[simp]

theorem TauCeti.ComoduleCat.comp_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ N) (g : N ⟶ P) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) m = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) m)

Composition of morphisms acts by ordinary function composition.

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : Comodule.Hom.toLinearMap 0 = 0

The zero morphism has the zero linear map underneath.

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_add (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f g : M ⟶ N) : (f + g).toLinearMap = f.toLinearMap + g.toLinearMap

Addition of morphisms is addition of the underlying linear maps.

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_nsmul (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (n : ℕ) (f : M ⟶ N) : (n • f).toLinearMap = n • f.toLinearMap

Natural-number scalar multiplication of morphisms is natural-number scalar multiplication of the underlying linear maps.

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_smul (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (r : R) (f : M ⟶ N) : (r • f).toLinearMap = r • f.toLinearMap

Scalar multiplication of morphisms is scalar multiplication of the underlying linear maps.

@[simp]

theorem TauCeti.ComoduleCat.toLinearMap_sum (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} {M N : ComoduleCat R C} (s : Finset ι) (f : ι → (M ⟶ N)) : (∑ i ∈ s, f i).toLinearMap = ∑ i ∈ s, (f i).toLinearMap

Finite sums of morphisms are finite sums of the underlying linear maps.

@[simp]

theorem TauCeti.ComoduleCat.zero_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom 0) m = 0

The zero morphism acts as the zero function.

@[simp]

theorem TauCeti.ComoduleCat.add_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f g : M ⟶ N) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (f + g)) m = (CategoryTheory.ConcreteCategory.hom f) m + (CategoryTheory.ConcreteCategory.hom g) m

Addition of morphisms acts by pointwise addition.

@[simp]

theorem TauCeti.ComoduleCat.nsmul_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (n : ℕ) (f : M ⟶ N) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (n • f)) m = n • (CategoryTheory.ConcreteCategory.hom f) m

Natural-number scalar multiplication of morphisms acts by pointwise natural-number scalar multiplication.

@[simp]

theorem TauCeti.ComoduleCat.smul_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (r : R) (f : M ⟶ N) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (r • f)) m = r • (CategoryTheory.ConcreteCategory.hom f) m

Scalar multiplication of morphisms acts by pointwise scalar multiplication.

@[simp]

theorem TauCeti.ComoduleCat.sum_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} {M N : ComoduleCat R C} (s : Finset ι) (f : ι → (M ⟶ N)) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (∑ i ∈ s, f i)) m = ∑ i ∈ s, (CategoryTheory.ConcreteCategory.hom (f i)) m

Finite sums of morphisms act by pointwise finite sums.

@[simp]

theorem TauCeti.ComoduleCat.add_comp (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f g : M ⟶ N) (h : N ⟶ P) : CategoryTheory.CategoryStruct.comp (f + g) h = CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h

Composition in ComoduleCat is additive in the left morphism.

@[simp]

theorem TauCeti.ComoduleCat.comp_add (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ N) (g h : N ⟶ P) : CategoryTheory.CategoryStruct.comp f (g + h) = CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h

Composition in ComoduleCat is additive in the right morphism.

@[simp]

theorem TauCeti.ComoduleCat.smul_comp (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (r : R) (f : M ⟶ N) (g : N ⟶ P) : CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g

Composition in ComoduleCat is compatible with scalar multiplication in the left morphism.

@[simp]

theorem TauCeti.ComoduleCat.comp_smul (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (r : R) (f : M ⟶ N) (g : N ⟶ P) : CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g

Composition in ComoduleCat is compatible with scalar multiplication in the right morphism.

theorem TauCeti.ComoduleCat.zero_comp (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : N ⟶ P) : CategoryTheory.CategoryStruct.comp 0 f = 0

Composing the zero morphism on the left gives the zero morphism.

theorem TauCeti.ComoduleCat.comp_zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f 0 = 0

Composing the zero morphism on the right gives the zero morphism.

@[instance_reducible]

instance TauCeti.ComoduleCat.hasZeroMorphisms (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.HasZeroMorphisms (ComoduleCat R C)

ComoduleCat has the standard categorical zero morphisms.

Equations

• TauCeti.ComoduleCat.hasZeroMorphisms R C = { zero := inferInstance, comp_zero := ⋯, zero_comp := ⋯ }

@[instance_reducible]

instance TauCeti.ComoduleCat.hasForgetToSemimodule (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.HasForget₂ (ComoduleCat R C) (SemimoduleCat R)

The forgetful functor from comodules to their underlying semimodules.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ComoduleCat.forget₂_obj (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) : (CategoryTheory.forget₂ (ComoduleCat R C) (SemimoduleCat R)).obj M = ↧↑M.toSemimoduleCat

The forgetful functor sends a comodule to its underlying semimodule.

@[simp]

theorem TauCeti.ComoduleCat.forget₂_map (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : (CategoryTheory.forget₂ (ComoduleCat R C) (SemimoduleCat R)).map f = SemimoduleCat.ofHom f.toLinearMap

The forgetful functor sends a comodule morphism to its underlying linear map.

def TauCeti.ComoduleCat.isoToLinearEquiv (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat

A categorical isomorphism of comodules induces the underlying linear equivalence.

Equations

• TauCeti.ComoduleCat.isoToLinearEquiv R C i = ((CategoryTheory.forget₂ (TauCeti.ComoduleCat R C) (SemimoduleCat R)).mapIso i).toLinearEquivₛ

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_toLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) : ↑(isoToLinearEquiv R C i) = i.hom.toLinearMap

The linear equivalence induced by a comodule isomorphism has the isomorphism's forward comodule morphism underneath.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_symm_toLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) : ↑(isoToLinearEquiv R C i).symm = i.inv.toLinearMap

The inverse of the linear equivalence induced by a comodule isomorphism has the isomorphism's inverse comodule morphism underneath.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) (m : ↑M.toSemimoduleCat) : (isoToLinearEquiv R C i) m = (CategoryTheory.ConcreteCategory.hom i.hom) m

The linear equivalence induced by a comodule isomorphism applies as its forward morphism.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_symm_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) (n : ↑N.toSemimoduleCat) : (isoToLinearEquiv R C i).symm n = (CategoryTheory.ConcreteCategory.hom i.inv) n

The inverse linear equivalence induced by a comodule isomorphism applies as the inverse morphism.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_refl (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) : isoToLinearEquiv R C (CategoryTheory.Iso.refl M) = LinearEquiv.refl R ↑M.toSemimoduleCat

The linear equivalence induced by the identity comodule isomorphism is the identity.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_symm (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) : isoToLinearEquiv R C i.symm = (isoToLinearEquiv R C i).symm

The linear equivalence induced by the inverse comodule isomorphism is the inverse linear equivalence.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_trans (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (i : M ≅ N) (j : N ≅ P) : isoToLinearEquiv R C (i ≪≫ j) = isoToLinearEquiv R C i ≪≫ₗ isoToLinearEquiv R C j

The linear equivalence induced by a composite comodule isomorphism is the composite of the induced linear equivalences.

def TauCeti.ComoduleCat.isoOfLinearEquiv (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (e : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) : M ≅ N

Build a comodule isomorphism from a linear equivalence whose forward map respects the coactions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ComoduleCat.isoOfLinearEquiv_hom_toLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (e : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) : (isoOfLinearEquiv R C e h).hom.toLinearMap = ↑e

The forward morphism of isoOfLinearEquiv has the original linear equivalence underneath.

@[simp]

theorem TauCeti.ComoduleCat.isoOfLinearEquiv_inv_toLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (e : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) : (isoOfLinearEquiv R C e h).inv.toLinearMap = ↑e.symm

The inverse morphism of isoOfLinearEquiv has the inverse linear equivalence underneath.

@[simp]

theorem TauCeti.ComoduleCat.isoOfLinearEquiv_hom_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (e : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (isoOfLinearEquiv R C e h).hom) m = e m

The forward morphism of isoOfLinearEquiv applies as the original linear equivalence.

@[simp]

theorem TauCeti.ComoduleCat.isoOfLinearEquiv_inv_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (e : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) (n : ↑N.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (isoOfLinearEquiv R C e h).inv) n = e.symm n

The inverse morphism of isoOfLinearEquiv applies as the inverse linear equivalence.

@[simp]

theorem TauCeti.ComoduleCat.isoToLinearEquiv_isoOfLinearEquiv (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (e : ↑M.toSemimoduleCat ≃ₗ[R] ↑N.toSemimoduleCat) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) : isoToLinearEquiv R C (isoOfLinearEquiv R C e h) = e

Converting isoOfLinearEquiv back to a linear equivalence recovers the original linear equivalence.

@[simp]

theorem TauCeti.ComoduleCat.isoOfLinearEquiv_isoToLinearEquiv (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (i : M ≅ N) : isoOfLinearEquiv R C (isoToLinearEquiv R C i) ⋯ = i

Rebuilding a comodule isomorphism from its induced linear equivalence recovers the original isomorphism.