Zulip Chat Archive

Stream: maths

Topic: category of groups


view this post on Zulip Ashwin Iyengar (Mar 22 2021 at 21:18):

Is the category of groups in mathlib? I saw Groupoid.lean in category_theory/category but not Group.lean

view this post on Zulip Adam Topaz (Mar 22 2021 at 21:18):

docs#Group

view this post on Zulip Adam Topaz (Mar 22 2021 at 21:19):

The algebraic categories are in algebra/category/

view this post on Zulip Ashwin Iyengar (Mar 22 2021 at 21:19):

Ahh ok thanks

view this post on Zulip Adam Topaz (Mar 22 2021 at 21:19):

and the naming convention is the categories of bundled foo is named Foo

view this post on Zulip Ashwin Iyengar (Mar 22 2021 at 21:22):

Ok good to know. I saw that standard simplicial sets and horns had been added, so I thought I might try to prove the lemma that every simplicial group is fibrant

view this post on Zulip Ashwin Iyengar (Mar 22 2021 at 21:25):

Using this definition for now

class fibration {S T : sSet} (f : S  T) : Prop :=
(lifting :
   (n : ) (i : fin (n+1)) (a : Λ[n,i]  S)
    (b : Δ[n]  T) (h : a  f = horn_inclusion n i  b),
   g : Δ[n]  S, g  f = b  horn_inclusion n i  g = a)

view this post on Zulip Adam Topaz (Mar 22 2021 at 21:27):

looks reasonable enough


Last updated: May 12 2021 at 08:14 UTC