## Stream: maths

### Topic: Fixed points of endomorphism form substructure

#### Keefer Rowan (May 27 2020 at 14:08):

I don't think this is anywhere in the library (note this is inspired by the complex inner product issue), but I want to add for a bunch of the algebraic structures (monoid, group, ring, field) that the fixed points of an endomorphism $f$, form a sub-x (where x is monoid, group, ring, field resp). Here's the one for monoid:

/-- The set of fixed points of an endomorphism f of a monoid M is a submonoid of M. -/
@[to_additive is_add_submonoid_fixed "The set of fixed points of an endomorphism f of an add_monoid M is a add_submonoid of M. "]
lemma is_submonoid_fixed (f : M →* M) : is_submonoid (fixed_points f) :=
begin
split,
{exact monoid_hom.map_one f},
intros a b a_def b_def,
change f (a * b) = a *b,
rw monoid_hom.map_mul,
change f a = a at a_def,
change f b = b at b_def,
simp *
end


It is in the file group_theory/submonoid.lean and is right under this lemma (on which the formatting was based):

/-- The union of an indexed, directed, nonempty set of submonoids of a monoid M is a submonoid
of M. -/
@[to_additive is_add_submonoid_Union_of_directed "The union of an indexed, directed, nonempty set of add_submonoids of an add_monoid M is an add_submonoid of M. "]
lemma is_submonoid_Union_of_directed {ι : Type*} [hι : nonempty ι]
(s : ι → set M) [∀ i, is_submonoid (s i)]
(directed : ∀ i j, ∃ k, s i ⊆ s k ∧ s j ⊆ s k) :
is_submonoid (⋃i, s i) := sorry


Is this all good?

#### Kevin Buzzard (May 27 2020 at 14:10):

I think is_submonoid is deprecated

#### Kevin Buzzard (May 27 2020 at 14:11):

you want to use submonoid

#### Kevin Buzzard (May 27 2020 at 14:13):

import group_theory.submonoid order.fixed_points

open order

def submonoid_fixed {M : Type*} [monoid M] (f : M →* M) :
submonoid M :=
{ carrier := fixed_points f,
one_mem' := monoid_hom.map_one f,
mul_mem' := begin
intros a b a_def b_def,
change f (a * b) = a *b,
rw monoid_hom.map_mul,
change f a = a at a_def,
change f b = b at b_def,
simp *
end }


Same proof, different implementation

#### Kevin Buzzard (May 27 2020 at 14:17):

Someone better than me at automation will probably be able to make simp do the tactic proof all in one go

#### Keefer Rowan (May 27 2020 at 14:18):

Cool, thanks. I was wondering how to state it in the bundled case.

#### Kevin Buzzard (May 27 2020 at 14:18):

Note that it's a definition, not a theorem, because of the carrier

#### Keefer Rowan (May 27 2020 at 14:20):

Yeah, that's why I couldn't figure out the correct statement at first, but it makes sense when you show it like that.

#### Keefer Rowan (May 27 2020 at 14:20):

For subgroups, subrings, and subfields, it's still all unbundled, right?

#### Kevin Buzzard (May 27 2020 at 14:22):

I think subgroups are bundled now. For the others, if you could bundle them first then that would be great :-) Bundling PR's are really good fun. Both Jason KY and Amelia Livingston (UG Imperial mathematicians) had early PR's which were just bundling unbundled structures and they both learnt a lot.

#### Kevin Buzzard (May 27 2020 at 14:22):

I'll be bundling normal subgroups in June and then attempting to refactor quotient groups based on them

#### Keefer Rowan (May 27 2020 at 14:23):

Looking at the group_theory/subgroups.lean, I don't see any bundled subgroup. Is there anywhere else worth looking? On a different branch?

#### Kevin Buzzard (May 27 2020 at 14:24):

For some reason Jason (aka Kexing Yang) made a new file bundled_subgroup and the PR police let him do it

#### Keefer Rowan (May 27 2020 at 14:25):

I see that. I guess to avoid breaking all the dependencies? How should one go about bundling? Replace the unbundled definition, redo all the theorems, and fix all broken dependencies?

#### Keefer Rowan (May 27 2020 at 14:25):

Is there a good way to find all broken dependencies?

#### Kevin Buzzard (May 27 2020 at 14:25):

Removing the unbundled definition is the hard part

#### Kevin Buzzard (May 27 2020 at 14:26):

I do not encourage learner undergraduates to do that. Basically what is going on is that for months people were saying "uuh, the correct thing to do is to bundle submodules, subgroups, group homs, ring homs etc, all at once, and to remove the unbundled ones, and it will be a monster PR" and of course nobody would do it

#### Keefer Rowan (May 27 2020 at 14:27):

What would you recommend doing?

#### Kevin Buzzard (May 27 2020 at 14:27):

but then I began to need it, so I started encouraging people to do the bundling but leave the unbundling alone, because then there will be a far more inefficient process involving much smaller PR's but at least I'd be able to use bundled group homs for the stuff I wanted to do with them

#### Kevin Buzzard (May 27 2020 at 14:29):

Well, first talk to @Yury G. Kudryashov and @Johan Commelin because they know the state of the art better than me. The question is what is next on the list of unbundled things which should be bundled, and the next question is whether bundling them is a good idea (for which I vote yes, but it would be interesting to have a poll)

#### Kevin Buzzard (May 27 2020 at 14:36):

PS I think you're also running into lean#197 , your goals shouldn't mention set.mem and this is hurting automation I think

#### Keefer Rowan (May 27 2020 at 14:50):

Question 1) What are the advantages of bundling that makes it worthwhile do all the work to change to library?
Question 2) How does one track all the dependencies without opening every file in Mathlib?

#### Johan Commelin (May 27 2020 at 14:54):

Without bundling, you need to find type classes all the time. And this didn't always work as expected.

#### Yury G. Kudryashov (May 27 2020 at 15:50):

We have meq_locus

#### Keefer Rowan (May 27 2020 at 16:11):

So what's the deal with fixing bundling? Is that something worth working on? Right now we have bundled and unbundled for both monoids and subgroups. Is the goal to kill off the unbundled?

#### Yury G. Kudryashov (May 27 2020 at 16:32):

As far as I understand, the goal is to kill unbundled homs and substructures.

#### Yury G. Kudryashov (May 27 2020 at 16:34):

Because in many cases we can construct bundled objects right away instead of relying on classes. At the same time [monoid M] etc are not deprecated because we don't want to write nat.monoid --> M

Last updated: May 18 2021 at 06:15 UTC