feat(Algebra/Category): the category of local algebras with a fixed residue field

[BryceT233]

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]

PR summary dbcdd9f0c8

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)	1807
Mathlib.Algebra.Category.LocAlgCat.Cotangent (new file)	1845
Mathlib.Algebra.Category.LocAlgCat.BaseCat (new file)	1962

---

Declarations diff

+ BaseCat
+ Hom
+ Hom.isLocalHom_toAlgHom
+ Hom.map_maximalIdeal_le
+ Ideal.annihilator_inf_ne_bot
+ IsSmallExtension
+ IsSmallExtension.toOfQuot_span_singleton
+ LocAlgCat
+ algebraMap_specialFiber_apply_eq_zero
+ algebraOfQuot
+ baseCotangentMap
+ baseCotangentMap_tmul
+ bijective_mapCotangent_iff
+ bijective_mapCotangent_toOfQuot_iff
+ coe_of
+ coe_ofPullback
+ comap_algebraMap_maximalIdeal
+ equivCotangent
+ equivCotangent_apply
+ equivCotangent_symm_apply
+ exact_baseCotangentMap_mapCotangent_toSpecialFiber
+ fromOfPullback
+ fullyFaithfulUliftFunctor
+ hom_inv_apply
+ induction_on_isSmallExtension
+ infinitesimalNeighborhood
+ 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 : Module k (CotangentSpace A) := .compHom _ (A.residueEquiv.symm : k →+* ResidueField A)
+ 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 [IsLocalHom (algebraMap Λ k)] : IsLocalHom (algebraMap Λ A)
+ instance [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)] :
+ instance {R : Type*} [CommSemiring R] [IsLocalRing R] : IsLocalRing (ULift R)
+ inv_hom_apply
+ 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
+ mapCotangent
+ mapCotangent_baseCotangentMap_apply
+ mapCotangent_id
+ mapCotangent_mapOfQuot_surjective_of_mapCotangent_surjective
+ mapCotangent_toCotangent
+ mapInfinitesimalNeighborhood
+ mapOfQuot
+ mapSpecialFiber
+ map_toAlgHom_toOfQuot_maximalIdeal_eq
+ not_isUnit_aeval_of_aeval_eq_zero
+ ofHom
+ ofHom_comp
+ ofHom_id
+ ofHom_toAlgHom_apply
+ ofIso
+ ofPullback
+ ofPullbackResidueAlgebra
+ ofQuotKerIsoOfSurjective
+ ofQuotResidueAlgebra
+ ofhom_toAlgHom
+ range_baseCotangentMap
+ residue
+ residueEquiv
+ residueEquiv_residue_apply
+ residueField_smul_cotangent
+ residue_apply
+ residue_comp_coe_ofIso
+ residue_eq_zero_iff
+ residue_ofPullback_apply
+ residue_ofQuot_mk_apply
+ residue_of_apply
+ residue_smul_cotangent
+ residue_surjective
+ residue_toRingHom
+ smul_cotangent_def
+ specialFiber
+ 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
+ toInfinitesimalNeighborhood_comp_map
+ toInfinitesimalNeighborhood_comp_mapInfinitesimalNeighborhood_toSpecialFiber
+ toOfQuot_comp_mapOfQuot
+ toOfQuot_comp_ofQuotKerIsoOfSurjective_hom
+ toSpecialFiber
+ uliftFunctor
++ isLocalHom_pullbackFst
++ isLocalHom_pullbackSnd
++ isUnit_pullback_mk_iff
++ mapCotangent_comp
++ of
++ ofQuot
++ pullback
++ pullbackFst
++ pullbackSnd
++ surjective_pullbackFst_of_surjective
++ surjective_pullbackSnd_of_surjective
++ toOfQuot

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
798	1	backward.privateInPublic
414	1	backward.privateInPublic.warn

Current commit 79b36d765f
Reference commit dbcdd9f0c8

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(RingTheory): adds two lemmas on Module.length #36657
• feat(Algebra/Ring): pullback for RingHom and AlgHom #37008
  By Dependent Issues (🤖). Happy coding!