category of groups

Stream: maths

[Ashwin Iyengar]

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

[Adam Topaz]

docs#Group

[Adam Topaz]

The algebraic categories are in algebra/category/

[Ashwin Iyengar]

Ahh ok thanks

[Adam Topaz]

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

[Ashwin Iyengar]

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

[Ashwin Iyengar]

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)

[Adam Topaz]

looks reasonable enough