Theorems · Theorem · ring theory

CoalgEquiv.ofCoalgHom_symm

∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (f : A →ₗc[R] B) (g : B →ₗc[R] A) (h₁ : f.comp g = CoalgHom.id R B)
  (h₂ : g.comp f = CoalgHom.id R A), (CoalgEquiv.ofCoalgHom f g h₁ h₂).symm = CoalgEquiv.ofCoalgHom g f h₂ h₁

Defined in

Mathlib.RingTheory.Coalgebra.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleCoalgebraStructCoalgebraStruct