feat(algebraic_geometry): descent theorem

[jjaassoonn]

---

[alexjbest]

Maybe you already saw it, but I posted some old code I had on this sort of material to Zulip today at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/thoughts.20on.20elliptic.20curves/near/265022015, its not the most general definition of a height function, and so the proof is easier than the one in Silverman say. But if it is at all useful to you feel free to reuse parts of it.

[jjaassoonn]

This proof is now sorry free, but I wonder if it is worth writing it in mathlib standard

[alexjbest]

This proof is now sorry free, but I wonder if it is worth writing it in mathlib standard

Nice! Personally I think it is worth adding to mathlib, its a really important result. I'm not sure what uses it has outside of proving the Mordell-Weil theorem, but that alone should be enough to justify adding it to mathlib IMO.

[jjaassoonn]

Can you add this for submonoid, add_subgroup, add_submonoid, subsemiring, and semiring too? Maybe in a new PR with the whole set.

Is it like #10908?

[riccardobrasca]

Is there a reason why you use A : Ab instead of [comm_group _]?

[jcommelin]

This will need better documentation, and better names (and namespacing) before it is ready for further review.

[jcommelin]

Please write a more detailed docstring, with capital letters and interpunction. Maybe add a reference to another source.

[jcommelin]

It seems that this is in the root namespace. Is that intentional?

[jcommelin]

Names should try to avoid referring to variables such as A.