Theorems · Definition · group theory

classifyingSpaceUniversalCover.cechNerveTerminalFromIsoCompForget

(G : Type u) →
  [inst : Monoid G] →
    CategoryTheory.cechNerveTerminalFrom G ≅
      CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G) (CategoryTheory.forget (Action (Type u) G))

As a simplicial set, cechNerveTerminalFrom of a monoid G is isomorphic to the universal cover of the classifying space of G as a simplicial set.

Defined in

Mathlib.RepresentationTheory.Homological.Resolution

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Monoid