Theorems · Inductive type · ring theory

Submodule.IsCoideal

{R : Type u_1} →
  {C : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup C] → [inst_2 : Module R C] → [CoalgebraStruct R C] → Submodule R C → Prop

An R-submodule I of an R-coalgebra C is a coideal if the counit vanishes on I and the comultiplication descends through the module quotient C ⧸ I.

Defined in

Mathlib.RingTheory.Coalgebra.Quotient

Cited by

17 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModuleCoalgebraStruct