Theorems · Definition · category theory

TopModuleCat.isColimitCoker

{R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M N : TopModuleCat R} →
        (φ : M ⟶ N) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (TopModuleCat.cokerπ φ) ⋯)

TopModuleCat.coker is indeed the cokernel in TopModuleCat R.

Defined in: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Cited by: 0 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites26

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
TopologicalSpacestatement and proof · cited by 24,529
RingHom.idproof · cited by 18,349
CategoryTheory.CategoryStruct.compproof · cited by 17,999
LinearMapproof · cited by 10,215
Ringstatement and proof · cited by 7,463
HasQuotient.Quotientproof · cited by 2,301
CategoryTheory.Limits.Cocone.ptproof · cited by 1,354
ModuleCat.carrierproof · cited by 997
LinearMap.rangeproof · cited by 893
CategoryTheory.Limits.WalkingParallelPairstatement · cited by 781
CategoryTheory.Limits.IsColimitstatement · cited by 773

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.