From 08fc3ef93ade1a2f86a83420bdcff910893a78bf Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 22 May 2026 17:26:14 +0100 Subject: [PATCH 1/2] add --- .../LocalRing/ResidueField/Basic.lean | 62 +++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean index 92801ec958611a..70c260c8160e9b 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean +++ b/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean @@ -113,6 +113,7 @@ theorem map_comp_residue (f : R →+* S) [IsLocalHom f] : (ResidueField.map f).comp (residue R) = (residue S).comp f := rfl +@[simp] theorem map_residue (f : R →+* S) [IsLocalHom f] (r : R) : ResidueField.map f (residue R r) = residue S (f r) := rfl @@ -206,6 +207,67 @@ lemma finite_of_finite [Module.Finite R S] (hfin : Finite (ResidueField R)) : end FiniteDimensional +omit [IsLocalRing R] + +variable [Algebra R S] [Algebra R T] + +/-- A local algebra homomorphism induces an algebra homomorphism on the residue fields. + +See `mapAlgHom'` for a variant where the base ring `R` is also quotiented. -/ +noncomputable def mapAlgHom (e : S →ₐ[R] T) [IsLocalHom e] : + ResidueField S →ₐ[R] ResidueField T where + __ := map e + commutes' x := by + simp [IsScalarTower.algebraMap_apply R S (ResidueField S), + IsScalarTower.algebraMap_apply R T (ResidueField T)] + +@[simp] +theorem mapAlgHom_residue (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : + mapAlgHom e (residue S x) = residue T (e x) := + rfl + +/-- A local algebra isomorphism induces an algebra isomorphism on the residue fields. + +See `mapAlgEquiv'` for a variant where the base ring `R` is also quotiented. -/ +noncomputable def mapAlgEquiv (e : S ≃ₐ[R] T) : ResidueField S ≃ₐ[R] ResidueField T where + __ := + -- todo: add better conversion between different spellings of the function in an `IsLocalHom` + haveI : IsLocalHom e.toRingEquiv := inferInstance + haveI : IsLocalHom (e : S →ₐ[R] T) := ⟨this.map_nonunit⟩ + mapAlgHom e.toAlgHom + __ := mapEquiv e.toRingEquiv + +@[simp] +theorem mapAlgEquiv_residue (e : S ≃ₐ[R] T) (x : S) : + mapAlgEquiv e (residue S x) = residue T (e x) := + rfl + +variable [IsLocalRing R] [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] + +/-- A local algebra homomorphism induces an algebra homomorphism on the residue fields. + +See `mapAlgHom` for a variant where the base ring `R` is not quotiented. -/ +noncomputable def mapAlgHom' (e : S →ₐ[R] T) [IsLocalHom e] : + ResidueField S →ₐ[ResidueField R] ResidueField T := + (mapAlgHom e).extendScalarsOfSurjective residue_surjective + +@[simp] +theorem mapAlgHom'_residue (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : + mapAlgHom' e (residue S x) = residue T (e x) := + rfl + +/-- A local algebra isomorphism induces an algebra isomorphism on the residue fields. + +See `mapAlgEquiv` for a variant where the base ring `R` is not quotiented. -/ +noncomputable def mapAlgEquiv' (e : S ≃ₐ[R] T) : + ResidueField S ≃ₐ[ResidueField R] ResidueField T := + (mapAlgEquiv e).extendScalarsOfSurjective residue_surjective + +@[simp] +theorem mapAlgEquiv'_residue (e : S ≃ₐ[R] T) (x : S) : + mapAlgEquiv' e (residue S x) = residue T (e x) := + rfl + end ResidueField end From 671cfefae1410ca04f8a58ebc8de9826e2b50942 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 28 May 2026 07:42:14 -0700 Subject: [PATCH 2/2] review --- Mathlib/Algebra/Algebra/Equiv.lean | 5 +++++ Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean | 12 ++++-------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean index e079099d6851dc..ade3aa884f2184 100644 --- a/Mathlib/Algebra/Algebra/Equiv.lean +++ b/Mathlib/Algebra/Algebra/Equiv.lean @@ -763,6 +763,11 @@ def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] : instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂) := Finite.of_injective _ AlgEquiv.coe_algHom_injective +-- TODO Morally this is just `isLocalHom_equiv`: can we obviate the need for this instance? +instance : IsLocalHom e.toAlgHom := by + have : IsLocalHom e.toRingEquiv := inferInstance + exact ⟨this.map_nonunit⟩ + end Semiring end AlgEquiv diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean index 70c260c8160e9b..25ccf5295ce240 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean +++ b/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean @@ -230,11 +230,7 @@ theorem mapAlgHom_residue (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : See `mapAlgEquiv'` for a variant where the base ring `R` is also quotiented. -/ noncomputable def mapAlgEquiv (e : S ≃ₐ[R] T) : ResidueField S ≃ₐ[R] ResidueField T where - __ := - -- todo: add better conversion between different spellings of the function in an `IsLocalHom` - haveI : IsLocalHom e.toRingEquiv := inferInstance - haveI : IsLocalHom (e : S →ₐ[R] T) := ⟨this.map_nonunit⟩ - mapAlgHom e.toAlgHom + __ := mapAlgHom e.toAlgHom __ := mapEquiv e.toRingEquiv @[simp] @@ -242,7 +238,7 @@ theorem mapAlgEquiv_residue (e : S ≃ₐ[R] T) (x : S) : mapAlgEquiv e (residue S x) = residue T (e x) := rfl -variable [IsLocalRing R] [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] +variable [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] /-- A local algebra homomorphism induces an algebra homomorphism on the residue fields. @@ -252,7 +248,7 @@ noncomputable def mapAlgHom' (e : S →ₐ[R] T) [IsLocalHom e] : (mapAlgHom e).extendScalarsOfSurjective residue_surjective @[simp] -theorem mapAlgHom'_residue (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : +theorem mapAlgHom'_residue [IsLocalRing R] (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : mapAlgHom' e (residue S x) = residue T (e x) := rfl @@ -264,7 +260,7 @@ noncomputable def mapAlgEquiv' (e : S ≃ₐ[R] T) : (mapAlgEquiv e).extendScalarsOfSurjective residue_surjective @[simp] -theorem mapAlgEquiv'_residue (e : S ≃ₐ[R] T) (x : S) : +theorem mapAlgEquiv'_residue [IsLocalRing R] (e : S ≃ₐ[R] T) (x : S) : mapAlgEquiv' e (residue S x) = residue T (e x) := rfl