Theorems · Theorem · group theory

classifyingSpaceUniversalCover_map

∀ (G : Type u) [inst : Monoid G] {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y),
  (classifyingSpaceUniversalCover G).map f =
    { hom := TypeCat.ofHom fun x => x ∘ ⇑(SimplexCategory.Hom.toOrderHom f.unop), comm := ⋯ }

Defined in

Mathlib.RepresentationTheory.Homological.Resolution

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

Monoid