feat(Algebra/Category/Ring/FilteredDescent): FP-algebra descent along filtered colimit (Stacks 00U3)#73
Open
chrisflav wants to merge 2 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
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
1 participant
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.