Isomorphisms of R-coalgebras

This file defines bundled isomorphisms of R-coalgebras. We simply mimic the early parts of Mathlib/Algebra/Module/Equiv.lean.

Main definitions

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

Notations

• 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 : Coalgebra.counit ∘ₗ self.toLinearMap = Coalgebra.counit
• map_comp_comul : TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ Coalgebra.comul = Coalgebra.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) : Coalgebra.counit ∘ₗ ↑f = Coalgebra.counit
• map_comp_comul (f : F) : TensorProduct.map ↑f ↑f ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ ↑f

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

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

Equations

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

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 CoalgEquiv.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 CoalgEquiv.toCoalgHom

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 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 = { coe := DFunLike.coe, coe_injective' := ⋯ }

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

@[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₁ : Coalgebra.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = Coalgebra.counit} {h₂ : TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ Coalgebra.comul = Coalgebra.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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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 = ⇑e

@[simp]

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

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 = ↑↑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.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.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_invFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (a✝ : A) : (CoalgEquiv.refl R A).invFun a✝ = a✝

@[simp]

theorem CoalgEquiv.refl_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (a : A) : (CoalgEquiv.refl R A) 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] : ↑(CoalgEquiv.refl R A) = 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] : ↑(CoalgEquiv.refl R A) = CoalgHom.id R A

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).symm, counit_comp := ⋯, map_comp_comul := ⋯, invFun := (↑e).symm.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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 = (↑e).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).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).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

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

@[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

@[simp]

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

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_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✝ : A) : (e₁₂.trans e₂₃) a✝ = e₂₃ (e₁₂ a✝)

@[simp]

theorem CoalgEquiv.trans_invFun {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₂₃).invFun a✝ = (↑e₁₂).symm ((↑e₂₃).symm a✝)

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₂₃) = ↑e₁₂ ≪≫ₗ ↑e₂₃

@[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₂₃)

@[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 = Coalgebra.mk ⋯ ⋯ ⋯