Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_RingTheory_AffineDilatation.lean

definition module

Affine dilatation algebras inside

For a commutative ring A, an ideal I \subseteq A and an element a \in A, this module constructs the affine dilatation (affine blow-up) algebra A[I/a] as a subalgebra of the localisation away from a. The generating set AffineDilatation.gen I a is the image of I under the map g \mapsto g/a into Localization.Away a, where the denominator is a itself regarded as an element of the submonoid of powers of a; AffineDilatation.mem_gen_iff records that membership in it means exactly being of the form g/a for some g \in I. Then AffineDilatation.subalgebra I a is the A-subalgebra of Localization.Away a generated by this set, i.e. Algebra.adjoin A (gen I a), so that concretely it is the subring A[g/a : g \in I] \subseteq A[1/a]; AffineDilatation.Ring I a is an abbreviation for the corresponding type, the coercion of that subalgebra, which thereby carries its A-algebra structure.

The remaining declarations give the elementary interface. For g \in I, AffineDilatation.divElem I a g hg is the element of Ring I a given by the fraction g/a together with its membership proof, and AffineDilatation.coe_divElem, AffineDilatation.divElem_mem identify its image in Localization.Away a with g/a and place that image in the generating set. AffineDilatation.coe_algebraMap says that the structure map A \to A[I/a] is, after inclusion, the localisation map A \to A[1/a], and AffineDilatation.algebraMap_mul_divElem records the defining relation a \cdot (g/a) = g inside A[I/a] for every g \in I. Two further lemmas state that the subalgebra is by definition the adjoin of the generating set and that the generating set is contained in it. No hypotheses are imposed on A, I or a beyond A being a commutative ring; in particular a need not lie in I, and finiteness or flatness properties are not part of the definition.

Relation to Mathlib

Mathlib has localisations away from an element and Algebra.adjoin, but no notion of affine blow-up or dilatation algebra; this is the project's own definition, packaged as a Subalgebra A (Localization.Away a).

Where it is used

These definitions are the affine-local input to the theory of dilatations (Néron blow-ups) developed in the modules importing them, where the basic properties of A[I/a] — the behaviour of a as a nonzerodivisor, the universal property, finite type and flatness over a discrete valuation ring — are established and used in the study of integral models.

References

  1. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 21, Springer, 1990, §3.2
  2. A. Mayeux, T. Richarz and M. Romagny, Néron blowups and low-degree cohomological applications, Algebraic Geometry 10 (2023), §2

References are suggested automatically and have not been individually verified.

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

Source file: Definitions/Def_RingTheory_AffineDilatation.lean

Declarations

Source

import Mathlib

set_option autoImplicit false

noncomputable section

universe u

namespace AffineDilatation

variable {A : Type u} [CommRing A]

def gen (I : Ideal A) (a : A) : Set (Localization.Away a) :=
  (fun g : A => IsLocalization.mk' (Localization.Away a) g
    (⟨a, Submonoid.mem_powers a⟩ : Submonoid.powers a)) '' (I : Set A)

def subalgebra (I : Ideal A) (a : A) : Subalgebra A (Localization.Away a) :=
  Algebra.adjoin A (gen I a)

abbrev Ring (I : Ideal A) (a : A) : Type u :=
  ↥(subalgebra I a)

def divElem (I : Ideal A) (a : A) (g : A) (hg : g ∈ I) : Ring I a :=
  ⟨IsLocalization.mk' (Localization.Away a) g (⟨a, Submonoid.mem_powers a⟩ : Submonoid.powers a),
    Algebra.subset_adjoin ⟨g, hg, rfl⟩⟩

@[simp]
theorem coe_divElem (I : Ideal A) (a : A) (g : A) (hg : g ∈ I) :
    ((divElem I a g hg : Ring I a) : Localization.Away a) =
      IsLocalization.mk' (Localization.Away a) g
        (⟨a, Submonoid.mem_powers a⟩ : Submonoid.powers a) :=
  rfl

theorem coe_algebraMap (I : Ideal A) (a : A) (g : A) :
    ((algebraMap A (Ring I a) g : Ring I a) : Localization.Away a) =
      algebraMap A (Localization.Away a) g :=
  rfl

theorem algebraMap_mul_divElem (I : Ideal A) (a : A) (g : A) (hg : g ∈ I) :
    algebraMap A (Ring I a) a * divElem I a g hg = algebraMap A (Ring I a) g := by
  apply Subtype.ext
  change algebraMap A (Localization.Away a) a *
      IsLocalization.mk' (Localization.Away a) g
        (⟨a, Submonoid.mem_powers a⟩ : Submonoid.powers a) =
    algebraMap A (Localization.Away a) g
  rw [mul_comm]
  exact IsLocalization.mk'_spec (Localization.Away a) g
    (⟨a, Submonoid.mem_powers a⟩ : Submonoid.powers a)

theorem mem_gen_iff (I : Ideal A) (a : A) (x : Localization.Away a) :
    x ∈ gen I a ↔ ∃ g ∈ I, IsLocalization.mk' (Localization.Away a) g
      (⟨a, Submonoid.mem_powers a⟩ : Submonoid.powers a) = x :=
  Iff.rfl

theorem subalgebra_eq_adjoin (I : Ideal A) (a : A) :
    subalgebra I a = Algebra.adjoin A (gen I a) :=
  rfl

theorem gen_subset (I : Ideal A) (a : A) :
    gen I a ⊆ (subalgebra I a : Set (Localization.Away a)) :=
  Algebra.subset_adjoin

theorem divElem_mem (I : Ideal A) (a : A) (g : A) (hg : g ∈ I) :
    ((divElem I a g hg : Ring I a) : Localization.Away a) ∈ gen I a :=
  ⟨g, hg, rfl⟩

end AffineDilatation

end

Statements phrased using this module (12)