feat(Algebra/Category): the category of local algebras with a fixed residue field by BryceT233 · Pull Request #37940 · leanprover-community/mathlib4

BryceT233 · 2026-04-12T01:30:37Z

This is an attempt to design the definitions of base category [Stacks, 06GC] and complete base category in deformation theory. The approach we take is to first introduce a larger category of local algebras with a fixed residue field, then define base category and complete base category to be full subcategories of this larger category via ObjectProperty.

To be specific:

In Defs.lean, we define LocAlgCat and LocAlgCat.Hom to be the type of objects and morphisms in the category, and provide a universe lift functor.
In Basic.lean, we add the basic construction ofQuot and toOfQuot, which is the quotient of an object in LocAlgCat by a proper Ideal. Then we use them to define infinitesimalNeighborhood and specialFiber for an object in LocAlgCat.
In Cotangent.lean, we introduce k-vector space structures on CotangentSpace of objects in LocAlgCat and prove the exactness of the conormal sequence for the special fiber.
In BaseCat.lean, we define BaseCat to be the full subcategory of LocAlgCat consisting of Artinian local algebras and introduce the type class of a small extension for morphisms in BaseCat. We show that any surjective morphism in BaseCat can be factored into a finite composition of small extensions [Stacks, 06GE]

This PR is intended to showcase the overall design and architecture, I will split this into smaller PRs once the community reaches a consensus on the design choices.

depends on: [Merged by Bors] - feat(RingTheory): adds two lemmas on Module.length #36657
depends on: feat(Algebra/Ring): pullback for RingHom and AlgHom #37008

github-actions · 2026-04-12T01:31:41Z

PR summary 597460a80f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.LocalRing.LocalSubring`	1
`Mathlib.Algebra.Group.Units.ULift` (new file)	140
`Mathlib.Algebra.Category.LocAlgCat.Defs` (new file)	1360
`Mathlib.Algebra.Category.LocAlgCat.Basic` (new file)	1978
`Mathlib.Algebra.Category.LocAlgCat.Cotangent` (new file)	1989
`Mathlib.Algebra.Category.LocAlgCat.BaseCat` (new file)	1991

Declarations diff

+ BaseCat
+ Hom
+ Hom.isLocalHom_toAlgHom
+ Hom.map_maximalIdeal_le
+ Ideal.annihilator_inf_ne_bot
+ IsEssSurj
+ IsEssSurj.comp
+ IsEssSurj.hom_iso
+ IsSmallExtension
+ IsSmallExtension.hom_iso
+ IsSmallExtension.toOfQuot_span_singleton
+ LocAlgCat
+ algebraMap_specialFiber_apply_eq_zero
+ algebraOfQuot
+ baseCotangentMap
+ baseCotangentMap_tmul
+ bijective_mapCotangent_iff
+ bijective_mapCotangent_toOfQuot_iff
+ coe_of
+ comap_algebraMap_maximalIdeal
+ equivCotangent
+ equivCotangent_apply
+ equivCotangent_symm_apply
+ exact_baseCotangentMap_mapCotangent_toSpecialFiber
+ exists_mem_maximalIdeal_toAlgHom_apply_add_eq
+ fullyFaithfulUliftFunctor
+ hom_inv_apply
+ induction_on_isSmallExtension
+ instance (A : BaseCat Λ k) : IsArtinianRing A.obj := A.property
+ instance (f : A ⟶ B) : Nontrivial (A ⧸ RingHom.ker (f.toAlgHom))
+ instance (n : ℕ) [NeZero n] : Nontrivial (A ⧸ maximalIdeal A ^ n) := by
+ instance : (uliftFunctor Λ k).Faithful := (fullyFaithfulUliftFunctor Λ k).faithful
+ instance : (uliftFunctor Λ k).Full := (fullyFaithfulUliftFunctor Λ k).full
+ instance : Category (LocAlgCat.{w} Λ k)
+ instance : CoeSort (LocAlgCat Λ k) (Type w) := ⟨carrier⟩
+ instance : IsScalarTower A k (CotangentSpace A) := .of_algebraMap_smul residue_smul_cotangent
+ instance : IsScalarTower Λ (ResidueField A) (CotangentSpace A) := .of_algebraMap_smul fun r x ↦ by
+ instance : IsScalarTower Λ k (CotangentSpace A) := .of_algebraMap_smul fun r x ↦ by
+ instance [Algebra.IsIntegral Λ k] : IsScalarTower (ResidueField Λ) k (CotangentSpace A)
+ instance [Algebra.IsIntegral Λ k] : IsScalarTower Λ (ResidueField Λ) (CotangentSpace A)
+ instance [Algebra.IsIntegral Λ k] : Module (ResidueField Λ) (CotangentSpace A)
+ instance [IsArtinianRing A] : IsArtinian Λ A
+ instance [IsArtinianRing A] : IsNoetherian Λ A
+ instance [IsArtinianRing A] [IsArtinianRing B] (f : A ⟶ C) (g : B ⟶ C) :
+ instance [IsLocalRing Λ] [Algebra.IsIntegral Λ k] :
+ instance {R : Type*} [CommSemiring R] [IsLocalRing R] : IsLocalRing (ULift R)
+ inv_hom_apply
+ isArtinianRing_ofPullback
+ isEssSurj_iff_isEssSurj_mapOfQuot
+ isEssSurj_toOfQuot_of_le
+ isFiniteLength_of_isArtinianRing
+ isLocalHom_algebraMap
+ isLocalHom_of_isIntegral
+ isLocalHom_pullbackFst
+ isLocalHom_pullbackSnd
+ isLocalRing_algHomPullback
+ isLocalRing_eqLocus
+ isLocalRing_ringHomPullback
+ isScalarTower_algebraOfQuot
+ isScalarTower_ofPullbackResidueAlgebra
+ isScalarTower_ofQuotResidueAlgebra
+ isScalarTower_ofQuotResidueAlgebra'
+ isSmallExtension_of_bijective
+ isSmallExtenstion_iff
+ isUnit_aeval_derivative_of_isSeparable
+ isUnit_down
+ isUnit_eqLocus_mk_iff
+ isUnit_up
+ isoEquivSubtypeAlgEquiv
+ isoMk
+ ker_residue
+ ker_toAlgHom_toOfQuot
+ length_restrictScalars
+ mapCotangent
+ mapCotangent_baseCotangentMap_apply
+ mapCotangent_mapOfQuot_surjective_of_mapCotangent_surjective
+ mapCotangent_toCotangent
+ map_toAlgHom_toOfQuot_maximalIdeal_eq
+ module_cotangentSpace
+ not_isUnit_aeval_of_aeval_eq_zero
+ ofHom
+ ofHom_comp
+ ofHom_id
+ ofHom_toAlgHom_apply
+ ofIso
+ ofPullbackOfIsSeparable
+ ofPullbackResidueAlgebra
+ ofQuotKerIsoOfSurjective
+ ofQuotResidueAlgebra
+ ofhom_toAlgHom
+ pullbackFst_isSmallExtension
+ range_baseCotangentMap
+ residue
+ residueEquiv
+ residueEquiv_residue_apply
+ residueField_smul_cotangent
+ residue_apply
+ residue_comp_coe_ofIso
+ residue_comp_pullbackFst
+ residue_eq_zero_iff
+ residue_ofQuot_mk_apply
+ residue_of_apply
+ residue_smul_cotangent
+ residue_surjective
+ residue_toRingHom
+ smul_cotangent_def
+ surjective_mapCotangent_of_surjective
+ surjective_mapCotangent_of_surjective_mapCotangent_mapSpecialFiber
+ surjective_mapCotangent_toOfQuot
+ surjective_mapCotangent_toSpecialFiber
+ surjective_of_surjective_mapCotangent
+ surjective_residue_comp_pullbackFst_of_isSeparable
+ surjective_toAlgHom_toOfQuot
+ toAlgHom_comp
+ toAlgHom_id
+ toAlgHom_mapOfQuot_apply
+ toAlgHom_ofQuotKerIsoOfSurjective_hom_apply
+ toAlgHom_ofQuotKerIsoOfSurjective_inv_apply
+ toAlgHom_toOfQuot_apply
+ toInfinitesimalNeighborhood_comp_map
+ toInfinitesimalNeighborhood_comp_mapInfinitesimalNeighborhood_toSpecialFiber
+ toOfQuot_comp_ofQuotKerIsoOfSurjective_hom
+ uliftFunctor
++ infinitesimalNeighborhood
++ isUnit_pullback_mk_iff
++ mapCotangent_comp
++ mapCotangent_id
++ mapInfinitesimalNeighborhood
++ mapOfQuot
++ mapSpecialFiber
++ of
++ ofPullback
++ ofQuot
++ pullback
++ specialFiber
++ surjective_pullbackFst_of_surjective
++ surjective_pullbackSnd_of_surjective
++ toInfinitesimalNeighborhood
++ toOfQuot
++ toOfQuot_comp_mapOfQuot
++ toSpecialFiber
++++ pullbackFst
++++ pullbackSnd
++++ pullback_comm_sq

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6217	1	backward.isDefEq.respectTransparency
798	1	backward.privateInPublic
414	1	backward.privateInPublic.warn

Current commit fde30a4c47
Reference commit 597460a80f

You can run this locally as

./scripts/reporting/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).

…o LocAlgCat

Deicyde · 2026-04-21T03:01:02Z

+  simpa using LocAlgCat.pullback_comm_sq f.hom g.hom hg
+
+@[stacks 06GH "(2)"]
+instance pullbackFst_isSmallExtension (f : A ⟶ C) (g : B ⟶ C) [IsSmallExtension g] :


Deicyde · 2026-04-21T03:01:08Z

+    (LocAlgCat.surjective_residue_comp_pullbackFst_of_isSeparable f.hom g.hom), inferInstance⟩
+
+@[stacks 06S5]
+theorem isEssSurj_iff_isEssSurj_mapOfQuot (f : A ⟶ B) {I : Ideal A.obj} {J : Ideal B.obj}


Deicyde · 2026-04-21T03:01:23Z

+
+open Submodule in
+@[elab_as_elim, stacks 06GE]
+theorem induction_on_isSmallExtension (hf : Surjective f.hom.toAlgHom)


Deicyde · 2026-04-21T03:04:49Z

+/-- The base category for deformation theory over `Λ`. This is the full subcategory of
+`LocAlgCat Λ k` consisting of Artinian local `Λ`-algebras with residue field `k`. -/
+@[stacks 06GC]
+abbrev BaseCat (Λ : Type u) [CommRing Λ] (k : Type v) [Field k] [Algebra Λ k] : Type _ :=


There is very heavy abbrev use in this file. I look at FGModuleCat for example, it only uses abbrev for FGModuleCat itself and of. Everything else is def.

Deicyde · 2026-04-21T03:07:36Z

+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in


Can you explain why these are here?

If you read the documentation of this command, you will see that it explains "This is a backwards compatibility option, intended to help migrating to new Lean releases... Please report an issue if you rely on this option."

Thanks for the review and comments, I will look into them in detail! For the set_option here, I thought this was because mk is made private in the definition of LocAlgCat, I found this pattern in files under the same Category folder like CommAlgCat.lean. I am not sure why mk is made private though.

Deicyde · 2026-04-21T03:36:12Z

 end LocalSubring
+
+
+theorem isLocalRing_eqLocus {R S : Type*} [Ring R] [Semiring S] [IsLocalRing R] (f g : R →+* S) :


Is this the best place for these? They feel like they are randomly stuck on the end of the file, they're not even in a section

Deicyde · 2026-04-21T03:38:52Z

+    apply IsLocalHom.map_nonunit at this; right
+    simpa [RingHom.isUnit_pullback_mk_iff] using ⟨hs, this⟩
+
+theorem isLocalRing_algHomPullback {R S T A : Type*} [CommSemiring R] [Ring S] [Algebra R S]


These seem like very strong assumptions. Check if there is a way to generalize this.

Deicyde · 2026-04-21T03:40:22Z

  (RingEquiv.quotientBot k) (by ext; rfl)

+variable (R k) in
+lemma isLocalHom_of_isIntegral [Algebra.IsIntegral R k] : IsLocalHom (algebraMap R k) := by


Is there is a reason why this is in the ResidueField file? It doesn't seem to rely on anything here. Try #find_home

Thanks, I removed the use of IsLocalHom instance very recently and this is something that I forgot to remove. edit: this is still needed but probably should be moved to where Algebra.ker_algebraMap_isMaximal_of_isIntegral goes

Deicyde · 2026-04-21T03:41:14Z

+open Submodule in
+theorem Ideal.annihilator_inf_ne_bot {R : Type*} [CommSemiring R] {I J : Ideal R}
+    (hI : IsNilpotent I) (hJ : J ≠ ⊥) : I.annihilator ⊓ J ≠ ⊥ := by
+  rcases hI with ⟨n, hn⟩


Deicyde · 2026-04-21T03:52:48Z

+
+namespace RingHom
+
+theorem isUnit_eqLocus_mk_iff (f g : A →+* C) {r : A} (r_in : r ∈ f.eqLocus g) :


I believe this duplicates CommRingCat.pullbackCone f g. Please try to use that instead.

Deicyde · 2026-04-21T04:00:17Z

+/-- The universe lift functor for `LocAlgCat` is fully faithful. -/
+def fullyFaithfulUliftFunctor : (uliftFunctor Λ k).FullyFaithful where
+  preimage {A B} f :=
+    letI : Algebra (ULift.{w'} A) k := ULift.algebra' ..


It is usually a bad sign when you have to thread a bunch of letI, haveI throughout your file. Something is messing up your instance resolution.

Deicyde · 2026-04-21T04:02:12Z

+open Submodule in
+theorem range_baseCotangentMap [Algebra.IsIntegral Λ k] :
+    A.baseCotangentMap.range = (mapCotangent A.toSpecialFiber).ker := ext fun x ↦ by
+  rcases (maximalIdeal A).toCotangent_surjective x with ⟨x, rfl⟩


Deicyde · 2026-04-21T04:03:12Z

+    [HenselianRing A (maximalIdeal A)] [HenselianRing B (maximalIdeal B)]
+    [Algebra.IsSeparable (ResidueField Λ) k] (f : A ⟶ C) (g : B ⟶ C) :
+    Surjective (A.residue.comp (f.toAlgHom.pullbackFst g.toAlgHom)) := by
+  obtain ⟨x, hx⟩ := Field.exists_primitive_element (ResidueField Λ) k


Deicyde · 2026-04-21T04:06:28Z

+
+end ArtinianRing
+
+lemma exists_mem_maximalIdeal_toAlgHom_apply_add_eq (f : A ⟶ C) (g : B ⟶ C) (a : A)


This should be in a section. Should also have a docstring.

Deicyde · 2026-04-21T04:06:46Z

+open Polynomial in
+@[stacks 06GH "(3)"]
+theorem surjective_residue_comp_pullbackFst_of_isSeparable [IsLocalRing Λ] [Module.Finite Λ k]
+    [HenselianRing A (maximalIdeal A)] [HenselianRing B (maximalIdeal B)]


Deicyde · 2026-04-21T04:10:55Z

+
+/-- The subalgebra of pairs `(a, b) : A × B` such that `f a = g b`, i.e.,
+  the pullback of f and g as a subalgebra of A × B. -/
+abbrev pullback (f : A →ₐ[R] C) (g : B →ₐ[R] C) : Subalgebra R (A × B) := equalizer


These do not belong in this file

Duplicate of AlgHom.equalizer

BryceT233 added 28 commits April 9, 2026 09:25

Update Basic.lean

47b8ec5

Merge branch 'leanprover-community:master' into LocAlgCat

c642855

Create ULift.lean

bb5e058

Update Mathlib.lean

61e6971

Create README.md

adec84c

Delete Mathlib/Algebra/Category/LocAlgCat/README.md

dfcfb78

Create Defs.lean

123df16

Update Defs.lean

2f7ff4e

Merge branch 'leanprover-community:master' into LocAlgCat

e9126ff

Update Defs.lean

73ada75

Update Mathlib.lean

98f8a2d

Update Defs.lean

bae1d90

Merge branch 'leanprover-community:master' into LocAlgCat

4ae9f40

Add files via upload

52d9e14

Add files via upload

feab79a

Update Mathlib.lean

6045824

Update Basic.lean

140d133

Update KrullDimension.lean

ec34740

Update Length.lean

456db0b

Update BaseCat.lean

0bb827a

Update Cotangent.lean

22f3a8b

Update Defs.lean

6f03216

Update Basic.lean

605501d

Update Basic.lean

95974fa

Update Basic.lean

477aff4

Update Cotangent.lean

a56d501

Update BaseCat.lean

4f399a4

Update Maps.lean

371f629

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 12, 2026

BryceT233 and others added 8 commits April 18, 2026 13:29

Merge branch 'leanprover-community:master' into LocAlgCat

e6ce6bf

cleanup

59b0ffb

Merge branch 'LocAlgCat' of https://github.com/BryceT233/mathlib4 int…

5060721

…o LocAlgCat

add results about ofPullback in artinian ring case

45b1c9e

add ofPullback in BaseCat

f9f9da1

replace IsLocalHom instances by Algebra.IsIntegral

7baea03

Merge branch 'leanprover-community:master' into LocAlgCat

d72ff8f

add IsEssSurj to BaseCat.lean

7fc3a68

Deicyde reviewed Apr 21, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Ideal/Cotangent.lean Outdated

Deicyde reviewed Apr 21, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Ideal/Cotangent.lean

Deicyde reviewed Apr 21, 2026

View reviewed changes

BryceT233 and others added 4 commits April 21, 2026 12:23

Update Cotangent.lean

9418034

[pre-commit.ci lite] apply automatic fixes

4049a2f

fix

bc0193b

Merge branch 'master' into LocAlgCat

fde30a4

		set_option backward.privateInPublic true in
		set_option backward.privateInPublic.warn false in

		end LocalSubring


		theorem isLocalRing_eqLocus {R S : Type} [Ring R] [Semiring S] [IsLocalRing R] (f g : R →+ S) :


		namespace RingHom

		theorem isUnit_eqLocus_mk_iff (f g : A →+* C) {r : A} (r_in : r ∈ f.eqLocus g) :


		end ArtinianRing

		lemma exists_mem_maximalIdeal_toAlgHom_apply_add_eq (f : A ⟶ C) (g : B ⟶ C) (a : A)

Conversation

BryceT233 commented Apr 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 597460a80f

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Deicyde Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Deicyde Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

BryceT233 Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

BryceT233 commented Apr 12, 2026 •

edited

Loading

github-actions bot commented Apr 12, 2026 •

edited

Loading

Deicyde Apr 21, 2026 •

edited

Loading

Deicyde Apr 21, 2026 •

edited

Loading

BryceT233 Apr 21, 2026 •

edited

Loading