Commit 2025-05-16 10:01 4d4b317a

View on Github →

feat(RingTheory/Coalgebra/Equiv, RingTheory/Bialgebra/Equiv): constructors for coalgebra and bialgebra equivalences (#24121) Add constructors for equivalences of coalgebras and bialgebras, similar to what already exists for equivalences of algebras:

  • CoalgEquiv.ofCoalgHom constructs a CoalgEquiv from a CoalgHom that has an inverse;
  • CoalgEquiv.ofBijective constructs a CoalgEquiv from a bijective CoalgHom;
  • BialgEquiv.ofBialgHom constructs a BialgEquiv from a CoalgHom that has an inverse;
  • BialgEquiv.ofBijective constructs a BialgEquiv from a bijective BialgHom. Also add some apply and coe lemmas, following the same model as for AlgEquivs. From Toric

Estimated changes