mathlib3
feat(category_theory/groupoid/quotient): quotients and presentations of groupoids
#17109
Open
Overview
Commits
167
Changes
View On GitHub
Commits
  • add free groupoid
    bottine committed 3 years ago
  • some mods
    bottine committed 3 years ago
  • formating
    bottine committed 3 years ago
  • make linter happy
    bottine committed 3 years ago
  • docs
    bottine committed 3 years ago
  • groupoid.inv = is_iso.inv; inv_equiv
    alreadydone committed 3 years ago
  • remove [simp] from groupoid.inv_comp/comp_inv
    alreadydone committed 3 years ago
  • forgotten namespace
    alreadydone committed 3 years ago
  • notsure
    bottine committed 3 years ago
  • Merge remote-tracking branch 'origin/groupoid_inv' into bottine/free_groupoid
    bottine committed 3 years ago
  • cleanup
    bottine committed 3 years ago
  • no tactic mode in prefunctor.ext
    bottine committed 3 years ago
  • docstring
    alreadydone committed 3 years ago
  • free groupoid via quotient of path category
    bottine committed 3 years ago
  • remove noise
    bottine committed 3 years ago
  • free gorupoid more stuff but stuck at spec and spec_unique
    bottine committed 3 years ago
  • need lift_spec and lift_unique for all of symmetrify, quotient, paths and then we should be good?
    bottine committed 3 years ago
  • lift_spec and lift_spec_unique work for the groupoid, but still need to define those for the building blocks
    bottine committed 3 years ago
  • all lifts and lift_specs and lift_spec_uniques done
    bottine committed 3 years ago
  • more stuff in quiver symmetrization
    bottine committed 3 years ago
  • word management messy messy
    bottine committed 3 years ago
  • details
    bottine committed 3 years ago
  • nosorry
    bottine committed 3 years ago
  • lints
    bottine committed 3 years ago
  • simp unhappy
    bottine committed 3 years ago
  • details
    bottine committed 3 years ago
  • Merge remote-tracking branch 'origin/groupoid_inv' into bottine/free_groupoid_cats
    bottine committed 3 years ago
  • instance priority
    bottine committed 3 years ago
  • linty
    bottine committed 3 years ago
  • some simplifications
    bottine committed 3 years ago
  • cleaning up and trying to understand how to compose
    bottine committed 3 years ago
  • red_step now an inductive type (proposed by @joelriou)
    bottine committed 3 years ago
  • docstring
    bottine committed 3 years ago
  • durdur
    bottine committed 3 years ago
  • stubs for ump
    bottine committed 3 years ago
  • `of` is a functor yay
    bottine committed 3 years ago
  • simpa instead of `simp, assumption`
    bottine committed 3 years ago
  • not ez
    bottine committed 3 years ago
  • cleanup for PR
    bottine committed 3 years ago
  • cleanup PR
    bottine committed 3 years ago
  • trying to make lean happy
    bottine committed 3 years ago
  • unwanted file
    bottine committed 3 years ago
  • happy lint
    bottine committed 3 years ago
  • Merge branch 'master' into bottine/free_groupoid_cats
    bottine committed 3 years ago
  • forward image and cleanup of discrete by using an inductively defined predicate
    bottine committed 3 years ago
  • towards graph_like subgroupoids and decomposition of normal subgroupoids
    bottine committed 3 years ago
  • correct statement
    bottine committed 3 years ago
  • stuff
    bottine committed 3 years ago
  • bringing back the quotient… no way around it, is there?
    bottine committed 3 years ago
  • bringing back the quotient… no way around it, is there? (pt 2)
    bottine committed 3 years ago
  • this way is probably relatively useless
    bottine committed 3 years ago
  • back on the 'two steps' approach to quotients!!
    bottine committed 3 years ago
  • ...
    bottine committed 3 years ago
  • reorg mostly
    bottine committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into bottine/subgroupoid_more
    bottine committed 3 years ago
  • stuff
    bottine committed 3 years ago
  • needed stuff
    bottine committed 3 years ago
  • getting sort of overwhelmed
    bottine committed 3 years ago
  • getting sort of overwhelmed
    bottine committed 3 years ago
  • blah
    bottine committed 3 years ago
  • commas
    bottine committed 3 years ago
  • isotropy quotient
    bottine committed 3 years ago
  • isotropy quotient done
    bottine committed 3 years ago
  • more towards quotients
    bottine committed 3 years ago
  • stopping for now
    bottine committed 3 years ago
  • comma slash indent
    bottine committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into bottine/subgroupoid
    bottine committed 3 years ago
  • instance
    bottine committed 3 years ago
  • missed instance
    bottine committed 3 years ago
  • nonempty instance plus eq_to_hom rather than eq.rec
    bottine committed 3 years ago
  • lolol
    bottine committed 3 years ago
  • lol₂
    bottine committed 3 years ago
  • coe_le and associated
    bottine committed 3 years ago
  • Update src/category_theory/groupoid/free_groupoid.lean
    bottine committed 3 years ago
  • Update src/category_theory/groupoid/free_groupoid.lean
    bottine committed 3 years ago
  • Update src/category_theory/groupoid/free_groupoid.lean
    bottine committed 3 years ago
  • Update src/category_theory/path_category.lean
    bottine committed 3 years ago
  • Update src/category_theory/path_category.lean
    bottine committed 3 years ago
  • Update src/category_theory/path_category.lean
    bottine committed 3 years ago
  • Update src/combinatorics/quiver/basic.lean
    bottine committed 3 years ago
  • Merge branch 'master' into bottine/free_groupoid_cats
    bottine committed 3 years ago
  • lift_unique homogen
    bottine committed 3 years ago
  • commas + forgot lift_unique homogen
    bottine committed 3 years ago
  • misc
    bottine committed 3 years ago
  • _root_
    bottine committed 3 years ago
  • functoriality
    bottine committed 3 years ago
  • quotient has ump
    bottine committed 3 years ago
  • corrections after @alreadydone + new defs
    bottine committed 3 years ago
  • Apply suggestions from code review
    bottine committed 3 years ago
  • some more corrections after @alreadydone
    bottine committed 3 years ago
  • more corrections
    bottine committed 3 years ago
  • set_like
    bottine committed 3 years ago
  • 100cols
    bottine committed 3 years ago
  • lots
    bottine committed 3 years ago
  • nolots
    bottine committed 3 years ago
  • lol
    bottine committed 3 years ago
  • conversion to eq_to_hom
    bottine committed 3 years ago
  • barf
    bottine committed 3 years ago
  • borf
    bottine committed 3 years ago
  • ok
    bottine committed 3 years ago
  • + more commits ...
FAQ Terms Privacy Refunds Impressum
Loading