Theorem: Ideal.inertiaDegIn_eq_inertiaDeg (FltRegular/NumberTheory/GaloisPrime.lean)

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
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

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⟩
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

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]
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

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
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

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σ]
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

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
State after:
no goals