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.

source

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 CoalgHom :

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
The backwards directed function underlying a linear equivalence.
left_inv : Function.LeftInverse self.invFun self.toFun
LinearEquiv.invFun is a left inverse to the linear equivalence's underlying function.
right_inv : Function.RightInverse self.invFun self.toFun
LinearEquiv.invFun is a right inverse to the linear equivalence's underlying function.

Instances For

source

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.

Instances For

source

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 :

Prop

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

Instances

source

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 = let __src := ↑f; let __src_1 := ↑f; { toCoalgHom := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

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 }

source

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

Instances For

source

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

source

@[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₁ : A ≃ₗc[R] B} {e₂ : A ≃ₗc[R] B} :

e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

source

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

source

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' := ⋯ }

source

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' := ⋯ }

source

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

Equations

⋯ = ⋯

source

@[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₁ : A ≃ₗc[R] B} {e₂ : A ≃ₗc[R] B} :

↑e₁ = ↑e₂ ↔ e₁ = e₂

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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 : A ≃ₗc[R] B} {e' : A ≃ₗc[R] B} (h : ∀ (x : A), e x = e' x) :

e = e'

source

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 : A ≃ₗc[R] B} {e' : A ≃ₗc[R] B} :

e = e' ↔ ∀ (x : A), e x = e' x

source

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 : A} {x' : A} :

x = x' → e x = e x'

source

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 : A ≃ₗc[R] B} {e' : A ≃ₗc[R] B} (h : e = e') (x : A) :

e x = e' x

source

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

source

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

source

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 = let __src := CoalgHom.id R A; let __src_1 := LinearEquiv.refl R A; { toCoalgHom := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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₂₃ = let __src := (↑e₂₃).comp ↑e₁₂; let __src_1 := e₁₂.toLinearEquiv.trans e₂₃.toLinearEquiv; { toCoalgHom := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }