[Merged by Bors] - feat(group_theory): use generic `subobject_class` lemmas #11758

Vierkantor · 2022-02-01T11:23:38Z

This subobject class refactor PR follows up from #11750 by moving the {zero,one,add,mul,...}_mem_class lemmas to the root namespace and marking the previous sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem lemmas as protected. This is the second part of #11545 to be split off.

I made the subobject parameter to the _mem lemmas implicit if it appears in the hypotheses, e.g.

lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M]
  {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s

instead of having (s : S) explicit. The generic _mem lemmas are not namespaced, so there is no dot notation that requires s to be explicit. Also there were already a couple of instances for the same operator where s was implicit and others where s was explicit, so some change was needed.

depends on: [Merged by Bors] - feat(*): define subobject classes from submonoid up to subfield #11750

The next part of my big refactoring plans: subobject classes in the same style as morphism classes. This PR introduces the following subclasses of `set_like`: * `one_mem_class`, `zero_mem_class`, `mul_mem_class`, `add_mem_class`, `inv_mem_class`, `neg_mem_class` * `submonoid_class`, `add_submonoid_class` * `subgroup_class`, `add_subgroup_class` * `subsemiring_class`, `subring_class`, `subfield_class` The main purpose of this refactor is that we can replace the wide variety of lemmas like `{add_submonoid,add_subgroup,subring,subfield,submodule,subwhatever}.{prod,sum}_mem` with a single `prod_mem` lemma that is generic over all types `B` that extend `submonoid`: ```lean @[to_additive] lemma prod_mem {M : Type*} [comm_monoid M] [set_like B M] [submonoid_class B M] {ι : Type*} {t : finset ι} {f : ι → M} (h : ∀c ∈ t, f c ∈ S) : ∏ c in t, f c ∈ S ``` ## API changes * When you extend a `struct subobject`, make sure to create a corresponding `subobject_class` instance. ## Upcoming PRs This PR splits out the first part of #11545, namely defining the subobject classes. I am planning these follow-up PRs for further parts of #11545: - [ ] make the subobject consistently implicit in `{add,mul}_mem` #11758 - [ ] remove duplicate instances like `subgroup.to_group` (replaced by the `subgroup_class.to_subgroup` instances that are added by this PR) #11759 - [ ] further deduplication such as `finsupp_sum_mem` ## Subclassing `set_like` Contrary to mathlib's typical subclass pattern, we don't extend `set_like`, but take a `set_like` instance parameter: ```lean class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] := (one_mem : ∀ (s : S), (1 : M) ∈ s) ``` instead of: ```lean class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] extends set_like S M := (one_mem : ∀ (s : S), (1 : M) ∈ s) ``` The main reason is that this avoids some big defeq checks when typechecking e.g. `x * y : s`, where `s : S` and `[comm_group G] [subgroup_class S G]`. Namely, the type `coe_sort s` could be given by `subgroup_class → @@submonoid_class _ _ (comm_group.to_group.to_monoid) → set_like → has_coe_to_sort` or by `subgroup_class → @@submonoid_class _ _ (comm_group.to_comm_monoid.to_monoid) → set_like → has_coe_to_sort`. When checking that `has_mul` on the first type is the same as `has_mul` on the second type, those two inheritance paths are unified many times over ([sometimes exponentially many](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60int.2Ecast_abs.60.20so.20slow.3F/near/266945077)). So it's important to keep the size of types small, and therefore we avoid `extends`-based inheritance. ## Defeq fixes Adding instances like `subgroup_class.to_group` means that there are now two (defeq) group instances for `subgroup`. This makes some code more fragile, until we can replace `subgroup.to_group` with its more generic form in a follow-up PR. Especially when taking subgroups of subgroups I needed to help the elaborator in a few places. These should be minimally invasive for other uses of the code. ## Timeout fixes Some of the leaf files started timing out, so I made a couple of fixes. Generally these can be classed as: * `squeeze_simps` * Give inheritance `subX_class S M` → `X s` (where `s : S`) a lower prority than `Y s` → `X s` so that `subY_class S M` → `Y s` → `X s` is preferred over `subY_class S M` → `subX_class S M` → `X s`. This addresses slow unifications when `x : s`, `s` is a submonoid of `t`, which is itself a subgroup of `G`: existing code expects to go `subgroup → group → monoid`, which got changed to `subgroup_class → submonoid_class → monoid`; when this kind of unification issue appears in your type this results in slow unification. By tweaking the priorities, we help the elaborator find our preferred instance, avoiding the big defeq checks. (The real fix should of course be to fix the unifier so it doesn't become exponential in these kinds of cases.) * Split a long proof with duplication into smaller parts. This was basically my last resort. I decided to bump the limit for the `fails_quickly` linter for `measure_theory.Lp_meas.complete_space`, which apparently just barely goes over this limit now. The time difference was about 10%-20% for that specific instance. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

leanprover-community-bot-assistant · 2022-04-05T14:51:57Z

This PR/issue depends on:

~~[Merged by Bors] - feat(*): define subobject classes from submonoid up to subfield #11750~~
By Dependent Issues (🤖). Happy coding!

The next part of my big refactoring plans: subobject classes in the same style as morphism classes. This PR introduces the following subclasses of `set_like`: * `one_mem_class`, `zero_mem_class`, `mul_mem_class`, `add_mem_class`, `inv_mem_class`, `neg_mem_class` * `submonoid_class`, `add_submonoid_class` * `subgroup_class`, `add_subgroup_class` * `subsemiring_class`, `subring_class`, `subfield_class` The main purpose of this refactor is that we can replace the wide variety of lemmas like `{add_submonoid,add_subgroup,subring,subfield,submodule,subwhatever}.{prod,sum}_mem` with a single `prod_mem` lemma that is generic over all types `B` that extend `submonoid`: ```lean @[to_additive] lemma prod_mem {M : Type*} [comm_monoid M] [set_like B M] [submonoid_class B M] {ι : Type*} {t : finset ι} {f : ι → M} (h : ∀c ∈ t, f c ∈ S) : ∏ c in t, f c ∈ S ``` ## API changes * When you extend a `struct subobject`, make sure to create a corresponding `subobject_class` instance. ## Upcoming PRs This PR splits out the first part of #11545, namely defining the subobject classes. I am planning these follow-up PRs for further parts of #11545: - [ ] make the subobject consistently implicit in `{add,mul}_mem` #11758 - [ ] remove duplicate instances like `subgroup.to_group` (replaced by the `subgroup_class.to_subgroup` instances that are added by this PR) #11759 - [ ] further deduplication such as `finsupp_sum_mem` ## Subclassing `set_like` Contrary to mathlib's typical subclass pattern, we don't extend `set_like`, but take a `set_like` instance parameter: ```lean class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] := (one_mem : ∀ (s : S), (1 : M) ∈ s) ``` instead of: ```lean class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] extends set_like S M := (one_mem : ∀ (s : S), (1 : M) ∈ s) ``` The main reason is that this avoids some big defeq checks when typechecking e.g. `x * y : s`, where `s : S` and `[comm_group G] [subgroup_class S G]`. Namely, the type `coe_sort s` could be given by `subgroup_class → @@submonoid_class _ _ (comm_group.to_group.to_monoid) → set_like → has_coe_to_sort` or by `subgroup_class → @@submonoid_class _ _ (comm_group.to_comm_monoid.to_monoid) → set_like → has_coe_to_sort`. When checking that `has_mul` on the first type is the same as `has_mul` on the second type, those two inheritance paths are unified many times over ([sometimes exponentially many](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60int.2Ecast_abs.60.20so.20slow.3F/near/266945077)). So it's important to keep the size of types small, and therefore we avoid `extends`-based inheritance. ## Defeq fixes Adding instances like `subgroup_class.to_group` means that there are now two (defeq) group instances for `subgroup`. This makes some code more fragile, until we can replace `subgroup.to_group` with its more generic form in a follow-up PR. Especially when taking subgroups of subgroups I needed to help the elaborator in a few places. These should be minimally invasive for other uses of the code. ## Timeout fixes Some of the leaf files started timing out, so I made a couple of fixes. Generally these can be classed as: * `squeeze_simps` * Give inheritance `subX_class S M` → `X s` (where `s : S`) a lower prority than `Y s` → `X s` so that `subY_class S M` → `Y s` → `X s` is preferred over `subY_class S M` → `subX_class S M` → `X s`. This addresses slow unifications when `x : s`, `s` is a submonoid of `t`, which is itself a subgroup of `G`: existing code expects to go `subgroup → group → monoid`, which got changed to `subgroup_class → submonoid_class → monoid`; when this kind of unification issue appears in your type this results in slow unification. By tweaking the priorities, we help the elaborator find our preferred instance, avoiding the big defeq checks. (The real fix should of course be to fix the unifier so it doesn't become exponential in these kinds of cases.) * Split a long proof with duplication into smaller parts. This was basically my last resort. I decided to bump the limit for the `fails_quickly` linter for `measure_theory.Lp_meas.complete_space`, which apparently just barely goes over this limit now. The time difference was about 10%-20% for that specific instance. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

…lean`

…ascript the coercion between subalgebra and submodule)

…ed params)

jcommelin

This is really cool! Thank you so much for all the effort you poured into this.

bors merge

This subobject class refactor PR follows up from #11750 by moving the `{zero,one,add,mul,...}_mem_class` lemmas to the root namespace and marking the previous `sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem` lemmas as `protected`. This is the second part of #11545 to be split off. I made the subobject parameter to the `_mem` lemmas implicit if it appears in the hypotheses, e.g. ```lean lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M] {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s ``` instead of having `(s : S)` explicit. The generic `_mem` lemmas are not namespaced, so there is no dot notation that requires `s` to be explicit. Also there were already a couple of instances for the same operator where `s` was implicit and others where `s` was explicit, so some change was needed.

bors · 2022-04-09T19:04:52Z

Build failed (retrying...):

Build mathlib

This subobject class refactor PR follows up from #11750 by moving the `{zero,one,add,mul,...}_mem_class` lemmas to the root namespace and marking the previous `sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem` lemmas as `protected`. This is the second part of #11545 to be split off. I made the subobject parameter to the `_mem` lemmas implicit if it appears in the hypotheses, e.g. ```lean lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M] {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s ``` instead of having `(s : S)` explicit. The generic `_mem` lemmas are not namespaced, so there is no dot notation that requires `s` to be explicit. Also there were already a couple of instances for the same operator where `s` was implicit and others where `s` was explicit, so some change was needed.

bors · 2022-04-09T19:16:11Z

This PR was included in a batch that was canceled, it will be automatically retried

This subobject class refactor PR follows up from #11750 by moving the `{zero,one,add,mul,...}_mem_class` lemmas to the root namespace and marking the previous `sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem` lemmas as `protected`. This is the second part of #11545 to be split off. I made the subobject parameter to the `_mem` lemmas implicit if it appears in the hypotheses, e.g. ```lean lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M] {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s ``` instead of having `(s : S)` explicit. The generic `_mem` lemmas are not namespaced, so there is no dot notation that requires `s` to be explicit. Also there were already a couple of instances for the same operator where `s` was implicit and others where `s` was explicit, so some change was needed.

bors · 2022-04-09T21:49:20Z

Build failed (retrying...):

Build mathlib

This subobject class refactor PR follows up from #11750 by moving the `{zero,one,add,mul,...}_mem_class` lemmas to the root namespace and marking the previous `sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem` lemmas as `protected`. This is the second part of #11545 to be split off. I made the subobject parameter to the `_mem` lemmas implicit if it appears in the hypotheses, e.g. ```lean lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M] {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s ``` instead of having `(s : S)` explicit. The generic `_mem` lemmas are not namespaced, so there is no dot notation that requires `s` to be explicit. Also there were already a couple of instances for the same operator where `s` was implicit and others where `s` was explicit, so some change was needed.

bors · 2022-04-10T03:33:35Z

Pull request successfully merged into master.

Build succeeded:

Vierkantor added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Feb 1, 2022

This was referenced Feb 1, 2022

WIP feat(*): define subobject classes up to subfield_class #11545

Closed

refactor(*): remove duplicate subobject instances #11759

Closed

[Merged by Bors] - feat(*): define subobject classes from submonoid up to subfield #11750

Closed

Vierkantor force-pushed the generic-mem_lemmas branch from 43d49ae to ffa91b7 Compare February 1, 2022 15:36

leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 2, 2022

Vierkantor force-pushed the generic-mem_lemmas branch from 714dd2d to 33a06bf Compare February 3, 2022 15:28

leanprover-community-bot-assistant added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Feb 3, 2022

leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 5, 2022

Vierkantor force-pushed the generic-mem_lemmas branch from 33a06bf to 13108bd Compare April 5, 2022 16:01

leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 5, 2022

Vierkantor added 12 commits April 8, 2022 13:22

chore(group_theory): replace subobject.op_mem lemmas with generic ones

157cf1a

Further protect the op_mem lemmas in subclasses of the op_mem_class

4c165e8

Fix algebra/pointwise.lean (parameters)

28b7944

Fix algebra/module/submodule_lattice.lean (param changes)

0b442a0

Fix data/dfinsupp/basic.lean (changed parameters)

256b8c2

Fix data/dfinsupp/basic.lean (changed parameters)

2bb5035

Fix linear_algebra/basic.lean (mostly changed params)

d76cb01

Fix linear_algebra/quotient.lean (changed parameters)

cccf471

Fix linear_algebra/finsupp.lean (changed parameters)

719045f

Fix algebra/algebra/basic.lean (changed parameters)

4f7d2bf

Fix algebra/algebra/operations.lean (changed parameters)

cd2317d

Fix algebra/algebra/tower.lean (changed parameters)

4d5128d

Vierkantor and others added 14 commits April 8, 2022 13:22

Fix ring_theory/integral_closure.lean (changed params, genericize)

53bfe68

Fix field_theory/intermediate_field.lean (delete duplicate lemmas)

03dd0ba

Fix ring_theory/local_properties.lean (genericize)

c681e34

Fix algebra/lie/cartan_subalgebra.lean (genericize)

3a14e40

Fix analysis/convex/cone.lean (genericize)

04f14ca

Fix ring_theory/ideal/basic.lean (protect more lemmas)

c937535

Fix ring_theory/jacobson_ideal.lean (changed params)

62b261c

Fix modifications to pow_mem in `group_theory/submonoid/membership.…

4c9bc9f

…lean`

Fix algebra/module/submodule.lean (duplicate instances)

5cfedd8

Fix linear_algebra/span.lean (changed params)

9bda6d1

Fix linear_algebra/prod.lean (changed params)

0159ea9

Fix algebra/algebra/subalgebra/basic.lean (remove duplicate lemma)

01a5008

Fix algebra/algebra/subalgebra/pointwise.lean (changed param, type …

42afb41

…ascript the coercion between subalgebra and submodule)

Fix ring_theory/graded_algebra/homogeneous_localization.lean (chang…

e764eef

…ed params)

Vierkantor force-pushed the generic-mem_lemmas branch from 25cbe4a to e764eef Compare April 8, 2022 11:38

jcommelin approved these changes Apr 9, 2022

View reviewed changes

leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 9, 2022

bors bot changed the title ~~feat(group_theory): use generic subobject_class lemmas~~ [Merged by Bors] - feat(group_theory): use generic subobject_class lemmas Apr 10, 2022

bors bot closed this Apr 10, 2022

bors bot deleted the generic-mem_lemmas branch April 10, 2022 03:33

collares mentioned this pull request Apr 11, 2022

[Merged by Bors] - feat(algebraic_geometry/projective_spectrum): structure sheaf of Proj of graded ring #13072

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(group_theory): use generic `subobject_class` lemmas #11758

[Merged by Bors] - feat(group_theory): use generic `subobject_class` lemmas #11758

Vierkantor commented Feb 1, 2022 •

edited

leanprover-community-bot-assistant commented Apr 5, 2022

jcommelin left a comment

bors bot commented Apr 9, 2022

bors bot commented Apr 9, 2022

bors bot commented Apr 9, 2022

bors bot commented Apr 10, 2022

[Merged by Bors] - feat(group_theory): use generic subobject_class lemmas #11758

[Merged by Bors] - feat(group_theory): use generic subobject_class lemmas #11758

Conversation

Vierkantor commented Feb 1, 2022 • edited

leanprover-community-bot-assistant commented Apr 5, 2022

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Apr 9, 2022

bors bot commented Apr 9, 2022

bors bot commented Apr 9, 2022

bors bot commented Apr 10, 2022

[Merged by Bors] - feat(group_theory): use generic `subobject_class` lemmas #11758

[Merged by Bors] - feat(group_theory): use generic `subobject_class` lemmas #11758

Vierkantor commented Feb 1, 2022 •

edited