English
In a ring, -a ∈ I if and only if a ∈ I.
Русский
В кольце -a ∈ I тогда же, когда a ∈ I.
LaTeX
$$$\forall a:\alpha, \; -a \in I \iff a \in I.$$$
Lean4
/-- If for every prime of `S`, the map `Spec Sₚ → Spec Rₚ` is surjective,
the algebra satisfies going down. -/
theorem of_specComap_localRingHom_surjective
(H :
∀ (P : Ideal S) [P.IsPrime],
Function.Surjective (Localization.localRingHom (P.under R) P (algebraMap R S) rfl).specComap) :
Algebra.HasGoingDown R S where
exists_ideal_le_liesOver_of_lt {p} _ Q _
hlt := by
let pl : Ideal (Localization.AtPrime <| Q.under R) := p.map (algebraMap R _)
have : pl.IsPrime := Ideal.isPrime_map_of_isLocalizationAtPrime (Q.under R) hlt.le
obtain ⟨⟨Pl, _⟩, hl⟩ := H Q ⟨pl, inferInstance⟩
refine ⟨Pl.under S, ?_, Ideal.IsPrime.under S Pl, ⟨?_⟩⟩
· exact (IsLocalization.AtPrime.orderIsoOfPrime _ Q ⟨Pl, inferInstance⟩).2.2
· replace hl : Pl.under _ = pl := by simpa using hl
rw [Ideal.under_under, ← Ideal.under_under (B := (Localization.AtPrime <| Q.under R)) Pl, hl,
Ideal.under_map_of_isLocalizationAtPrime (Q.under R) hlt.le]
