feat(Algebra/Category): introduce 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 introduce 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 right-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: feat(RingTheory): adds two lemmas on Module.length #36657

[github-actions]

PR summary 6b3e5a3312

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Group.Units.ULift (new file)	140
Mathlib.Algebra.Category.LocAlgCat.Defs (new file)	1356
Mathlib.Algebra.Category.LocAlgCat.Basic (new file)	1357
Mathlib.Algebra.Category.LocAlgCat.Cotangent (new file)	1764
Mathlib.Algebra.Category.LocAlgCat.BaseCat (new file)	1879

---

Declarations diff

+ BaseCat
+ Hom
+ Hom.isLocalHom_toAlgHom
+ Hom.map_maximalIdeal_le
+ Ideal.annihilator_inf_ne_bot
+ IsSmallExtension
+ IsSmallExtension.toOfQuot_span_singleton
+ LocAlgCat
+ Submodule.length_le_length_restrictScalars
+ Submodule.length_quotient_lt
+ algebraMap_specialFiber_apply_eq_zero
+ algebraOfQuot
+ baseCotangentMap
+ baseCotangentMap_tmul
+ coe_of
+ comap_algebraMap_maximalIdeal
+ exact_baseCotangentMap_mapCotangent_toSpecialFiber
+ fullyFaithfulUliftFunctor
+ hom_inv_apply
+ induction_on_isSmallExtension
+ infinitesimalNeighborhood
+ instance (A : BaseCat Λ k) : IsArtinianRing A.obj := A.property
+ 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
+ isScalarTower_algebraOfQuot
+ isScalarTower_ofQuotResidueAlgebra
+ isScalarTower_ofQuotResidueAlgebra'
+ isSmallExtension_of_bijective
+ isSmallExtenstion_iff
+ isUnit_down
+ isUnit_up
+ isoEquivSubtypeAlgEquiv
+ isoMk
+ ker_residue
+ ker_toAlgHom_toOfQuot
+ krullDim_le_of_orderEmbedding
+ lt_add_left
+ mapCotangent
+ mapCotangent_toCotangent
+ mapInfinitesimalNeighborhood
+ mapOfQuot
+ mapSpecialFiber
+ map_toAlgHom_toOfQuot_maximalIdeal_eq
+ ofHom
+ ofHom_comp
+ ofHom_id
+ ofHom_toAlgHom_apply
+ ofIso
+ ofQuotResidueAlgebra
+ ofhom_toAlgHom
+ range_baseCotangentMap
+ residue
+ residueEquiv
+ residueEquiv_residue_apply
+ residueField_smul_cotangent
+ residue_apply
+ residue_comp_coe_ofIso
+ residue_eq_zero_iff
+ residue_ofQuot_mk_apply
+ residue_of_apply
+ residue_smul_cotangent
+ residue_surjective
+ residue_toRingHom
+ smul_cotangent_def
+ specialFiber
+ surjective_mapCotangent_toOfQuot
+ surjective_mapCotangent_toSpecialFiber
+ surjective_toAlgHom_toOfQuot
+ toAlgHom_comp
+ toAlgHom_id
+ toAlgHom_mapOfQuot_apply
+ toAlgHom_toOfQuot_apply
+ toInfinitesimalNeighborhood
+ toOfQuot_comp_mapOfQuot
+ toSpecialFiber
+ uliftFunctor
++ of
++ ofQuot
++ 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
806	1	backward.privateInPublic
416	1	backward.privateInPublic.warn

Current commit c53938e2ad
Reference commit 6b3e5a3312

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:

• feat(RingTheory): adds two lemmas on Module.length #36657
  By Dependent Issues (🤖). Happy coding!