# Zulip Chat Archive

## Stream: maths

### Topic: Union_of_directed

#### Kevin Buzzard (Aug 12 2020 at 10:32):

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 (Aug 12 2020 at 10:46):

I think I will do this after refactoring `algebra.direct_limit`

, which will happen after #3733 is merged

#### Kevin Buzzard (Aug 12 2020 at 10:57):

OK then I'll leave `bundled_subring.lean`

with no `Union_of_directed`

for now.

#### Kevin Buzzard (Aug 12 2020 at 12:19):

aah, several hundred lines later I have run into `mem_supr_of_directed`

#### Yury G. Kudryashov (Aug 12 2020 at 14:27):

And AFAIR `mem_Sup_of_directed`

#### Yury G. Kudryashov (Aug 12 2020 at 20:49):

The first version of bundled `submonoid`

s 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.

Last updated: May 18 2021 at 06:15 UTC