feat(AlgebraicGeometry): function fields and Faltings' theorem

[alreadydone]

No description provided.

[MichaelStollBayreuth]

Otherwise LGTM.

[MichaelStollBayreuth]

Maybe you can also add a concrete special case, e.g.,

theorem faltngs_hyperelliptic {K : Type*} [Field K] [NumberField K] {f : Polynomial K} (hf : f.discr ≠ 0) (hd : 5 ≤ f.natDegree) :
    {x : K | IsSquare (f.eval x)}.Finite := by
  sorry

It would be interesting to see if (1) models can find simpler proofs for the special case, (2) models can deduce the concrete application from the general result.

[alreadydone]

Nice idea! I'd use Polynomial.Separable for hf though.

[MichaelStollBayreuth]

Strangely, according to loogle, there is no result in Mathlib that connects Polynomial.Separable and Polynomial.discr... I guess this is because Polynomial.discr has very little API.

[alreadydone]

Yeah apparently @kckennylau added Polynomial.discr relatively recently.

[alreadydone]

Maybe you can also add a concrete special case, e.g.,

I think it's better that you open a separate PR to add it in another file (maybe under NumberTheory is more suitable than AlgebraicGeometry for this one), since it doesn't mention function fields. This file would be suitable for further eval_problems about function fields, like Riemann Roch ...

[alreadydone]

Instead of the old Is1DFunctionField I introduced

class BundledFunctionField extends
  Algebra (RatFunc K) F, IsScalarTower K (RatFunc K) F, FunctionField K F

to make statements shorter.