[GOAL]
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
⊢ P = span {x}
[PROOFSTEP]
letI := Classical.decEq (Ideal R)
[GOAL]
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
⊢ P = span {x}
[PROOFSTEP]
have hx0 : x ≠ 0 := by
  rintro rfl
  exact hxP2 (zero_mem _)
[GOAL]
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
x_mem : 0 ∈ P
hxP2 : ¬0 ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬0 ∈ Q
⊢ False
[PROOFSTEP]
exact hxP2 (zero_mem _)
[GOAL]
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
⊢ P = span {x}
[PROOFSTEP]
by_cases hP0 : P = ⊥
[GOAL]
case pos
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : P = ⊥
⊢ P = span {x}
[PROOFSTEP]
subst hP0
[GOAL]
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP : IsPrime ⊥
x_mem : x ∈ ⊥
hxP2 : ¬x ∈ ⊥ ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ ⊥ → ¬x ∈ Q
⊢ ⊥ = span {x}
[PROOFSTEP]
rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]
[GOAL]
case neg
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
⊢ P = span {x}
[PROOFSTEP]
have hspan0 : span ({ x } : Set R) ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp hx0
[GOAL]
case neg
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ P = span {x}
[PROOFSTEP]
have span_le := (Ideal.span_singleton_le_iff_mem _).mpr x_mem
[GOAL]
case neg
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
⊢ P = span {x}
[PROOFSTEP]
refine'
  associated_iff_eq.mp
    ((associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0).mpr
      (le_antisymm ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 hspan0).mp _) _))
[GOAL]
case neg.refine'_1
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
⊢ P ∣ span {x}
[PROOFSTEP]
rwa [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
[GOAL]
case neg.refine'_2
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
⊢ normalizedFactors (span {x}) ≤ normalizedFactors P
[PROOFSTEP]
simp only [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, normalize_eq,
  Multiset.le_iff_count, Multiset.count_singleton]
[GOAL]
case neg.refine'_2
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
⊢ ∀ (a : Ideal R), Multiset.count a (normalizedFactors (span {x})) ≤ if a = P then 1 else 0
[PROOFSTEP]
intro Q
[GOAL]
case neg.refine'_2
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ if Q = P then 1 else 0
[PROOFSTEP]
split_ifs with hQ
[GOAL]
case pos
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 1
[PROOFSTEP]
subst hQ
[GOAL]
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : IsPrime Q
x_mem : x ∈ Q
hxP2 : ¬x ∈ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), IsPrime Q_1 → Q_1 ≠ Q → ¬x ∈ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 1
[PROOFSTEP]
refine' (Ideal.count_normalizedFactors_eq _ _).le
[GOAL]
case pos.refine'_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : IsPrime Q
x_mem : x ∈ Q
hxP2 : ¬x ∈ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), IsPrime Q_1 → Q_1 ≠ Q → ¬x ∈ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ span {x} ≤ Q ^ 1
[PROOFSTEP]
simp only [Ideal.span_singleton_le_iff_mem, pow_one]
[GOAL]
case pos.refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : IsPrime Q
x_mem : x ∈ Q
hxP2 : ¬x ∈ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), IsPrime Q_1 → Q_1 ≠ Q → ¬x ∈ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ ¬span {x} ≤ Q ^ (1 + 1)
[PROOFSTEP]
simp only [Ideal.span_singleton_le_iff_mem, pow_one]
[GOAL]
case pos.refine'_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : IsPrime Q
x_mem : x ∈ Q
hxP2 : ¬x ∈ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), IsPrime Q_1 → Q_1 ≠ Q → ¬x ∈ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ x ∈ Q
[PROOFSTEP]
assumption
[GOAL]
case pos.refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : IsPrime Q
x_mem : x ∈ Q
hxP2 : ¬x ∈ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), IsPrime Q_1 → Q_1 ≠ Q → ¬x ∈ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ ¬x ∈ Q ^ (1 + 1)
[PROOFSTEP]
assumption
[GOAL]
case neg
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0
[PROOFSTEP]
by_cases hQp : IsPrime Q
[GOAL]
case pos
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : IsPrime Q
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0
[PROOFSTEP]
skip
[GOAL]
case pos
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : IsPrime Q
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0
[PROOFSTEP]
refine' (Ideal.count_normalizedFactors_eq _ _).le
[GOAL]
case pos.refine'_1
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : IsPrime Q
⊢ span {x} ≤ Q ^ 0
[PROOFSTEP]
simp only [Ideal.span_singleton_le_iff_mem, zero_add, pow_one, pow_zero, one_eq_top, Submodule.mem_top]
[GOAL]
case pos.refine'_2
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : IsPrime Q
⊢ ¬span {x} ≤ Q ^ (0 + 1)
[PROOFSTEP]
simp only [Ideal.span_singleton_le_iff_mem, zero_add, pow_one, pow_zero, one_eq_top, Submodule.mem_top]
[GOAL]
case pos.refine'_2
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : IsPrime Q
⊢ ¬x ∈ Q
[PROOFSTEP]
exact hxQ _ hQp hQ
[GOAL]
case neg
R : Type u_1
inst✝² : CommRing R
P : Ideal R
hP : IsPrime P
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : ¬x ∈ P ^ 2
hxQ : ∀ (Q : Ideal R), IsPrime Q → Q ≠ P → ¬x ∈ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : ¬IsPrime Q
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0
[PROOFSTEP]
exact
  (Multiset.count_eq_zero.mpr fun hQi =>
      hQp (isPrime_of_prime (irreducible_iff_prime.mp (irreducible_of_normalized_factor _ hQi)))).le
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤
⊢ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
have hinv := I.mul_inv
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤
hinv : ↑I * ↑I⁻¹ = 1
⊢ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
set J := Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R { v })
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
have hJ : IsLocalization.coeSubmodule A J = ↑I * Submodule.span R { v } := by
  -- Porting note: had to insert `val_eq_coe` into this rewrite.
      -- Arguably this is because `Subtype.ext_iff` is breaking the `FractionalIdeal` API.
  rw [Subtype.ext_iff, val_eq_coe, coe_mul, val_eq_coe, coe_one] at hinv 
  apply Submodule.map_comap_eq_self
  rw [← Submodule.one_eq_range, ← hinv]
  exact Submodule.mul_le_mul_right ((Submodule.span_singleton_le_iff_mem _ _).2 hv)
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
[PROOFSTEP]
rw [Subtype.ext_iff, val_eq_coe, coe_mul, val_eq_coe, coe_one] at hinv 
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
[PROOFSTEP]
apply Submodule.map_comap_eq_self
[GOAL]
case h
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ ↑↑I * Submodule.span R {v} ≤ LinearMap.range (Algebra.linearMap R A)
[PROOFSTEP]
rw [← Submodule.one_eq_range, ← hinv]
[GOAL]
case h
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ ↑↑I * Submodule.span R {v} ≤ ↑↑I * ↑↑I⁻¹
[PROOFSTEP]
exact Submodule.mul_le_mul_right ((Submodule.span_singleton_le_iff_mem _ _).2 hv)
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
have : (1 : A) ∈ ↑I * Submodule.span R { v } :=
  by
  rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]
  exact ⟨1, (algebraMap R _).map_one⟩
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ 1 ∈ ↑↑I * Submodule.span R {v}
[PROOFSTEP]
rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ ∃ y, ↑(algebraMap R A) y = 1
[PROOFSTEP]
exact ⟨1, (algebraMap R _).map_one⟩
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
⊢ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
obtain ⟨w, hw, hvw⟩ := Submodule.mem_mul_span_singleton.1 this
[GOAL]
case intro.intro
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
refine' ⟨⟨w, _⟩⟩
[GOAL]
case intro.intro
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑↑I = Submodule.span R {w}
[PROOFSTEP]
rw [← FractionalIdeal.coe_spanSingleton S, ← inv_inv I, eq_comm]
[GOAL]
case intro.intro
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑(spanSingleton S w) = ↑↑I⁻¹⁻¹
[PROOFSTEP]
refine' congr_arg (↑) (Units.eq_inv_of_mul_eq_one_left (le_antisymm _ _))
[GOAL]
case intro.intro.refine'_1
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑I⁻¹ * spanSingleton S w ≤ 1
[PROOFSTEP]
conv_rhs => rw [← hinv, mul_comm]
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
| 1
[PROOFSTEP]
rw [← hinv, mul_comm]
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
| 1
[PROOFSTEP]
rw [← hinv, mul_comm]
[GOAL]
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
| 1
[PROOFSTEP]
rw [← hinv, mul_comm]
[GOAL]
case intro.intro.refine'_1
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑I⁻¹ * spanSingleton S w ≤ ↑I⁻¹ * ↑I
[PROOFSTEP]
apply FractionalIdeal.mul_le_mul_left (FractionalIdeal.spanSingleton_le_iff_mem.mpr hw)
[GOAL]
case intro.intro.refine'_2
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ 1 ≤ ↑I⁻¹ * spanSingleton S w
[PROOFSTEP]
rw [FractionalIdeal.one_le, ← hvw, mul_comm]
[GOAL]
case intro.intro.refine'_2
R✝ : Type u_1
inst✝⁴ : CommRing R✝
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ v * w ∈ ↑I⁻¹ * spanSingleton S w
[PROOFSTEP]
exact FractionalIdeal.mul_mem_mul hv (FractionalIdeal.mem_spanSingleton_self _ _)
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : I * I' = 1
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
have hinv' := hinv
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv hinv' : I * I' = 1
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
rw [Subtype.ext_iff, val_eq_coe, coe_mul] at hinv 
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
let s := hf.toFinset
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
haveI := Classical.decEq (Ideal R)
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
have coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤ :=
  by
  simp_rw [Finset.mem_erase, hf.mem_toFinset]
  rintro M hM M' ⟨hne, hM'⟩
  exact Ideal.IsMaximal.coprime_of_ne hM hM' hne.symm
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
⊢ ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
[PROOFSTEP]
simp_rw [Finset.mem_erase, hf.mem_toFinset]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
⊢ ∀ (M : Ideal R), M ∈ {I | IsMaximal I} → ∀ (M' : Ideal R), M' ≠ M ∧ M' ∈ {I | IsMaximal I} → M ⊔ M' = ⊤
[PROOFSTEP]
rintro M hM M' ⟨hne, hM'⟩
[GOAL]
case intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
M : Ideal R
hM : M ∈ {I | IsMaximal I}
M' : Ideal R
hne : M' ≠ M
hM' : M' ∈ {I | IsMaximal I}
⊢ M ⊔ M' = ⊤
[PROOFSTEP]
exact Ideal.IsMaximal.coprime_of_ne hM hM' hne.symm
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
have nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M := fun M hM =>
  left_lt_sup.1 ((hf.mem_toFinset.1 hM).ne_top.lt_top.trans_eq (Ideal.sup_iInf_eq_top <| coprime M hM).symm)
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
have : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M :=
  by
  intro M hM; by_contra' h
  obtain ⟨x, hx, hxM⟩ :=
    SetLike.exists_of_lt
      ((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).ne_top.lt_top).trans_eq hinv.symm)
  refine' hxM (Submodule.map₂_le.2 _ hx); exact h
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
⊢ ∀ (M : Ideal R), M ∈ s → ∃ a, a ∈ I ∧ ∃ b, b ∈ I' ∧ ¬a * b ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
intro M hM
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
M : Ideal R
hM : M ∈ s
⊢ ∃ a, a ∈ I ∧ ∃ b, b ∈ I' ∧ ¬a * b ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
by_contra' h
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
M : Ideal R
hM : M ∈ s
h : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → a * b ∈ IsLocalization.coeSubmodule A M
⊢ False
[PROOFSTEP]
obtain ⟨x, hx, hxM⟩ :=
  SetLike.exists_of_lt
    ((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).ne_top.lt_top).trans_eq hinv.symm)
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
M : Ideal R
hM : M ∈ s
h : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → a * b ∈ IsLocalization.coeSubmodule A M
x : A
hx : x ∈ ↑I * ↑I'
hxM : ¬x ∈ IsLocalization.coeSubmodule A M
⊢ False
[PROOFSTEP]
refine' hxM (Submodule.map₂_le.2 _ hx)
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
M : Ideal R
hM : M ∈ s
h : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → a * b ∈ IsLocalization.coeSubmodule A M
x : A
hx : x ∈ ↑I * ↑I'
hxM : ¬x ∈ IsLocalization.coeSubmodule A M
⊢ ∀ (m : A), m ∈ ↑I → ∀ (n : A), n ∈ ↑I' → ↑(↑(LinearMap.mul R A) m) n ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
this : ∀ (M : Ideal R), M ∈ s → ∃ a, a ∈ I ∧ ∃ b, b ∈ I' ∧ ¬a * b ∈ IsLocalization.coeSubmodule A M
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
choose! a ha b hb hm using this
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
choose! u hu hum using fun M hM => SetLike.not_le_iff_exists.1 (nle M hM)
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
let v := ∑ M in s, u M • b M
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
have hv : v ∈ I' := Submodule.sum_mem _ fun M hM => Submodule.smul_mem _ _ <| hb M hM
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
⊢ Submodule.IsPrincipal ↑I
[PROOFSTEP]
refine'
  FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top (Units.mkOfMulEqOne I I' hinv') hv
    (of_not_not fun h => _)
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
⊢ False
[PROOFSTEP]
obtain ⟨M, hM, hJM⟩ := Ideal.exists_le_maximal _ h
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hM : IsMaximal M
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
⊢ False
[PROOFSTEP]
replace hM := hf.mem_toFinset.2 hM
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
⊢ False
[PROOFSTEP]
have : ∀ a ∈ I, ∀ b ∈ I', ∃ c, algebraMap R _ c = a * b :=
  by
  intro a ha b hb; have hi := hinv.le
  obtain ⟨c, -, hc⟩ := hi (Submodule.mul_mem_mul ha hb)
  exact ⟨c, hc⟩
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
⊢ ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
[PROOFSTEP]
intro a ha b hb
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ (M : Ideal R), M ∈ s → a✝ M ∈ I
b✝ : Ideal R → A
hb✝ : ∀ (M : Ideal R), M ∈ s → b✝ M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a✝ M * b✝ M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
⊢ ∃ c, ↑(algebraMap R A) c = a * b
[PROOFSTEP]
have hi := hinv.le
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ (M : Ideal R), M ∈ s → a✝ M ∈ I
b✝ : Ideal R → A
hb✝ : ∀ (M : Ideal R), M ∈ s → b✝ M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a✝ M * b✝ M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
hi : ↑I * ↑I' ≤ ↑1
⊢ ∃ c, ↑(algebraMap R A) c = a * b
[PROOFSTEP]
obtain ⟨c, -, hc⟩ := hi (Submodule.mul_mem_mul ha hb)
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ (M : Ideal R), M ∈ s → a✝ M ∈ I
b✝ : Ideal R → A
hb✝ : ∀ (M : Ideal R), M ∈ s → b✝ M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a✝ M * b✝ M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
hi : ↑I * ↑I' ≤ ↑1
c : R
hc : ↑(Algebra.linearMap R A) c = a * b
⊢ ∃ c, ↑(algebraMap R A) c = a * b
[PROOFSTEP]
exact ⟨c, hc⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
⊢ False
[PROOFSTEP]
have hmem : a M * v ∈ IsLocalization.coeSubmodule A M :=
  by
  obtain ⟨c, hc⟩ := this _ (ha M hM) v hv
  refine' IsLocalization.coeSubmodule_mono _ hJM ⟨c, _, hc⟩
  have := Submodule.mul_mem_mul (ha M hM) (Submodule.mem_span_singleton_self v)
  rwa [← hc] at this 
[GOAL]
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
⊢ a M * v ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
obtain ⟨c, hc⟩ := this _ (ha M hM) v hv
[GOAL]
case intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hc : ↑(algebraMap R A) c = a M * v
⊢ a M * v ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
refine' IsLocalization.coeSubmodule_mono _ hJM ⟨c, _, hc⟩
[GOAL]
case intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hc : ↑(algebraMap R A) c = a M * v
⊢ c ∈ ↑(Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}))
[PROOFSTEP]
have := Submodule.mul_mem_mul (ha M hM) (Submodule.mem_span_singleton_self v)
[GOAL]
case intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝¹ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this✝ : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hc : ↑(algebraMap R A) c = a M * v
this : a M * v ∈ ↑I * Submodule.span R {v}
⊢ c ∈ ↑(Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}))
[PROOFSTEP]
rwa [← hc] at this 
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : a M * v ∈ IsLocalization.coeSubmodule A M
⊢ False
[PROOFSTEP]
simp_rw [Finset.mul_sum, mul_smul_comm] at hmem 
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : ∑ x in Set.Finite.toFinset hf, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
⊢ False
[PROOFSTEP]
rw [← s.add_sum_erase _ hM, Submodule.add_mem_iff_left] at hmem 
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) ∈ IsLocalization.coeSubmodule A M
⊢ False
[PROOFSTEP]
refine' hm M hM _
[GOAL]
case intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) ∈ IsLocalization.coeSubmodule A M
⊢ a M * b M ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
obtain ⟨c, hc : algebraMap R A c = a M * b M⟩ := this _ (ha M hM) _ (hb M hM)
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) ∈ IsLocalization.coeSubmodule A M
c : R
hc : ↑(algebraMap R A) c = a M * b M
⊢ a M * b M ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
rw [← hc] at hmem ⊢
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hmem : u M • ↑(algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
hc : ↑(algebraMap R A) c = a M * b M
⊢ ↑(algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
rw [Algebra.smul_def, ← _root_.map_mul] at hmem 
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hmem : ↑(algebraMap R A) (u M * c) ∈ IsLocalization.coeSubmodule A M
hc : ↑(algebraMap R A) c = a M * b M
⊢ ↑(algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
obtain ⟨d, hdM, he⟩ := hmem
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hc : ↑(algebraMap R A) c = a M * b M
d : R
hdM : d ∈ ↑M
he : ↑(Algebra.linearMap R A) d = ↑(algebraMap R A) (u M * c)
⊢ ↑(algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
rw [IsLocalization.injective _ hS he] at hdM 
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
c : R
hc : ↑(algebraMap R A) c = a M * b M
d : R
hdM : u M * c ∈ ↑M
he : ↑(Algebra.linearMap R A) d = ↑(algebraMap R A) (u M * c)
⊢ ↑(algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
exact Submodule.mem_map_of_mem (((hf.mem_toFinset.1 hM).isPrime.mem_or_mem hdM).resolve_left <| hum M hM)
[GOAL]
case intro.intro.a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
⊢ ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
refine' Submodule.sum_mem _ fun M' hM' => _
[GOAL]
case intro.intro.a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ∈ Finset.erase s M
⊢ u M' • (a M * b M') ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
rw [Finset.mem_erase] at hM' 
[GOAL]
case intro.intro.a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
⊢ u M' • (a M * b M') ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M' hM'.2)
[GOAL]
case intro.intro.a.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : ↑(algebraMap R A) c = a M * b M'
⊢ u M' • (a M * b M') ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
rw [← hc, Algebra.smul_def, ← _root_.map_mul]
[GOAL]
case intro.intro.a.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ (M : Ideal R), M ∈ s → u M ∈ ⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M'
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : ↑(algebraMap R A) c = a M * b M'
⊢ ↑(algebraMap R A) (u M' * c) ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
specialize hu M' hM'.2
[GOAL]
case intro.intro.a.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : ↑(algebraMap R A) c = a M * b M'
hu : u M' ∈ ⨅ (M'_1 : Ideal R) (_ : M'_1 ∈ Finset.erase s M'), M'_1
⊢ ↑(algebraMap R A) (u M' * c) ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
simp_rw [Ideal.mem_iInf, Finset.mem_erase] at hu 
[GOAL]
case intro.intro.a.intro
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite {I | IsMaximal I}
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := Set.Finite.toFinset hf
this✝ : DecidableEq (Ideal R)
coprime : ∀ (M : Ideal R), M ∈ s → ∀ (M' : Ideal R), M' ∈ Finset.erase s M → M ⊔ M' = ⊤
nle : ∀ (M : Ideal R), M ∈ s → ¬⨅ (M' : Ideal R) (_ : M' ∈ Finset.erase s M), M' ≤ M
a : Ideal R → A
ha : ∀ (M : Ideal R), M ∈ s → a M ∈ I
b : Ideal R → A
hb : ∀ (M : Ideal R), M ∈ s → b M ∈ I'
hm : ∀ (M : Ideal R), M ∈ s → ¬a M * b M ∈ IsLocalization.coeSubmodule A M
u : Ideal R → R
hum : ∀ (M : Ideal R), M ∈ s → ¬u M ∈ M
v : A := ∑ M in s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M
hM : M ∈ Set.Finite.toFinset hf
this : ∀ (a : A), a ∈ I → ∀ (b : A), b ∈ I' → ∃ c, ↑(algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x in Finset.erase s M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : ↑(algebraMap R A) c = a M * b M'
hu : ∀ (i : Ideal R), i ≠ M' ∧ i ∈ Set.Finite.toFinset hf → u M' ∈ i
⊢ ↑(algebraMap R A) (u M' * c) ∈ IsLocalization.coeSubmodule A M
[PROOFSTEP]
exact Submodule.mem_map_of_mem (M.mul_mem_right _ <| hu M ⟨hM'.1.symm, hM⟩)
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
obtain rfl | hI := eq_or_ne I ⊥
[GOAL]
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
⊢ Submodule.IsPrincipal ⊥
[PROOFSTEP]
exact bot_isPrincipal
[GOAL]
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit
[GOAL]
case inr.hf
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ Set.Finite {I | IsMaximal I}
[PROOFSTEP]
apply h.subset
[GOAL]
case inr.hf
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ {I | IsMaximal I} ⊆ {I | IsPrime I}
[PROOFSTEP]
exact @Ideal.IsMaximal.isPrime _ _
[GOAL]
case inr.hI
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit ↑I
[PROOFSTEP]
exact isUnit_of_mul_eq_one _ _ (FractionalIdeal.coe_ideal_mul_inv I hI)
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
[PROOFSTEP]
have non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
  map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _) p.primeCompl_le_nonZeroDivisors
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
[PROOFSTEP]
letI : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
[PROOFSTEP]
haveI : IsScalarTower R (Localization.AtPrime p) Sₚ :=
  IsScalarTower.of_algebraMap_eq fun x => by
    -- Porting note: replaced `erw` with a `rw` followed by `exact` to help infer implicits
    rw [IsScalarTower.algebraMap_apply R S]
    exact (IsLocalization.map_eq (T := Algebra.algebraMapSubmonoid S (primeCompl p)) (Submonoid.le_comap_map _) x).symm
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
x : R
⊢ ↑(algebraMap R Sₚ) x = ↑(algebraMap (Localization.AtPrime p) Sₚ) (↑(algebraMap R (Localization.AtPrime p)) x)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply R S]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
x : R
⊢ ↑(algebraMap S Sₚ) (↑(algebraMap R S) x) =
    ↑(algebraMap (Localization.AtPrime p) Sₚ) (↑(algebraMap R (Localization.AtPrime p)) x)
[PROOFSTEP]
exact (IsLocalization.map_eq (T := Algebra.algebraMapSubmonoid S (primeCompl p)) (Submonoid.le_comap_map _) x).symm
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this : IsScalarTower R (Localization.AtPrime p) Sₚ
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
[PROOFSTEP]
obtain ⟨pid, p', ⟨hp'0, hp'p⟩, hpu⟩ :=
  (DiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime p)).mp
    (IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain R hp0 _)
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
[PROOFSTEP]
have : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥ :=
  by
  rw [Submodule.ne_bot_iff] at hp0 ⊢
  obtain ⟨x, x_mem, x_ne⟩ := hp0
  exact
    ⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
      IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
        (mem_nonZeroDivisors_of_ne_zero x_ne)⟩
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
⊢ LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
[PROOFSTEP]
rw [Submodule.ne_bot_iff] at hp0 ⊢
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : ∃ x, x ∈ p ∧ x ≠ 0
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
⊢ ∃ x, x ∈ LocalRing.maximalIdeal (Localization.AtPrime p) ∧ x ≠ 0
[PROOFSTEP]
obtain ⟨x, x_mem, x_ne⟩ := hp0
[GOAL]
case intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
x : R
x_mem : x ∈ p
x_ne : x ≠ 0
⊢ ∃ x, x ∈ LocalRing.maximalIdeal (Localization.AtPrime p) ∧ x ≠ 0
[PROOFSTEP]
exact
  ⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
    IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
      (mem_nonZeroDivisors_of_ne_zero x_ne)⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
[PROOFSTEP]
rw [← Multiset.singleton_le, ← normalize_eq P, ←
  normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, ←
  dvd_iff_normalizedFactors_le_normalizedFactors hP0, dvd_iff_le,
  IsScalarTower.algebraMap_eq R (Localization.AtPrime p) Sₚ, ← Ideal.map_map, Localization.AtPrime.map_eq_maximalIdeal,
  Ideal.map_le_iff_le_comap, hpu (LocalRing.maximalIdeal _) ⟨this, _⟩, hpu (comap _ _) ⟨_, _⟩]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ comap (algebraMap (Localization.AtPrime p) Sₚ) P ≠ ⊥
[PROOFSTEP]
have hRS : Algebra.IsIntegral R S := isIntegral_of_noetherian (isNoetherian_of_isNoetherianRing_of_finite R S)
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
hRS : Algebra.IsIntegral R S
⊢ comap (algebraMap (Localization.AtPrime p) Sₚ) P ≠ ⊥
[PROOFSTEP]
exact mt (Ideal.eq_bot_of_comap_eq_bot (isIntegral_localization hRS)) hP0
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ IsPrime (comap (algebraMap (Localization.AtPrime p) Sₚ) P)
[PROOFSTEP]
exact Ideal.comap_isPrime (algebraMap (Localization.AtPrime p) Sₚ) P
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ IsPrime (LocalRing.maximalIdeal (Localization.AtPrime p))
[PROOFSTEP]
exact (LocalRing.maximalIdeal.isMaximal _).isPrime
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Ideal.map (algebraMap R Sₚ) p ≠ 0
[PROOFSTEP]
rw [Ne.def, zero_eq_bot, Ideal.map_eq_bot_iff_of_injective]
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ ¬p = ⊥
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Function.Injective ↑(algebraMap R Sₚ)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq R S Sₚ]
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
inst✝¹⁴ : IsDedekindDomain R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : IsDomain S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Free R S
inst✝⁹ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁸ : IsPrime p
Sₚ : Type u_3
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsDomain Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : DecidableEq (Ideal Sₚ)
P : Ideal Sₚ
hP : IsPrime P
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S (primeCompl p) ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra (primeCompl p) S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : IsPrime p'
this : LocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Function.Injective ↑(RingHom.comp (algebraMap S Sₚ) (algebraMap R S))
[PROOFSTEP]
exact (IsLocalization.injective Sₚ non_zero_div).comp (NoZeroSMulDivisors.algebraMap_injective _ _)
[GOAL]
R : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
⊢ IsPrincipalIdealRing Sₚ
[PROOFSTEP]
letI := Classical.decEq (Ideal Sₚ)
[GOAL]
R : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
⊢ IsPrincipalIdealRing Sₚ
[PROOFSTEP]
letI := Classical.decPred fun P : Ideal Sₚ => P.IsPrime
[GOAL]
R : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
⊢ IsPrincipalIdealRing Sₚ
[PROOFSTEP]
refine'
  IsPrincipalIdealRing.of_finite_primes
    (Set.Finite.ofFinset
      (Finset.filter (fun P => P.IsPrime) ({⊥} ∪ (normalizedFactors (Ideal.map (algebraMap R Sₚ) p)).toFinset)) fun P =>
      _)
[GOAL]
R : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
P : Ideal Sₚ
⊢ P ∈ Finset.filter (fun P => IsPrime P) ({⊥} ∪ Multiset.toFinset (normalizedFactors (map (algebraMap R Sₚ) p))) ↔
    P ∈ {I | IsPrime I}
[PROOFSTEP]
rw [Finset.mem_filter, Finset.mem_union, Finset.mem_singleton, Set.mem_setOf, Multiset.mem_toFinset]
[GOAL]
R : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
P : Ideal Sₚ
⊢ (P = ⊥ ∨ P ∈ normalizedFactors (map (algebraMap R Sₚ) p)) ∧ IsPrime P ↔ IsPrime P
[PROOFSTEP]
exact
  and_iff_right_of_imp fun hP =>
    or_iff_not_imp_left.mpr (IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime S p hp0 hP)
