Documentation

Mathlib.Algebra.Category.CoalgCat.Basic

The category of coalgebras over a commutative ring #

We introduce the bundled category CoalgCat of coalgebras over a fixed commutative ring R along with the forgetful functor to ModuleCat.

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

source
structure CoalgCat (R : Type u) [CommRing R] extends ModuleCat R :
Type (max u (v + 1))

The category of R-coalgebras.

Instances For
    source
    instance CoalgCat.instCoeSortType {R : Type u} [CommRing R] :
    CoeSort (CoalgCat R) (Type v)
    Equations
      source
      @[simp]
      theorem CoalgCat.moduleCat_of_toModuleCat {R : Type u} [CommRing R] (X : CoalgCat R) :
      ModuleCat.of R ↑X.toModuleCat = X.toModuleCat
      source
      @[reducible, inline]
      abbrev CoalgCat.of (R : Type u) [CommRing R] (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] :
      CoalgCat R

      The object in the category of R-coalgebras associated to an R-coalgebra.

      Equations
        Instances For
          source
          @[simp]
          theorem CoalgCat.of_comul {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] :
          CoalgebraStruct.comul = CoalgebraStruct.comul
          source
          @[simp]
          theorem CoalgCat.of_counit {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] :
          CoalgebraStruct.counit = CoalgebraStruct.counit
          source
          structure CoalgCat.Hom {R : Type u} [CommRing R] (V W : CoalgCat R) :
          Type v

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

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

                Turn a morphism in CoalgCat back into a CoalgHom.

                Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev CoalgCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (f : X →ₗc[R] Y) :
                    of R X ⟶ of R Y

                    Typecheck a CoalgHom as a morphism in CoalgCat R.

                    Equations
                      Instances For
                        source
                        theorem CoalgCat.Hom.toCoalgHom_injective {R : Type u} [CommRing R] (V W : CoalgCat R) :
                        Function.Injective toCoalgHom'
                        source
                        theorem CoalgCat.hom_ext {R : Type u} [CommRing R] {M N : CoalgCat R} (f g : M ⟶ N) (h : Hom.toCoalgHom f = Hom.toCoalgHom g) :
                        f = g
                        source
                        theorem CoalgCat.hom_ext_iff {R : Type u} [CommRing R] {M N : CoalgCat R} {f g : M ⟶ N} :
                        f = g ↔ Hom.toCoalgHom f = Hom.toCoalgHom g
                        source
                        @[simp]
                        theorem CoalgCat.toCoalgHom_comp {R : Type u} [CommRing R] {M N U : CoalgCat R} (f : M ⟶ N) (g : N ⟶ U) :
                        Hom.toCoalgHom (CategoryTheory.CategoryStruct.comp f g) = (Hom.toCoalgHom g).comp (Hom.toCoalgHom f)
                        source
                        @[simp]
                        theorem CoalgCat.toCoalgHom_id {R : Type u} [CommRing R] {M : CoalgCat R} :
                        Hom.toCoalgHom (CategoryTheory.CategoryStruct.id M) = CoalgHom.id R ↑M.toModuleCat
                        source
                        instance CoalgCat.hasForgetToModule {R : Type u} [CommRing R] :
                        CategoryTheory.HasForget₂ (CoalgCat R) (ModuleCat R)
                        Equations
                          source
                          @[simp]
                          theorem CoalgCat.forget₂_obj {R : Type u} [CommRing R] (X : CoalgCat R) :
                          (CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X.toModuleCat
                          source
                          @[simp]
                          theorem CoalgCat.forget₂_map {R : Type u} [CommRing R] (X Y : CoalgCat R) (f : X ⟶ Y) :
                          (CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).map f = ModuleCat.ofHom ↑(Hom.toCoalgHom f)
                          source
                          def CoalgEquiv.toCoalgIso {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) :
                          CoalgCat.of R X ≅ CoalgCat.of R Y

                          Build an isomorphism in the category CoalgCat R from a CoalgEquiv.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem CoalgEquiv.toCoalgIso_hom {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) :
                              e.toCoalgIso.hom = CoalgCat.ofHom ↑e
                              source
                              @[simp]
                              theorem CoalgEquiv.toCoalgIso_inv {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) :
                              e.toCoalgIso.inv = CoalgCat.ofHom ↑e.symm
                              source
                              @[simp]
                              theorem CoalgEquiv.toCoalgIso_refl {R : Type u} [CommRing R] {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] :
                              (refl R X).toCoalgIso = CategoryTheory.Iso.refl (CoalgCat.of R X)
                              source
                              @[simp]
                              theorem CoalgEquiv.toCoalgIso_symm {R : Type u} [CommRing R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [Coalgebra R X] [Coalgebra R Y] (e : X ≃ₗc[R] Y) :
                              e.symm.toCoalgIso = e.toCoalgIso.symm
                              source
                              @[simp]
                              theorem CoalgEquiv.toCoalgIso_trans {R : Type u} [CommRing R] {X Y Z : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] [AddCommGroup Z] [Module R Z] [Coalgebra R X] [Coalgebra R Y] [Coalgebra R Z] (e : X ≃ₗc[R] Y) (f : Y ≃ₗc[R] Z) :
                              (e.trans f).toCoalgIso = e.toCoalgIso ≪≫ f.toCoalgIso
                              source
                              def CategoryTheory.Iso.toCoalgEquiv {R : Type u} [CommRing R] {X Y : CoalgCat R} (i : X ≅ Y) :
                              ↑X.toModuleCat ≃ₗc[R] ↑Y.toModuleCat

                              Build a CoalgEquiv from an isomorphism in the category CoalgCat R.

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Iso.toCoalgEquiv_toCoalgHom {R : Type u} [CommRing R] {X Y : CoalgCat R} (i : X ≅ Y) :
                                  ↑i.toCoalgEquiv = CoalgCat.Hom.toCoalgHom i.hom
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Iso.toCoalgEquiv_refl {R : Type u} [CommRing R] {X : CoalgCat R} :
                                  (refl X).toCoalgEquiv = CoalgEquiv.refl R ↑X.toModuleCat
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Iso.toCoalgEquiv_symm {R : Type u} [CommRing R] {X Y : CoalgCat R} (e : X ≅ Y) :
                                  e.symm.toCoalgEquiv = e.toCoalgEquiv.symm
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Iso.toCoalgEquiv_trans {R : Type u} [CommRing R] {X Y Z : CoalgCat R} (e : X ≅ Y) (f : Y ≅ Z) :
                                  (e ≪≫ f).toCoalgEquiv = e.toCoalgEquiv.trans f.toCoalgEquiv
                                  source
                                  instance CoalgCat.forget_reflects_isos {R : Type u} [CommRing R] :
                                  (CategoryTheory.forget (CoalgCat R)).ReflectsIsomorphisms