[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
h : Fintype (M ⧸ S)
⊢ cardQuot S = Fintype.card (M ⧸ S)
[PROOFSTEP]
suffices Fintype (M ⧸ S.toAddSubgroup) by convert AddSubgroup.index_eq_card S.toAddSubgroup
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
h : Fintype (M ⧸ S)
this : Fintype (M ⧸ toAddSubgroup S)
⊢ cardQuot S = Fintype.card (M ⧸ S)
[PROOFSTEP]
convert AddSubgroup.index_eq_card S.toAddSubgroup
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
h : Fintype (M ⧸ S)
⊢ Fintype (M ⧸ toAddSubgroup S)
[PROOFSTEP]
convert h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
P : Submodule R M
⊢ toAddSubgroup P = ⊤ ↔ P = ⊤
[PROOFSTEP]
simp [SetLike.ext_iff]
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
let b := Module.Free.chooseBasis ℤ S
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
cases isEmpty_or_nonempty (Module.Free.ChooseBasisIndex ℤ S)
[GOAL]
case inl
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
haveI : Subsingleton S := Function.Surjective.subsingleton b.repr.toEquiv.symm.surjective
[GOAL]
case inl
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
this : Subsingleton S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
nontriviality S
[GOAL]
case inl
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
this : Subsingleton S
inst✝ : Nontrivial S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
this : Subsingleton S
inst✝ : Nontrivial S
⊢ False
[PROOFSTEP]
exact not_nontrivial_iff_subsingleton.mpr ‹Subsingleton S› ‹Nontrivial S›
[GOAL]
case inr
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
haveI : Infinite S := Infinite.of_surjective _ b.repr.toEquiv.surjective
[GOAL]
case inr
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
by_cases hI : I = ⊥
[GOAL]
case pos
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
hI : I = ⊥
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
rw [hI, Submodule.bot_mul, cardQuot_bot, zero_mul]
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
hI : ¬I = ⊥
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
by_cases hJ : J = ⊥
[GOAL]
case pos
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
hI : ¬I = ⊥
hJ : J = ⊥
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
rw [hJ, Submodule.mul_bot, cardQuot_bot, mul_zero]
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
hI : ¬I = ⊥
hJ : ¬J = ⊥
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
have hIJ : I * J ≠ ⊥ := mt Ideal.mul_eq_bot.mp (not_or_of_not hI hJ)
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
hI : ¬I = ⊥
hJ : ¬J = ⊥
hIJ : I * J ≠ ⊥
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
letI := Classical.decEq (Module.Free.ChooseBasisIndex ℤ S)
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this✝ : Infinite S
hI : ¬I = ⊥
hJ : ¬J = ⊥
hIJ : I * J ≠ ⊥
this : DecidableEq (Module.Free.ChooseBasisIndex ℤ S) := Classical.decEq (Module.Free.ChooseBasisIndex ℤ S)
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
letI := I.fintypeQuotientOfFreeOfNeBot hI
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this✝¹ : Infinite S
hI : ¬I = ⊥
hJ : ¬J = ⊥
hIJ : I * J ≠ ⊥
this✝ : DecidableEq (Module.Free.ChooseBasisIndex ℤ S) := Classical.decEq (Module.Free.ChooseBasisIndex ℤ S)
this : Fintype (S ⧸ I) := Ideal.fintypeQuotientOfFreeOfNeBot I hI
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
letI := J.fintypeQuotientOfFreeOfNeBot hJ
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this✝² : Infinite S
hI : ¬I = ⊥
hJ : ¬J = ⊥
hIJ : I * J ≠ ⊥
this✝¹ : DecidableEq (Module.Free.ChooseBasisIndex ℤ S) := Classical.decEq (Module.Free.ChooseBasisIndex ℤ S)
this✝ : Fintype (S ⧸ I) := Ideal.fintypeQuotientOfFreeOfNeBot I hI
this : Fintype (S ⧸ J) := Ideal.fintypeQuotientOfFreeOfNeBot J hJ
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
letI := (I * J).fintypeQuotientOfFreeOfNeBot hIJ
[GOAL]
case neg
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
coprime : I ⊔ J = ⊤
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this✝³ : Infinite S
hI : ¬I = ⊥
hJ : ¬J = ⊥
hIJ : I * J ≠ ⊥
this✝² : DecidableEq (Module.Free.ChooseBasisIndex ℤ S) := Classical.decEq (Module.Free.ChooseBasisIndex ℤ S)
this✝¹ : Fintype (S ⧸ I) := Ideal.fintypeQuotientOfFreeOfNeBot I hI
this✝ : Fintype (S ⧸ J) := Ideal.fintypeQuotientOfFreeOfNeBot J hJ
this : Fintype (S ⧸ I * J) := Ideal.fintypeQuotientOfFreeOfNeBot (I * J) hIJ
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
rw [cardQuot_apply, cardQuot_apply, cardQuot_apply,
  Fintype.card_eq.mpr ⟨(Ideal.quotientMulEquivQuotientProd I J coprime).toEquiv⟩, Fintype.card_prod]
[GOAL]
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)
[PROOFSTEP]
have : a * d - a * d' ∈ P ^ (i + 1) := by
  convert Ideal.mul_mem_mul a_mem h using 1 <;> simp [mul_sub, pow_succ, mul_comm]
[GOAL]
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d - a * d' ∈ P ^ (i + 1)
[PROOFSTEP]
convert Ideal.mul_mem_mul a_mem h using 1
[GOAL]
case h.e'_4
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d - a * d' = a * (d - d')
[PROOFSTEP]
simp [mul_sub, pow_succ, mul_comm]
[GOAL]
case h.e'_5
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ P ^ (i + 1) = P ^ i * P
[PROOFSTEP]
simp [mul_sub, pow_succ, mul_comm]
[GOAL]
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)
[PROOFSTEP]
convert Ideal.add_mem _ this (Ideal.sub_mem _ e_mem e'_mem) using 1
[GOAL]
case h.e'_4
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') = a * d - a * d' + (e - e')
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
c_mem : c ∈ P ^ i
⊢ ∃ d e, e ∈ P ^ (i + 1) ∧ a * d + e = c
[PROOFSTEP]
suffices eq_b : P ^ i = Ideal.span { a } ⊔ P ^ (i + 1)
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
c_mem : c ∈ P ^ i
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d e, e ∈ P ^ (i + 1) ∧ a * d + e = c
[PROOFSTEP]
rw [eq_b] at c_mem
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d e, e ∈ P ^ (i + 1) ∧ a * d + e = c
[PROOFSTEP]
simp only [mul_comm a]
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d e, e ∈ P ^ (i + 1) ∧ d * a + e = c
[PROOFSTEP]
exact Ideal.mem_span_singleton_sup.mp c_mem
[GOAL]
case eq_b
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
c_mem : c ∈ P ^ i
⊢ P ^ i = span {a} ⊔ P ^ (i + 1)
[PROOFSTEP]
refine
  (Ideal.eq_prime_pow_of_succ_lt_of_le hP (lt_of_le_of_ne le_sup_right ?_)
      (sup_le (Ideal.span_le.mpr (Set.singleton_subset_iff.mpr a_mem)) (Ideal.pow_succ_lt_pow hP i).le)).symm
[GOAL]
case eq_b
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
c_mem : c ∈ P ^ i
⊢ P ^ (i + 1) ≠ span {a} ⊔ P ^ (i + 1)
[PROOFSTEP]
contrapose! a_not_mem with this
[GOAL]
case eq_b
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a ∈ P ^ (i + 1)
[PROOFSTEP]
rw [this]
[GOAL]
case eq_b
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a ∈ span {a} ⊔ P ^ (i + 1)
[PROOFSTEP]
exact mem_sup.mpr ⟨a, mem_span_singleton_self a, 0, by simp, by simp⟩
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ 0 ∈ P ^ (i + 1)
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a + 0 = a
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P✝ : Ideal S
P_prime✝ : IsPrime P✝
hP✝ : P✝ ≠ ⊥
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
a b : S
a_not_mem : ¬a ∈ P ^ (i + 1)
ab_mem : a * b ∈ P ^ (i + 1)
⊢ b ∈ P
[PROOFSTEP]
simp only [← Ideal.span_singleton_le_iff_mem, ← Ideal.dvd_iff_le, pow_succ, ←
  Ideal.span_singleton_mul_span_singleton] at a_not_mem ab_mem ⊢
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P✝ : Ideal S
P_prime✝ : IsPrime P✝
hP✝ : P✝ ≠ ⊥
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
i : ℕ
a b : S
a_not_mem : ¬P * P ^ i ∣ span {a}
ab_mem : P * P ^ i ∣ span {a} * span {b}
⊢ P ∣ span {b}
[PROOFSTEP]
exact (prime_pow_succ_dvd_mul (Ideal.prime_of_isPrime hP P_prime) ab_mem).resolve_left a_not_mem
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a d d' e e' : S
a_not_mem : ¬a ∈ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ d - d' ∈ P
[PROOFSTEP]
have h' : a * (d - d') ∈ P ^ (i + 1) :=
  by
  convert Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
  ring
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a d d' e e' : S
a_not_mem : ¬a ∈ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ a * (d - d') ∈ P ^ (i + 1)
[PROOFSTEP]
convert Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
[GOAL]
case h.e'_4
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a d d' e e' : S
a_not_mem : ¬a ∈ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ a * (d - d') = a * d + e - (a * d' + e') + (e' - e)
[PROOFSTEP]
ring
[GOAL]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
P : Ideal S
P_prime : IsPrime P
hP : P ≠ ⊥
inst✝ : IsDedekindDomain S
i : ℕ
a d d' e e' : S
a_not_mem : ¬a ∈ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
h' : a * (d - d') ∈ P ^ (i + 1)
⊢ d - d' ∈ P
[PROOFSTEP]
exact Ideal.mem_prime_of_mul_mem_pow hP a_not_mem h'
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
i : ℕ
⊢ cardQuot (P ^ i) = cardQuot P ^ i
[PROOFSTEP]
let _ := Module.Free.chooseBasis ℤ S
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
i : ℕ
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (P ^ i) = cardQuot P ^ i
[PROOFSTEP]
classical
induction' i with i ih
· simp
letI := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i.succ) (pow_ne_zero _ hP)
letI := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (pow_ne_zero _ hP)
letI := Ideal.fintypeQuotientOfFreeOfNeBot P hP
have : P ^ (i + 1) < P ^ i := Ideal.pow_succ_lt_pow hP i
suffices hquot : map (P ^ i.succ).mkQ (P ^ i) ≃ S ⧸ P
· rw [pow_succ (cardQuot P), ← ih, cardQuot_apply (P ^ i.succ), ←
    card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le, cardQuot_apply (P ^ i), cardQuot_apply P]
  congr 1
  rw [Fintype.card_eq]
  exact ⟨hquot⟩
choose a a_mem a_not_mem using SetLike.exists_of_lt this
choose f g hg hf using fun c (hc : c ∈ P ^ i) => Ideal.exists_mul_add_mem_pow_succ hP a c a_mem a_not_mem hc
choose k hk_mem hk_eq using fun c' (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)) => Submodule.mem_map.mp hc'
refine Equiv.ofBijective (fun c' => Quotient.mk'' (f (k c' c'.prop) (hk_mem c' c'.prop))) ⟨?_, ?_⟩
· rintro ⟨c₁', hc₁'⟩ ⟨c₂', hc₂'⟩ h
  rw [Subtype.mk_eq_mk, ← hk_eq _ hc₁', ← hk_eq _ hc₂', mkQ_apply, mkQ_apply, Submodule.Quotient.eq, ←
    hf _ (hk_mem _ hc₁'), ← hf _ (hk_mem _ hc₂')]
  refine Ideal.mul_add_mem_pow_succ_inj _ _ _ _ _ _ a_mem (hg _ _) (hg _ _) ?_
  simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.eq] using h
· intro d'
  refine Quotient.inductionOn' d' fun d => ?_
  have hd' := (mem_map (f := mkQ (P ^ i.succ))).mpr ⟨a * d, Ideal.mul_mem_right d _ a_mem, rfl⟩
  refine ⟨⟨_, hd'⟩, ?_⟩
  simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.Quotient.eq, Subtype.coe_mk]
  refine Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_not_mem (hg _ (hk_mem _ hd')) (zero_mem _) ?_
  rw [hf, add_zero]
  exact (Submodule.Quotient.eq _).mp (hk_eq _ hd')
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
i : ℕ
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (P ^ i) = cardQuot P ^ i
[PROOFSTEP]
induction' i with i ih
[GOAL]
case zero
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (P ^ Nat.zero) = cardQuot P ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
⊢ cardQuot (P ^ Nat.succ i) = cardQuot P ^ Nat.succ i
[PROOFSTEP]
letI := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i.succ) (pow_ne_zero _ hP)
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
⊢ cardQuot (P ^ Nat.succ i) = cardQuot P ^ Nat.succ i
[PROOFSTEP]
letI := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (pow_ne_zero _ hP)
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝ : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
⊢ cardQuot (P ^ Nat.succ i) = cardQuot P ^ Nat.succ i
[PROOFSTEP]
letI := Ideal.fintypeQuotientOfFreeOfNeBot P hP
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝¹ : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
⊢ cardQuot (P ^ Nat.succ i) = cardQuot P ^ Nat.succ i
[PROOFSTEP]
have : P ^ (i + 1) < P ^ i := Ideal.pow_succ_lt_pow hP i
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
⊢ cardQuot (P ^ Nat.succ i) = cardQuot P ^ Nat.succ i
[PROOFSTEP]
suffices hquot : map (P ^ i.succ).mkQ (P ^ i) ≃ S ⧸ P
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
hquot : { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
⊢ cardQuot (P ^ Nat.succ i) = cardQuot P ^ Nat.succ i
[PROOFSTEP]
rw [pow_succ (cardQuot P), ← ih, cardQuot_apply (P ^ i.succ), ←
  card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le, cardQuot_apply (P ^ i), cardQuot_apply P]
[GOAL]
case succ
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
hquot : { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
⊢ Fintype.card { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } * Fintype.card (S ⧸ P ^ i) =
    Fintype.card (S ⧸ P) * Fintype.card (S ⧸ P ^ i)
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
hquot : { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
⊢ Fintype.card { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } = Fintype.card (S ⧸ P)
[PROOFSTEP]
rw [Fintype.card_eq]
[GOAL]
case succ.e_a
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
hquot : { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
⊢ Nonempty ({ x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P)
[PROOFSTEP]
exact ⟨hquot⟩
[GOAL]
case hquot
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
⊢ { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
[PROOFSTEP]
choose a a_mem a_not_mem using SetLike.exists_of_lt this
[GOAL]
case hquot
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
⊢ { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
[PROOFSTEP]
choose f g hg hf using fun c (hc : c ∈ P ^ i) => Ideal.exists_mul_add_mem_pow_succ hP a c a_mem a_not_mem hc
[GOAL]
case hquot
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
⊢ { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
[PROOFSTEP]
choose k hk_mem hk_eq using fun c' (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)) => Submodule.mem_map.mp hc'
[GOAL]
case hquot
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
⊢ { x // x ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) } ≃ S ⧸ P
[PROOFSTEP]
refine Equiv.ofBijective (fun c' => Quotient.mk'' (f (k c' c'.prop) (hk_mem c' c'.prop))) ⟨?_, ?_⟩
[GOAL]
case hquot.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
⊢ Function.Injective fun c' =>
    Quotient.mk''
      (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
        (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i))
[PROOFSTEP]
rintro ⟨c₁', hc₁'⟩ ⟨c₂', hc₂'⟩ h
[GOAL]
case hquot.refine_1.mk.mk
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
c₁' : S ⧸ P ^ Nat.succ i
hc₁' : c₁' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
c₂' : S ⧸ P ^ Nat.succ i
hc₂' : c₂' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
h :
  (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := c₁', property := hc₁' } =
    (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := c₂', property := hc₂' }
⊢ { val := c₁', property := hc₁' } = { val := c₂', property := hc₂' }
[PROOFSTEP]
rw [Subtype.mk_eq_mk, ← hk_eq _ hc₁', ← hk_eq _ hc₂', mkQ_apply, mkQ_apply, Submodule.Quotient.eq, ←
  hf _ (hk_mem _ hc₁'), ← hf _ (hk_mem _ hc₂')]
[GOAL]
case hquot.refine_1.mk.mk
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
c₁' : S ⧸ P ^ Nat.succ i
hc₁' : c₁' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
c₂' : S ⧸ P ^ Nat.succ i
hc₂' : c₂' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
h :
  (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := c₁', property := hc₁' } =
    (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := c₂', property := hc₂' }
⊢ a * f (k c₁' hc₁') (_ : k c₁' hc₁' ∈ P ^ i) + g (k c₁' hc₁') (_ : k c₁' hc₁' ∈ P ^ i) -
      (a * f (k c₂' hc₂') (_ : k c₂' hc₂' ∈ P ^ i) + g (k c₂' hc₂') (_ : k c₂' hc₂' ∈ P ^ i)) ∈
    P ^ Nat.succ i
[PROOFSTEP]
refine Ideal.mul_add_mem_pow_succ_inj _ _ _ _ _ _ a_mem (hg _ _) (hg _ _) ?_
[GOAL]
case hquot.refine_1.mk.mk
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
c₁' : S ⧸ P ^ Nat.succ i
hc₁' : c₁' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
c₂' : S ⧸ P ^ Nat.succ i
hc₂' : c₂' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
h :
  (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := c₁', property := hc₁' } =
    (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := c₂', property := hc₂' }
⊢ f (k c₁' hc₁') (_ : k c₁' hc₁' ∈ P ^ i) - f (k c₂' hc₂') (_ : k c₂' hc₂' ∈ P ^ i) ∈ P
[PROOFSTEP]
simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.eq] using h
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
⊢ Function.Surjective fun c' =>
    Quotient.mk''
      (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
        (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i))
[PROOFSTEP]
intro d'
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
⊢ ∃ a,
    (fun c' =>
          Quotient.mk''
            (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
              (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
        a =
      d'
[PROOFSTEP]
refine Quotient.inductionOn' d' fun d => ?_
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
d : S
⊢ ∃ a,
    (fun c' =>
          Quotient.mk''
            (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
              (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
        a =
      Quotient.mk'' d
[PROOFSTEP]
have hd' := (mem_map (f := mkQ (P ^ i.succ))).mpr ⟨a * d, Ideal.mul_mem_right d _ a_mem, rfl⟩
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
d : S
hd' : ↑(mkQ (P ^ Nat.succ i)) (a * d) ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
⊢ ∃ a,
    (fun c' =>
          Quotient.mk''
            (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
              (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
        a =
      Quotient.mk'' d
[PROOFSTEP]
refine ⟨⟨_, hd'⟩, ?_⟩
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
d : S
hd' : ↑(mkQ (P ^ Nat.succ i)) (a * d) ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
⊢ (fun c' =>
        Quotient.mk''
          (f (k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ : k ↑c' (_ : ↑c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈ P ^ i)))
      { val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' } =
    Quotient.mk'' d
[PROOFSTEP]
simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.Quotient.eq, Subtype.coe_mk]
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
d : S
hd' : ↑(mkQ (P ^ Nat.succ i)) (a * d) ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
⊢ f
        (k (↑(mkQ (P ^ Nat.succ i)) (a * d))
          (_ : ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' } ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
        (_ :
          k ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' }
              (_ : ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' } ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈
            P ^ i) -
      d ∈
    P
[PROOFSTEP]
refine Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_not_mem (hg _ (hk_mem _ hd')) (zero_mem _) ?_
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
d : S
hd' : ↑(mkQ (P ^ Nat.succ i)) (a * d) ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
⊢ a *
          f
            (k (↑(mkQ (P ^ Nat.succ i)) (a * d))
              (_ : ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' } ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)))
            (_ :
              k ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' }
                  (_ :
                    ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' } ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) ∈
                P ^ i) +
        g (k (↑(mkQ (P ^ Nat.succ i)) (a * d)) hd') (_ : k (↑(mkQ (P ^ Nat.succ i)) (a * d)) hd' ∈ P ^ i) -
      (a * d + 0) ∈
    P ^ (i + 1)
[PROOFSTEP]
rw [hf, add_zero]
[GOAL]
case hquot.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
P : Ideal S
P_prime : Ideal.IsPrime P
hP : P ≠ ⊥
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite ℤ S
inst✝ : Module.Free ℤ S
x✝ : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this✝² : Fintype (S ⧸ P ^ Nat.succ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ Nat.succ i) (_ : P ^ Nat.succ i ≠ 0)
this✝¹ : Fintype (S ⧸ P ^ i) := Ideal.fintypeQuotientOfFreeOfNeBot (P ^ i) (_ : P ^ i ≠ 0)
this✝ : Fintype (S ⧸ P) := Ideal.fintypeQuotientOfFreeOfNeBot P hP
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_not_mem : ¬a ∈ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ Nat.succ i) → c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ Nat.succ i) (hc' : c' ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)), ↑(mkQ (P ^ Nat.succ i)) (k c' hc') = c'
d' : S ⧸ P
d : S
hd' : ↑(mkQ (P ^ Nat.succ i)) (a * d) ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)
⊢ k (↑(mkQ (P ^ Nat.succ i)) (a * d))
        (_ : ↑{ val := ↑(mkQ (P ^ Nat.succ i)) (a * d), property := hd' } ∈ map (mkQ (P ^ Nat.succ i)) (P ^ i)) -
      a * d ∈
    P ^ (i + 1)
[PROOFSTEP]
exact (Submodule.Quotient.eq _).mp (hk_eq _ hd')
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
let b := Module.Free.chooseBasis ℤ S
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
cases isEmpty_or_nonempty (Module.Free.ChooseBasisIndex ℤ S)
[GOAL]
case inl
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
haveI : Subsingleton S := Function.Surjective.subsingleton b.repr.toEquiv.symm.surjective
[GOAL]
case inl
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
this : Subsingleton S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
nontriviality S
[GOAL]
case inl
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
this : Subsingleton S
inst✝ : Nontrivial S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty (Module.Free.ChooseBasisIndex ℤ S)
this : Subsingleton S
inst✝ : Nontrivial S
⊢ False
[PROOFSTEP]
exact not_nontrivial_iff_subsingleton.mpr ‹Subsingleton S› ‹Nontrivial S›
[GOAL]
case inr
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
haveI : Infinite S := Infinite.of_surjective _ b.repr.toEquiv.surjective
[GOAL]
case inr
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
exact
  UniqueFactorizationMonoid.multiplicative_of_coprime cardQuot I J (cardQuot_bot _ _)
    (fun {I J} hI => by simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top])
    (fun {I} i hI =>
      have : Ideal.IsPrime I := Ideal.isPrime_of_prime hI
      cardQuot_pow_of_prime hI.ne_zero)
    fun {I J} hIJ =>
    cardQuot_mul_of_coprime
      (Ideal.isUnit_iff.mp (hIJ _ (Ideal.dvd_iff_le.mpr le_sup_left) (Ideal.dvd_iff_le.mpr le_sup_right)))
[GOAL]
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I✝ J✝ : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty (Module.Free.ChooseBasisIndex ℤ S)
this : Infinite S
I J : Submodule S S
hI : IsUnit J
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
⊢ cardQuot 0 = 0
[PROOFSTEP]
rw [Ideal.zero_eq_bot, cardQuot_bot]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
⊢ ZeroHom.toFun { toFun := cardQuot, map_zero' := (_ : cardQuot 0 = 0) } 1 = 1
[PROOFSTEP]
dsimp only
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
⊢ cardQuot 1 = 1
[PROOFSTEP]
rw [Ideal.one_eq_top, cardQuot_top]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
⊢ ZeroHom.toFun { toFun := cardQuot, map_zero' := (_ : cardQuot 0 = 0) } (I * J) =
    ZeroHom.toFun { toFun := cardQuot, map_zero' := (_ : cardQuot 0 = 0) } I *
      ZeroHom.toFun { toFun := cardQuot, map_zero' := (_ : cardQuot 0 = 0) } J
[PROOFSTEP]
dsimp only
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I J : Ideal S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J
[PROOFSTEP]
rw [cardQuot_mul]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
⊢ ↑absNorm ⊥ = 0
[PROOFSTEP]
rw [← Ideal.zero_eq_bot, _root_.map_zero]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
⊢ ↑absNorm ⊤ = 1
[PROOFSTEP]
rw [← Ideal.one_eq_top, _root_.map_one]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ ↑absNorm I = 1 ↔ I = ⊤
[PROOFSTEP]
rw [absNorm_apply, cardQuot_eq_one_iff]
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
by_cases hI : I = ⊥
[GOAL]
case pos
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : I = ⊥
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
subst hI
[GOAL]
case pos
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
E : Type u_2
e : E
inst✝ : AddEquivClass E S { x // x ∈ ⊥ }
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype ⊥)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm ⊥
[PROOFSTEP]
have : (1 : S) ≠ 0 := one_ne_zero
[GOAL]
case pos
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
E : Type u_2
e : E
inst✝ : AddEquivClass E S { x // x ∈ ⊥ }
this : 1 ≠ 0
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype ⊥)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm ⊥
[PROOFSTEP]
have : (1 : S) = 0 := EquivLike.injective e (Subsingleton.elim _ _)
[GOAL]
case pos
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
E : Type u_2
e : E
inst✝ : AddEquivClass E S { x // x ∈ ⊥ }
this✝ : 1 ≠ 0
this : 1 = 0
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype ⊥)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm ⊥
[PROOFSTEP]
contradiction
[GOAL]
case neg
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let ι := Module.Free.ChooseBasisIndex ℤ S
[GOAL]
case neg
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let b := Module.Free.chooseBasis ℤ S
[GOAL]
case neg
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case neg.inl
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty ι
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
nontriviality S
[GOAL]
case neg.inl
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Infinite S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty ι
inst✝ : Nontrivial S
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
exact
  (not_nontrivial_iff_subsingleton.mpr (Function.Surjective.subsingleton b.repr.toEquiv.symm.surjective)
      (by infer_instance)).elim
[GOAL]
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Infinite S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : IsEmpty ι
inst✝ : Nontrivial S
⊢ Nontrivial S
[PROOFSTEP]
infer_instance
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
letI := Ideal.fintypeQuotientOfFreeOfNeBot I hI
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let a := I.smithCoeffs b hI
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let b' := I.ringBasis b hI
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let ab := I.selfBasis b hI
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
have ab_eq := I.selfBasis_def b hI
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let e' : S ≃ₗ[ℤ] I := b'.equiv ab (Equiv.refl _)
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let f : S →ₗ[ℤ] S := (I.subtype.restrictScalars ℤ).comp (e' : S →ₗ[ℤ] I)
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
let f_apply : ∀ x, f x = b'.equiv ab (Equiv.refl _) x := fun x => rfl
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
suffices (LinearMap.det f).natAbs = Ideal.absNorm I by
  calc
    _ = (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ (AddEquiv.toIntLinearEquiv e : S ≃ₗ[ℤ] I))).natAbs :=
      rfl
    _ = (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ _)).natAbs :=
      (Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _))
    _ = absNorm I := this
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
this : Int.natAbs (↑LinearMap.det f) = ↑absNorm I
⊢ Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) (AddMonoidHom.toIntLinearMap ↑e))) = ↑absNorm I
[PROOFSTEP]
calc
  _ = (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ (AddEquiv.toIntLinearEquiv e : S ≃ₗ[ℤ] I))).natAbs :=
    rfl
  _ = (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ _)).natAbs :=
    (Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _))
  _ = absNorm I := this
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
⊢ Int.natAbs (↑LinearMap.det f) = ↑absNorm I
[PROOFSTEP]
have ha : ∀ i, f (b' i) = a i • b' i := by intro i;
  rw [f_apply, b'.equiv_apply, Equiv.refl_apply, ab_eq]
    -- `det f` is equal to `∏ i, a i`,
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
⊢ ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
[PROOFSTEP]
intro i
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
i : Module.Free.ChooseBasisIndex ℤ S
⊢ ↑f (↑b' i) = a i • ↑b' i
[PROOFSTEP]
rw [f_apply, b'.equiv_apply, Equiv.refl_apply, ab_eq]
  -- `det f` is equal to `∏ i, a i`,
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
⊢ Int.natAbs (↑LinearMap.det f) = ↑absNorm I
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
⊢ Int.natAbs (↑LinearMap.det f) = ↑absNorm I
[PROOFSTEP]
calc
  Int.natAbs (LinearMap.det f) = Int.natAbs (LinearMap.toMatrix b' b' f).det := by rw [LinearMap.det_toMatrix]
  _ = Int.natAbs (Matrix.diagonal a).det := ?_
  _ = Int.natAbs (∏ i, a i) := by rw [Matrix.det_diagonal]
  _ = ∏ i, Int.natAbs (a i) := (map_prod Int.natAbsHom a Finset.univ)
  _ = Fintype.card (S ⧸ I) := ?_
  _ = absNorm I := (Submodule.cardQuot_apply _).symm
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
⊢ Int.natAbs (↑LinearMap.det f) = Int.natAbs (Matrix.det (↑(LinearMap.toMatrix b' b') f))
[PROOFSTEP]
rw [LinearMap.det_toMatrix]
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
⊢ Int.natAbs (Matrix.det (Matrix.diagonal a)) = Int.natAbs (∏ i : Module.Free.ChooseBasisIndex ℤ S, a i)
[PROOFSTEP]
rw [Matrix.det_diagonal]
[GOAL]
case neg.inr.calc_1
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
⊢ Int.natAbs (Matrix.det (↑(LinearMap.toMatrix b' b') f)) = Int.natAbs (Matrix.det (Matrix.diagonal a))
[PROOFSTEP]
congr 2
[GOAL]
case neg.inr.calc_1.e_m.e_M
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(LinearMap.toMatrix b' b') f = Matrix.diagonal a
[PROOFSTEP]
ext i j
[GOAL]
case neg.inr.calc_1.e_m.e_M.a.h
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
i j : Module.Free.ChooseBasisIndex ℤ S
⊢ ↑(LinearMap.toMatrix b' b') f i j = Matrix.diagonal a i j
[PROOFSTEP]
rw [LinearMap.toMatrix_apply, ha, LinearEquiv.map_smul, Basis.repr_self, Finsupp.smul_single, smul_eq_mul, mul_one]
[GOAL]
case neg.inr.calc_1.e_m.e_M.a.h
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
i j : Module.Free.ChooseBasisIndex ℤ S
⊢ ↑(Finsupp.single j (a j)) i = Matrix.diagonal a i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
i j : Module.Free.ChooseBasisIndex ℤ S
h : i = j
⊢ ↑(Finsupp.single j (a j)) i = Matrix.diagonal a i j
[PROOFSTEP]
rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
[GOAL]
case neg
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
i j : Module.Free.ChooseBasisIndex ℤ S
h : ¬i = j
⊢ ↑(Finsupp.single j (a j)) i = Matrix.diagonal a i j
[PROOFSTEP]
rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne (Ne.symm h)]
  -- Now we map everything through the linear equiv `S ≃ₗ (ι → ℤ)`,
    -- which maps `(S ⧸ I)` to `Π i, ZMod (a i).nat_abs`.
[GOAL]
case neg.inr.calc_2
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i : Module.Free.ChooseBasisIndex ℤ S, Int.natAbs (a i) = Fintype.card (S ⧸ I)
[PROOFSTEP]
haveI : ∀ i, NeZero (a i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr (Ideal.smithCoeffs_ne_zero b I hI i)⟩
[GOAL]
case neg.inr.calc_2
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝ : AddEquivClass E S { x // x ∈ I }
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝² : Fintype (S ⧸ I) := fintypeQuotientOfFreeOfNeBot I hI
this✝¹ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ { x // x ∈ I } := selfBasis b I hI
ab_eq :
  ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
e' : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e'
f_apply : ∀ (x : S), ↑f x = ↑(↑(Basis.equiv b' ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑f (↑b' i) = a i • ↑b' i
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (Int.natAbs (a i))
⊢ ∏ i : Module.Free.ChooseBasisIndex ℤ S, Int.natAbs (a i) = Fintype.card (S ⧸ I)
[PROOFSTEP]
simp_rw [Fintype.card_eq.mpr ⟨(Ideal.quotientEquivPiZMod I b hI).toEquiv⟩, Fintype.card_pi, ZMod.card]
[GOAL]
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Infinite S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ { x // x ∈ I }
⊢ Int.natAbs (↑(Basis.det b) (Subtype.val ∘ ↑bI)) = ↑absNorm I
[PROOFSTEP]
let e := b.equiv bI (Equiv.refl _)
[GOAL]
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Infinite S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ { x // x ∈ I }
e : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b bI (Equiv.refl ι)
⊢ Int.natAbs (↑(Basis.det b) (Subtype.val ∘ ↑bI)) = ↑absNorm I
[PROOFSTEP]
calc
  (b.det ((Submodule.subtype I).restrictScalars ℤ ∘ bI)).natAbs =
      (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ (e : S →ₗ[ℤ] I))).natAbs :=
    by rw [Basis.det_comp_basis]
  _ = _ := natAbs_det_equiv I e
[GOAL]
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Infinite S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ { x // x ∈ I }
e : S ≃ₗ[ℤ] { x // x ∈ I } := Basis.equiv b bI (Equiv.refl ι)
⊢ Int.natAbs (↑(Basis.det b) (↑(↑ℤ (Submodule.subtype I)) ∘ ↑bI)) =
    Int.natAbs (↑LinearMap.det (LinearMap.comp (↑ℤ (Submodule.subtype I)) ↑e))
[PROOFSTEP]
rw [Basis.det_comp_basis]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ ↑absNorm (span {r}) = Int.natAbs (↑(Algebra.norm ℤ) r)
[PROOFSTEP]
rw [Algebra.norm_apply]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ ↑absNorm (span {r}) = Int.natAbs (↑LinearMap.det (↑(Algebra.lmul ℤ S) r))
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : r = 0
⊢ ↑absNorm (span {r}) = Int.natAbs (↑LinearMap.det (↑(Algebra.lmul ℤ S) r))
[PROOFSTEP]
simp only [hr, Ideal.span_zero, Algebra.coe_lmul_eq_mul, eq_self_iff_true, Ideal.absNorm_bot, LinearMap.det_zero'',
  Set.singleton_zero, _root_.map_zero, Int.natAbs_zero]
[GOAL]
case neg
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
⊢ ↑absNorm (span {r}) = Int.natAbs (↑LinearMap.det (↑(Algebra.lmul ℤ S) r))
[PROOFSTEP]
letI := Ideal.fintypeQuotientOfFreeOfNeBot (span { r }) (mt span_singleton_eq_bot.mp hr)
[GOAL]
case neg
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := fintypeQuotientOfFreeOfNeBot (span {r}) (_ : ¬span {r} = ⊥)
⊢ ↑absNorm (span {r}) = Int.natAbs (↑LinearMap.det (↑(Algebra.lmul ℤ S) r))
[PROOFSTEP]
let b := Module.Free.chooseBasis ℤ S
[GOAL]
case neg
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := fintypeQuotientOfFreeOfNeBot (span {r}) (_ : ¬span {r} = ⊥)
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ ↑absNorm (span {r}) = Int.natAbs (↑LinearMap.det (↑(Algebra.lmul ℤ S) r))
[PROOFSTEP]
rw [← natAbs_det_equiv _ (b.equiv (basisSpanSingleton b hr) (Equiv.refl _))]
[GOAL]
case neg
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := fintypeQuotientOfFreeOfNeBot (span {r}) (_ : ¬span {r} = ⊥)
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ Int.natAbs
      (↑LinearMap.det
        (LinearMap.comp (↑ℤ (Submodule.subtype (span {r})))
          (AddMonoidHom.toIntLinearMap
            ↑(Basis.equiv b (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))))) =
    Int.natAbs (↑LinearMap.det (↑(Algebra.lmul ℤ S) r))
[PROOFSTEP]
congr
[GOAL]
case neg.e_m.h.e_6.h
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := fintypeQuotientOfFreeOfNeBot (span {r}) (_ : ¬span {r} = ⊥)
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ LinearMap.comp (↑ℤ (Submodule.subtype (span {r})))
      (AddMonoidHom.toIntLinearMap
        ↑(Basis.equiv b (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))) =
    ↑(Algebra.lmul ℤ S) r
[PROOFSTEP]
refine b.ext fun i => ?_
[GOAL]
case neg.e_m.h.e_6.h
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
this : Fintype (S ⧸ span {r}) := fintypeQuotientOfFreeOfNeBot (span {r}) (_ : ¬span {r} = ⊥)
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
i : Module.Free.ChooseBasisIndex ℤ S
⊢ ↑(LinearMap.comp (↑ℤ (Submodule.subtype (span {r})))
          (AddMonoidHom.toIntLinearMap
            ↑(Basis.equiv b (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))))
      (↑b i) =
    ↑(↑(Algebra.lmul ℤ S) r) (↑b i)
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ ↑(↑absNorm I) ∣ ↑(Algebra.norm ℤ) x
[PROOFSTEP]
rw [← Int.dvd_natAbs, ← absNorm_span_singleton x, Int.coe_nat_dvd]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ ↑absNorm I ∣ ↑absNorm (span {x})
[PROOFSTEP]
exact absNorm_dvd_absNorm_of_le ((span_singleton_le_iff_mem _).mpr h)
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
s : Set S
⊢ ↑absNorm (span {r}) ∣ Int.natAbs (↑(Algebra.norm ℤ) r)
[PROOFSTEP]
rw [absNorm_span_singleton]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : Irreducible (↑absNorm I)
h : IsUnit I
⊢ IsUnit (↑absNorm I)
[PROOFSTEP]
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using h
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : Irreducible (↑absNorm I)
⊢ ∀ (a b : Ideal S), I = a * b → IsUnit a ∨ IsUnit b
[PROOFSTEP]
rintro a b rfl
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
a b : Ideal S
hI : Irreducible (↑absNorm (a * b))
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using hI.isUnit_or_isUnit (_root_.map_mul absNorm a b)
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ ↑(↑absNorm I) ∈ I
[PROOFSTEP]
rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast, Quotient.index_eq_zero]
[GOAL]
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Infinite S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ span {↑(↑absNorm I)} ≤ I
[PROOFSTEP]
simp only [Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Ideal.absNorm_mem I]
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
⊢ Set.Finite {I | ↑absNorm I = n}
[PROOFSTEP]
let f := fun I : Ideal S => Ideal.map (Ideal.Quotient.mk (@Ideal.span S _ {↑n})) I
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Set.Finite {I | ↑absNorm I = n}
[PROOFSTEP]
refine @Set.Finite.of_finite_image _ _ _ f ?_ ?_
[GOAL]
case refine_1
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Set.Finite (f '' {I | ↑absNorm I = n})
[PROOFSTEP]
suffices Finite (S ⧸ @Ideal.span S _ {↑n})
  by
  let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
  refine @Set.Finite.of_finite_image _ _ _ g ?_ (SetLike.coe_injective.injOn _)
  exact Set.Finite.subset (@Set.finite_univ _ (@Set.finite' _ this)) (Set.subset_univ _)
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
⊢ Set.Finite (f '' {I | ↑absNorm I = n})
[PROOFSTEP]
let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
g : Ideal (S ⧸ span {↑n}) → Set (S ⧸ span {↑n}) := SetLike.coe
⊢ Set.Finite (f '' {I | ↑absNorm I = n})
[PROOFSTEP]
refine @Set.Finite.of_finite_image _ _ _ g ?_ (SetLike.coe_injective.injOn _)
[GOAL]
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
g : Ideal (S ⧸ span {↑n}) → Set (S ⧸ span {↑n}) := SetLike.coe
⊢ Set.Finite (g '' (f '' {I | ↑absNorm I = n}))
[PROOFSTEP]
exact Set.Finite.subset (@Set.finite_univ _ (@Set.finite' _ this)) (Set.subset_univ _)
[GOAL]
case refine_1
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Finite (S ⧸ span {↑n})
[PROOFSTEP]
rw [← absNorm_ne_zero_iff, absNorm_span_singleton]
[GOAL]
case refine_1
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Int.natAbs (↑(Algebra.norm ℤ) ↑n) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using ne_of_gt hn
[GOAL]
case refine_2
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Set.InjOn f {I | ↑absNorm I = n}
[PROOFSTEP]
intro I hI J hJ h
[GOAL]
case refine_2
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | ↑absNorm I = n}
J : Ideal S
hJ : J ∈ {I | ↑absNorm I = n}
h : f I = f J
⊢ I = J
[PROOFSTEP]
rw [← comap_map_mk (span_singleton_absNorm_le I), ← hI.symm, ← comap_map_mk (span_singleton_absNorm_le J), ← hJ.symm]
[GOAL]
case refine_2
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Infinite S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : 0 < n
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | ↑absNorm I = n}
J : Ideal S
hJ : J ∈ {I | ↑absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) J)
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
x : R
hx : x ∈ ↑(Algebra.norm R) '' ↑⊥
⊢ x = 0
[PROOFSTEP]
simpa using hx
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
I : Ideal S
⊢ spanNorm R I = ⊥ ↔ I = ⊥
[PROOFSTEP]
simp only [spanNorm, Ideal.span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, Algebra.norm_eq_zero_iff_of_basis (Module.Free.chooseBasis R S), @eq_bot_iff _ _ _ I,
  SetLike.le_def]
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
I : Ideal S
⊢ (∀ (a : S), a ∈ I → a = 0) ↔ ∀ ⦃x : S⦄, x ∈ I → x ∈ ⊥
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
x : R
hx : x ∈ ↑(Algebra.norm R) '' ↑(span {r})
⊢ ↑(Algebra.norm R) r ∣ x
[PROOFSTEP]
obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r x : S
hx' : x ∈ ↑(span {r})
hx : ↑(Algebra.norm R) x ∈ ↑(Algebra.norm R) '' ↑(span {r})
⊢ ↑(Algebra.norm R) r ∣ ↑(Algebra.norm R) x
[PROOFSTEP]
exact map_dvd _ (mem_span_singleton.mp hx')
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ spanNorm R ⊤ = ⊤
[PROOFSTEP]
rw [← Ideal.span_singleton_one, spanNorm_singleton]
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ span {↑(Algebra.norm R) 1} = ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ map f (spanNorm R I) = span (↑f ∘ ↑(Algebra.norm R) '' ↑I)
[PROOFSTEP]
rw [spanNorm, map_span, Set.image_image]
  -- Porting note: `Function.comp` reducibility
[GOAL]
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ span ((fun x => ↑f (↑(Algebra.norm R) x)) '' ↑I) = span (↑f ∘ ↑(Algebra.norm R) '' ↑I)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
[PROOFSTEP]
cases h : subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Subsingleton R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
[PROOFSTEP]
haveI := IsLocalization.unique R Rₘ M
[GOAL]
case inl
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Subsingleton R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
this : Unique Rₘ
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
[PROOFSTEP]
let b := Module.Free.chooseBasis R S
[GOAL]
case inr
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
[PROOFSTEP]
rw [map_spanNorm]
[GOAL]
case inr
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = span (↑(algebraMap R Rₘ) ∘ ↑(Algebra.norm R) '' ↑I)
[PROOFSTEP]
refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
[GOAL]
case inr.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ ↑(map (algebraMap S Sₘ) I) ⊆
    ↑(Algebra.norm Rₘ) ⁻¹' ↑(Submodule.span Rₘ (↑(algebraMap R Rₘ) ∘ ↑(Algebra.norm R) '' ↑I))
[PROOFSTEP]
rintro a' ha'
[GOAL]
case inr.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a' : Sₘ
ha' : a' ∈ ↑(map (algebraMap S Sₘ) I)
⊢ a' ∈ ↑(Algebra.norm Rₘ) ⁻¹' ↑(Submodule.span Rₘ (↑(algebraMap R Rₘ) ∘ ↑(Algebra.norm R) '' ↑I))
[PROOFSTEP]
simp only [Set.mem_preimage, submodule_span_eq, ← map_spanNorm, SetLike.mem_coe,
  IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
  IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
[GOAL]
case inr.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a' : Sₘ
ha' : ∃ a b, a' * ↑(algebraMap S Sₘ) ↑b = ↑(algebraMap S Sₘ) ↑a
⊢ ∃ a b, ↑(Algebra.norm Rₘ) a' * ↑(algebraMap R Rₘ) ↑b = ↑(algebraMap R Rₘ) ↑a
[PROOFSTEP]
obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
[GOAL]
case inr.refine_1.intro.mk.intro.mk.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has :
  a' *
      ↑(algebraMap S Sₘ)
        ↑{ val := ↑(algebraMap R S) s, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = ↑(algebraMap R S) s) } =
    ↑(algebraMap S Sₘ) ↑{ val := a, property := ha }
⊢ ∃ a b, ↑(Algebra.norm Rₘ) a' * ↑(algebraMap R Rₘ) ↑b = ↑(algebraMap R Rₘ) ↑a
[PROOFSTEP]
refine
  ⟨⟨Algebra.norm R a, norm_mem_spanNorm _ _ ha⟩, ⟨s ^ Fintype.card (Module.Free.ChooseBasisIndex R S), pow_mem hs _⟩,
    ?_⟩
[GOAL]
case inr.refine_1.intro.mk.intro.mk.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has :
  a' *
      ↑(algebraMap S Sₘ)
        ↑{ val := ↑(algebraMap R S) s, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = ↑(algebraMap R S) s) } =
    ↑(algebraMap S Sₘ) ↑{ val := a, property := ha }
⊢ ↑(Algebra.norm Rₘ) a' *
      ↑(algebraMap R Rₘ)
        ↑{ val := s ^ Fintype.card (Module.Free.ChooseBasisIndex R S),
            property := (_ : s ^ Fintype.card (Module.Free.ChooseBasisIndex R S) ∈ M) } =
    ↑(algebraMap R Rₘ) ↑{ val := ↑(Algebra.norm R) a, property := (_ : ↑(Algebra.norm R) a ∈ spanNorm R I) }
[PROOFSTEP]
simp only [Submodule.coe_mk, Subtype.coe_mk, map_pow] at has ⊢
[GOAL]
case inr.refine_1.intro.mk.intro.mk.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has : a' * ↑(algebraMap S Sₘ) (↑(algebraMap R S) s) = ↑(algebraMap S Sₘ) a
⊢ ↑(Algebra.norm Rₘ) a' * ↑(algebraMap R Rₘ) s ^ Fintype.card (Module.Free.ChooseBasisIndex R S) =
    ↑(algebraMap R Rₘ) (↑(Algebra.norm R) a)
[PROOFSTEP]
apply_fun Algebra.norm Rₘ at has
[GOAL]
case inr.refine_1.intro.mk.intro.mk.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has : ↑(Algebra.norm Rₘ) (a' * ↑(algebraMap S Sₘ) (↑(algebraMap R S) s)) = ↑(Algebra.norm Rₘ) (↑(algebraMap S Sₘ) a)
⊢ ↑(Algebra.norm Rₘ) a' * ↑(algebraMap R Rₘ) s ^ Fintype.card (Module.Free.ChooseBasisIndex R S) =
    ↑(algebraMap R Rₘ) (↑(Algebra.norm R) a)
[PROOFSTEP]
rwa [_root_.map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ,
  Algebra.norm_algebraMap_of_basis (b.localizationLocalization Rₘ M Sₘ), Algebra.norm_localization R M a] at has
[GOAL]
case inr.refine_2
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ ↑I ⊆
    ↑(algebraMap R Rₘ) ∘ ↑(Algebra.norm R) ⁻¹' ↑(Submodule.span Rₘ (↑(Algebra.norm Rₘ) '' ↑(map (algebraMap S Sₘ) I)))
[PROOFSTEP]
intro a ha
[GOAL]
case inr.refine_2
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a : S
ha : a ∈ ↑I
⊢ a ∈ ↑(algebraMap R Rₘ) ∘ ↑(Algebra.norm R) ⁻¹' ↑(Submodule.span Rₘ (↑(Algebra.norm Rₘ) '' ↑(map (algebraMap S Sₘ) I)))
[PROOFSTEP]
rw [Set.mem_preimage, Function.comp_apply, ← Algebra.norm_localization (Sₘ := Sₘ) R M a]
[GOAL]
case inr.refine_2
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
I : Ideal S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : Module.Free R S
M : Submonoid R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁹ : CommRing Rₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
h✝ : Nontrivial R
h : (_ : Subsingleton R ∨ Nontrivial R) = (_ : Subsingleton R ∨ Nontrivial R)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
a : S
ha : a ∈ ↑I
⊢ ↑(Algebra.norm Rₘ) (↑(algebraMap S Sₘ) a) ∈ ↑(Submodule.span Rₘ (↑(Algebra.norm Rₘ) '' ↑(map (algebraMap S Sₘ) I)))
[PROOFSTEP]
exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I J : Ideal S
⊢ spanNorm R I * spanNorm R J ≤ spanNorm R (I * J)
[PROOFSTEP]
rw [spanNorm, spanNorm, spanNorm, Ideal.span_mul_span', ← Set.image_mul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I J : Ideal S
⊢ span (↑(Algebra.norm R) '' (↑I * ↑J)) ≤ span (↑(Algebra.norm R) '' ↑(I * J))
[PROOFSTEP]
refine Ideal.span_mono (Set.monotone_image ?_)
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I J : Ideal S
⊢ ↑I * ↑J ≤ ↑(I * J)
[PROOFSTEP]
rintro _ ⟨x, y, hxI, hyJ, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
I J : Ideal S
x y : S
hxI : x ∈ ↑I
hyJ : y ∈ ↑J
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(I * J)
[PROOFSTEP]
exact Ideal.mul_mem_mul hxI hyJ
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
[PROOFSTEP]
refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J
[PROOFSTEP]
cases' eq_bot_or_top (spanNorm R I) with hI hI
[GOAL]
case inl
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J
[PROOFSTEP]
rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
[GOAL]
case inl
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanNorm R J
[PROOFSTEP]
exact bot_le
[GOAL]
case inr
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J
[PROOFSTEP]
rw [hI, Ideal.top_mul]
[GOAL]
case inr
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J
[PROOFSTEP]
cases' eq_bot_or_top (spanNorm R J) with hJ hJ
[GOAL]
case inr.inl
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R J
[PROOFSTEP]
rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
[GOAL]
case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J
[PROOFSTEP]
rw [hJ]
[GOAL]
case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
I J : Ideal S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
[PROOFSTEP]
cases subsingleton_or_nontrivial S
[GOAL]
case inl
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Subsingleton S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
[PROOFSTEP]
have : ∀ I : Ideal S, I = ⊤ := fun I => Subsingleton.elim I ⊤
[GOAL]
case inl
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Subsingleton S
this : ∀ (I : Ideal S), I = ⊤
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
[PROOFSTEP]
simp [this I, this J, this (I * J)]
[GOAL]
case inr
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J
[PROOFSTEP]
refine eq_of_localization_maximal ?_
[GOAL]
case inr
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ ∀ (P : Ideal R) (x : IsMaximal P),
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
      map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
intro P hP
[GOAL]
case inr
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
by_cases hP0 : P = ⊥
[GOAL]
case pos
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
subst hP0
[GOAL]
case pos
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : IsMaximal ⊥
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
rw [spanNorm_mul_of_bot_or_top]
[GOAL]
case pos.eq_bot_or_top
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : IsMaximal ⊥
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
[PROOFSTEP]
intro I
[GOAL]
case pos.eq_bot_or_top
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I✝ J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : IsMaximal ⊥
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤
[PROOFSTEP]
refine or_iff_not_imp_right.mpr fun hI => ?_
[GOAL]
case pos.eq_bot_or_top
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I✝ J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : IsMaximal ⊥
I : Ideal R
hI : ¬I = ⊤
⊢ I = ⊥
[PROOFSTEP]
exact (hP.eq_of_le hI bot_le).symm
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
let P' := Algebra.algebraMapSubmonoid S P.primeCompl
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
letI : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
haveI : IsScalarTower R (Localization.AtPrime P) (Localization P') :=
  IsScalarTower.of_algebraMap_eq
    (fun x => (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this✝ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
this : IsScalarTower R (Localization.AtPrime P) (Localization P')
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
have h : P' ≤ S⁰ :=
  map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _) P.primeCompl_le_nonZeroDivisors
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this✝ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
this : IsScalarTower R (Localization.AtPrime P) (Localization P')
h : P' ≤ S⁰
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
haveI : IsDomain (Localization P') := IsLocalization.isDomain_localization h
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this✝¹ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
this✝ : IsScalarTower R (Localization.AtPrime P) (Localization P')
h : P' ≤ S⁰
this : IsDomain (Localization P')
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
haveI : IsDedekindDomain (Localization P') := IsLocalization.isDedekindDomain S h _
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this✝² : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
this✝¹ : IsScalarTower R (Localization.AtPrime P) (Localization P')
h : P' ≤ S⁰
this✝ : IsDomain (Localization P')
this : IsDedekindDomain (Localization P')
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
letI := Classical.decEq (Ideal (Localization P'))
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this✝³ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
this✝² : IsScalarTower R (Localization.AtPrime P) (Localization P')
h : P' ≤ S⁰
this✝¹ : IsDomain (Localization P')
this✝ : IsDedekindDomain (Localization P')
this : DecidableEq (Ideal (Localization P')) := Classical.decEq (Ideal (Localization P'))
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
haveI : IsPrincipalIdealRing (Localization P') := IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P hP0
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : IsMaximal P
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S (primeCompl P)
this✝⁴ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra (primeCompl P) S
this✝³ : IsScalarTower R (Localization.AtPrime P) (Localization P')
h : P' ≤ S⁰
this✝² : IsDomain (Localization P')
this✝¹ : IsDedekindDomain (Localization P')
this✝ : DecidableEq (Ideal (Localization P')) := Classical.decEq (Ideal (Localization P'))
this : IsPrincipalIdealRing (Localization P')
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
[PROOFSTEP]
rw [Ideal.map_mul, ← spanNorm_localization R I P.primeCompl (Localization P'), ←
  spanNorm_localization R J P.primeCompl (Localization P'), ←
  spanNorm_localization R (I * J) P.primeCompl (Localization P'), Ideal.map_mul, ← (I.map _).span_singleton_generator, ←
  (J.map _).span_singleton_generator, span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
  spanNorm_singleton, span_singleton_mul_span_singleton, _root_.map_mul]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
⊢ ZeroHom.toFun { toFun := spanNorm R, map_zero' := (_ : spanNorm R ⊥ = ⊥) } 1 = 1
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
⊢ spanNorm R 1 = 1
[PROOFSTEP]
rw [one_eq_top, spanNorm_top R, one_eq_top]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
⊢ ↑(relNorm R) ⊥ = ⊥
[PROOFSTEP]
simpa only [zero_eq_bot] using _root_.map_zero (relNorm R : Ideal S →*₀ _)
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
⊢ ↑(relNorm R) ⊤ = ⊤
[PROOFSTEP]
simpa only [one_eq_top] using map_one (relNorm R : Ideal S →*₀ _)