LocalizationIntersection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Recovering a global coefficient from its local representations

The denominator-ideal argument works in any commutative algebra. It identifies the intersection of maximal localizations inside a fraction field with the base ring, both as subalgebra membership and through actual local elements.

theorem OAI.CirculantHadamard.exists_base_of_local_denominators line 20

Source documentation

If every maximal ideal admits a denominator outside it taking z into the base ring's image, then z itself lies in that image.

theorem exists_base_of_local_denominators
    {R : Type uR} {K : Type uK} [CommRing R] [CommRing K] [Algebra R K]
    (z : K)
    (hz : ∀ m : MaximalSpectrum R, ∃ a s : R,
      s ∉ m.asIdeal ∧ algebraMap R K s * z = algebraMap R K a) :
    ∃ r : R, algebraMap R K r = z := by
…

theorem OAI.CirculantHadamard.exists_base_of_mem_all_maximal_localizations line 48

Source documentation

Membership in every maximal localization, realized inside a common fraction field, gives a base-ring representative.

theorem exists_base_of_mem_all_maximal_localizations
    {z : K}
    (hz : ∀ m : MaximalSpectrum R,
      z ∈ Localization.subalgebra.ofField K m.asIdeal.primeCompl
        m.asIdeal.primeCompl_le_nonZeroDivisors) :
    ∃ r : R, algebraMap R K r = z := by
…

theorem OAI.CirculantHadamard.exists_base_of_localization_images line 63

Source documentation

A fraction-field element represented by an actual element of each maximal local ring is the image of a base-ring element.

theorem exists_base_of_localization_images
    {z : K}
    (hz : ∀ m : MaximalSpectrum R, ∃ y : Localization.AtPrime m.asIdeal,
      Localization.mapToFractionRing K m.asIdeal.primeCompl
        (Localization.AtPrime m.asIdeal)
        m.asIdeal.primeCompl_le_nonZeroDivisors y = z) :
    ∃ r : R, algebraMap R K r = z := by
…