Localization.AtPrime.map_eq_maximalIdeal
theorem Localization.AtPrime.map_eq_maximalIdeal :
∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime],
Ideal.map (algebraMap R (Localization.AtPrime I)) I = LocalRing.maximalIdeal (Localization I.primeCompl)
The theorem `Localization.AtPrime.map_eq_maximalIdeal` states that for any commutative semiring `R` and any prime ideal `I` of `R`, the image of `I` under the localization map at the complement of `I` is a maximal ideal. Moreover, this maximal ideal is unique and corresponds to the maximal ideal produced by the local ring structure induced by the localization at the complement of `I`.
More concisely: For any commutative semiring R and prime ideal I, the image of I under the localization map at the complement of I is a unique maximal ideal equal to the maximal ideal of the local ring at I.
|
IsLocalization.AtPrime.to_map_mem_maximal_iff
theorem IsLocalization.AtPrime.to_map_mem_maximal_iff :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
(I : Ideal R) [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (x : R) (h : optParam (LocalRing S) ⋯),
(algebraMap R S) x ∈ LocalRing.maximalIdeal S ↔ x ∈ I
This theorem states that for any commutative semiring `R`, given a type `S` that is also a commutative semiring and an 'algebra' over `R`, and given a prime ideal `I` of `R`, if `S` is isomorphic to the localization of `R` at the complement of `I`, then for any element `x` of `R`, and assuming `S` is a local ring, the image of `x` under the algebra homomorphism from `R` to `S` is in the maximal ideal of `S` if and only if `x` is in the prime ideal `I`.
The use of "optParam" allows for an optional parameter to be supplied for the type `LocalRing S`, and a default parameter is used if none is supplied. The "algebraMap" function maps elements from `R` to `S` according to the given algebra structure. The "LocalRing.maximalIdeal" refers to the ideal of `S` consisting of non-unit elements.
More concisely: Given a commutative semiring `R`, a commutative semiring `S` isomorphic to the localization of `R` at the complement of a prime ideal `I`, and an algebra homomorphism from `R` to `S`, an element `x` in `R` maps to a non-unit element in `S` if and only if `x` is in `I`.
|
Ideal.primeCompl_le_nonZeroDivisors
theorem Ideal.primeCompl_le_nonZeroDivisors :
∀ {R : Type u_1} [inst : CommSemiring R] (P : Ideal R) [hp : P.IsPrime] [inst_1 : NoZeroDivisors R],
P.primeCompl ≤ nonZeroDivisors R
This theorem states that for any commutative semiring `R`, if `P` is a prime ideal within `R` and `R` does not contain any zero divisors (i.e., `R` is an integral domain), then the complement of the prime ideal `P` is a subset of the set of non-zero divisors of `R`. In simple terms, if we remove the elements of the prime ideal `P` from the semiring `R`, all remaining elements will not be zero divisors.
More concisely: If `R` is a commutative semiring with no zero divisors and `P` is a prime ideal in `R`, then the complement of `P` in `R` is contained in the set of non-zero divisors of `R`.
|
Localization.AtPrime.comap_maximalIdeal
theorem Localization.AtPrime.comap_maximalIdeal :
∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime],
Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization I.primeCompl)) = I
The theorem `Localization.AtPrime.comap_maximalIdeal` states that for any commutative semiring `R` and any prime ideal `I` in `R`, the unique maximal ideal of the localization of `R` at the complement of `I` (`Localization.AtPrime I`), when mapped back to `R` via the comap function with respect to the ring homomorphism given by the algebra structure (`algebraMap`), equals the original prime ideal `I`. In other words, the localization process doesn't change the prime ideal when we consider its image in the localized ring and pull it back to the original ring.
More concisely: The unique maximal ideal of a commutative semiring localized at the complement of a prime ideal maps back to the original prime ideal under the algebra homomorphism.
|
Localization.localRingHom.proof_4
theorem Localization.localRingHom.proof_4 :
∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_2} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
(J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P),
I = Ideal.comap f J → I.primeCompl ≤ Submonoid.comap f J.primeCompl
This theorem states that for any commutative semirings `R` and `P`, a prime ideal `I` of `R`, a prime ideal `J` of `P`, and a ring homomorphism `f` from `R` to `P`, if `I` is the preimage of `J` under `f`, then the complement of `I` is a submonoid of the preimage of the complement of `J` under `f`. In other words, if we map `I` to `J` using `f`, then the elements of `R` not in `I` are mapped to the elements of `P` not in `J`.
More concisely: If `f` is a ring homomorphism from a commutative semiring `R` to another commutative semiring `P`, `I` is a prime ideal of `R`, `J` is a prime ideal of `P`, and `I = f^(-1)(J)`, then `f(R \ I) ⊆ P \ J`.
|
Localization.localRingHom_to_map
theorem Localization.localRingHom_to_map :
∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
(J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R),
(Localization.localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) =
(algebraMap P (Localization.AtPrime J)) (f x)
This theorem states that for any commutative semiring `R`, another commutative semiring `P`, a prime ideal `I` of `R`, and a prime ideal `J` of `P`, if there is a ring homomorphism `f` from `R` to `P` such that `I` is the preimage of `J` under `f`, then for any element `x` of `R`, the image of `x` under the ring homomorphism induced by the localization of `R` at `I` to the localization of `P` at `J` (denoted `Localization.localRingHom I J f hIJ`) followed by the embedding of `R` into the localization of `R` at `I` (denoted `algebraMap R (Localization.AtPrime I)`) is equal to the image of the image of `x` under `f` under the embedding of `P` into the localization of `P` at `J` (denoted `algebraMap P (Localization.AtPrime J)`). In mathematical notation, this means that if $f: R \rightarrow P$ is a ring homomorphism and $I$ is the preimage of a prime ideal $J$ in $P$ under $f$, then for any $x \in R$ we have
$$(\text{Localization.localRingHom } I J f hIJ) \circ (\text{algebraMap } R \rightarrow \text{Localization.AtPrime } I) (x) = (\text{algebraMap } P \rightarrow \text{Localization.AtPrime } J) \circ f(x)$$
More concisely: For any commutative semirings `R` and `P`, prime ideals `I` of `R` and `J` of `P`, and a ring homomorphism `f` from `R` to `P` with `I` the preimage of `J` under `f`, the images of any element `x` in `R` under the respective local ring homomorphisms and embeddings are equal: `(Localization.localRingHom I J f hIJ) (algebraMap R (Localization.AtPrime I) x) = algebraMap P (Localization.AtPrime J) (f x)`.
|