Documentation

Mathlib.Algebra.Category.HopfAlgebraCat.Basic

The category of Hopf algebras over a commutative ring #

We introduce the bundled category HopfAlgebraCat of Hopf algebras over a fixed commutative ring R along with the forgetful functor to BialgebraCat.

This file mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

structure HopfAlgebraCat (R : Type u) [CommRing R] extends CategoryTheory.Bundled :
Type (max u (v + 1))

The category of R-Hopf algebras.

Instances For
    Equations
    • HopfAlgebraCat.instCoeSortType = { coe := fun (x : HopfAlgebraCat R) => x.toBundled }
    @[simp]
    theorem HopfAlgebraCat.of_str (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :
    (HopfAlgebraCat.of R X).str = inferInstance
    @[simp]
    theorem HopfAlgebraCat.of_instHopfAlgebra (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :
    (HopfAlgebraCat.of R X).instHopfAlgebra = inferInstance
    @[simp]
    theorem HopfAlgebraCat.of_α (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :
    (HopfAlgebraCat.of R X).toBundled = X
    def HopfAlgebraCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [HopfAlgebra R X] :

    The object in the category of R-Hopf algebras associated to an R-Hopf algebra.

    Equations
    Instances For
      @[simp]
      theorem HopfAlgebraCat.of_comul {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] :
      Coalgebra.comul = Coalgebra.comul
      @[simp]
      theorem HopfAlgebraCat.of_counit {R : Type u} [CommRing R] {X : Type v} [Ring X] [HopfAlgebra R X] :
      Coalgebra.counit = Coalgebra.counit
      theorem HopfAlgebraCat.Hom.ext_iff {R : Type u} :
      ∀ {inst : CommRing R} {V W : HopfAlgebraCat R} {x y : V.Hom W}, x = y x.toBialgHom = y.toBialgHom
      theorem HopfAlgebraCat.Hom.ext {R : Type u} :
      ∀ {inst : CommRing R} {V W : HopfAlgebraCat R} {x y : V.Hom W}, x.toBialgHom = y.toBialgHomx = y
      structure HopfAlgebraCat.Hom {R : Type u} [CommRing R] (V : HopfAlgebraCat R) (W : HopfAlgebraCat R) :

      A type alias for BialgHom to avoid confusion between the categorical and algebraic spellings of composition.

      Instances For
        theorem HopfAlgebraCat.Hom.toBialgHom_injective {R : Type u} [CommRing R] (V : HopfAlgebraCat R) (W : HopfAlgebraCat R) :
        Function.Injective HopfAlgebraCat.Hom.toBialgHom
        theorem HopfAlgebraCat.hom_ext_iff {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} {f : X Y} {g : X Y} :
        f = g f.toBialgHom = g.toBialgHom
        theorem HopfAlgebraCat.hom_ext {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} (f : X Y) (g : X Y) (h : f.toBialgHom = g.toBialgHom) :
        f = g
        @[reducible, inline]
        abbrev HopfAlgebraCat.ofHom {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (f : X →ₐc[R] Y) :

        Typecheck a BialgHom as a morphism in HopfAlgebraCat R.

        Equations
        Instances For
          @[simp]
          theorem HopfAlgebraCat.toBialgHom_comp {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} {Z : HopfAlgebraCat R} (f : X Y) (g : Y Z) :
          (CategoryTheory.CategoryStruct.comp f g).toBialgHom = g.toBialgHom.comp f.toBialgHom
          @[simp]
          theorem HopfAlgebraCat.toBialgHom_id {R : Type u} [CommRing R] {M : HopfAlgebraCat R} :
          (CategoryTheory.CategoryStruct.id M).toBialgHom = BialgHom.id R M.toBundled
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem BialgEquiv.toHopfAlgebraCatIso_inv_toBialgHom {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) :
          e.toHopfAlgebraCatIso.inv.toBialgHom = e.symm
          @[simp]
          theorem BialgEquiv.toHopfAlgebraCatIso_hom_toBialgHom {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) :
          e.toHopfAlgebraCatIso.hom.toBialgHom = e
          def BialgEquiv.toHopfAlgebraCatIso {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) :

          Build an isomorphism in the category HopfAlgebraCat R from a BialgEquiv.

          Equations
          Instances For
            @[simp]
            @[simp]
            theorem BialgEquiv.toHopfAlgebraCatIso_symm {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [HopfAlgebra R X] [HopfAlgebra R Y] (e : X ≃ₐc[R] Y) :
            e.symm.toHopfAlgebraCatIso = e.toHopfAlgebraCatIso.symm
            @[simp]
            theorem BialgEquiv.toHopfAlgebraCatIso_trans {R : Type u} [CommRing R] {X : Type v} {Y : Type v} {Z : Type v} [Ring X] [Ring Y] [Ring Z] [HopfAlgebra R X] [HopfAlgebra R Y] [HopfAlgebra R Z] (e : X ≃ₐc[R] Y) (f : Y ≃ₐc[R] Z) :
            (e.trans f).toHopfAlgebraCatIso = e.toHopfAlgebraCatIso ≪≫ f.toHopfAlgebraCatIso
            def CategoryTheory.Iso.toHopfAlgEquiv {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} (i : X Y) :
            X.toBundled ≃ₐc[R] Y.toBundled

            Build a BialgEquiv from an isomorphism in the category HopfAlgebraCat R.

            Equations
            • i.toHopfAlgEquiv = { toCoalgHom := i.hom.toBialgHom.toCoalgHom, invFun := i.inv.toBialgHom, left_inv := , right_inv := , map_mul' := }
            Instances For
              @[simp]
              theorem CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} (i : X Y) :
              i.toHopfAlgEquiv = i.hom.toBialgHom
              @[simp]
              theorem CategoryTheory.Iso.toHopfAlgEquiv_refl {R : Type u} [CommRing R] {X : HopfAlgebraCat R} :
              (CategoryTheory.Iso.refl X).toHopfAlgEquiv = BialgEquiv.refl R X.toBundled
              @[simp]
              theorem CategoryTheory.Iso.toHopfAlgEquiv_symm {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} (e : X Y) :
              e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm
              @[simp]
              theorem CategoryTheory.Iso.toHopfAlgEquiv_trans {R : Type u} [CommRing R] {X : HopfAlgebraCat R} {Y : HopfAlgebraCat R} {Z : HopfAlgebraCat R} (e : X Y) (f : Y Z) :
              (e ≪≫ f).toHopfAlgEquiv = e.toHopfAlgEquiv.trans f.toHopfAlgEquiv
              Equations
              • =