Skip to content
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

Jump to bottom

feat(AlgebraicGeometry): flat morphisms of schemes #19790

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

feat(AlgebraicGeometry): flat morphisms of schemes #19790

wants to merge 15 commits into from
+219 −3

Conversation

chrisflav
Copy link
Collaborator

@chrisflav chrisflav commented Dec 8, 2024 •
edited
Loading

... and show that Flat can be checked on stalks. The latter is shown more generally for any morphism property of schemes associated to a property of ring maps satisfying RingHom.OfLocalizationPrime.

Open in Gitpod

@chrisflav chrisflav added the t-algebraic-geometry Algebraic geometry label Dec 8, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 8, 2024 •
edited
Loading

PR summary 998147ac96

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.AlgebraicGeometry.Morphisms.Flat (new file) 1967

Declarations diff

+ Flat
+ RespectsIso.arrow_mk_iso_iff
+ Spec.map_surjective
+ arrowStalkMapIsoOfInseparable
+ coe_resLE_base
+ comp
+ iff_flat_stalkMap
+ instance (priority := 900) [IsOpenImmersion f] : Flat f
+ instance : HasRingHomProperty @Flat RingHom.Flat
+ instance : MorphismProperty.IsMultiplicative @Flat
+ instance : MorphismProperty.IsStableUnderComposition @Flat
+ isStableUnderBaseChange
+ localRingHom
+ ofLocalizationPrime
+ resLEStalkMap
+ stalkIso_inv
+ ι_base_apply
++ of_stalkMap
++ stalkMap

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).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 8, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 9, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 22, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 22, 2024
chrisflav
chrisflav commented Jan 8, 2025
View reviewed changes
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
Comment on lines +671 to +672
(hQ : ∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (_ : Q f)
(J : Ideal S) (_ : J.IsPrime), Q (Localization.localRingHom _ J f rfl))
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could give this a name (I don't think this follows from RingHom.LocalizationPreserves, since it differs by composition with a localization map), but maybe it is fine to just leave it as is for now and see if we need this more often.

erdOne
erdOne reviewed Jan 17, 2025
View reviewed changes
Mathlib/AlgebraicGeometry/Scheme.lean
@@ -761,6 +761,14 @@ lemma stalkMap_germ_apply (U : Y.Opens) (x : X) (hx : f.base x ∈ U) (y) :
X.presheaf.germ (f ⁻¹ᵁ U) x hx (f.app U y) :=
PresheafedSpace.stalkMap_germ_apply f.toPshHom U x hx y

/-- If `x` and `y` are inseparable, the stalk maps are isomorphic. -/
noncomputable def arrowStalkMapIsoOfInseparable {x y : X}
(h : Inseparable x y) : Arrow.mk (f.stalkMap x) ≅ Arrow.mk (f.stalkMap y) :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think using x = y here makes it easier to use. Since the underlying space of a scheme is sober, no generality is lost.

erdOne
erdOne reviewed Jan 17, 2025
View reviewed changes
Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

/-- A morphism of schemes `f : X ⟶ Y` is flat if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, the induced map `Γ(Y, U) ⟶ Γ(X, V)` is flat.
-/
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you point to iff_flat_stalkMap here, as that is the more common definition in the literature? (also in the module docstring)

@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 17, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@erdOne erdOne erdOne left review comments

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes t-algebraic-geometry Algebraic geometry
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@chrisflav @mathlib4-dependent-issues-bot @erdOne @leanprover-community-bot-assistant