Ideal.finrank_quotient_map
theorem Ideal.finrank_quotient_map :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (p : Ideal R) [inst_2 : Algebra R S]
(K : Type u_1) [inst_3 : Field K] [inst_4 : Algebra R K] [hRK : IsFractionRing R K] (L : Type u_2)
[inst_5 : Field L] [inst_6 : Algebra S L] [inst_7 : IsFractionRing S L] [inst_8 : IsDomain S]
[inst_9 : IsDedekindDomain R] [inst_10 : Algebra K L] [inst_11 : Algebra R L] [inst_12 : IsScalarTower R K L]
[inst_13 : IsScalarTower R S L] [inst_14 : IsIntegralClosure S R L] [hp : p.IsMaximal]
[inst_15 : IsNoetherian R S],
FiniteDimensional.finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = FiniteDimensional.finrank K L
This theorem states that if `p` is a maximal ideal in a commutative ring `R`, and `S` is the integral closure of `R` in a field `L`, then the dimension of the quotient `S/pS` over `R/p` (denoted as `[S/pS : R/p]`) is equal to the field extension degree `[Frac(S) : Frac(R)]`. Here, `Frac(R)` and `Frac(S)` denote the field of fractions of `R` and `S` respectively. The theorem utilizes a number of properties about `R` and `S`, including being a Dedekind domain and Noetherian, as well as the notion of integral closure, scalar towers, and fraction fields.
More concisely: The dimension of the quotient of the integral closure of a Dedekind domain `R` in a field `L` modulo its integral closure's maximal ideal equals the degree of the field extension of the fraction fields of `R` and `S`.
|
Ideal.finrank_prime_pow_ramificationIdx
theorem Ideal.finrank_prime_pow_ramificationIdx :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (f : R →+* S) (p : Ideal R) (P : Ideal S)
[inst_2 : IsDedekindDomain S],
P ≠ ⊥ →
∀ [inst_3 : p.IsMaximal] [inst_4 : P.IsPrime] (he : Ideal.ramificationIdx f p P ≠ 0),
FiniteDimensional.finrank (R ⧸ p) (S ⧸ P ^ Ideal.ramificationIdx f p P) =
Ideal.ramificationIdx f p P * FiniteDimensional.finrank (R ⧸ p) (S ⧸ P)
This theorem states that if `p` is a maximal ideal in a commutative ring `R`, `S` is a commutative ring that extends `R`, and the ideal `P` raised to the power `e` lies over `p`, then the rank of the module `S/(P^e)` over `R/p`, expressed as a natural number, equals `e` times the rank of `S/P` over `R/p`. These ranks are obtained using the `FiniteDimensional.finrank` function. The `Ideal.ramificationIdx` function is used to get the value of `e`, the ramification index of `P` over `p`. This is all under the condition that `S` is a Dedekind domain and `P` is a prime ideal in `S`, and that `P` is not the zero ideal and the ramification index of `P` over `p` is not zero.
More concisely: If `p` is a maximal ideal in a commutative ring `R`, `S` is a Dedekind domain extending `R`, `P` is a prime ideal in `S` lying over `p`, and the ramification index of `P` over `p` is a positive non-zero integer `e`, then the rank of `S/(P^e)` over `R/p` equals `e` times the rank of `S/P` over `R/p`.
|
Ideal.sum_ramification_inertia
theorem Ideal.sum_ramification_inertia :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (p : Ideal R) [inst_2 : IsDedekindDomain S]
[inst_3 : Algebra R S] (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L]
[inst_6 : IsDedekindDomain R] [inst_7 : Algebra R K] [inst_8 : IsFractionRing R K] [inst_9 : Algebra S L]
[inst_10 : IsFractionRing S L] [inst_11 : Algebra K L] [inst_12 : Algebra R L] [inst_13 : IsScalarTower R S L]
[inst_14 : IsScalarTower R K L] [inst_15 : IsNoetherian R S] [inst_16 : IsIntegralClosure S R L]
[inst_17 : p.IsMaximal],
p ≠ ⊥ →
((UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset.sum fun P =>
Ideal.ramificationIdx (algebraMap R S) p P * Ideal.inertiaDeg (algebraMap R S) p P) =
FiniteDimensional.finrank K L
The theorem, known as the **fundamental identity** of ramification index and inertia degree, states that in a setting where `S` is a finite `R`-module and `p` is a maximal ideal in `R`, for each prime `P` lying over `p`, the sum of the product of the ramification index `e P` and the inertia degree `f P` equals the rank of the field extension `Frac(S) : Frac(R)`. This implies that the sum of the products of the ramification indices and inertia degrees for all primes lying over a given maximal ideal is an invariant of the field extension.
In more mathematical terms, it can be written as:
`∑ P, e P * f P = [Frac(S) : Frac(R)]`.
Here, `e P` is the ramification index of `P` over `p`, which is the largest exponent `n` such that `p` is contained in `P^n`. `f P` is the inertia degree of `P` over `p`. The field `Frac(S)` is the field of fractions of `S`, and `Frac(R)` is the field of fractions of `R`. The notation `[Frac(S) : Frac(R)]` represents the rank of the field extension `Frac(S)` over `Frac(R)`.
More concisely: The sum of the products of the ramification indices and inertia degrees for all primes lying over a maximal ideal equals the rank of the corresponding field extension in the ring of fractions.
|
Ideal.rank_prime_pow_ramificationIdx
theorem Ideal.rank_prime_pow_ramificationIdx :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (f : R →+* S) (p : Ideal R) (P : Ideal S)
[inst_2 : IsDedekindDomain S] [inst_3 : p.IsMaximal] [inst_4 : P.IsPrime],
P ≠ ⊥ →
∀ (he : Ideal.ramificationIdx f p P ≠ 0),
Module.rank (R ⧸ p) (S ⧸ P ^ Ideal.ramificationIdx f p P) =
Ideal.ramificationIdx f p P • Module.rank (R ⧸ p) (S ⧸ P)
The theorem `Ideal.rank_prime_pow_ramificationIdx` states that if `p` is a maximal ideal in a commutative ring `R`, `S` is a commutative ring that extends `R`, and `P^e` is an ideal in `S` that lies over `p`, then the dimension of the quotient ring `S/(P^e)` over `R/p` is equal to `e` times the dimension of the quotient ring `S/P` over `R/p`. Here, `e` is the ramification index of `P` over `p`, which is the largest exponent such that `p` is contained in `P^n`. This is under the assumption that `S` is a Dedekind domain, `p` is maximal and `P` is prime.
More concisely: If `p` is a maximal ideal in a Dedekind domain `R`, `S` is a commutative ring extending `R`, `P` is a prime ideal in `S` lying over `p`, and `e` is the ramification index of `P` over `p`, then the quotient rings `S/(P^e)` and `(R/p)^e` are isomorphic as `R/p`-modules.
|
Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial
theorem Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_1)
[inst_3 : Field K] [inst_4 : Algebra R K] [hRK : IsFractionRing R K] {V : Type u_3} {V' : Type u_4}
{V'' : Type u_5} [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : Module K V]
[inst_8 : IsScalarTower R K V] [inst_9 : AddCommGroup V'] [inst_10 : Module R V'] [inst_11 : Module S V']
[inst_12 : IsScalarTower R S V'] [inst_13 : AddCommGroup V''] [inst_14 : Module R V'']
[inst_15 : IsDedekindDomain R],
RingHom.ker (algebraMap R S) ≠ ⊤ →
∀ (f : V'' →ₗ[R] V),
Function.Injective ⇑f →
∀ (f' : V'' →ₗ[R] V') {ι : Type u_6} {b : ι → V''},
LinearIndependent S (⇑f' ∘ b) → LinearIndependent K (⇑f ∘ b)
This theorem states that: Given an integral domain `R` with its field of fractions `K`, a ring extension `S / R`, a vector space `V` over `K`, and a module `V'` over `S`, if there exists a subset `V''` that is an intersection of `V` and `V'`, and a family of vectors `b` from `V''` which is linearly independent over `S` in `V'`, then `b` is also linearly independent over `R` in `V`. The theorem holds under the condition that the inclusion function `algebraMap R S : R → S` is nontrivial and `R` is a Dedekind domain. Note that the function `f' : V'' → V'` does not necessarily need to be injective.
More concisely: Given an integral domain R with its field of fractions K, a ring extension S/R, a vector space V over K, a module V' over S, a linearly independent family of vectors b in V∩V', and a nontrivial inclusion map algebraMap R S : R → S from R into S, then b is also linearly independent in V over R.
|
Ideal.FinrankQuotientMap.span_eq_top
theorem Ideal.FinrankQuotientMap.span_eq_top :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (p : Ideal R) [inst_2 : Algebra R S]
{K : Type u_1} [inst_3 : Field K] [inst_4 : Algebra R K] {L : Type u_2} [inst_5 : Field L] [inst_6 : Algebra S L]
[inst_7 : IsFractionRing S L] [inst_8 : IsDomain R] [inst_9 : IsDomain S] [inst_10 : Algebra K L]
[inst_11 : IsNoetherian R S] [inst_12 : Algebra R L] [inst_13 : IsScalarTower R S L]
[inst_14 : IsScalarTower R K L] [inst_15 : IsIntegralClosure S R L] [inst_16 : NoZeroSMulDivisors R K],
p ≠ ⊤ →
∀ (b : Set S),
Submodule.span R b ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p) = ⊤ →
Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
The theorem `Ideal.FinrankQuotientMap.span_eq_top` states that if an ideal `p` of a commutative ring `R` is such that `R / p` is nontrivial, and a set `b` modulo `p` spans a quotient semiring `S/p` as an `R/p`-space, then `b` itself spans the field of fractions of `S` as a `K`-space, where `K` is a field that embeds `R` (we can take `K` as the field of fractions of `R`). `L` is a field extension of `K` and `S` is the integral closure of `R` in `L`. In other words, the theorem circumvents quotients by requiring that the union of `b` and `pS` spans `S`. This theorem is defined in the context of several conditions, including the assumptions that `S` is a Fraction Ring over `L`, `R` and `S` are domains, `S` is an integral closure of `R` in `L`, and there are no zero scalar multiplication divisors in `R` and `K`.
More concisely: If an ideal `p` of a domain `R` makes the quotient ring `R/p` nontrivial and a set `b` modulo `p` spans the integral closure `S` of `R` in a field extension `L`, then `b` and `pS` span the field of fractions of `S` as a `K`-vector space, where `K` is the field of fractions of `R`.
|
Ideal.rank_pow_quot_aux
theorem Ideal.rank_pow_quot_aux :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (f : R →+* S) (p : Ideal R) (P : Ideal S)
[hfp : NeZero (Ideal.ramificationIdx f p P)] [inst_2 : IsDedekindDomain S] [inst_3 : p.IsMaximal]
[inst_4 : P.IsPrime],
P ≠ ⊥ →
∀ {i : ℕ},
i < Ideal.ramificationIdx f p P →
Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (P ^ i)) =
Module.rank (R ⧸ p) (S ⧸ P) +
Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (P ^ (i + 1)))
The theorem `Ideal.rank_pow_quot_aux` states that in the context of a commutative ring `R`, a commutative ring `S`, a ring homomorphism `f` from `R` to `S`, an ideal `p` of `R`, an ideal `P` of `S`, and a non-zero ramification index of `P` over `p`, under the conditions that `S` is a Dedekind domain, `p` is maximal, `P` is prime, and `P` is not the zero ideal, for any natural number `i` that is less than the ramification index of `P` over `p`, the rank of the `R/p`-module `(P^i / P^e)` is equal to the rank of the `R/p`-module `(P^(i+1) / P^e)` plus the rank of the `R/p`-module `P / S`, where `e` denotes the ramification index of `P` over `p`. In simpler terms, it states that the dimension of the quotient space `(P^i / P^e)` in the quotient ring `R / p` is the sum of the dimensions of the quotient spaces `(P^(i+1) / P^e)` and `P / S` in the same quotient ring.
More concisely: For a commutative ring homomorphism from a maximal, prime ideal of a Dedekind domain to a ring with non-zero ramification index, the rank of the quotient module of the power ideal in the source ring modulo the ideal and its power in the target ring, both divided by the ramified ideal, sum up to the rank of the quotient module of the power ideal and the ideal in the source ring.
|
Ideal.le_pow_ramificationIdx
theorem Ideal.le_pow_ramificationIdx :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S},
Ideal.map f p ≤ P ^ Ideal.ramificationIdx f p P
This theorem states that, for any commutative rings `R` and `S`, and any ring homomorphism `f` from `R` to `S`, and any ideals `p` in `R` and `P` in `S`, the ideal obtained by mapping the ideal `p` under `f` (denoted by `Ideal.map f p`) is a subset of the `P` raised to the power of the ramification index of `P` over `p` (denoted by `P ^ Ideal.ramificationIdx f p P`). The ramification index in this case is the largest exponent `n` such that `p` is contained in `P^n`. If there is no such `n` (because `p` is not contained in any power of `P`), then the ramification index is defined to be 0.
More concisely: For any commutative rings R and S, ring homomorphism f from R to S, and ideals p in R and P in S, Ideal.map f p is contained in P ^ Ideal.ramificationIdx f p P.
|
Ideal.ramificationIdx_spec
theorem Ideal.ramificationIdx_spec :
∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S}
{n : ℕ}, Ideal.map f p ≤ P ^ n → ¬Ideal.map f p ≤ P ^ (n + 1) → Ideal.ramificationIdx f p P = n
The theorem `Ideal.ramificationIdx_spec` states that for any given commutative rings `R` and `S`, a ring homomorphism `f` from `R` to `S`, ideals `p` of `R` and `P` of `S`, and a natural number `n`, if the image of the ideal `p` under the map `f` is contained in the `n`-th power of `P` and is not contained in the `(n+1)`-th power of `P`, then the ramification index of `P` over `p` under the map `f` is `n`. Here, the ramification index is the highest power `n` such that `P^n` contains the image of `p` under `f`.
More concisely: If a ring homomorphism maps an ideal to a power of another ideal and not to a higher power, then the ramification index of the second ideal over the first is equal to the power.
|