internlm/Lean-Github huggingface dataset:
Theorem: Ideal.inertiaDegIn_bot
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : IsDedekindDomain R
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra S L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra R L
inst✝⁸ : IsScalarTower R S L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : IsIntegralClosure S R L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Nontrivial R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsNoetherian R S
inst✝ : Algebra.IsIntegral R S
H : ⊥.IsMaximal
this✝² : {⊥}.Nonempty
hR : IsField R
hS : IsField S
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S
Tactic:
rw [← Ideal.map_bot (f := algebraMap R S), ← finrank_quotient_map (R := R) (S := S) ⊥ R S]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : IsDedekindDomain R
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra S L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra R L
inst✝⁸ : IsScalarTower R S L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : IsIntegralClosure S R L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Nontrivial R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsNoetherian R S
inst✝ : Algebra.IsIntegral R S
H : ⊥.IsMaximal
this✝² : {⊥}.Nonempty
hR : IsField R
hS : IsField S
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ (map (algebraMap R S) ⊥) =
    FiniteDimensional.finrank (R ⧸ ⊥) (S ⧸ map (algebraMap R S) ⊥)
Theorem: Ideal.inertiaDegIn_bot
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : IsDedekindDomain R
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra S L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra R L
inst✝⁸ : IsScalarTower R S L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : IsIntegralClosure S R L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Nontrivial R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsNoetherian R S
inst✝ : Algebra.IsIntegral R S
H : ⊥.IsMaximal
this✝² : {⊥}.Nonempty
hR : IsField R
hS : IsField S
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ (map (algebraMap R S) ⊥) =
    FiniteDimensional.finrank (R ⧸ ⊥) (S ⧸ map (algebraMap R S) ⊥)
Tactic:
exact inertiaDeg_algebraMap _ _
Proof state after:
no goals
Theorem: Ideal.inertiaDegIn_bot
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : IsDedekindDomain R
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra S L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra R L
inst✝⁸ : IsScalarTower R S L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : IsIntegralClosure S R L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Nontrivial R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsNoetherian R S
inst✝ : Algebra.IsIntegral R S
H : ⊥.IsMaximal
⊢ {⊥}.Nonempty
Tactic:
simp
Proof state after:
no goals
Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
⊢ ramificationIdxIn S p = ramificationIdx (algebraMap R S) p P
Tactic:
delta ramificationIdxIn
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
⊢ (if h : (primesOver S p).Nonempty then ramificationIdx (algebraMap R S) p (Exists.choose h) else 0) =
    ramificationIdx (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
⊢ (if h : (primesOver S p).Nonempty then ramificationIdx (algebraMap R S) p (Exists.choose h) else 0) =
    ramificationIdx (algebraMap R S) p P
Tactic:
have : (primesOver S p).Nonempty := ⟨P, hP⟩
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
⊢ (if h : (primesOver S p).Nonempty then ramificationIdx (algebraMap R S) p (Exists.choose h) else 0) =
    ramificationIdx (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
⊢ (if h : (primesOver S p).Nonempty then ramificationIdx (algebraMap R S) p (Exists.choose h) else 0) =
    ramificationIdx (algebraMap R S) p P
Tactic:
rw [dif_pos this]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
⊢ ramificationIdx (algebraMap R S) p (Exists.choose this) = ramificationIdx (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
⊢ ramificationIdx (algebraMap R S) p (Exists.choose this) = ramificationIdx (algebraMap R S) p P
Tactic:
have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S hP this.choose_spec
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ ramificationIdx (algebraMap R S) p (Exists.choose this) = ramificationIdx (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ ramificationIdx (algebraMap R S) p (Exists.choose this) = ramificationIdx (algebraMap R S) p P
Tactic:
rw [← hσ]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ ramificationIdx (algebraMap R S) p (comap ((galRestrict R K L S) σ) P) = ramificationIdx (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ ramificationIdx (algebraMap R S) p (comap ((galRestrict R K L S) σ) P) = ramificationIdx (algebraMap R S) p P
Tactic:
exact Ideal.ramificationIdx_comap_eq (galRestrict R K L S σ) p P
Proof state after:
no goals
Theorem: Ideal.inertiaDegIn_eq_inertiaDeg
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
⊢ inertiaDegIn S p = inertiaDeg (algebraMap R S) p P
Tactic:
delta inertiaDegIn
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
⊢ (if h : (primesOver S p).Nonempty then inertiaDeg (algebraMap R S) p (Exists.choose h) else 0) =
    inertiaDeg (algebraMap R S) p P
Theorem: Ideal.inertiaDegIn_eq_inertiaDeg
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
⊢ (if h : (primesOver S p).Nonempty then inertiaDeg (algebraMap R S) p (Exists.choose h) else 0) =
    inertiaDeg (algebraMap R S) p P
Tactic:
have : (primesOver S p).Nonempty := ⟨P, hP⟩
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
⊢ (if h : (primesOver S p).Nonempty then inertiaDeg (algebraMap R S) p (Exists.choose h) else 0) =
    inertiaDeg (algebraMap R S) p P
Theorem: Ideal.inertiaDegIn_eq_inertiaDeg
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
⊢ (if h : (primesOver S p).Nonempty then inertiaDeg (algebraMap R S) p (Exists.choose h) else 0) =
    inertiaDeg (algebraMap R S) p P
Tactic:
rw [dif_pos this]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
⊢ inertiaDeg (algebraMap R S) p (Exists.choose this) = inertiaDeg (algebraMap R S) p P
Theorem: Ideal.inertiaDegIn_eq_inertiaDeg
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
⊢ inertiaDeg (algebraMap R S) p (Exists.choose this) = inertiaDeg (algebraMap R S) p P
Tactic:
have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S hP this.choose_spec
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ inertiaDeg (algebraMap R S) p (Exists.choose this) = inertiaDeg (algebraMap R S) p P
Theorem: Ideal.inertiaDegIn_eq_inertiaDeg
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ inertiaDeg (algebraMap R S) p (Exists.choose this) = inertiaDeg (algebraMap R S) p P
Tactic:
rw [← hσ]
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ inertiaDeg (algebraMap R S) p (comap ((galRestrict R K L S) σ) P) = inertiaDeg (algebraMap R S) p P
Theorem: Ideal.inertiaDegIn_eq_inertiaDeg
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
P : Ideal S
hP : P ∈ primesOver S p
inst✝ : p.IsMaximal
this : (primesOver S p).Nonempty
σ : L ≃ₐ[K] L
hσ : comap ((galRestrict R K L S) σ) P = Exists.choose this
⊢ inertiaDeg (algebraMap R S) p (comap ((galRestrict R K L S) σ) P) = inertiaDeg (algebraMap R S) p P
Tactic:
exact Ideal.inertiaDeg_comap_eq (galRestrict R K L S σ) p P
Proof state after:
no goals
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_primesOver
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
classical
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
have := IsIntegralClosure.isDedekindDomain R K L S
have := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
have := IsIntegralClosure.isNoetherian R K L S
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hRS
rw [← Ideal.sum_ramification_inertia (S := S) p K L hp, ← coe_primesOverFinset S p hp,
  Set.ncard_coe_Finset, mul_comm, ← smul_eq_mul, ← Finset.sum_const]
apply Finset.sum_congr rfl
simp_rw [← Finset.mem_coe, coe_primesOverFinset S p hp]
intro P hP
rw [Ideal.ramificationIdxIn_eq_ramificationIdx K L p P hP,
  Ideal.inertiaDegIn_eq_inertiaDeg K L p P hP]
Proof state after:
no goals
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_primesOver
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this : IsDomain S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_primesOver
Proof state before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this : IsDomain S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
have := IsIntegralClosure.isDedekindDomain R K L S
Proof state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L