Theorem: Ideal.ramificationIdxIn_eq_ramificationIdx (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
⊢ ramificationIdxIn S p = ramificationIdx (algebraMap R S) p P
Tactic:
delta ramificationIdxIn
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

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

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

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

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

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