Documentation

Mathlib.Algebra.Category.BialgCat.Basic

The category of bialgebras over a commutative ring #

We introduce the bundled category BialgCat of bialgebras over a fixed commutative ring R along with the forgetful functors to CoalgCat and AlgCat.

This file mimics Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean.

source
structure BialgCat (R : Type u) [CommRing R] :
Type (max u (v + 1))

The category of R-bialgebras.

Instances For
    source
    instance BialgCat.instCoeSortType {R : Type u} [CommRing R] :
    CoeSort (BialgCat R) (Type v)
    Equations
      source
      def BialgCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :
      BialgCat R

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

      Equations
        Instances For
          source
          @[simp]
          theorem BialgCat.of_instRing (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :
          (of R X).instRing = inst✝
          source
          @[simp]
          theorem BialgCat.of_carrier (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :
          (of R X).carrier = X
          source
          @[simp]
          theorem BialgCat.of_instBialgebra (R : Type u) [CommRing R] (X : Type v) [Ring X] [Bialgebra R X] :
          (of R X).instBialgebra = inst✝
          source
          @[simp]
          theorem BialgCat.of_comul {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :
          CoalgebraStruct.comul = CoalgebraStruct.comul
          source
          @[simp]
          theorem BialgCat.of_counit {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :
          CoalgebraStruct.counit = CoalgebraStruct.counit
          source
          structure BialgCat.Hom {R : Type u} [CommRing R] (V W : BialgCat R) :
          Type v

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

          Instances For
            source
            theorem BialgCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {V W : BialgCat R} {x y : V.Hom W} (toBialgHom' : x.toBialgHom' = y.toBialgHom') :
            x = y
            source
            theorem BialgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {V W : BialgCat R} {x y : V.Hom W} :
            x = y ↔ x.toBialgHom' = y.toBialgHom'
            source
            instance BialgCat.category {R : Type u} [CommRing R] :
            CategoryTheory.Category.{v, max (v + 1) u} (BialgCat R)
            Equations
              source
              instance BialgCat.concreteCategory {R : Type u} [CommRing R] :
              CategoryTheory.ConcreteCategory (BialgCat R) fun (x1 x2 : BialgCat R) => x1.carrier →ₐc[R] x2.carrier
              Equations
                source
                @[reducible, inline]
                abbrev BialgCat.Hom.toBialgHom {R : Type u} [CommRing R] {X Y : BialgCat R} (f : X.Hom Y) :
                X.carrier →ₐc[R] Y.carrier

                Turn a morphism in BialgCat back into a BialgHom.

                Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev BialgCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (f : X →ₐc[R] Y) :
                    of R X ⟶ of R Y

                    Typecheck a BialgHom as a morphism in BialgCat R.

                    Equations
                      Instances For
                        source
                        theorem BialgCat.Hom.toBialgHom_injective {R : Type u} [CommRing R] (V W : BialgCat R) :
                        Function.Injective toBialgHom
                        source
                        theorem BialgCat.hom_ext {R : Type u} [CommRing R] {X Y : BialgCat R} (f g : X ⟶ Y) (h : Hom.toBialgHom f = Hom.toBialgHom g) :
                        f = g
                        source
                        theorem BialgCat.hom_ext_iff {R : Type u} [CommRing R] {X Y : BialgCat R} {f g : X ⟶ Y} :
                        f = g ↔ Hom.toBialgHom f = Hom.toBialgHom g
                        source
                        @[simp]
                        theorem BialgCat.toBialgHom_comp {R : Type u} [CommRing R] {X Y Z : BialgCat R} (f : X ⟶ Y) (g : Y ⟶ Z) :
                        Hom.toBialgHom (CategoryTheory.CategoryStruct.comp f g) = (Hom.toBialgHom g).comp (Hom.toBialgHom f)
                        source
                        @[simp]
                        theorem BialgCat.toBialgHom_id {R : Type u} [CommRing R] {M : BialgCat R} :
                        Hom.toBialgHom (CategoryTheory.CategoryStruct.id M) = BialgHom.id R M.carrier
                        source
                        instance BialgCat.hasForget {R : Type u} [CommRing R] :
                        CategoryTheory.HasForget (BialgCat R)
                        Equations
                          source
                          instance BialgCat.hasForgetToAlgebra {R : Type u} [CommRing R] :
                          CategoryTheory.HasForget₂ (BialgCat R) (AlgCat R)
                          Equations
                            source
                            @[simp]
                            theorem BialgCat.forget₂_algebra_obj {R : Type u} [CommRing R] (X : BialgCat R) :
                            (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj X = AlgCat.of R X.carrier
                            source
                            @[simp]
                            theorem BialgCat.forget₂_algebra_map {R : Type u} [CommRing R] (X Y : BialgCat R) (f : X ⟶ Y) :
                            (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).map f = AlgCat.ofHom ↑(Hom.toBialgHom f)
                            source
                            instance BialgCat.hasForgetToCoalgebra {R : Type u} [CommRing R] :
                            CategoryTheory.HasForget₂ (BialgCat R) (CoalgCat R)
                            Equations
                              source
                              @[simp]
                              theorem BialgCat.forget₂_coalgebra_obj {R : Type u} [CommRing R] (X : BialgCat R) :
                              (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).obj X = CoalgCat.of R X.carrier
                              source
                              @[simp]
                              theorem BialgCat.forget₂_coalgebra_map {R : Type u} [CommRing R] (X Y : BialgCat R) (f : X ⟶ Y) :
                              (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).map f = CoalgCat.ofHom ↑(Hom.toBialgHom f)
                              source
                              def BialgEquiv.toBialgIso {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
                              BialgCat.of R X ≅ BialgCat.of R Y

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

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem BialgEquiv.toBialgIso_hom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
                                  e.toBialgIso.hom = BialgCat.ofHom ↑e
                                  source
                                  @[simp]
                                  theorem BialgEquiv.toBialgIso_inv {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
                                  e.toBialgIso.inv = BialgCat.ofHom ↑e.symm
                                  source
                                  @[simp]
                                  theorem BialgEquiv.toBialgIso_refl {R : Type u} [CommRing R] {X : Type v} [Ring X] [Bialgebra R X] :
                                  (refl R X).toBialgIso = CategoryTheory.Iso.refl (BialgCat.of R X)
                                  source
                                  @[simp]
                                  theorem BialgEquiv.toBialgIso_symm {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Ring Y] [Bialgebra R X] [Bialgebra R Y] (e : X ≃ₐc[R] Y) :
                                  e.symm.toBialgIso = e.toBialgIso.symm
                                  source
                                  @[simp]
                                  theorem BialgEquiv.toBialgIso_trans {R : Type u} [CommRing R] {X Y 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).toBialgIso = e.toBialgIso ≪≫ f.toBialgIso
                                  source
                                  def CategoryTheory.Iso.toBialgEquiv {R : Type u} [CommRing R] {X Y : BialgCat R} (i : X ≅ Y) :
                                  X.carrier ≃ₐc[R] Y.carrier

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

                                  Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Iso.toBialgEquiv_toBialgHom {R : Type u} [CommRing R] {X Y : BialgCat R} (i : X ≅ Y) :
                                      ↑i.toBialgEquiv = i.hom.toBialgHom'
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Iso.toBialgEquiv_refl {R : Type u} [CommRing R] {X : BialgCat R} :
                                      (refl X).toBialgEquiv = BialgEquiv.refl R X.carrier
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Iso.toBialgEquiv_symm {R : Type u} [CommRing R] {X Y : BialgCat R} (e : X ≅ Y) :
                                      e.symm.toBialgEquiv = e.toBialgEquiv.symm
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Iso.toBialgEquiv_trans {R : Type u} [CommRing R] {X Y Z : BialgCat R} (e : X ≅ Y) (f : Y ≅ Z) :
                                      (e ≪≫ f).toBialgEquiv = e.toBialgEquiv.trans f.toBialgEquiv
                                      source
                                      instance BialgCat.forget_reflects_isos {R : Type u} [CommRing R] :
                                      (CategoryTheory.forget (BialgCat R)).ReflectsIsomorphisms