feat(RingTheory): adds lemmas/instances related to integral maps to a field and residue fields (leanprover-community#36790)

This PR adds some lemmas and instances related to integral maps to a field and residue fields.

Author: BryceT233

Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

@@ -632,6 +632,14 @@ theorem Algebra.IsIntegral.isField_iff_isField [IsDomain S]
     (hRS : Function.Injective (algebraMap R S)) : IsField R ↔ IsField S :=
   ⟨isField_of_isIntegral_of_isField', isField_of_isIntegral_of_isField hRS⟩
 
+variable (R)
+theorem Algebra.ker_algebraMap_isMaximal_of_isIntegral (k : Type*) [Field k] [Algebra R k]
+    [Algebra.IsIntegral R k] : (RingHom.ker (algebraMap R k)).IsMaximal := by
+  have := Ideal.bot_isMaximal (K := k)
+  rw [RingHom.ker, Ideal.Quotient.maximal_ideal_iff_isField_quotient]
+  exact isField_of_isIntegral_of_isField Ideal.algebraMap_quotient_injective
+    (Ideal.Quotient.field _).toIsField
+
 end Algebra
 
 theorem integralClosure_idem {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] :

Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean

@@ -7,6 +7,9 @@ module
 
 public import Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 public import Mathlib.FieldTheory.Separable
+public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
+
+import Mathlib.RingTheory.Finiteness.Quotient
 
 /-! # Instances on residue fields -/
 
@@ -66,3 +69,22 @@ instance [p.IsPrime] [q.IsPrime] [Algebra.IsIntegral A B] :
     obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
     simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]
   refine .extendScalars (Ideal.injective_algebraMap_quotient_residueField p)
+
+namespace IsLocalRing
+
+variable {R k : Type*} [CommRing R] [IsLocalRing R] [Field k] [Algebra R k]
+
+instance ResidueField.algebraOfIsIntegral [Algebra.IsIntegral R k] : Algebra (ResidueField R) k :=
+  (Ideal.Quotient.lift (maximalIdeal R) (algebraMap R k)
+    (by simp [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k)])).toAlgebra
+
+instance ResidueField.isScalarTowerOfIsIntegral [Algebra.IsIntegral R k] :
+    IsScalarTower R (ResidueField R) k :=
+  .of_algebraMap_eq fun _ ↦ rfl
+
+instance [Module.Finite R k] : Module.Finite (ResidueField R) k := .of_equiv_equiv
+  (Ideal.quotEquivOfEq (show Ideal.comap (algebraMap R k) ⊥ = maximalIdeal R by
+    rw [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k), RingHom.ker]))
+  (RingEquiv.quotientBot k) (by ext; rfl)
+
+end IsLocalRing