feat(RingTheory): flat extension of local ring

[Thmoas-Guan]

This PR mainly formalize the theorem [Stacks 03C3] for flat extension of local ring.

---

• depends on: feat(Algebra/CommRingCat): colimit of local ring via local hom #39075

[github-actions]

PR summary 26fdeaa70a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.Ring.FilteredColimitsLocal (new file)	1437
Mathlib.RingTheory.Flat.Extension (new file)	2120

---

Declarations diff

+ FlatExtension
+ Hom
+ Hom.comp
+ Hom.id
+ Hom.mk'
+ IsScalarTower.algebraMap_range_le
+ SuccStruct
+ adjoinAlgebraicToK
+ adjoinAlgebraic_isLocalRing
+ adjoinAlgebraic_maximalIdeal_eq_map
+ adjoinAlgebraic_maximalIdeal_map_isMaximal
+ adjoinAlgebraic_mem_range
+ adjoinTranscendentalToK
+ adjoinTranscendental_aeval_ker
+ adjoinTranscendental_maximalIdeal_eq_map
+ adjoinTranscendental_mem_range
+ algebraMapKCocone
+ algebraMap_comp_ι_eq
+ algebraMap_eq_zero
+ algebraMap_range_lt_of_not_surjective
+ coconeOfCoconeForget
+ coconeOfCoconeForgetPt
+ exists_isLocalHom_flat
+ exists_isLocalHom_flat'
+ ind_flat_eq_flat
+ instance (J : Type u) [LinearOrder J] [Nonempty J] (C : Type w) [Category.{v} C]
+ instance (S : FlatExtension R K) : IsLocalHom (algebraMap R S)
+ instance (S : FlatExtension R K) : IsLocalHom (algebraMap S K) := by
+ instance (S₁ S₂ : FlatExtension R K) (f : S₁.Hom S₂) : IsLocalHom f.algHom.toRingHom := by
+ instance (S₁ S₂ : FlatExtension R K) :
+ instance (x : K) (int : IsIntegral S x) :
+ instance (x : K) (int : IsIntegral S x) : Algebra (adjoinAlgebraic K S x int) K
+ instance (x : K) (int : IsIntegral S x) : Module.Finite S (adjoinAlgebraic K S x int)
+ instance (x : K) (int : IsIntegral S x) : Module.Free S (adjoinAlgebraic K S x int)
+ instance : Category (FlatExtension R K)
+ instance : CoeSort (FlatExtension R K) (Type u) := ⟨FlatExtension.Ring⟩
+ instance : ConcreteCategory (FlatExtension R K)
+ instance : HasColimitsOfShape J (FlatExtension R K)
+ instance : HasFilteredColimitsOfSize.{u, u} (FlatExtension R K)
+ instance : HasForget₂ (FlatExtension R K) CommRingCat.{u}
+ instance : ReflectsFilteredColimits (forget CommRingCat.{u})
+ isColimitCoconeOfCoconeForget
+ isColimit_residueFieldCocone
+ isIntegral_residueField_iff
+ isLocalHom_desc
+ isLocalHom_ι
+ isLocalRing_of_isColimit
+ maximalIdeal_eq_iSup_of_isColimit
+ maximalIdeal_eq_iUnion_of_isColimit
+ minpoly_residueField_eq_map
+ nonunits_eq_iUnion_of_isColimit
+ nonunits_le_of_isColimit
+ residueFieldCocone
+ residueFieldCocone'
+ residueFieldFunctor
+ residueField_eq_iUnion_fieldRange_of_isColimit
+ residueField_exists_rep
+ residueField_map_desc_eq_isColimit_residueFieldCocone_desc
+ residueField_map_desc_eq_isColimit_residueFieldCocone_desc'
+ span_minpoly_le_ker
+ toAdjoinAlgebraic
+ toAdjoinTranscendental
+ trivial
++ adjoinAlgebraic
++ adjoinTranscendental
++ instance (x : K) (nint : ¬ IsIntegral S x) :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Algebra/CommRingCat): colimit of local ring via local hom #39075
  By Dependent Issues (🤖). Happy coding!