Inheriting a comodule through an injective map #
A linear coaction inherits the comodule laws from an ambient comodule if its inclusion intertwines coactions and remains injective after tensoring with the double coalgebra. This permits restriction to split homogeneous pieces without assuming the coalgebra flat.
@[implicit_reducible]
def
TauCeti.Comodule.ofInjective
{R : Type u_1}
{C : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
[AddCommMonoid N]
[Module R N]
(ρ : N →ₗ[R] TensorProduct R N C)
(i : N →ₗ[R] M)
(hi : Function.Injective ⇑i)
(hiCC : Function.Injective ⇑(LinearMap.rTensor (TensorProduct R C C) i))
(hρ : LinearMap.rTensor C i ∘ₗ ρ = coact ∘ₗ i)
:
Comodule R C N
Inherit the comodule laws from an equivariant inclusion. Injectivity after tensoring
with C ⊗ C suffices for coassociativity; injectivity of the inclusion suffices for the
counit law. In particular, a split inclusion requires no flatness hypothesis on C.
Equations
- TauCeti.Comodule.ofInjective ρ i hi hiCC hρ = { coact := ρ, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }
Instances For
@[simp]
theorem
TauCeti.Comodule.ofInjective_coact
{R : Type u_1}
{C : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
[AddCommMonoid N]
[Module R N]
(ρ : N →ₗ[R] TensorProduct R N C)
(i : N →ₗ[R] M)
(hi : Function.Injective ⇑i)
(hiCC : Function.Injective ⇑(LinearMap.rTensor (TensorProduct R C C) i))
(hρ : LinearMap.rTensor C i ∘ₗ ρ = coact ∘ₗ i)
:
The coaction inherited through an inclusion is the specified linear coaction.