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.

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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 BialgEquiv.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 BialgEquiv.toBialgHom

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

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

Equations

• ⋯ = ⋯

@[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] {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} {h₆ : ∀ (x y : A), { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun (x * y) = { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun x * { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun y} : ⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅, map_mul' := h₆ } = f

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

@[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.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.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_apply (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (a : A) : (BialgEquiv.refl R A) a = a

@[simp]

theorem BialgEquiv.refl_invFun (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (a✝ : A) : (BialgEquiv.refl R A).invFun a✝ = a✝

@[simp]

theorem BialgEquiv.refl_toCoalgEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : ↑(BialgEquiv.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] : ↑(BialgEquiv.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

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

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

@[simp]

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

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_invFun {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₂₃).invFun 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₂₃)