refactor `StarAlgEquiv` to extend `StarRingEquiv`

Stream: mathlib4

[Monica Omar]

At the moment, docs#StarAlgEquiv extends docs#RingEquiv and has two additional properties: map_star' and map_smul'. Since we now have docs#StarRingEquiv, shouldn't we let StarAlgEquiv extend it? This wouldn't really change much (besides simplifying some proofs since we wouldn't need to provide map_star'), it would be a very minor refactoring.

[Jireh Loreaux]

That's fine. At one point I had a plan to refactor AlgEquiv to allow for non-unital algebras, but I never finished it.

[Monica Omar]

That would be a good next step. Then StarAlgEquiv would literally just extend StarRingEquiv and AlgEquiv, which would be nice.

I can try refactoring AlgEquiv sometime soon if you don't want to :)

[Jireh Loreaux]

@Monica Omar #8686

[Monica Omar]

ufft from 2 years ago. 35+ files have merge conflicts. Wouldn't it be better to just start over @Jireh Loreaux?

[Ruben Van de Velde]

I'm guessing it'd be roughly equal amount of work either way

[Monica Omar]

Wouldn't it confuse some users that there's docs#NonUnitalAlgHom and docs#AlgHom, but then (after a refactor) there would only be a non-unital docs#AlgEquiv? Wouldn't it make more sense to have NonUnitalAlgEquiv to match the homomorphisms? forget what I said

[Monica Omar]

we already have docs#NonUnitalAlgEquivClass, but in the /StarAlgHom file (with a note that says that it's mostly an implementation detail for docs#StarAlgEquivClass, which no longer exists apparently?)

[Jireh Loreaux]

Monica Omar said:

ufft from 2 years ago. 35+ files have merge conflicts. Wouldn't it be better to just start over Jireh Loreaux?

Yes, it might indeed be easier to start over, but you can look at that PR to see what I did / how I approached it. Some of the fixes may still work.

[Jireh Loreaux]

StarAlgEquivClass went away because we started unbundling some of the morphism classes for performance reasons, and that note about NonUnitalAlgEquivClass never got updated.

[Jireh Loreaux]

Note that NonUnitalAlgEquivClass is a strict generalization of AlgEquivClass in the sense that the type class assumptions are more general, and in the narrower case (i.e., when you have Algebras), NonUnitalAlgEquivClass implies AlgEquivClass.

[Monica Omar]

There's only one file left to fix for the refactoring of AlgEquiv: #29354

The problem is with Ideal.Quotient.stabilizerHom_surjective_of_profinite in RingTheory/Invariant/Profinite, I don't know what's going on here. It's causing a timeout for some reason. If someone can help with this, I'd appreciate it :)

[Kevin Buzzard]

set_option maxHeartbeats 400000 in fixes it, although this isn't ideal.

[Monica Omar]

Definitely not ideal. Do you know what is happening here?

[Kevin Buzzard]

The trace is one of those annoying traces where the numbers don't add up:

              [] [1.479886] obtain ⟨N, hN⟩ :=
                    ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one (stabilizer_isOpen G x) (one_mem _) ▼
                [Meta.check] [0.145134] ✅️ (∃ H, ↑H ⊆ ↑(MulAction.stabilizer G x)) → ((stabilizerHom Q P G) ⟨a, ⋯⟩) ((mk Q) x) = σ ((mk Q) x) ▶

The sum of the numbers in the more indented lines (0.145) is supposed to add up to the number in the less indented line (1.47) so there's a missing 1.3 seconds which is really hard to explain without running a debugger or something. I'm travelling right now but were I to be at home with a two screen setup I would be tempted to open two copies of mathlib on master and your branch and see if the numbers were very different or whether you've just pushed something over the edge.

[Kevin Buzzard]

Sometimes changes just cause things like this to happen but it's annoying not really understanding where the missing 1.3 seconds are.

[Aaron Liu]

maybe the time is disappearing into a function whose trace is not enabled

[Aaron Liu]

like death by a thousand whnfs

[Kevin Buzzard]

No idea why, but this fixes it:

  · ext x
    have hx := Ideal.Quotient.mk_surjective x
    obtain ⟨x, rfl⟩ := hx
    have hx := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    obtain ⟨N, hN⟩ := hx
    lift x to B' N.1.1 using fun (g : ↑N.toOpenSubgroup) ↦ hN g.2

i.e. break up the two obtains into two steps, and then give a hint to the lift about what the type of g is shrug

[Monica Omar]

It's giving me a timeout with that. I'll try again tomorrow. Been on this branch for 8 hours straight :zzz:.

[Kevin Buzzard]

I'm surprised we're having different experiences. Here's the entire proof, which isn't timing out for me:

/-- The stabilizer subgroup of `Q` surjects onto `Aut((B/Q)/(A/P))`. -/
theorem Ideal.Quotient.stabilizerHom_surjective_of_profinite
    (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P]
    [Algebra.IsInvariant A B G] :
    Function.Surjective (Ideal.Quotient.stabilizerHom Q P G) := by
  intro σ
  let B' := FixedPoints.subalgebra A B
  obtain ⟨s, hs⟩ := nonempty_sections_of_finite_cofiltered_system
    (stabilizerHomSurjectiveAuxFunctor (G := G) P Q σ)
  let a := (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv.hom
    ⟨fun N ↦ (s N).1.1, (fun {N N'} f ↦ congr($(hs f).1.1))⟩
  have (N : OpenNormalSubgroup G) : QuotientGroup.mk (s := N.1.1) a = (s N).1 :=
    congr_fun (congr_arg Subtype.val (ConcreteCategory.congr_hom (ProfiniteGrp.of
      G).isoLimittoFiniteQuotientFunctor.inv_hom_id (Subtype.mk (fun N ↦ (s N).1.1) _))) N
  refine ⟨⟨a, ?_⟩, ?_⟩
  · ext x
    obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    lift x to B' N.1.1 using fun g ↦ hN g.2
    change x ∈ (a • Q).under (B' N.1.1) ↔ x ∈ Q.under (B' N.1.1)
    rw [← (s N).1.2]
    simp only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe
          (F := RingEquiv _ _)]
    congr! 2
    ext y
    rw [← this]
    rfl
  · ext x
    have hx := Ideal.Quotient.mk_surjective x
    obtain ⟨x, rfl⟩ := hx
    have hx := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    obtain ⟨N, hN⟩ := hx
    lift x to B' N.1.1 using fun (g : ↑N.toOpenSubgroup) ↦ hN g.2
    change Ideal.Quotient.mk Q (QuotientGroup.mk (s := N) a • x).1 = _
    rw [this]
    exact DFunLike.congr_fun (s N).2 (Ideal.Quotient.mk _ x)

[Kevin Buzzard]

It's a beautiful result, it shows the existence of Frobenius elements. It was first proved for G finite in FLT (perhaps modulo one or two intermediate sorries) and then ported over to mathlib by Thomas Browning and then generalised to profinite groups by Andrew Yang. I had no idea the theorem was true in this generality; Joel Riou pointed it out to me. I learnt the proof from Bourbaki.

[Monica Omar]

Ahh. It does work. My bad. I forgot about the first obtain and only thought about the second one.

[Kevin Buzzard]

Yeah sorry, I should have posted the entire proof first rather than a random fragment.

[Monica Omar]

The benchmark results on #29354 don't look great :/
Does anyone have any thoughts on what to do to make things run smoother here?

[Kevin Buzzard]

I think that this is always the problem with these refactors. It does not surprise me that things are slower and I think that this might just be inevitable. It would be good if someone could prove me wrong!

[Kevin Buzzard]

I also think that whilst we traditionally look at the reds and greens in the output and go "oh dear, more red than green this must be a step in the wrong direction", these percentages are kind of meaningless in some sense because just knowing the percentage increase or decrease doesn't tell you too much about the absolute changes. Here's another way of looking at it: the total build has gone up 100 billion instructions but the total lint has gone down over 100 billion instructions and so actually there's a net win here.

[Aaron Liu]

but why is lint faster

[Monica Omar]

It's no longer faster after I did some extra generalizations.

So there's two things that I'm not sure what to do about:
1- @[to_additive] failing: see comment
2- a type mismatch error: see comment

Besides that, there were 2 other things I've commented on where things were strange.

If anyone wants to take a look and help out, that would be great :)

[Monica Omar]

There's a new problem with the refactor pr #29354 now, after the Gal(_/_) notation was pushed earlier today.
The problem is with MathlibTest/GalNotation.
@Andrew Yang since you authored it, can you take a look?

At the moment, it's printing _ ≃ₐ[_] _ for everything.

[Andrew Yang]

You changed the arity for AlgEquiv so you should change line 41 of Galois/Notation.lean to

  guard <| (← getExpr).isAppOfArity ``AlgEquiv 9

And line 43 to

  let #[R, A, B, _, _, _, _, _, _] := (← getExpr).getAppArgs | failure

[Monica Omar]

Merging master to #29354 today gave me another timeout error with the RingTheory/Invariant/Profinite file again, but this time with a definition: Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor.
set_option maxHeartbeats 201000 in fixes it, but that's not really a good fix.
If someone can help with this, I'd appreciate it :)

[Monica Omar]

I'm not sure what's going wrong that this file keeps timing out

[Andrew Yang]

Can you try !benching the PR to see if your refactor slows down only that file or everything else and if so by how much?

[Andrew Yang]

I am guessing this change is requiring lean to go through the CommRing -> CommSemiring -> CommMonoid -> Monoid -> Semigroup -> Mul chain a lot more times and because there are multiple (reducibly defeq) such paths lean is spending more time to unify them.

[Monica Omar]

Yeah probably. Let's see. For reference, the last bench from 6 weeks ago:

build: +129.853⬝10⁹ (+0.08%)
lint:  -120.806⬝10⁹ (-1.72%)

https://github.com/leanprover-community/mathlib4/pull/29354#issuecomment-3289623504

[Monica Omar]

things are so much worse now than 6 weeks ago:

build   +758.462⬝10⁹    (+0.44%)
lint    +22.396⬝10⁹     (+0.33%)

https://github.com/leanprover-community/mathlib4/pull/29354#issuecomment-3469614397