Add Frobenius elements

[jouglasheen]

Frobenius elements

[kbuzzard]

@jjaassoonn @jouglasheen can you clarify why there are two files here? My instinct is to merge this PR (but ideally with the file in for_mathlib) and then refactor it until it's appropriate to go into mathlib.

[jouglasheen]

@kbuzzard @jjaassoonn CrazyFrobenius.lean is an obsolete version of ExistsFrobenius.lean. We can delete CrazyFrobenius.lean.

[kbuzzard]

Can you delete it and bump to current main? Or is this hard?

[jouglasheen]

I tried to delete the file by right-clicking this:

but apparently that's not the way to do it. I don't know how to delete it or bump to the main branch.

[joelriou]

This is a special case of https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/GroupAction/Quotient.html#MulAction.ofQuotientStabilizer

[kim-em]

I tried to delete the file by right-clicking this:

@jouglasheen, to delete the file, do it on the command line: git rm FLT/CrazyFrobenius.lean and then commit and push as usual.

[kim-em]

@jouglasheen:

I don't know how to ... bump to the main branch.

You can just do:

git checkout CrazyFrobenius
git fetch
git merge origin/main

If the merge works, then just git push. Otherwise, learn how to deal with git conflicts. :-)

[kim-em]

Naming things with ' is rarely a good idea. Can you think up a name that gives the human a hint? Even AKLB_Ideal?

[kim-em]

Alternatively can you make it private??

[kbuzzard]

The file compiles fine with

@[nolint unusedArguments] abbrev Ideal' (A K L B : Type*) [CommSemiring A]
  [CommSemiring B] [Algebra A B] [CommSemiring K] [Semiring L]
  [Algebra A K] [Algebra B L]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] := Ideal B

which confirms that Ideal' B only needs to know "it's in an A K L B set-up" which might be code for a commutative square (with the diagonal filled in) in the same way that three Algebra instances and an IsScalarTower is code for a commutative triangle.

[joelriou]

It seems to me that many lemmas and definitions until here would apply to any element in B instead of the carefully chosen β. It may be worth generalizing the construction of F, etc, in that generality.

[jouglasheen]

@semorrison @joelriou Thank you very much for the reviews and help with github. I have succeeded in deleting the obsolete file and I think I have succeeded in merging to the main branch.

Please, excuse some delay in responding to your reviews (I am currently studying for exams).

[kbuzzard]

Thanks!

[kbuzzard]

The file compiles fine with

@[nolint unusedArguments] abbrev Ideal' (A K L B : Type*) [CommSemiring A]
  [CommSemiring B] [Algebra A B] [CommSemiring K] [Semiring L]
  [Algebra A K] [Algebra B L]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] := Ideal B

which confirms that Ideal' B only needs to know "it's in an A K L B set-up" which might be code for a commutative square (with the diagonal filled in) in the same way that three Algebra instances and an IsScalarTower is code for a commutative triangle.