Stream: maths

Topic: category of groups

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

docs#Group

Adam Topaz (Mar 22 2021 at 21:19):

The algebraic categories are in algebra/category/

Ahh ok thanks

Adam Topaz (Mar 22 2021 at 21:19):

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

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

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)


Adam Topaz (Mar 22 2021 at 21:27):

looks reasonable enough

Last updated: May 12 2021 at 08:14 UTC