Theorem: prod_primesOverFinset_pow_ramificationIdxIn (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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ (∏ P ∈ primesOverFinset S p, P) ^ Ideal.ramificationIdxIn S p = Ideal.map (algebraMap R S) p
Tactic:
classical
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 _ _)
delta Finset.prod
simp only [Multiset.toFinset_val, Multiset.map_id', ← Multiset.prod_nsmul,
  ramificationIdxIn_smul_primesOverFinset K L, ← associated_iff_eq]
apply factors_prod
rwa [Ne, Ideal.zero_eq_bot, Ideal.map_eq_bot_iff_of_injective hRS]
State after:
no goals

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ (∏ P ∈ primesOverFinset S p, P) ^ Ideal.ramificationIdxIn S p = Ideal.map (algebraMap R S) p
Tactic:
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 _ _)
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ (∏ P ∈ primesOverFinset S p, P) ^ Ideal.ramificationIdxIn S p = Ideal.map (algebraMap R S) 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ (∏ P ∈ primesOverFinset S p, P) ^ Ideal.ramificationIdxIn S p = Ideal.map (algebraMap R S) p
Tactic:
delta Finset.prod
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ (Multiset.map (fun P => P) (primesOverFinset S p).val).prod ^ Ideal.ramificationIdxIn S p =
    Ideal.map (algebraMap R S) 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ (Multiset.map (fun P => P) (primesOverFinset S p).val).prod ^ Ideal.ramificationIdxIn S p =
    Ideal.map (algebraMap R S) p
Tactic:
simp only [Multiset.toFinset_val, Multiset.map_id', ← Multiset.prod_nsmul,
  ramificationIdxIn_smul_primesOverFinset K L, ← associated_iff_eq]
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Associated (factors (Ideal.map (algebraMap R S) p)).prod (Ideal.map (algebraMap R S) 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Associated (factors (Ideal.map (algebraMap R S) p)).prod (Ideal.map (algebraMap R S) p)
Tactic:
apply factors_prod
State after:
case ane0
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.map (algebraMap R S) p ≠ 0

State before:
case ane0
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.map (algebraMap R S) p ≠ 0
Tactic:
rwa [Ne, Ideal.zero_eq_bot, Ideal.map_eq_bot_iff_of_injective hRS]
State after:
no goals

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
State after:
no goals