feat(Algebra/Category/Ring/FilteredDescent): FP-algebra descent along filtered colimit (Stacks 00U3)#73
Open
chrisflav wants to merge 9 commits into
Conversation
… filtered colimit (Stacks 00U3) Proves that if `F : J ⥤ CommRingCat` is filtered with colimit cocone `c` and `φ : c.pt ⟶ A` is finitely presented, then there exists a finite stage `j₀` with an FP map `φⱼ : F.obj j₀ ⟶ Aⱼ` such that the square is a pushout (equivalently, `A ≃ c.pt ⊗[F.obj j₀] Aⱼ`). This is Stacks Tag 00U3. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
chrisflav
added
archon
…eview Address the review of chrisflav#73: - Promote `exists_finset_lift` to a public lemma `exists_lift_finset_of_isColimit` and move it next to the existing `FilteredColimits.lean`. - Drop the redundant `c.ι.app j₀ ≫ φ = φⱼ ≫ ψ` conjunct from the existential (it is just `IsPushout.w`). - Replace the ~40-line manual `IsPushout` construction with `Algebra.IsPushout.of_equiv (P.tensorModelOfHasCoeffsEquiv R₀)` followed by `CommRingCat.isPushout_of_isPushout`, eliminating the `eIso`/four-naturality -squares boilerplate. - Split the main proof into three steps: (a) lift coefficients to a finite stage, (b) build the descended model, (c) conclude the pushout. - Rename `exists_fp_algebra_descent_of_isColimit` to `exists_finitePresentation_descent_of_isColimit` and tag it with `@[stacks 00U3]`.
chrisflav
removed
the
awaiting-auto-review
chrisflav
added
the
awaiting-auto-review
chrisflav
added
awaiting-auto-review
Generalize the finset-jointly-surjective lemma to filtered colimits of types (per maths review), and apply the suggested style/naming fixes (per style review): - Move `exists_lift_finset_of_isColimit` to a new file under `Proetale/Mathlib/CategoryTheory/Limits/Types/Filtered.lean` under the name `jointly_surjective_finset_of_isColimit`, generalised to any filtered colimit of types with `lift : s → F.obj j`. - Rename `exists_finitePresentation_descent_of_isColimit` to `exists_finitePresentation_isPushout_of_isColimit`. - Build `ψAlg` directly from `tensorModelOfHasCoeffsHom` instead of routing through `eAlg.restrictScalars`; scope the `Algebra.TensorProduct.rightAlgebra` local instance to the pushout branch where it is needed. - Replace `change … ; rfl` with `rfl`, switch tactic-mode `letI`/`haveI` to `let _`/`have`, switch `fun … =>` to `fun … ↦`, fold trivial single-use `have`s, drop noise type ascriptions and step labels. - Add a copyright header to `Proetale/Mathlib/Algebra/Category/Ring/FilteredColimits.lean`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
removed
the
awaiting-auto-review
jjdishere
reviewed
Jun 9, 2026
Collaborator
|
orchestra address review |
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…orts Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
jjdishere
approved these changes
Jun 9, 2026
jjdishere
reviewed
Jun 9, 2026
jjdishere
left a comment
jjdishere
left a comment
Collaborator
There was a problem hiding this comment.
Add this lemma and its proof in the blueprint blueprint/src/chapters/more-on-local-structure.tex, add \lean and \leanon, add proper \uses in the blue print where this lemma is used.
Collaborator
|
orchestra address review |
…olimit) Per review on PR chrisflav#73, document the new lemma `CommRingCat.exists_finitePresentation_isPushout_of_isColimit` in the blueprint with `\lean` and `\leanok` annotations, including a sketch of the proof.
jjdishere
reviewed
Jun 9, 2026
jjdishere
left a comment
jjdishere
left a comment
Collaborator
There was a problem hiding this comment.
orchestra address review
Collaborator
|
orchestra address review |
…uage
Replace the cocone notation c.pt / c_{j_0} with the colimit ring R and
indexed family (R_j)_{j in J}; rephrase the proof accordingly.
jjdishere
reviewed
Jun 9, 2026
Collaborator
There was a problem hiding this comment.
which theroem further uses lemma:fp-algebra-descent-filtered-colim? please add \uses
Collaborator
|
orchestra address review |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
Proetale/Mathlib/Algebra/Category/Ring/FilteredDescent.lean, which proves Stacks Tag 00U3: ifF : J ⥤ CommRingCatis a filtered diagram with colimit coconecandφ : c.pt ⟶ Ais a finitely presented ring map, then there exists a finite stagej₀ : J, an objectAⱼand an FP mapφⱼ : F.obj j₀ ⟶ Aⱼ, and a mapψ : Aⱼ ⟶ Asuch that the squareis a pushout (equivalently,
A ≃ c.pt ⊗[F.obj j₀] Aⱼ).Proetale/Mathlib/Algebra/Category/Ring/FilteredDescent.lean(191 lines, 0 sorries)Proetale.leanSource
Upstreamed from the
archonbranch (Proetale/Mathlib/Algebra/Category/Ring/FilteredDescent.lean), with style fixes: removed unused instance names, removed prohibitedshow ... frominsiderw, cleaned up redundant comments.