BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Sophie Morel (CNRS/ENS de Lyon)
DTSTART:20260121T173000Z
DTEND:20260121T180000Z
DTSTAMP:20260420T025808Z
UID:LT2026/24
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/24/">
 Nori's construction in Lean\, or the many ways that a formalization projec
 t can fail.</a>\nby Sophie Morel (CNRS/ENS de Lyon) as part of Lean Togeth
 er 2026\n\n\nAbstract\nNori's construction\, also known as Nori's universa
 l factorization\, is a 2-universal construction in category theory. Though
  it looks very abstract and can be deduced from existing results in a few 
 lines\, it underlies the construction of the far from trivial category of 
 Nori motives.\nThe goal of this talk is to briefly explain what Nori's con
 struction is and why I wanted to formalize it\, then to report on the many
  things that went wrong (and a couple that went right). \nFamiliarity with
  categories would be helpful to follow the details.\n
LOCATION:https://researchseminars.org/talk/LT2026/24/
END:VEVENT
END:VCALENDAR