feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma

[yonggyuchoimath]

This PR introduces the following simple lemma:

• AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine: A morphism between affine schemes is flat and surjective if and only if the corresponding map on global sections is faithfully flat.

Co-authored-by: Christian Merten

[github-actions]

PR summary d9d1cc1012

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ flat_and_surjective_iff_faithfullyFlat_of_isAffine

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[chrisflav]

Please avoid pinging people in PR descriptions (this means they get a notification whenever someone does a git rebase involving this commit and pushes it somewhere). If you want to indicate co-authorship, please add a line "Co-authored by: Name " instead.

[yonggyuchoimath]

My apologies for that. Thank you for letting me know, and I've added Co-authored-by.

[yonggyuchoimath]

I'll move base_factorization_type to another file (or try to avoid it) and remove WIP.

WIP

[yonggyuchoimath]

I've decided to exclude everything except flat_and_surjective_iff_of_faithfullyFlat_of_isAffine in this PR, as the statements are not optimal at this stage and it should be easy to reproduce them later.

-WIP

[yonggyuchoimath]

Thanks! I've committed all the suggestions.

-awaiting-author

[chrisflav]

LGTM, but I am a co-author. @erdOne could you please have a look?