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.

Notation

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

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

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

An equivalence of bialgebras is an invertible bialgebra homomorphism.

Equations

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

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

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

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

• ↑f = { toCoalgEquiv := ↑f, map_mul' := ⋯ }

@[implicit_reducible]

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

• BialgEquivClass.instCoeToBialgEquiv = { coe := fun (f : F) => ↑f }

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

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

• f.toBialgHom = { toCoalgHom := f.toCoalgHom, map_one' := ⋯, map_mul' := ⋯ }

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

• f.toAlgEquiv = { toFun := f.toFun, invFun := f.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

• f.toEquiv = f.toEquiv

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

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

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

• BialgEquiv.instFunLike = { coe := DFunLike.coe, coe_injective' := ⋯ }

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

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

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

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

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

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

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

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

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

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

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

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

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'

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

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'

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

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

• BialgEquiv.Simps.apply f = ⇑f

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

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

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

• BialgEquiv.refl R A = { toCoalgEquiv := CoalgEquiv.refl R A, map_mul' := ⋯ }

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

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

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

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

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

• e.symm = { toCoalgEquiv := (↑e).symm, map_mul' := ⋯ }

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

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

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

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

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

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

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

• e₁₂.trans e₂₃ = { toCoalgEquiv := (↑e₁₂).trans ↑e₂₃, map_mul' := ⋯ }

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

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

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

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

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

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

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

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

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

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

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

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 a coalgebra morphism has an inverse, it is a coalgebra isomorphism.

Equations

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

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

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₁

def BialgEquiv.ofAlgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A ≃ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f) : A ≃ₐc[R] B

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

Equations

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

@[simp]

theorem BialgEquiv.ofAlgEquiv_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A ≃ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f) (a✝ : A) : (ofAlgEquiv f counit_comp map_comp_comul) a✝ = f.toFun a✝

@[simp]

theorem BialgEquiv.toLinearMap_ofAlgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A ≃ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f) : ↑↑(ofAlgEquiv f counit_comp map_comp_comul) = ↑↑f

noncomputable def BialgEquiv.ofBijective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra 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

• BialgEquiv.ofBijective f hf = BialgEquiv.ofAlgEquiv (AlgEquiv.ofBijective (↑f) hf) ⋯ ⋯

@[simp]

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

@[simp]

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