Formalizing polynomial laws and the universal divided power algebra
summary
Formalization in Lean/Mathlib of polynomial laws and the first steps of Roby’s universal divided power algebra constructs the graded algebra and a partial divided power structure, fixes a found mistake in Roby 1965 (an omitted tensor) and repairs the proof so the final theorem still holds, extends definitions to commutative semirings and universe-polymorphic algebras, implements many explicit isomorphisms that papers omit, and produces artifacts for reuse though some automation of compatibility proofs does not yet succeed.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:24Universal properties
- 1:49Divided power algebras
- 3:14Robbie’s construction
- 5:45Motivation
- 7:11Formal definition
- 9:00Informal vs formal
- 10:28Universes in formalization
- 12:11Omitted isomorphisms
- 13:36Automation in Lean
- 14:41Summary
- 15:26Q&A
- 16:30Divided powers connection
- 17:14Universe levels
related talks
19mAutomated Verification of Fundamental Algebraic Laws
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
25mFormalising Perfectoid Spaces
27mFunctorial Semantics for Partial Theories
24mAn Order-Theoretic Analysis of Universe Polymorphism
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
35mModular Construction of Multi-sorted Free Extensions
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)