`Definitions/Def_Deformations_IsResidueAlgebra.lean`

definition moduleadapted from the Imperial College London FLT project: FLT/Deformations/IsResidueAlgebra.lean

The class `IsResidueAlgebra` of local algebras

Fix a commutative ring \mathcal O and a local \mathcal O-algebra A, and write \mathfrak k(A) for IsLocalRing.ResidueField A, i.e. A/\mathfrak m_A. The class IsResidueAlgebra 𝓞 A is a one-field proposition: its field isSurjective' asserts that the structure map \mathcal O \to \mathfrak k(A), that is \mathcal O \to A \to A/\mathfrak m_A, is surjective; algebraMap_surjective restates this field. Under the further assumptions that \mathcal O is itself local and that \mathcal O \to A is a local homomorphism, algebraMap_bijective states that the induced map of residue fields \mathfrak k(\mathcal O) \to \mathfrak k(A) is bijective — injectivity because it is a homomorphism of fields, surjectivity because it is surjective after precomposition with the surjection \mathcal O \to \mathfrak k(\mathcal O) — and algEquiv packages it as an isomorphism \mathfrak k(\mathcal O) \simeq \mathfrak k(A) of \mathcal O-algebras.

Three closure properties are registered. A local ring \mathcal O is a residue algebra over itself. For an ideal I \subseteq A with A/I nontrivial, A/I (local, as a surjective image of A) is again a residue algebra over \mathcal O. If B is a local \mathcal O-algebra that is a residue algebra over \mathcal O, and B is an A-algebra compatibly with the \mathcal O-actions, then of_restrictScalars gives that B is a residue algebra over A.

Finally, approximate lifting of elements: exists_sub_mem_maximalIdeal says that for every r \in A there is a \in \mathcal O with r - a \cdot 1 \in \mathfrak m_A; preimage chooses such an a, with preimage_spec and residue_preimage recording the congruence and the resulting equality of residues, and residue_preimage_eq_iff characterising, for \mathcal O local and \mathcal O \to A local, the residue of preimage 𝓞 r in \mathfrak k(\mathcal O) in terms of the residue of r and the map \mathfrak k(\mathcal O) \to \mathfrak k(A).

Relation to Mathlib

Mathlib has no class expressing that a local algebra has residue field generated by the base ring; IsResidueAlgebra is the project's own, stated in terms of Mathlib's IsLocalRing.ResidueField. The surjectivity of IsLocalRing.ResidueField.map along a surjective local homomorphism, used for the quotient instance, is supplied by an imported project module.

Where it is used

This is the residue-field condition imposed on the coefficient rings in Mazur's deformation theory: the objects over which deformation functors of a residual representation \bar\rho with values in \mathfrak k are defined are local \mathcal O-algebras whose residue field is identified with that of \mathcal O. The quotient and restriction-of-scalars instances, and the choice of representatives preimage, are the basic bookkeeping used when working with such algebras and their Artinian quotients.

References

B. Mazur, Deforming Galois representations, in: Galois Groups over \mathbb{Q}, MSRI Publications 16, Springer, 1989, 385–437
M. Schlessinger, Functors of Artin rings, Transactions of the American Mathematical Society 130 (1968), 208–222
B. de Smit and H. W. Lenstra, Jr., Explicit construction of universal deformation rings, in: Modular Forms and Fermat's Last Theorem, Springer, 1997, 313–326

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

90 lines
13 declarations
used in the statements of 0 theorems and imported by 0 proofs
imports 2 definition modules

Source file: Definitions/Def_Deformations_IsResidueAlgebra.lean

Imports

Imported by

Def_Deformations_ProartinianCat

Declarations

classIsResidueAlgebra
fieldIsResidueAlgebra.isSurjective'
lemmaIsResidueAlgebra.algebraMap_surjective
lemmaIsResidueAlgebra.algebraMap_bijective
defIsResidueAlgebra.algEquiv
lemmaIsResidueAlgebra.of_restrictScalars
lemmaIsResidueAlgebra.exists_sub_mem_maximalIdeal
defIsResidueAlgebra.preimage
lemmaIsResidueAlgebra.preimage_spec
lemmaIsResidueAlgebra.residue_preimage
lemmaIsResidueAlgebra.residue_preimage_eq_iff

Source

import Mathlib
import Definitions.Def_Mathlib_RingTheory_LocalRing_Defs
import Definitions.Def_Deformations_Deformations_Lemmas

set_option autoImplicit false

open Function IsLocalRing

variable (𝓞 : Type*) [CommRing 𝓞]

local notation3:max "𝓴" 𝓞:max => (IsLocalRing.ResidueField 𝓞)

variable (A : Type*) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A]

class IsResidueAlgebra : Prop where
  isSurjective' : Surjective (algebraMap 𝓞 (𝓴 A))

namespace IsResidueAlgebra

variable [IsResidueAlgebra 𝓞 A]

lemma algebraMap_surjective : Surjective (algebraMap 𝓞 (𝓴 A)) := isSurjective'

variable [IsLocalRing 𝓞] [IsLocalHom (algebraMap 𝓞 A)] in
lemma algebraMap_bijective : Bijective (algebraMap (𝓴 𝓞) (𝓴 A)) := by
  have hsurj1 := IsLocalRing.residue_surjective (R := 𝓞)
  have hsurj2 := IsResidueAlgebra.algebraMap_surjective 𝓞 A
  exact ⟨(algebraMap (𝓴 𝓞) (𝓴 A)).injective,
    (Function.Surjective.of_comp_iff (algebraMap (𝓴 𝓞) (𝓴 A)) hsurj1).mp hsurj2⟩

variable [IsLocalRing 𝓞] [IsLocalHom (algebraMap 𝓞 A)] in

noncomputable def algEquiv : 𝓴 𝓞 ≃ₐ[𝓞] 𝓴 A :=
  .ofBijective (IsScalarTower.toAlgHom _ _ _) (algebraMap_bijective _ _)

instance [IsLocalRing 𝓞] : IsResidueAlgebra 𝓞 𝓞 := ⟨IsLocalRing.residue_surjective⟩

section Quotient

instance (I : Ideal A) [Nontrivial (A ⧸ I)] : IsResidueAlgebra 𝓞 (A ⧸ I) where
  isSurjective' :=
    have : IsLocalHom (Ideal.Quotient.mk I) := .of_surjective _ Ideal.Quotient.mk_surjective
    (IsLocalRing.ResidueField.map_surjective _ Ideal.Quotient.mk_surjective).comp
      (IsResidueAlgebra.algebraMap_surjective 𝓞 A)

end Quotient

section Relative

variable {𝓞 A}
variable {B : Type*} [CommRing B] [Algebra 𝓞 B] [IsLocalRing B] [IsResidueAlgebra 𝓞 B]

omit [IsLocalRing A] [IsResidueAlgebra 𝓞 A] in
lemma of_restrictScalars [Algebra A B] [IsScalarTower 𝓞 A B] : IsResidueAlgebra A B where
  isSurjective' := by
    refine .of_comp (g := algebraMap 𝓞 A) ?_
    rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]
    exact IsResidueAlgebra.algebraMap_surjective _ _

end Relative

open IsLocalRing

variable {A}

lemma exists_sub_mem_maximalIdeal (r : A) : ∃ a, r - algebraMap 𝓞 A a ∈ maximalIdeal _ := by
  obtain ⟨a, ha⟩ := IsResidueAlgebra.algebraMap_surjective 𝓞 _ (residue _ r)
  refine ⟨a, ?_⟩
  rw [← Ideal.Quotient.eq]
  exact ha.symm

noncomputable
def preimage (r : A) : 𝓞 := (exists_sub_mem_maximalIdeal 𝓞 r).choose

lemma preimage_spec (r : A) : r - algebraMap 𝓞 A (preimage 𝓞 r) ∈ maximalIdeal _ :=
  (exists_sub_mem_maximalIdeal 𝓞 r).choose_spec

lemma residue_preimage (r : A) : residue _ (algebraMap _ _ (preimage 𝓞 r)) = residue _ r :=
  (Ideal.Quotient.eq.mpr (preimage_spec 𝓞 r)).symm

variable [IsLocalRing 𝓞] [IsLocalHom (algebraMap 𝓞 A)] in
lemma residue_preimage_eq_iff {r : A} {a} :
    residue _ (preimage 𝓞 r) = a ↔ residue _ r = ResidueField.map (algebraMap 𝓞 A) a := by
  rw [← (IsResidueAlgebra.algebraMap_bijective 𝓞 A).1.eq_iff]
  erw [ResidueField.map_residue]
  rw [residue_preimage]
  rfl

end IsResidueAlgebra

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).