Theorem: Ideal.spanIntNorm_map
Proof state before:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : IsIntegrallyClosed R
inst✝¹⁰ : IsDomain R
inst✝⁹ : IsDomain S
inst✝⁸ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
I : Ideal R
⊢ spanIntNorm R (map (algebraMap R S) I) = I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S)
Tactic:
classical
nontriviality R
nontriviality S
refine eq_of_localization_maximal ?_
intro P hPd
let P' := Algebra.algebraMapSubmonoid S P.primeCompl
let Rₚ := Localization.AtPrime P
let Sₚ := Localization P'
letI : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
haveI : IsScalarTower R Rₚ Sₚ :=
  IsScalarTower.of_algebraMap_eq (fun x =>
    (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
have h : P' ≤ S⁰ :=
  map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _)
    P.primeCompl_le_nonZeroDivisors
haveI : IsDomain Sₚ := IsLocalization.isDomain_localization h
haveI : IsDedekindDomain Sₚ := IsLocalization.isDedekindDomain S h _
haveI : IsPrincipalIdealRing Rₚ := IsLocalization.AtPrime.PID_of_dedekind_domain P Rₚ
haveI := isIntegrallyClosed_of_isLocalization P.primeCompl P.primeCompl_le_nonZeroDivisors Rₚ
haveI := NoZeroSMulDivisors_of_isLocalization R S Rₚ Sₚ _ P.primeCompl_le_nonZeroDivisors
haveI := Module.Finite_of_isLocalization R S Rₚ Sₚ P.primeCompl
let K := FractionRing R
let f : Rₚ →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) P.primeCompl_le_nonZeroDivisors
letI := f.toAlgebra
have : IsScalarTower R Rₚ K := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ K
let L := FractionRing S
let g : Sₚ →+* L := IsLocalization.map _ (M := P') (T := S⁰) (RingHom.id S) h
letI := g.toAlgebra
haveI : IsScalarTower S Sₚ (FractionRing S) := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHom.comp_id])
letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
  P' Sₚ (FractionRing S)
letI := ((algebraMap K L).comp f).toAlgebra
haveI : IsScalarTower Rₚ K L := IsScalarTower.of_algebraMap_eq' rfl
haveI : IsScalarTower Rₚ Sₚ L := by
  apply IsScalarTower.of_algebraMap_eq'
  apply IsLocalization.ringHom_ext P.primeCompl
  rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₚ), RingHom.comp_assoc,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₚ,
    IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
    RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
haveI : IsIntegralClosure Sₚ Rₚ L := IsIntegralClosure.of_isIntegrallyClosed _ _ _
haveI : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
  apply IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv
    (FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv
  apply IsLocalization.ringHom_ext R⁰
  ext
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp,
    RingHom.coe_coe, Function.comp_apply, ← IsScalarTower.algebraMap_apply]
  simp only [IsScalarTower.algebraMap_apply R Rₚ (FractionRing R), AlgEquiv.coe_ringEquiv,
    AlgEquiv.commutes, IsScalarTower.algebraMap_apply R S L,
    IsScalarTower.algebraMap_apply S Sₚ L]
  simp only [← IsScalarTower.algebraMap_apply]
  rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing Rₚ), ← IsScalarTower.algebraMap_apply Rₚ,
    ← IsScalarTower.algebraMap_apply]
haveI : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (S := S)
  (Rₘ := Localization.AtPrime P) (Sₘ := Localization P') _ _ P.primeCompl_le_nonZeroDivisors]
rw [Ideal.map_pow, I.map_map, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R Rₚ Sₚ,
  ← I.map_map, ← (I.map _).span_singleton_generator, Ideal.map_span, Set.image_singleton,
  spanIntNorm_singleton, Ideal.span_singleton_pow]
congr 2
apply IsFractionRing.injective Rₚ K
rw [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
  IsScalarTower.algebraMap_apply Rₚ K L, Algebra.norm_algebraMap, map_pow]
Proof state after:
no goals