Documentation

Mathlib.RingTheory.Coalgebra.IsFrobenius

Frobenius equations #

This file defines Coalgebra.IsFrobenius and shows some elementary results.

A coalgebra with an algebra structure is said to be Frobenius when the Frobenius equation is satisfied: (id ⊗ mul') ∘ assoc ∘ (comul ⊗ id) = (mul' ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul), which in diagrams looks like

|    |             |    |
|    μ             μ    |
|   / \           / \   |
 \ /   |    =    |   \ /
  δ    |         |    δ
  |    |         |    |

where μ stands for multiplication and δ for comultiplication. We define the left diagram as Coalgebra.IsFrobenius.left and the right as Coalgebra.IsFrobenius.right in order to shorten the names.

When the Frobenius equations are satisfied, we actually get (id ⊗ mul') ∘ assoc ∘ (comul ⊗ id) = comul ∘ mul' = (mul' ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul), which in diagrams looks like

|    |                           |    |
|    μ           |   |           μ    |
|   / \           \ /           / \   |
 \ /   |    =    δ ∘ μ    =    |   \ /
  δ    |          / \          |    δ
  |    |         |   |         |    |

In texts, this is what the Frobenius equations are usually referred to as.

Main definitions and results #

TODO #

Definition and basic properties #

source
def Coalgebra.IsFrobenius.left (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [CoalgebraStruct R A] :
TensorProduct R A A →ₗ[R] TensorProduct R A A

The left-hand side of the Frobenius equation: (id ⊗ mul) ∘ assoc ∘ (comul ⊗ id).

Equations
Instances For
    source
    theorem Coalgebra.IsFrobenius.left_def (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [CoalgebraStruct R A] :
    left R A = LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul
    source
    def Coalgebra.IsFrobenius.right (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [CoalgebraStruct R A] :
    TensorProduct R A A →ₗ[R] TensorProduct R A A

    The right-hand side of the Frobenius equation: (mul ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul).

    Equations
    Instances For
      source
      theorem Coalgebra.IsFrobenius.right_def (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [CoalgebraStruct R A] :
      right R A = LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A comul
      source
      class Coalgebra.IsFrobenius (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [CoalgebraStruct R A] :
      Prop

      A coalgebra with an algebra structure is said to be Frobenius when the Frobenius equation is satisfied, i.e., IsFrobenius.left and IsFrobenius.right are equal, in other words,

      (id ⊗ mul') ∘ assoc ∘ (comul ⊗ id) = (mul' ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul).

      See IsFrobenius.left_eq and IsFrobenius.right_eq which refer to each side of the equality being equal to comul ∘ mul'.

      When the Frobenius equations are satisfied, the bilinear form mul.compr₂ counit is nondegenerate and bijective (see IsFrobenius.nondegenerate_compr₂_mul_counit and IsFrobenius.bijective_compr₂_mul_counit).

      • left_eq_right : left R A = right R A

        The Frobenius equation.

      Instances
        source
        instance Coalgebra.IsFrobenius.of_commSemiring {R : Type u_1} [CommSemiring R] :
        IsFrobenius R R
        source
        theorem Coalgebra.IsFrobenius.left_eq_comul_comp_mul' {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Coalgebra R A] [IsFrobenius R A] :
        left R A = comul ∘ₗ LinearMap.mul' R A
        source
        theorem Coalgebra.IsFrobenius.right_eq_comul_comp_mul' {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Coalgebra R A] [IsFrobenius R A] :
        right R A = comul ∘ₗ LinearMap.mul' R A

        Unital coalgebras #

        When our coalgebra is unital and satisfies the Frobenius equations, we get that the counit is nondegenerate, and that it is finite and projective.

        source
        instance Coalgebra.IsFrobenius.instFinite {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonAssocSemiring A] [Module R A] [Coalgebra R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsFrobenius R A] :
        Module.Finite R A
        source
        instance Coalgebra.IsFrobenius.instProjective {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonAssocSemiring A] [Module R A] [Coalgebra R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsFrobenius R A] :
        Module.Projective R A
        source
        theorem Coalgebra.IsFrobenius.forall_counit_mul_left_eq_zero_iff {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonAssocSemiring A] [Module R A] [Coalgebra R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsFrobenius R A] {a : A} :
        (∀ (b : A), counit (a * b) = 0) ↔ a = 0

        The bilinear form (mul R A).compr₂ counit is separating left. This is the simplified version, see nondegenerate_compr₂_mul_counit.

        source
        theorem Coalgebra.IsFrobenius.forall_counit_mul_right_eq_zero_iff {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonAssocSemiring A] [Module R A] [Coalgebra R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsFrobenius R A] {a : A} :
        (∀ (b : A), counit (b * a) = 0) ↔ a = 0

        The bilinear form (mul R A).compr₂ counit is separating right. This is the simplified version, see nondegenerate_compr₂_mul_counit.

        source
        theorem Coalgebra.IsFrobenius.nondegenerate_compr₂_mul_counit {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonAssocSemiring A] [Module R A] [Coalgebra R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsFrobenius R A] :
        ((LinearMap.mul R A).compr₂ counit).Nondegenerate

        The bilinear form mul.compr₂ counit is nondegenerate.

        source
        theorem Coalgebra.IsFrobenius.compr₂_mul_counit_bijective {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonAssocSemiring A] [Module R A] [Coalgebra R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsFrobenius R A] :
        Function.Bijective ⇑((LinearMap.mul R A).compr₂ counit)

        The bilinear form mul.compr₂ counit is bijective.

        The snake equations #

        Composing the Frobenius equations with the counit and algebra map gives the so called "snake" equations.

        source
        theorem Coalgebra.IsFrobenius.lTensor_counit_comp_left_comp_rTensor_algebraLinearMap {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] [Coalgebra R A] [IsFrobenius R A] :
        LinearMap.lTensor A counit ∘ₗ left R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) = ↑(TensorProduct.comm R R A)

        Composing the left Frobenius equation with Coalgebra.counit and Algebra.linearMap. See rTensor_counit_comp_right_comp_lTensor_algebraLinearMap for the right Frobenius equation version.

        (This is sometimes known as the left snake equation.)

        source
        theorem Coalgebra.IsFrobenius.rTensor_counit_comp_right_comp_lTensor_algebraLinearMap {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] [Coalgebra R A] [IsFrobenius R A] :
        LinearMap.rTensor A counit ∘ₗ right R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) = ↑(TensorProduct.comm R A R)

        Composing the right Frobenius equation with Coalgebra.counit and Algebra.linearMap. See lTensor_counit_comp_left_comp_rTensor_algebraLinearMap for the left Frobenius equation version.

        (This is sometimes known as the right snake equation.)

        Bialgebras and the Frobenius equations #

        If a bialgebra A over R satisfies the Frobenius equations, then A is isomorphic to the underlying ring R.

        source
        @[simp]
        theorem Bialgebra.comul_apply_eq_of_isFrobenius {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Bialgebra R A] [Coalgebra.IsFrobenius R A] (a : A) :
        CoalgebraStruct.comul a = a ⊗ₜ[R] 1
        source
        theorem Bialgebra.comul_eq_of_isFrobenius {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Bialgebra R A] [Coalgebra.IsFrobenius R A] :
        CoalgebraStruct.comul = (TensorProduct.mk R A A).flip 1
        source
        @[simp]
        theorem Bialgebra.algebraMap_counit_of_isFrobenius {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Bialgebra R A] [Coalgebra.IsFrobenius R A] (a : A) :
        (algebraMap R A) (CoalgebraStruct.counit a) = a
        source
        theorem Bialgebra.algebraMap_bijective_of_isFrobenius {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Bialgebra R A] [Coalgebra.IsFrobenius R A] :
        Function.Bijective ⇑(algebraMap R A)
        source
        theorem Bialgebra.counit_bijective_of_isFrobenius {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Bialgebra R A] [Coalgebra.IsFrobenius R A] :
        Function.Bijective ⇑CoalgebraStruct.counit
        source
        theorem Bialgebra.algebraOfId_bijective_of_isFrobenius {R : Type u_1} [CommSemiring R] {A : Type u_3} [Semiring A] [Bialgebra R A] [Coalgebra.IsFrobenius R A] :
        Function.Bijective ⇑(Algebra.ofId R A)

        When a bialgebra satisfies the Frobenius equations, we get R ≃ A. So if R and A are not isomorphic, then A cannot satisfy the Frobenius equations.