KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map
theorem KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
{I : Ideal R} [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
[inst_6 : NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥)
(hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x),
UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I) =
Multiset.map
(fun f => ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
(UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach
The **Kummer-Dedekind Theorem** states that, given a commutative ring `R`, a commutative ring `S` over `R`, an element `x` of `S`, and a maximal ideal `I` of `R` that is not the zero ideal, under the conditions that `R` is an integral domain, `R` is integrally closed, `S` is a Dedekind domain, and there are no zero divisors from `R` to `S`, if the preimage of the conductor of `R` under the embedding of `R` into `S` union `I` equals the whole ring `R` and `x` is integral over `R`, then the multiset of normalized factors of the ideal `I` under the embedding of `R` into `S` is the same as the multiset obtained by mapping each factor in the multiset of normalized factors of the minimal polynomial of `x` over the quotient ring `R/I` under a certain equivalence between factors, attached with its occurrence index.
More concisely: Given an integral domain `R` that is integrally closed, a Dedekind domain `S` with no zero divisors from `R` to `S`, an element `x` integral over `R` in `S`, and a maximal ideal `I` of `R` such that `R` maps densely into `S/I` and `R` has conductor equal to `R` under this embedding, then the normalized factorization of `I` in `S` is equivalent to the normalized factorization of the minimal polynomial of `x` in `R/I`.
|
comap_map_eq_map_adjoin_of_coprime_conductor
theorem comap_map_eq_map_adjoin_of_coprime_conductor :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
{I : Ideal R},
Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S) →
Ideal.comap (algebraMap (↥(Algebra.adjoin R {x})) S) (Ideal.map (algebraMap R S) I) =
Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I
This theorem states that for any commutative ring `R`, commutative ring `S`, ring homomorphism given by the algebra structure from `R` to `S`, element `x` from `S`, and ideal `I` of `R`, if the join of the preimage of the conductor of `R` under the ring homomorphism and the ideal `I` is the complete lattice, and the ring homomorphism from the minimal subalgebra that includes `x` to `S` is injective, then the preimage of the span of the image of the ideal `I` under the ring homomorphism is equal to the span of the image of the ideal `I` under the ring homomorphism from `R` to the minimal subalgebra that includes `x`. In other words, the theorem provides a technical result about the relationship between the preimage of an ideal under a ring homomorphism and the image of the ideal under a different ring homomorphism in the context of algebras and conductors.
More concisely: If `R` and `S` are commutative rings, `f : R → S` is a ring homomorphism, `x ∈ S`, `I ⊆ R` is an ideal, the preimage of the conductor of `R` under `f` and `I` form a complete lattice, and the restriction of `f` to the minimal subalgebra containing `x` is injective, then the preimage of the ideal `I` under `f` equals the span of the image of `I` under `f` restricted to the minimal subalgebra containing `x`.
|
KummerDedekind.multiplicity_factors_map_eq_multiplicity
theorem KummerDedekind.multiplicity_factors_map_eq_multiplicity :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
{I : Ideal R} [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
[inst_6 : NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥)
(hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) {J : Ideal S}
(hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)),
multiplicity J (Ideal.map (algebraMap R S) I) =
multiplicity (↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
(Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
The theorem `KummerDedekind.multiplicity_factors_map_eq_multiplicity` is the second part of the Kummer-Dedekind Theorem in the case of monogenic extension. It states that for any Commutative Rings `R` and `S` with `S` being a Dedekind domain, an algebra structure between them, and given an integral element `x` of `S` over `R`, a maximal ideal `I` of `R` different from zero ideal, and an ideal `J` in the normalized factors of the image of `I` under the algebra map, the multiplicity of `J` in this image is the same as the multiplicity of the corresponding factor in the polynomial map of the minimal polynomial of `x` over the quotient ring `R/I`. This theorem essentially asserts that the bijection `FactorsEquiv'` defined in the first part of the Kummer-Dedekind Theorem preserves multiplicities.
More concisely: For a monogenic extension of commutative rings R and S with S a Dedekind domain, the multiplicity of an ideal J in the image of a maximal ideal I under the algebra map equals the multiplicity of the corresponding factor in the minimal polynomial of an integral element x over R/I.
|
prod_mem_ideal_map_of_mem_conductor
theorem prod_mem_ideal_map_of_mem_conductor :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
{I : Ideal R} {p : R} {z : S},
p ∈ Ideal.comap (algebraMap R S) (conductor R x) →
z ∈ Ideal.map (algebraMap R S) I →
(algebraMap R S) p * z ∈
⇑(algebraMap (↥(Algebra.adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)
This theorem asserts that in the context of commutative rings `R` and `S` with an algebra structure on `S` over `R`, given an element `x` from `S`, an ideal `I` of `R`, and an element `p` from `R` that lies in the intersection of `C` (the conductor of `R`) and `R`, if `z` is in the ideal generated by the image of `I` under the algebra map from `R` to `S`, then the product of `p` (under the same algebra map) and `z` is contained in the image of the ideal generated by `I` under the algebra map from `R` to the subalgebra generated by `R` and `x` in `S`. This result is a technical lemma relating ideals and conductors in the context of ring extensions and the associated algebra structures.
More concisely: Given commutative rings `R` and `S` with `S` an algebra over `R`, if `x` is an element of `S`, `I` is an ideal of `R`, `p` is an element of `R` in the intersection of the conductor of `R` and `R`, and `z` is in the image of `I` under the algebra map from `R` to `S`, then `p * z` is in the image of `I` under the algebra map from `R` to the subalgebra of `S` generated by `R` and `x`.
|