Fixed points of endomorphism form substructure

Stream: maths

[Keefer Rowan]

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_submonoid`s 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]

I think is_submonoid is deprecated

[Kevin Buzzard]

you want to use submonoid

[Kevin Buzzard]

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]

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

[Keefer Rowan]

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

[Kevin Buzzard]

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

[Keefer Rowan]

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]

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

[Kevin Buzzard]

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]

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

[Keefer Rowan]

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]

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

[Keefer Rowan]

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]

Is there a good way to find all broken dependencies?

[Kevin Buzzard]

Removing the unbundled definition is the hard part

[Kevin Buzzard]

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]

What would you recommend doing?

[Kevin Buzzard]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

We have meq_locus

[Keefer Rowan]

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]

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

[Yury G. Kudryashov]

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