-
Notifications
You must be signed in to change notification settings - Fork 15
Pull requests: chrisflav/proetale
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat(Mathlib/RingTheory/Etale/Henselian): sections and coprime factorizations over Henselian local rings (Stacks 04GG)
fable
#200
opened Jul 17, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/WeakDimension): cartesian diagram for integrally closed algebraic extensions (Stacks 092U)
fable
#199
opened Jul 16, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/IdentifiesLocalRings): hom-set bijection for algebras identifying local rings (Stacks 096L)
fable
#198
opened Jul 16, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/IntegralLocal): an integral domain integral over a Henselian local ring is local
fable
#197
opened Jul 16, 2026 by
chrisflav
Owner
Loading…
feat(Mathlib/AlgebraicGeometry/Sites/Small): continuity of the functors between small P-sites
fable
#196
opened Jul 16, 2026 by
chrisflav
Owner
Loading…
feat(Mathlib/CategoryTheory/MorphismProperty/Ind): close
op_isFinitelyPresentable sorry
fable
#195
opened Jul 16, 2026 by
chrisflav
Owner
Loading…
feat(Mathlib/CategoryTheory/Functor/Flat): evaluation of a pointwise left Kan extension as a colimit without smallness
#189
opened Jul 11, 2026 by
chrisflav
Owner
Loading…
feat(AlgebraicGeometry/Sites/EtaleCohomology): the étale cohomology system of the constant sheaves ℤ/ℓⁿℤ
#188
opened Jul 11, 2026 by
chrisflav
Owner
Loading…
feat(AlgebraicGeometry/Sites/ElladicCohomology): the sheaf of continuous functions on the pro-étale site
#187
opened Jul 11, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/IntegralLocal): tensor product of local rings with purely inseparable residue field extension is local (Stacks 092Y)
fable
#183
opened Jun 24, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/WeaklyEtaleField): a weakly étale extension of fields is separable algebraic (Stacks 092P)
fable
#179
opened Jun 12, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/WLocalization): close
zeroLocus_ideal_eq and isWLocalRing sorries
fable
#178
opened Jun 12, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/IndEtale): nontrivial idempotents in ind-étale algebras over fields
fable
#177
opened Jun 12, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/Bijective): a weakly étale bijective-on-residue-fields local hom is an isomorphism
fable
#170
opened Jun 12, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/IndWeaklyEtale): every ind-étale algebra is weakly étale
fable
#169
opened Jun 12, 2026 by
chrisflav
Owner
Loading…
feat(Mathlib/RingTheory/WeaklyEtale/GoDown): faithfully flat intermediate descent of weakly étale algebras
archon
Upstreamed from `archon` branch
#160
opened Jun 9, 2026 by
chrisflav
Owner
Loading…
3 tasks done
feat(Topology/SpectralSpace/WLocal/Pullback): fill sorries for Stacks 096C (second part)
archon
Upstreamed from `archon` branch
#158
opened Jun 9, 2026 by
chrisflav
Owner
Loading…
2 tasks done
chore: bump mathlib to 236391b
auto-bump
dependencies
#131
opened Jun 2, 2026 by
github-actions
Bot
Loading…
feat(Algebra/WContractible): w-localness and π₀-equivalence of Upstreamed from `archon` branch
Restriction
archon
#130
opened Jun 2, 2026 by
chrisflav
Owner
Loading…
2 tasks done
feat(Mathlib/RingTheory/LocalRing): extended maximal ideal lies in Jacobson radical for finite extensions
archon
Upstreamed from `archon` branch
#108
opened May 25, 2026 by
chrisflav
Owner
Loading…
feat(Algebra/IndZariski): fill Upstreamed from `archon` branch
bijectiveOnStalks_algebraMap and of_colimitPresentation sorries
archon
#92
opened May 22, 2026 by
chrisflav
Owner
Loading…
1 task done
feat(Algebra/Category/Ring/FilteredDescent): FP-algebra descent along filtered colimit (Stacks 00U3)
archon
Upstreamed from `archon` branch
#73
opened May 21, 2026 by
chrisflav
Owner
Loading…
ProTip!
Adding no:label will show everything without a label.