!4#4052 Algebra.DirectLimit (needed for `Ext`)

Stream: mathlib4

[Kevin Buzzard]

This PR !4#4052 is on the way to Ext groups, which would be really good to get into Lean 4 because we need them for cohomology theories. One definition from the file:

def DirectLimit : Type max v w :=
  DirectSum ι G ⧸
    (span R <|
      { a |
        ∃ (i j : _)(H : i ≤ j)(x : _),
          DirectSum.lof R ι G i x - DirectSum.lof R ι G j (f i j H x) = a })
#align module.direct_limit Module.DirectLimit

@Adam Topaz is this the sort of thing which is now done with TypeMax?

[Kevin Buzzard]

DirectSum.{v, w} (ι : Type v) (β : ι → Type w) [inst✝ : (i : ι) → AddCommMonoid (β i)] : Type (max w v)

[Kevin Buzzard]

(Matt Ballard told me "no, unless it's causing problems")

[Kevin Buzzard]

There are some rewrites failing in this PR, and I am dreading having to fill in the underscores manually in things like rw [(FreeCommRing.lift _).map_neg]

[Kevin Buzzard]

I had meant to look at this again today but haven't had the time yet. There are some failing rewrites.

[Kevin Buzzard]

There's also

Error: ./././Mathlib/Algebra/DirectLimit.lean:590:11: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  fun a ↦ Set.decidableUnion s t a
inferred
  fun a ↦ propDecidable ((fun x ↦ x ∈ s ∪ t) a)

[Eric Wieser]

That looks like a misplaced open Classical

[Kevin Buzzard]

OK there's only a few errors left but I can't get rid of them.

[Kevin Buzzard]

This now compiles. Thanks a lot @Joël Riou !