Skip to content

[Merged by Bors] - feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma #30237

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma #30237

Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
28a6fa7
use factorization instead of factor
yonggyuchoimath Oct 4, 2025
64ce476
polish
yonggyuchoimath Oct 4, 2025
c3aff3a
Merge branch 'master' into yonggyuchoimath-simple-flat-2
yonggyuchoimath Oct 5, 2025
c44c428
Update Flat.lean
yonggyuchoimath Oct 5, 2025
58f56f2
remove non-robust
yonggyuchoimath Oct 13, 2025
cb3651b
remove section
yonggyuchoimath Oct 13, 2025
f15f7b1
remove import
yonggyuchoimath Oct 13, 2025
1f1d985
Merge branch 'master' into yonggyuchoimath-simple-flat-2
yonggyuchoimath Oct 13, 2025
63104e5
Update Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
yonggyuchoimath Oct 22, 2025
df5a9f2
Update Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
yonggyuchoimath Oct 22, 2025
b18a83c
Merge branch 'master' into yonggyuchoimath-simple-flat-2
yonggyuchoimath Oct 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions Mathlib/AlgebraicGeometry/Morphisms/Flat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,14 @@ lemma epi_of_flat_of_surjective (f : X ⟶ Y) [Flat f] [Surjective f] : Epi f :=
(Flat.stalkMap f x) (f.toLRSHom.prop x)
exact ‹RingHom.FaithfullyFlat _›.injective

lemma flat_and_surjective_iff_faithfullyFlat_of_isAffine [IsAffine X] [IsAffine Y] :
Flat f ∧ Surjective f ↔ f.appTop.hom.FaithfullyFlat := by
rw [RingHom.FaithfullyFlat.iff_flat_and_comap_surjective,
MorphismProperty.arrow_mk_iso_iff @Surjective (arrowIsoSpecΓOfIsAffine f),
MorphismProperty.arrow_mk_iso_iff @Flat (arrowIsoSpecΓOfIsAffine f),
← HasRingHomProperty.Spec_iff (P := @Flat), surjective_iff]
rfl

end Flat

end AlgebraicGeometry