Isomorphisms of `R`-bialgebras #

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

Main definitions #

BialgEquiv R A B: the type of R-bialgebra isomorphisms between A and B.

Notations #

A ≃ₐc[R] B : R-bialgebra equivalence from A to B.

source

structure BialgEquiv (R : Type u) [CommSemiring R] (A : Type v) (B : Type w) [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] extends A ≃ₗc[R] B, A ≃* B :

Type (max v w)

An equivalence of bialgebras is an invertible bialgebra 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
map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y

Instances For

source

def «term_≃ₐc[_]_» :

Lean.TrailingParserDescr

An equivalence of bialgebras is an invertible bialgebra homomorphism.

Equations

Instances For

source

class BialgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] extends CoalgEquivClass F R A B, MulEquivClass F A B :

Prop

BialgEquivClass F R A B asserts F is a type of bundled bialgebra 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
map_mul (f : F) (a b : A) : f (a * b) = f a * f b

Instances

source

@[instance 100]

instance BialgEquivClass.toBialgHomClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [BialgEquivClass F R A B] :

BialgHomClass F R A B

source

def BialgEquivClass.toBialgEquiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [BialgEquivClass F R A B] (f : F) :

A ≃ₐc[R] B

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

Equations

Instances For

source

instance BialgEquivClass.instCoeToBialgEquiv {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [BialgEquivClass F R A B] :

CoeHead F (A ≃ₐc[R] B)

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

Equations

source

@[instance 100]

instance BialgEquivClass.toAlgEquivClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [EquivLike F A B] [BialgEquivClass F R A B] :

AlgEquivClass F R A B

source

def BialgEquiv.toBialgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐc[R] B) :

A →ₐc[R] B

The bialgebra morphism underlying a bialgebra equivalence.

Equations

Instances For

source

def BialgEquiv.toAlgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐc[R] B) :

A ≃ₐ[R] B

The algebra equivalence underlying a bialgebra equivalence.

Equations

Instances For

source

def BialgEquiv.toEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :

(A ≃ₐc[R] B) → A ≃ B

The equivalence of types underlying a bialgebra equivalence.

Equations

Instances For

source

theorem BialgEquiv.toEquiv_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :

Function.Injective toEquiv

source

@[simp]

theorem BialgEquiv.toEquiv_inj {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e₁ e₂ : A ≃ₐc[R] B} :

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

source

theorem BialgEquiv.toBialgHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :

Function.Injective toBialgHom

source

instance BialgEquiv.instEquivLike {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :

EquivLike (A ≃ₐc[R] B) A B

Equations

source

instance BialgEquiv.instFunLike {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :

FunLike (A ≃ₐc[R] B) A B

Equations

source

instance BialgEquiv.instBialgEquivClass {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :

BialgEquivClass (A ≃ₐc[R] B) R A B

source

@[simp]

theorem BialgEquiv.toBialgHom_inj {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e₁ e₂ : A ≃ₐc[R] B} :

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

source

@[simp]

theorem BialgEquiv.coe_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₗc[R] B) (h : ∀ (x y : A), e.toFun (x * y) = e.toFun x * e.toFun y) :

↑{ toCoalgEquiv := e, map_mul' := h } = e

source

@[simp]

theorem BialgEquiv.coe_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

⇑↑e = ⇑e

source

@[simp]

theorem BialgEquiv.toCoalgEquiv_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐc[R] B) :

f.toCoalgEquiv = ↑f

source

@[simp]

theorem BialgEquiv.toBialgHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐc[R] B) :

f.toBialgHom = ↑f

source

@[simp]

theorem BialgEquiv.toAlgEquiv_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐc[R] B) :

f.toAlgEquiv = ↑f

source

@[simp]

theorem BialgEquiv.coe_toCoalgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

⇑↑e = ⇑e

source

@[simp]

theorem BialgEquiv.coe_toBialgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

⇑↑e = ⇑e

source

@[simp]

theorem BialgEquiv.coe_toAlgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

⇑↑e = ⇑e

source

theorem BialgEquiv.toCoalgEquiv_toCoalgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

↑e = ↑↑e

source

theorem BialgEquiv.toBialgHom_toAlgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

↑↑e = ↑e

source

theorem BialgEquiv.ext {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e e' : A ≃ₐc[R] B} (h : ∀ (x : A), e x = e' x) :

e = e'

source

theorem BialgEquiv.ext_iff {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e e' : A ≃ₐc[R] B} :

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

source

theorem BialgEquiv.congr_arg {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e : A ≃ₐc[R] B} {x x' : A} :

x = x' → e x = e x'

source

theorem BialgEquiv.congr_fun {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {e e' : A ≃ₐc[R] B} (h : e = e') (x : A) :

e x = e' x

source

def BialgEquiv.Simps.apply {R : Type u} [CommSemiring R] {α : Type v} {β : Type w} [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β] (f : α ≃ₐc[R] β) :

α → β

See Note [custom simps projection]

Equations

Instances For

source

def BialgEquiv.Simps.symm_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

B → A

See Note [custom simps projection]

Equations

Instances For

source

def BialgEquiv.refl (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] :

A ≃ₐc[R] A

The identity map is a bialgebra equivalence.

Equations

Instances For

source

@[simp]

theorem BialgEquiv.refl_symm_apply (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (a✝ : A) :

(refl R A).symm a✝ = a✝

source

@[simp]

theorem BialgEquiv.refl_apply (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (a : A) :

(refl R A) a = a

source

@[simp]

theorem BialgEquiv.refl_toCoalgEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] :

↑(refl R A) = CoalgEquiv.refl R A

source

@[simp]

theorem BialgEquiv.refl_toBialgHom {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] :

↑(refl R A) = BialgHom.id R A

source

def BialgEquiv.symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

B ≃ₐc[R] A

Bialgebra equivalences are symmetric.

Equations

Instances For

source

@[simp]

theorem BialgEquiv.symm_toCoalgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

↑e.symm = (↑e).symm

source

theorem BialgEquiv.invFun_eq_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

e.invFun = ⇑e.symm

source

theorem BialgEquiv.coe_toEquiv_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

e.toEquiv.symm = ↑e.symm

source

@[simp]

theorem BialgEquiv.toEquiv_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

e.symm.toEquiv = e.toEquiv.symm

source

@[simp]

theorem BialgEquiv.coe_toEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

⇑e.toEquiv = ⇑e

source

@[simp]

theorem BialgEquiv.coe_symm_toEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

⇑e.toEquiv.symm = ⇑e.symm

source

def BialgEquiv.trans {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra 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

Bialgebra equivalences are transitive.

Equations

Instances For

source

@[simp]

theorem BialgEquiv.trans_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra 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

@[simp]

theorem BialgEquiv.trans_symm_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra 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✝)

source

@[simp]

theorem BialgEquiv.trans_toCoalgEquiv {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra 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₂₃

source

@[simp]

theorem BialgEquiv.trans_toBialgHom {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra 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₁₂

source

@[simp]

theorem BialgEquiv.coe_toEquiv_trans {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra 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₂₃)

source

@[simp]

theorem BialgEquiv.apply_symm_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) (x : B) :

e (e.symm x) = x

source

@[simp]

theorem BialgEquiv.symm_apply_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) (x : A) :

e.symm (e x) = x

source

@[simp]

theorem BialgEquiv.comp_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

(↑e).comp ↑e.symm = BialgHom.id R B

source

@[simp]

theorem BialgEquiv.symm_comp {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

(↑e.symm).comp ↑e = BialgHom.id R A

source

@[simp]

theorem BialgEquiv.toRingEquiv_toRingHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

↑↑e = ↑e

source

@[simp]

theorem BialgEquiv.toAlgEquiv_toRingHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (e : A ≃ₐc[R] B) :

↑↑e = ↑e

source

def BialgEquiv.ofBialgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ : f.comp g = BialgHom.id R B) (h₂ : g.comp f = BialgHom.id R A) :

A ≃ₐc[R] B

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

Equations

Instances For

source

@[simp]

theorem BialgEquiv.coe_ofBialgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ : f.comp g = BialgHom.id R B) (h₂ : g.comp f = BialgHom.id R A) :

↑(ofBialgHom f g h₁ h₂) = f

source

theorem BialgEquiv.ofBialgHom_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ : f.comp g = BialgHom.id R B) (h₂ : g.comp f = BialgHom.id R A) :

(ofBialgHom f g h₁ h₂).symm = ofBialgHom g f h₂ h₁

source

def BialgEquiv.ofAlgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) :

A ≃ₐc[R] B

Construct a bialgebra equiv from an algebra equiv respecting counit and comultiplication.

Equations

Instances For

source

@[simp]

theorem BialgEquiv.ofAlgEquiv_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) (a✝ : A) :

(ofAlgEquiv f counit_comp map_comp_comul) a✝ = f.toFun a✝

source

@[simp]

theorem BialgEquiv.toLinearMap_ofAlgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A ≃ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) :

↑↑(ofAlgEquiv f counit_comp map_comp_comul) = ↑↑f

source

noncomputable def BialgEquiv.ofBijective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (hf : Function.Bijective ⇑f) :

A ≃ₐc[R] B

Promotes a bijective bialgebra homomorphism to a bialgebra equivalence.

Equations

Instances For

source

@[simp]

theorem BialgEquiv.ofBijective_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (hf : Function.Bijective ⇑f) (a✝ : A) :

(ofBijective f hf) a✝ = f a✝

source

@[simp]

theorem BialgEquiv.coe_ofBijective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (hf : Function.Bijective ⇑f) :

⇑(ofBijective f hf) = ⇑f

Documentation

Mathlib.RingTheory.Bialgebra.Equiv

Isomorphisms of `R`-bialgebras #

Main definitions #

Notations #

Isomorphisms of R-bialgebras #

Main definitions #

Notations #

Isomorphisms of `R`-bialgebras #