Union_of_directed

Stream: maths

[Kevin Buzzard]

There are some Union_of_directed lemmas in deprecated. The union of a bunch of subgroups of a group typically is not a subgroup, because if $h$ is in H and $k$ is in K then $hk$ might be in neither. The fix is to consider directed unions instead, i.e. unions over collections of subgroups such that for all H and K, there exists J with H<=J and K<=J.

So deprecated/submonoid has is_add_submonoid_Union_of_directed, and the same story for subgroups. There is is_subfield_Union_of_directed in subfield.lean but this will be deprecated one day, and a similar story for is_subring_Union_of_directed in ring_theory.subring. In particular most of the usages of this concept are on the way out. The only other time Union_of_directed shows up in mathlib is in linear_algebra.basis where it's proved for linear independence.

We're on the home straight for bundling subrings, but is_subring_Union_of_directed is not there yet because it relies on stuff which isn't there. Should all these lemmas be ported to the bundled situation (i.e. should we have this lemma for groups?)

Example:

lemma subring_Union_of_directed {ι : Type*} [hι : nonempty ι] (s : ι → subring R)
  (directed : ∀ i j, ∃ k, s i ≤ s k ∧ s j ≤ s k) :
  subring R :=
{ carrier := (⋃i, s i),
...

The alternative is to express this stuff using Sup, i.e. that the canonical map from the lattice of subrings to the lattice of subsets preserves directed Sups. But I'm not even sure we have a way to express this in mathlib. Do we have morphisms of partial orders and predicates saying that they preserve various lattice structures? Filtered Sup is a thing, I am seeing filtered colimits more and more in mathematics nowadays.

[Kenny Lau]

I think I will do this after refactoring algebra.direct_limit, which will happen after #3733 is merged

[Kevin Buzzard]

OK then I'll leave bundled_subring.lean with no Union_of_directed for now.

[Kevin Buzzard]

aah, several hundred lines later I have run into mem_supr_of_directed

[Yury G. Kudryashov]

And AFAIR mem_Sup_of_directed

[Yury G. Kudryashov]

The first version of bundled submonoids had Sup_of_directed. I later converted this to mem_Sup_of_directed because I think that this is a better API for bundled objects.