Documentation

Mathlib.Algebra.Category.BialgebraCat.Basic

The category of bialgebras over a commutative ring #

We introduce the bundled category BialgebraCat of bialgebras over a fixed commutative ring R along with the forgetful functors to CoalgebraCat and AlgebraCat.

This file mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

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

The category of R-bialgebras.

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

    The object in the category of R-bialgebras associated to an R-bialgebra.

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

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

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

        Typecheck a BialgHom as a morphism in BialgebraCat R.

        Equations
        Instances For
          @[simp]
          theorem BialgebraCat.toBialgHom_comp {R : Type u} [CommRing R] {X : BialgebraCat R} {Y : BialgebraCat R} {Z : BialgebraCat R} (f : X Y) (g : Y Z) :
          (CategoryTheory.CategoryStruct.comp f g).toBialgHom = g.toBialgHom.comp f.toBialgHom
          @[simp]
          theorem BialgebraCat.toBialgHom_id {R : Type u} [CommRing R] {M : BialgebraCat 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 BialgebraCat.forget₂_algebra_map {R : Type u} [CommRing R] (X : BialgebraCat R) (Y : BialgebraCat R) (f : X Y) :
          (CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R)).map f = f.toBialgHom
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem BialgEquiv.toBialgebraCatIso_hom_toBialgHom {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
          e.toBialgebraCatIso.hom.toBialgHom = e
          @[simp]
          theorem BialgEquiv.toBialgebraCatIso_inv_toBialgHom {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
          e.toBialgebraCatIso.inv.toBialgHom = e.symm
          def BialgEquiv.toBialgebraCatIso {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :

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

          Equations
          Instances For
            @[simp]
            theorem BialgEquiv.toBialgebraCatIso_refl {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :
            @[simp]
            theorem BialgEquiv.toBialgebraCatIso_symm {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
            e.symm.toBialgebraCatIso = e.toBialgebraCatIso.symm
            @[simp]
            theorem BialgEquiv.toBialgebraCatIso_trans {R : Type u} [CommRing R] {X : Type v} {Y : Type v} {Z : Type v} [Ring X] [Ring Y] [Ring Z] [Bialgebra R X] [Bialgebra R Y] [Bialgebra R Z] (e : X ≃ₐc[R] Y) (f : Y ≃ₐc[R] Z) :
            (e.trans f).toBialgebraCatIso = e.toBialgebraCatIso ≪≫ f.toBialgebraCatIso
            def CategoryTheory.Iso.toBialgEquiv {R : Type u} [CommRing R] {X : BialgebraCat R} {Y : BialgebraCat R} (i : X Y) :
            X.toBundled ≃ₐc[R] Y.toBundled

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

            Equations
            • i.toBialgEquiv = { toCoalgHom := i.hom.toBialgHom.toCoalgHom, invFun := i.inv.toBialgHom, left_inv := , right_inv := , map_mul' := }
            Instances For
              @[simp]
              theorem CategoryTheory.Iso.toBialgEquiv_toBialgHom {R : Type u} [CommRing R] {X : BialgebraCat R} {Y : BialgebraCat R} (i : X Y) :
              i.toBialgEquiv = i.hom.toBialgHom
              @[simp]
              theorem CategoryTheory.Iso.toBialgEquiv_refl {R : Type u} [CommRing R] {X : BialgebraCat R} :
              (CategoryTheory.Iso.refl X).toBialgEquiv = BialgEquiv.refl R X.toBundled
              @[simp]
              theorem CategoryTheory.Iso.toBialgEquiv_symm {R : Type u} [CommRing R] {X : BialgebraCat R} {Y : BialgebraCat R} (e : X Y) :
              e.symm.toBialgEquiv = e.toBialgEquiv.symm
              @[simp]
              theorem CategoryTheory.Iso.toBialgEquiv_trans {R : Type u} [CommRing R] {X : BialgebraCat R} {Y : BialgebraCat R} {Z : BialgebraCat R} (e : X Y) (f : Y Z) :
              (e ≪≫ f).toBialgEquiv = e.toBialgEquiv.trans f.toBialgEquiv
              instance BialgebraCat.forget_reflects_isos {R : Type u} [CommRing R] :
              (CategoryTheory.forget (BialgebraCat R)).ReflectsIsomorphisms
              Equations
              • =