[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let a := I.smithCoeffs b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let b' := I.ringBasis b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let ab := I.selfBasis b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
have ab_eq := I.selfBasis_def b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
have mem_I_iff : ∀ x, x ∈ I ↔ ∀ i, a i ∣ b'.repr x i := by
  intro x
  rw [ab.mem_ideal_iff']
  simp_rw [ab_eq]
  have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i :=
    by
    intro c i
    simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
  constructor
  · rintro ⟨c, rfl⟩ i
    exact ⟨c i, this c i⟩
  · rintro ha
    choose c hc using ha
    exact
      ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
        -- Now we map everything through the linear equiv `S ≃ₗ (ι → R)`,
          -- which maps `I` to `I' := Π i, a i ℤ`.
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
⊢ ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
[PROOFSTEP]
rw [ab.mem_ideal_iff']
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ (∃ c, x = ∑ i : ι, c i • ↑(↑ab i)) ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
[PROOFSTEP]
simp_rw [ab_eq]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ (∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x) ↔
    ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
[PROOFSTEP]
have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i :=
  by
  intro c i
  simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
⊢ ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
[PROOFSTEP]
intro c i
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
c : ι → R
i : ι
⊢ ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
[PROOFSTEP]
simp only [← MulAction.mul_smul, b'.repr_sum_self, mul_comm]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
⊢ (∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x) ↔
    ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
⊢ (∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x) →
    ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
[PROOFSTEP]
rintro ⟨c, rfl⟩ i
[GOAL]
case mp.intro
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
c : ι → R
i : ι
⊢ smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr (∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x)) i
[PROOFSTEP]
exact ⟨c i, this c i⟩
[GOAL]
case mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
⊢ (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i) →
    ∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x
[PROOFSTEP]
rintro ha
[GOAL]
case mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
ha : ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr x) i
⊢ ∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x
[PROOFSTEP]
choose c hc using ha
[GOAL]
case mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
x : S
this : ∀ (c : ι → R) (i : ι), ↑(↑b'.repr (∑ j : ι, c j • a j • ↑b' j)) i = a i * c i
c : ι → R
hc : ∀ (i : ι), ↑(↑(ringBasis b I hI).repr x) i = smithCoeffs b I hI i * c i
⊢ ∃ c, x = ∑ x : ι, c x • smithCoeffs b I hI x • ↑(ringBasis b I hI) x
[PROOFSTEP]
exact
  ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
    -- Now we map everything through the linear equiv `S ≃ₗ (ι → R)`,
      -- which maps `I` to `I' := Π i, a i ℤ`.
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span ({a i} : Set R)
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
have : Submodule.map (b'.equivFun : S →ₗ[R] ι → R) (I.restrictScalars R) = I' :=
  by
  ext x
  simp only [Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ, Submodule.restrictScalars_mem,
    mem_I_iff, smul_eq_mul, forall_true_left, LinearEquiv.coe_coe, Basis.equivFun_apply]
  constructor
  · rintro ⟨y, hy, rfl⟩ i
    exact hy i
  · rintro hdvd
    refine' ⟨∑ i, x i • b' i, fun i => _, _⟩ <;> rw [b'.repr_sum_self]
    · exact hdvd i
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
⊢ Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ x ∈ Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) ↔ x ∈ I'
[PROOFSTEP]
simp only [Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ, Submodule.restrictScalars_mem,
  mem_I_iff, smul_eq_mul, forall_true_left, LinearEquiv.coe_coe, Basis.equivFun_apply]
[GOAL]
case h
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ (∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x) ↔
    ∀ (i : ι), smithCoeffs b I hI i ∣ x i
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ (∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x) →
    ∀ (i : ι), smithCoeffs b I hI i ∣ x i
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩ i
[GOAL]
case h.mp.intro.intro
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
y : S
hy : ∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i
i : ι
⊢ smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i
[PROOFSTEP]
exact hy i
[GOAL]
case h.mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
⊢ (∀ (i : ι), smithCoeffs b I hI i ∣ x i) →
    ∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x
[PROOFSTEP]
rintro hdvd
[GOAL]
case h.mpr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
⊢ ∃ y, (∀ (i : ι), smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr y) i) ∧ ↑(↑(ringBasis b I hI).repr y) = x
[PROOFSTEP]
refine' ⟨∑ i, x i • b' i, fun i => _, _⟩
[GOAL]
case h.mpr.refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
i : ι
⊢ smithCoeffs b I hI i ∣ ↑(↑(ringBasis b I hI).repr (∑ i : ι, x i • ↑b' i)) i
[PROOFSTEP]
rw [b'.repr_sum_self]
[GOAL]
case h.mpr.refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
⊢ ↑(↑(ringBasis b I hI).repr (∑ i : ι, x i • ↑b' i)) = x
[PROOFSTEP]
rw [b'.repr_sum_self]
[GOAL]
case h.mpr.refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
x : ι → R
hdvd : ∀ (i : ι), smithCoeffs b I hI i ∣ x i
i : ι
⊢ smithCoeffs b I hI i ∣ x i
[PROOFSTEP]
exact hdvd i
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
refine'
  ((Submodule.Quotient.restrictScalarsEquiv R I).restrictScalars R).symm.trans (σ₁₂ := RingHom.id R) (σ₃₂ :=
    RingHom.id R) _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ (S ⧸ Submodule.restrictScalars R I) ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
refine'
  (Submodule.Quotient.equiv (I.restrictScalars R) I' b'.equivFun this).trans (σ₁₂ := RingHom.id R) (σ₃₂ := RingHom.id R)
    _
[GOAL]
case refine'_3.refine'_1
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3.refine'_2
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ RingHomInvPair (RingHom.id R) (RingHom.id R)
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3.refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ ((ι → R) ⧸ I') ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
classical
let this := Submodule.quotientPi (show ∀ _, Submodule R R from fun i => span ({a i} : Set R))
exact this
[GOAL]
case refine'_3.refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
⊢ ((ι → R) ⧸ I') ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
let this := Submodule.quotientPi (show ∀ _, Submodule R R from fun i => span ({a i} : Set R))
[GOAL]
case refine'_3.refine'_3
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain S
inst✝ : Finite ι
I : Ideal S
b : Basis ι R S
hI : I ≠ ⊥
this✝¹ : Fintype ι
a : ι → R := smithCoeffs b I hI
b' : Basis ι R S := ringBasis b I hI
ab : Basis ι R { x // x ∈ I } := selfBasis b I hI
ab_eq : ∀ (i : ι), ↑(↑(selfBasis b I hI) i) = smithCoeffs b I hI i • ↑(ringBasis b I hI) i
mem_I_iff : ∀ (x : S), x ∈ I ↔ ∀ (i : ι), a i ∣ ↑(↑b'.repr x) i
I' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span {a i}
this✝ : Submodule.map (↑(Basis.equivFun b')) (Submodule.restrictScalars R I) = I'
this : ((ι → R) ⧸
    Submodule.pi Set.univ
      (let_fun this := fun i => span {a i};
      this)) ≃ₗ[R]
  (i : ι) → R ⧸ (fun this => this) (fun i => span {a i}) i :=
  Submodule.quotientPi
    (let_fun this := fun i => span {a i};
    this)
⊢ ((ι → R) ⧸ I') ≃ₗ[R] (i : ι) → R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
exact this
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
let b := Module.Free.chooseBasis ℤ S
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
let a := I.smithCoeffs b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
let e := I.quotientEquivPiZMod b hI
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
e : S ⧸ I ≃+ ((i : Module.Free.ChooseBasisIndex ℤ S) → ZMod (Int.natAbs (smithCoeffs b I hI i))) :=
  quotientEquivPiZMod I b hI
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
haveI : ∀ i, NeZero (a i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr (smithCoeffs_ne_zero b I hI i)⟩
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
e : S ⧸ I ≃+ ((i : Module.Free.ChooseBasisIndex ℤ S) → ZMod (Int.natAbs (smithCoeffs b I hI i))) :=
  quotientEquivPiZMod I b hI
this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (Int.natAbs (a i))
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
classical exact Fintype.ofEquiv (∀ i, ZMod (a i).natAbs) e.symm
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain S
inst✝² : Finite ι
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
e : S ⧸ I ≃+ ((i : Module.Free.ChooseBasisIndex ℤ S) → ZMod (Int.natAbs (smithCoeffs b I hI i))) :=
  quotientEquivPiZMod I b hI
this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (Int.natAbs (a i))
⊢ Fintype (S ⧸ I)
[PROOFSTEP]
exact Fintype.ofEquiv (∀ i, ZMod (a i).natAbs) e.symm
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : IsDomain S
inst✝⁴ : Finite ι
F : Type u_4
inst✝³ : CommRing F
inst✝² : Algebra F R
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F R S
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ (S ⧸ I) ≃ₗ[F] ⨁ (i : ι), R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : IsDomain S
inst✝⁴ : Finite ι
F : Type u_4
inst✝³ : CommRing F
inst✝² : Algebra F R
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F R S
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
this : Fintype ι
⊢ (S ⧸ I) ≃ₗ[F] ⨁ (i : ι), R ⧸ span {smithCoeffs b I hI i}
[PROOFSTEP]
exact ((I.quotientEquivPiSpan b _).restrictScalars F).trans (DirectSum.linearEquivFunOnFintype _ _ _).symm
[GOAL]
ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsPrincipalIdealRing R
inst✝⁹ : IsDomain S
inst✝⁸ : Finite ι✝
F : Type u_4
inst✝⁷ : CommRing F
inst✝⁶ : Algebra F R
inst✝⁵ : Algebra F S
inst✝⁴ : IsScalarTower F R S
b✝ : Basis ι✝ R S
I : Ideal S
hI : I ≠ ⊥
ι : Type u_5
inst✝³ : Fintype ι
b : Basis ι R S
inst✝² : Nontrivial F
inst✝¹ : ∀ (i : ι), Module.Free F (R ⧸ span {smithCoeffs b I hI i})
inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ span {smithCoeffs b I hI i})
⊢ FiniteDimensional.finrank F (S ⧸ I) = ∑ i : ι, FiniteDimensional.finrank F (R ⧸ span {smithCoeffs b I hI i})
[PROOFSTEP]
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, FiniteDimensional.finrank_directSum]
