LocalizationIntersection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The two-localization intersection used in the rigidity argument

This module supplies the denominator-clearing step in Section 5 of the source: for relatively prime elements a and d in a unique factorization domain, the localizations away from a and d intersect in the original ring inside its fraction field. Relative primeness here means that every common divisor is a unit; it does not incorrectly assume that the ideal (a,d) is the unit ideal.

theorem OAI.StableCoordinate.exists_algebraMap_eq_of_two_power_denominators line 28

Source documentation

Clearing two relatively prime power denominators forces an element of an overring into the original ring. The overring need not be a field.

theorem exists_algebraMap_eq_of_two_power_denominators
    (hinj : Function.Injective (algebraMap A K))
    {a d : A} (ha : a ≠ 0) (had : IsRelPrime a d)
    {z : K} {m n : ℕ} {r s : A}
    (hr : z * algebraMap A K (a ^ m) = algebraMap A K r)
    (hs : z * algebraMap A K (d ^ n) = algebraMap A K s) :
    ∃ t : A, algebraMap A K t = z := by
…

theorem OAI.StableCoordinate.powers_le_nonZeroDivisors line 56
Source documentation
Powers of a nonzero element are legitimate fraction-field denominators.
```
theorem powers_le_nonZeroDivisors {a : A} (ha : a ≠ 0) :
    Submonoid.powers a ≤ nonZeroDivisors A := by
…
```
def OAI.StableCoordinate.awayInFractionField line 62
Source documentation
The localization A[a⁻¹], realized as an actual subalgebra of a fraction field.
```
noncomputable def awayInFractionField (a : A) (ha : a ≠ 0) : Subalgebra A K :=
…
```
theorem OAI.StableCoordinate.mem_awayInFractionField_iff line 67
Source documentation
Membership in a one-element localization can be expressed by clearing a power denominator.
```
theorem mem_awayInFractionField_iff (a : A) (ha : a ≠ 0) (z : K) :
    z ∈ awayInFractionField K a ha ↔
      ∃ (n : ℕ) (r : A), z * algebraMap A K (a ^ n) = algebraMap A K r := by
…
```
Mentions: OAI.StableCoordinate.awayInFractionField
theorem OAI.StableCoordinate.awayInFractionField_inf_eq_bot line 88
Source documentation
The two principal localizations at relatively prime elements intersect in the base ring, as subalgebras of its fraction field.
```
theorem awayInFractionField_inf_eq_bot {a d : A} (ha : a ≠ 0) (hd : d ≠ 0)
    (had : IsRelPrime a d) :
    awayInFractionField K a ha ⊓ awayInFractionField K d hd = ⊥ := by
…
```
Mentions: OAI.StableCoordinate.awayInFractionField
theorem OAI.StableCoordinate.isRelPrime_X_of_ne line 107
Source documentation
Distinct independent polynomial variables are relatively prime in the common-divisor sense required by the intersection argument.
```
theorem isRelPrime_X_of_ne {i j : σ} (hij : i ≠ j) :
    IsRelPrime (MvPolynomial.X i : MvPolynomial σ k) (MvPolynomial.X j) := by
…
```

theorem OAI.StableCoordinate.polynomial_variable_localizations_inf_eq_bot line 114

Source documentation

Specialization of the two-chart intersection result to distinct variables of a polynomial ring over a field.

theorem polynomial_variable_localizations_inf_eq_bot
    (K : Type*) [Field K] [Algebra (MvPolynomial σ k) K]
    [IsFractionRing (MvPolynomial σ k) K] {i j : σ} (hij : i ≠ j) :
    awayInFractionField K (MvPolynomial.X i : MvPolynomial σ k) (MvPolynomial.X_ne_zero i) ⊓
      awayInFractionField K (MvPolynomial.X j : MvPolynomial σ k) (MvPolynomial.X_ne_zero j) = ⊥ := by
…

Mentions: OAI.StableCoordinate.awayInFractionField