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.

@[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

• TopModuleCat.ker φ = ↧↥(↑(TopModuleCat.Hom.hom φ)).ker

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

• TopModuleCat.kerι φ = TopModuleCat.ofHom { toLinearMap := (↑(TopModuleCat.Hom.hom φ)).ker.subtype, cont := ⋯ }

instance TopModuleCat.instMonoKerι {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) : CategoryTheory.Mono (kerι φ)

@[simp]

theorem TopModuleCat.kerι_comp {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp (kerι φ) φ = 0

@[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

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

• One or more equations did not get rendered due to their size.

@[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

• TopModuleCat.coker φ = ↧(↑N.toModuleCat ⧸ (↑(TopModuleCat.Hom.hom φ)).range)

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

• TopModuleCat.cokerπ φ = TopModuleCat.ofHom { toLinearMap := (↑(TopModuleCat.Hom.hom φ)).range.mkQ, cont := ⋯ }

@[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

theorem TopModuleCat.cokerπ_surjective {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) : Function.Surjective ⇑(Hom.hom (cokerπ φ))

instance TopModuleCat.instEpiCokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) : CategoryTheory.Epi (cokerπ φ)

@[simp]

theorem TopModuleCat.comp_cokerπ {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp φ (cokerπ φ) = 0

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

• One or more equations did not get rendered due to their size.

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