Isomorphisms of R-coalgebras

This file defines bundled isomorphisms of R-coalgebras. We largely mirror the basic API of Mathlib/Algebra/Module/Equiv/Defs.lean.

Main definitions

• CoalgEquiv R A B: the type of R-coalgebra isomorphisms between A and B.

Notation

• A ≃ₗc[R] B : R-coalgebra equivalence from A to B.

structure CoalgEquiv (R : Type u_5) [CommSemiring R] (A : Type u_6) (B : Type u_7) [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] extends A →ₗc[R] B, A ≃ₗ[R] B : Type (max u_6 u_7)

An equivalence of coalgebras is an invertible coalgebra homomorphism.

• toFun : A → B
• map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : A) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• counit_comp : CoalgebraStruct.counit ∘ₗ self.toLinearMap = CoalgebraStruct.counit
• map_comp_comul : TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ self.toLinearMap
• invFun : B → A
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun

def «term_≃ₗc[_]_» : Lean.TrailingParserDescr

An equivalence of coalgebras is an invertible coalgebra homomorphism.

Equations

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

class CoalgEquivClass (F : Type u_5) (R : outParam (Type u_6)) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] extends CoalgHomClass F R A B, SemilinearEquivClass F (RingHom.id R) A B : Prop

CoalgEquivClass F R A B asserts F is a type of bundled coalgebra equivalences from A to B.

• map_add (f : F) (x y : A) : f (x + y) = f x + f y
• map_smulₛₗ (f : F) (c : R) (x : A) : f (c • x) = (RingHom.id R) c • f x
• counit_comp (f : F) : CoalgebraStruct.counit ∘ₗ ↑f = CoalgebraStruct.counit
• map_comp_comul (f : F) : TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f

def CoalgEquiv.ofClass {F : Type u_5} {R : Type u_6} {A : Type u_7} {B : Type u_8} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) : A ≃ₗc[R] B

Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence.

Equations

• ↑f = { toCoalgHom := ↑f, invFun := (↑f).invFun, left_inv := ⋯, right_inv := ⋯ }

@[deprecated CoalgEquiv.ofClass (since := "2026-09-08")]

def CoalgEquivClass.toCoalgEquiv {F : Type u_5} {R : Type u_6} {A : Type u_7} {B : Type u_8} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) : A ≃ₗc[R] B

Alias of CoalgEquiv.ofClass.

---

Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence.

Equations

• @CoalgEquivClass.toCoalgEquiv = @CoalgEquiv.ofClass

@[instance_reducible]

instance CoalgEquivClass.instCoeToCoalgEquiv {F : Type u_5} {R : Type u_6} {A : Type u_7} {B : Type u_8} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [CoalgEquivClass F R A B] : CoeHead F (A ≃ₗc[R] B)

Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence.

Equations

• CoalgEquivClass.instCoeToCoalgEquiv = { coe := fun (f : F) => ↑f }

def CoalgEquiv.toEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : (A ≃ₗc[R] B) → A ≃ B

The equivalence of types underlying a coalgebra equivalence.

Equations

• f.toEquiv = f.toLinearEquiv.toEquiv

theorem CoalgEquiv.toEquiv_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Function.Injective toEquiv

@[simp]

theorem CoalgEquiv.toEquiv_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e₁ e₂ : A ≃ₗc[R] B} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

theorem CoalgEquiv.toCoalgHom_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Function.Injective toCoalgHom

@[instance_reducible, macro_inline]

instance CoalgEquiv.instEquivLike {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : EquivLike (A ≃ₗc[R] B) A B

Equations

• CoalgEquiv.instEquivLike = { coe := fun (e : A ≃ₗc[R] B) => e.toFun, inv := CoalgEquiv.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

@[instance_reducible, macro_inline]

instance CoalgEquiv.instFunLike {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : FunLike (A ≃ₗc[R] B) A B

Equations

• CoalgEquiv.instFunLike = EquivLike.toFunLike

instance CoalgEquiv.instCoalgEquivClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : CoalgEquivClass (A ≃ₗc[R] B) R A B

@[instance_reducible]

instance CoalgEquiv.instCoeOutLinearEquivId {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : CoeOut (A ≃ₗc[R] B) (A ≃ₗ[R] B)

Equations

• CoalgEquiv.instCoeOutLinearEquivId = { coe := CoalgEquiv.toLinearEquiv }

@[simp]

theorem CoalgEquiv.toCoalgHom_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e₁ e₂ : A ≃ₗc[R] B} : ↑e₁ = ↑e₂ ↔ e₁ = e₂

@[simp]

theorem CoalgEquiv.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A → B} {h : ∀ (x y : A), f (x + y) = f x + f y} {h₀ : ∀ (m : R) (x : A), { toFun := f, map_add' := h }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h }.toFun x} {h₁ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = CoalgebraStruct.counit} {h₂ : TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ }} {h₃ : B → A} {h₄ : Function.LeftInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun} {h₅ : Function.RightInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun} : ⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ } = f

@[simp]

theorem CoalgEquiv.coe_ofClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑↑e = ⇑e

@[simp]

theorem CoalgEquiv.coe_coalgHomOfClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑↑e = ⇑e

@[deprecated CoalgEquiv.coe_coalgHomOfClass (since := "2026-09-09")]

theorem CoalgEquiv.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑↑e = ⇑e

Alias of CoalgEquiv.coe_coalgHomOfClass.

@[deprecated "Now a syntactic tautology" (since := "2026-04-12")]

theorem CoalgEquiv.toLinearEquiv_eq_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₗc[R] B) : f.toLinearEquiv = f.toLinearEquiv

@[simp]

theorem CoalgEquiv.toCoalgHom_eq_ofClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₗc[R] B) : f.toCoalgHom = ↑f

@[deprecated CoalgEquiv.toCoalgHom_eq_ofClass (since := "2026-09-09")]

theorem CoalgEquiv.toCoalgHom_eq_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₗc[R] B) : f.toCoalgHom = ↑f

Alias of CoalgEquiv.toCoalgHom_eq_ofClass.

@[simp]

theorem CoalgEquiv.coe_toLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑e.toLinearEquiv = ⇑e

@[deprecated CoalgEquiv.coe_coalgHomOfClass (since := "2026-09-09")]

theorem CoalgEquiv.coe_toCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑↑e = ⇑e

Alias of CoalgEquiv.coe_coalgHomOfClass.

theorem CoalgEquiv.toLinearEquiv_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ↑e.toLinearEquiv = ↑↑e

theorem CoalgEquiv.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e e' : A ≃ₗc[R] B} (h : ∀ (x : A), e x = e' x) : e = e'

theorem CoalgEquiv.ext_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e e' : A ≃ₗc[R] B} : e = e' ↔ ∀ (x : A), e x = e' x

theorem CoalgEquiv.congr_arg {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e : A ≃ₗc[R] B} {x x' : A} : x = x' → e x = e x'

theorem CoalgEquiv.congr_fun {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e e' : A ≃ₗc[R] B} (h : e = e') (x : A) : e x = e' x

def CoalgEquiv.symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : B ≃ₗc[R] A

Coalgebra equivalences are symmetric.

Equations

• e.symm = { toLinearMap := ↑e.toLinearEquiv.symm, counit_comp := ⋯, map_comp_comul := ⋯, invFun := e.toLinearEquiv.symm.invFun, left_inv := ⋯, right_inv := ⋯ }

def CoalgEquiv.Simps.apply {R : Type u_5} [CommSemiring R] {α : Type u_6} {β : Type u_7} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [CoalgebraStruct R α] [CoalgebraStruct R β] (f : α ≃ₗc[R] β) : α → β

See Note [custom simps projection]

Equations

• CoalgEquiv.Simps.apply f = ⇑f

def CoalgEquiv.Simps.symm_apply {R : Type u_5} [CommSemiring R] {A : Type u_6} {B : Type u_7} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : B → A

See Note [custom simps projection]

Equations

• CoalgEquiv.Simps.symm_apply e = ⇑e.symm

def CoalgEquiv.refl (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : A ≃ₗc[R] A

The identity map is a coalgebra equivalence.

Equations

• CoalgEquiv.refl R A = { toCoalgHom := CoalgHom.id R A, invFun := (LinearEquiv.refl R A).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CoalgEquiv.refl_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (x : A) : (refl R A) x = x

@[simp]

theorem CoalgEquiv.refl_symm_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (a✝ : A) : (refl R A).symm a✝ = a✝

@[simp]

theorem CoalgEquiv.refl_toLinearEquiv {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : (refl R A).toLinearEquiv = LinearEquiv.refl R A

@[simp]

theorem CoalgEquiv.refl_toCoalgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : ↑(refl R A) = CoalgHom.id R A

@[simp]

theorem CoalgEquiv.symm_toLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : e.symm.toLinearEquiv = e.toLinearEquiv.symm

theorem CoalgEquiv.coe_symm_toLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑e.toLinearEquiv.symm = ⇑e.symm

@[simp]

theorem CoalgEquiv.symm_toCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ↑↑e.symm = ↑e.toLinearEquiv.symm

@[simp]

theorem CoalgEquiv.symm_apply_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) (x : A) : e.symm (e x) = x

@[simp]

theorem CoalgEquiv.apply_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) (x : B) : e (e.symm x) = x

@[simp]

theorem CoalgEquiv.invFun_eq_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : e.invFun = ⇑e.symm

theorem CoalgEquiv.coe_toEquiv_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : e.toEquiv.symm = ↑e.symm

@[simp]

theorem CoalgEquiv.toEquiv_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : e.symm.toEquiv = e.toEquiv.symm

@[simp]

theorem CoalgEquiv.coe_toEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑e.toEquiv = ⇑e

@[simp]

theorem CoalgEquiv.coe_symm_toEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) : ⇑e.toEquiv.symm = ⇑e.symm

def CoalgEquiv.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Module R B] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (e₁₂ : A ≃ₗc[R] B) (e₂₃ : B ≃ₗc[R] C) : A ≃ₗc[R] C

Coalgebra equivalences are transitive.

Equations

• e₁₂.trans e₂₃ = { toCoalgHom := (↑e₂₃).comp ↑e₁₂, invFun := (e₁₂.toLinearEquiv.trans e₂₃.toLinearEquiv).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CoalgEquiv.trans_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Module R B] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (e₁₂ : A ≃ₗc[R] B) (e₂₃ : B ≃ₗc[R] C) (a✝ : C) : (e₁₂.trans e₂₃).symm a✝ = e₁₂.symm (e₂₃.symm a✝)

@[simp]

theorem CoalgEquiv.trans_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Module R B] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (e₁₂ : A ≃ₗc[R] B) (e₂₃ : B ≃ₗc[R] C) (x : A) : (e₁₂.trans e₂₃) x = e₂₃ (e₁₂ x)

theorem CoalgEquiv.trans_toLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Module R B] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] {e₁₂ : A ≃ₗc[R] B} {e₂₃ : B ≃ₗc[R] C} : (e₁₂.trans e₂₃).toLinearEquiv = e₁₂.toLinearEquiv ≪≫ₗ e₂₃.toLinearEquiv

@[simp]

theorem CoalgEquiv.trans_toCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Module R B] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] {e₁₂ : A ≃ₗc[R] B} {e₂₃ : B ≃ₗc[R] C} : ↑(e₁₂.trans e₂₃) = e₂₃.comp ↑e₁₂

@[simp]

theorem CoalgEquiv.coe_toEquiv_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Module R B] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] {e₁₂ : A ≃ₗc[R] B} {e₂₃ : B ≃ₗc[R] C} : (↑e₁₂).trans ↑e₂₃ = ↑(e₁₂.trans e₂₃)

def CoalgEquiv.ofCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [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) : A ≃ₗc[R] B

If a coalgebra morphism has an inverse, it is a coalgebra isomorphism.

Equations

• CoalgEquiv.ofCoalgHom f g h₁ h₂ = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, counit_comp := ⋯, map_comp_comul := ⋯, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CoalgEquiv.coe_ofCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [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) : ↑(ofCoalgHom f g h₁ h₂) = f

theorem CoalgEquiv.ofCoalgHom_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [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) : (ofCoalgHom f g h₁ h₂).symm = ofCoalgHom g f h₂ h₁

noncomputable def CoalgEquiv.ofBijective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (hf : Function.Bijective ⇑f) : A ≃ₗc[R] B

Promotes a bijective coalgebra homomorphism to a coalgebra equivalence.

Equations

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

@[simp]

theorem CoalgEquiv.ofBijective_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (hf : Function.Bijective ⇑f) (a : A) : (ofBijective hf) a = f a

@[simp]

theorem CoalgEquiv.coe_ofBijective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (hf : Function.Bijective ⇑f) : ⇑(ofBijective hf) = ⇑f

@[reducible]

def CoalgEquiv.toCoalgebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R B] (f : A ≃ₗc[R] B) : Coalgebra R B

Let A be an R-coalgebra and let B be an R-module with a CoalgebraStruct. A linear equivalence A ≃ₗ[R] B that respects the CoalgebraStructs defines an R-coalgebra structure on B.

Equations

• f.toCoalgebra = { toCoalgebraStruct := inst✝, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }