LocalizationMaps.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Maps between coefficient localizations and maximal ideals over primes

The localization map uses the actual contraction of the target prime ideal. Its denominator condition follows from the definition of contraction; no integrality is needed for this map. Integrality is used separately to prove maximality of contractions and existence of maximal ideals over rational primes.

def OAI.CirculantHadamard.localizationAtComapMap line 27

Source documentation

The actual map from the localization at a contracted prime ideal.

noncomputable def localizationAtComapMap (f : A →+* B) (m : Ideal B) [m.IsPrime] :
    Localization.AtPrime (m.comap f) →+* Localization.AtPrime m :=
…

theorem OAI.CirculantHadamard.localizationAtComapMap_algebraMap line 32

Source documentation

The induced map agrees with the original ring map on coefficients.

@[simp] theorem localizationAtComapMap_algebraMap (f : A →+* B)
    (m : Ideal B) [m.IsPrime] (a : A) :
    localizationAtComapMap f m (algebraMap A (Localization.AtPrime (m.comap f)) a) =
      algebraMap B (Localization.AtPrime m) (f a) :=
…

Mentions: OAI.CirculantHadamard.localizationAtComapMap

theorem OAI.CirculantHadamard.localizationAtComapMap_mk' line 39

Source documentation

Both numerator and denominator follow the coefficient inclusion.

theorem localizationAtComapMap_mk' (f : A →+* B) (m : Ideal B) [m.IsPrime]
    (a : A) (s : (m.comap f).primeCompl) :
    localizationAtComapMap f m (IsLocalization.mk' (Localization.AtPrime (m.comap f)) a s) =
      IsLocalization.mk' (Localization.AtPrime m) (f a)
        (⟨f s, s.2⟩ : m.primeCompl) :=
…

Mentions: OAI.CirculantHadamard.localizationAtComapMap

theorem OAI.CirculantHadamard.localizationAtComapMap_injective line 48
Source documentation
An inclusion into a domain remains injective after the two prime localizations, even though the target inverts additional denominators.
```
theorem localizationAtComapMap_injective [IsDomain B] (f : A →+* B)
    (hf : Function.Injective f) (m : Ideal B) [m.IsPrime] :
    Function.Injective (localizationAtComapMap f m) := by
…
```
Mentions: OAI.CirculantHadamard.localizationAtComapMap
theorem OAI.CirculantHadamard.localizationAtComapMap_isUnit line 64
Source documentation
Units used by the local comparison remain units in the larger coefficient localization.
```
theorem localizationAtComapMap_isUnit (f : A →+* B) (m : Ideal B) [m.IsPrime]
    {x : Localization.AtPrime (m.comap f)} (hx : IsUnit x) :
    IsUnit (localizationAtComapMap f m x) :=
…
```
Mentions: OAI.CirculantHadamard.localizationAtComapMap
theorem OAI.CirculantHadamard.maximal_comap_of_integral line 70
Source documentation
Integral coefficient extensions preserve maximality on contraction.
```
theorem maximal_comap_of_integral (f : A →+* B) (hf : f.IsIntegral)
    (m : Ideal B) [m.IsMaximal] : (m.comap f).IsMaximal :=
…
```

theorem OAI.CirculantHadamard.exists_maximal_ideal_over_nat_prime line 79

Source documentation

Every rational prime has a maximal ideal above it in an integral integer algebra with injective integer map. The conclusion retains the exact contraction as well as membership of the prime in the maximal ideal.

theorem exists_maximal_ideal_over_nat_prime (B : Type uB) [CommRing B]
    [Algebra ℤ B] [Algebra.IsIntegral ℤ B]
    (hB : Function.Injective (algebraMap ℤ B)) {p : ℕ} (hp : p.Prime) :
    ∃ m : Ideal B, m.IsMaximal ∧
      m.comap (algebraMap ℤ B) = Ideal.span ({(p : ℤ)} : Set ℤ) ∧ (p : B) ∈ m := by
…

theorem OAI.CirculantHadamard.exists_maximal_ideal_over_nat_prime_of_charZero line 101

Source documentation

Characteristic zero supplies the injective integer map automatically.

theorem exists_maximal_ideal_over_nat_prime_of_charZero (B : Type uB) [CommRing B]
    [CharZero B] [Algebra ℤ B] [Algebra.IsIntegral ℤ B] {p : ℕ} (hp : p.Prime) :
    ∃ m : Ideal B, m.IsMaximal ∧
      m.comap (algebraMap ℤ B) = Ideal.span ({(p : ℤ)} : Set ℤ) ∧ (p : B) ∈ m :=
…