Documentation

Mathlib.Algebra.Category.ModuleCat.Topology.Homology

TopModuleCat is a CategoryWithHomology #

TopModuleCat R, the category of topological R-modules, is not an abelian category. But since the topology on subquotients is well-defined, we can still talk about homology in this category. See the CategoryWithHomology (TopModuleCat R) instance in this file.

source
@[reducible, inline]
abbrev TopModuleCat.ker {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
TopModuleCat R

Kernel in TopModuleCat R is the kernel of the linear map with the subspace topology.

Equations
    Instances For
      source
      def TopModuleCat.kerι {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
      ker φ ⟶ M

      The inclusion map from the kernel in TopModuleCat R.

      Equations
        Instances For
          source
          instance TopModuleCat.instMonoKerι {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
          CategoryTheory.Mono (kerι φ)
          source
          @[simp]
          theorem TopModuleCat.kerι_comp {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
          CategoryTheory.CategoryStruct.comp (kerι φ) φ = 0
          source
          @[simp]
          theorem TopModuleCat.kerι_apply {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) (x : (fun (X : TopModuleCat R) => ↑X.toModuleCat) (ker φ)) :
          (CategoryTheory.ConcreteCategory.hom (kerι φ)) x = ↑x
          source
          def TopModuleCat.isLimitKer {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (kerι φ) ⋯)

          TopModuleCat.ker is indeed the kernel in TopModuleCat R.

          Equations
            Instances For
              source
              @[reducible, inline]
              abbrev TopModuleCat.coker {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
              TopModuleCat R

              Cokernel in TopModuleCat R is the cokernel of the linear map with the quotient topology.

              Equations
                Instances For
                  source
                  def TopModuleCat.cokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
                  N ⟶ coker φ

                  The projection map to the cokernel in TopModuleCat R.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem TopModuleCat.hom_cokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) (x : ↑N.toModuleCat) :
                      (Hom.hom (cokerπ φ)) x = (LinearMap.range (Hom.hom φ)).mkQ x
                      source
                      theorem TopModuleCat.cokerπ_surjective {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
                      Function.Surjective ⇑(Hom.hom (cokerπ φ))
                      source
                      instance TopModuleCat.instEpiCokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
                      CategoryTheory.Epi (cokerπ φ)
                      source
                      @[simp]
                      theorem TopModuleCat.comp_cokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
                      CategoryTheory.CategoryStruct.comp φ (cokerπ φ) = 0
                      source
                      def TopModuleCat.isColimitCoker {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (cokerπ φ) ⋯)

                      TopModuleCat.coker is indeed the cokernel in TopModuleCat R.

                      Equations
                        Instances For
                          source
                          instance TopModuleCat.instCategoryWithHomology {R : Type u} [Ring R] [TopologicalSpace R] :
                          CategoryTheory.CategoryWithHomology (TopModuleCat R)