Commit 2024-12-21 08:53 2e468db5

feat: algebraic hierarchy on DirectLimit (#19893) Order/DirectedInverseSystem.lean: define the DirectLimit of a DirectedSystem of types as a quotient (by a setoid (equivalence relation)) of the Sigma type (disjoint union). Provide the induction lemmas and map/lift constructions used to define algebraic operations on DirectLimit. New file Algebra/Colimit/DirectLimit.lean: the first 400 lines are boilerplate code that defines algebraic instances on DirectLImit from magma (Mul) to Field. To make everything "hom-polymorphic", the DirectedSystem consists of FunLikes rather than plain/unbundled functions, and we use algebraic hom typeclasses (e.g. LinearMapClass, RingHomClass) everywhere. The remaining 70 lines essentially shows that DirectLimit is the colimit in the categories of Module and Ring. Algebra/DirectLimit.lean: renamed to Algebra/Colimit/ModuleRing.lean. This file was originally added @kckennylau 5 years ago in [mathlib3#754](https://github.com/leanprover-community/mathlib3/pull/754) and defines Module.DirectLimit and Ring.DirectLimit as quotients of the universal objects (DirectSum and FreeCommRing). This definition is more general and suitable for arbitrary colimits, but makes it very cumbersome to prove of.zero_exact lemmas (130+ lines!); for DirectLimit constructed as quotients of the disjoint union, these are just by definition. We golf these proofs by constructing isomorphisms between Module/Ring.DirectLimit and _root_.DirectLimit. I have more work done that generalizes most lemmas there to work for arbitrary colimits, that's why I put it under a new Colimit directory. Data/Int/Cast/Lemmas.lean: add map_intCast' Data/Nat/Cast/Basic.lean: golf a lemma Order/Directed.lean: add a lemma ModelTheory/DirectLimit.lean: change two lemmas to aliases of the general FunLike lemmas