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
🔸 coverage
@[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.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      instance TopModuleCat.instMonoKerι {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
      CategoryTheory.Mono (kerι φ)
      source
      📐 coverage
      @[simp]
      theorem TopModuleCat.kerι_comp {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
      CategoryTheory.CategoryStruct.comp (kerι φ) φ = 0
      source
      📐 coverage
      @[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
      🔸 coverage
      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.

      Instances For
        source
        🔸 coverage
        @[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.

        Instances For
          source
          🔸 coverage
          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.

          Instances For
            source
            📐 coverage
            @[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 = (↑(Hom.hom φ)).range.mkQ x
            source
            📐 coverage
            theorem TopModuleCat.cokerπ_surjective {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
            Function.Surjective ⇑(Hom.hom (cokerπ φ))
            source
            📐 coverage
            instance TopModuleCat.instEpiCokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
            CategoryTheory.Epi (cokerπ φ)
            source
            📐 coverage
            @[simp]
            theorem TopModuleCat.comp_cokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) :
            CategoryTheory.CategoryStruct.comp φ (cokerπ φ) = 0
            source
            🔸 coverage
            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.

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