IsLocalization_AtPrime_surjective_and_ker_pi_span_mul_quotient_of_moduleFinite.lean

theorem mem_range_iff (x : K) :
    x ∈ Set.range (algebraMap R K) ↔ ∃ a s : A, s ∉ m ∧ x = algebraMap A K a * (algebraMap A K
      s)⁻¹

theorem algebraMap_ne_zero {s : A} (hs : s ∉ m) : algebraMap A K s ≠ 0

def locSub : Submodule k K where
  carrier := {x | ∃ a s : A, s ∉ m ∧ x = algebraMap A K a * (algebraMap A K s)⁻¹}
  add_mem' := by
    rintro _ _ ⟨a, s, hs, rfl⟩ ⟨a', s', hs', rfl⟩
    refine ⟨a * s' + a' * s, s * s', fun h => (hm.isPrime.mem_or_mem h).elim hs hs', ?_⟩
    have := algebraMap_ne_zero (K := K) m hs
    have := algebraMap_ne_zero (K := K) m hs'
    simp only [map_add, map_mul]
    field_simp
  zero_mem' := ⟨0, 1, fun h => hm.ne_top ((Ideal.eq_top_iff_one m).mpr h), by simp⟩
  smul_mem' := by
    rintro c _ ⟨a, s, hs, rfl⟩
    refine ⟨algebraMap k A c * a, s, hs, ?_⟩
    rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, mul_assoc]

theorem mem_locSub_iff (x : K) :
    x ∈ locSub k m ↔ ∃ a s : A, s ∉ m ∧ x = algebraMap A K a * (algebraMap A K s)⁻¹

def locBSub : Submodule k K where
  carrier := {x | ∃ b : K, b ∈ B ∧ ∃ s : A, s ∉ m ∧ x = b * (algebraMap A K s)⁻¹}
  add_mem' := by
    rintro _ _ ⟨b, hb, s, hs, rfl⟩ ⟨b', hb', s', hs', rfl⟩
    refine ⟨algebraMap A K s' * b + algebraMap A K s * b', B.add_mem (B.mul_mem (B.algebraMap_mem
      s') hb)
      (B.mul_mem (B.algebraMap_mem s) hb'), s * s', fun h => (hm.isPrime.mem_or_mem h).elim hs
        hs', ?_⟩
    have := algebraMap_ne_zero (K := K) m hs
    have := algebraMap_ne_zero (K := K) m hs'
    simp only [map_mul]
    field_simp
  zero_mem' := ⟨0, B.zero_mem, 1, fun h => hm.ne_top ((Ideal.eq_top_iff_one m).mpr h), by simp⟩
  smul_mem' := by
    rintro c _ ⟨b, hb, s, hs, rfl⟩
    refine ⟨c • b, ?_, s, hs, by rw [smul_mul_assoc]⟩
    rw [← IsScalarTower.algebraMap_smul A c b]
    exact B.smul_mem hb _

theorem mem_locBSub_iff (x : K) :
    x ∈ locBSub k m B ↔ ∃ b : K, b ∈ B ∧ ∃ s : A, s ∉ m ∧ x = b * (algebraMap A K s)⁻¹

theorem locSub_le_locBSub : locSub k m ≤ locBSub k m B

theorem le_locBSub : (Submodule.span k (B : Set K)) ≤ locBSub k m B

theorem span_range_eq_locSub : Submodule.span k (Set.range (algebraMap R K)) = locSub k m

theorem span_mul_range_eq_locBSub :
    Submodule.span k ((B : Set K) * Set.range (algebraMap R K)) = locBSub k m B

theorem exists_denominator (hB : Module.Finite A B) :
    ∃ d : A, d ≠ 0 ∧ ∀ b : K, b ∈ B → ∃ a : A, algebraMap A K d * b = algebraMap A K a

theorem finite_setOf_isMaximal_mem (hdim : ∀ p : Ideal A, p.IsPrime → p ≠ ⊥ → p.IsMaximal) {d : A}
  (hd : d ≠ 0) :
    {m : Ideal A | m.IsMaximal ∧ d ∈ m}.Finite

theorem exists_pow_forall_mul_mem (hdim : ∀ p : Ideal A, p.IsPrime → p ≠ ⊥ → p.IsMaximal)
    (m : Ideal A) [hm : m.IsMaximal] {d : A} (hd : d ≠ 0) :
    ∃ N : ℕ, ∀ x ∈ m ^ N, ∃ a s : A, s ∉ m ∧ s * x = d * a

theorem mul_mem_locSub_of {d : A} (hdB : ∀ b : K, b ∈ B → ∃ a : A, algebraMap A K d * b =
  algebraMap A K a)
    {N : ℕ} (hN : ∀ x ∈ m ^ N, ∃ a s : A, s ∉ m ∧ s * x = d * a)
    {x : A} (hx : x ∈ m ^ N) {b : K} (hb : b ∈ B) :
    algebraMap A K x * b ∈ locSub k m (K := K)

theorem exists_algebraMap_add_mem {k A : Type u} [Field k] [CommRing A] [Algebra k A] (m : Ideal A)
    (hres : Function.Surjective (algebraMap k (A ⧸ m))) (a : A) :
    ∃ (c : k) (n : A), n ∈ m ∧ a = algebraMap k A c + n

theorem finite_quotient_pow (k A : Type u) [Field k] [CommRing A] [IsNoetherianRing A] [Algebra k A]
    (m : Ideal A) [m.IsMaximal] (hres : Function.Surjective (algebraMap k (A ⧸ m))) (N : ℕ) :
    Module.Finite k (A ⧸ m ^ N)

theorem finite_of_surjective_of_smul_pow_le {k A : Type u} [Field k] [CommRing A]
  [IsNoetherianRing A] [Algebra k A]
    (m : Ideal A) [m.IsMaximal] (hres : Function.Surjective (algebraMap k (A ⧸ m))) (N : ℕ)
    {V : Type u} [AddCommGroup V] [Module k V] {ι : Type u} [Finite ι]
    (f : (ι → A) →ₗ[k] V) (hf : Function.Surjective f)
    (hker : ∀ g : ι → A, (∀ i, g i ∈ m ^ N) → f g = 0) :
    Module.Finite k V

theorem mul_inv_mem_locSub {x : K} (hx : x ∈ locSub k m (K := K)) {s : A} (hs : s ∉ m) :
    x * (algebraMap A K s)⁻¹ ∈ locSub k m (K := K)

theorem exists_mul_sub_one_mem_pow {s : A} (hs : s ∉ m) (N : ℕ) : ∃ t : A, t * s - 1 ∈ m ^ N

theorem _root_.IsLocalization.AtPrime.surjective_and_ker_pi_span_mul_quotient_of_moduleFinite
    (k : Type u) [Field k] {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Algebra k A]
    (K : Type u) [Field K] [Algebra k K] [Algebra A K] [IsScalarTower k A K] [IsFractionRing A K]
    (hdim : ∀ p : Ideal A, p.IsPrime → p ≠ ⊥ → p.IsMaximal)
    (hres : ∀ m : Ideal A, m.IsMaximal → Function.Surjective (algebraMap k (A ⧸ m)))
    {X : Type u} (P : X → Prop) (R : X → Type u) [∀ z, CommRing (R z)] [∀ z, Algebra (R z) K]
    [∀ z : {z : X // P z}, Algebra A (R z.1)] [∀ z : {z : X // P z}, IsScalarTower A (R z.1) K]
    (𝔪 : {z : X // P z} → Ideal A) [∀ z, (𝔪 z).IsMaximal] (h𝔪 : Function.Injective 𝔪)
    [∀ z : {z : X // P z}, IsLocalization.AtPrime (R z.1) (𝔪 z)]
    (B : Subalgebra A K) (hB : Module.Finite A B) :
    let Bz : X → Submodule k K := fun z =>
      Submodule.span k ((B : Set K) * Set.range (algebraMap (R z) K))
    let Q : X → Type u := fun z =>
      ↥(Bz z) ⧸ (Submodule.span k (Set.range (algebraMap (R z) K))).comap (Bz z).subtype
    let φ : ↥(Submodule.span k (B : Set K)) →ₗ[k] ((z : {z : X // P z}) → Q z.1) :=
      LinearMap.pi fun z =>
        (Submodule.mkQ ((Submodule.span k (Set.range (algebraMap (R z.1) K))).comap
          (Bz z.1).subtype)).comp (Submodule.inclusion (Submodule.span_mono
        (fun b hb => Set.mem_mul.mpr ⟨b, hb, 1, ⟨1, map_one _⟩, mul_one b⟩)))
    Function.Surjective φ ∧
      LinearMap.ker φ = (⨅ z : {z : X // P z}, Submodule.span k (Set.range (algebraMap (R z.1)
        K))).comap
        (Submodule.span k (B : Set K)).subtype ∧
      {z : {z : X // P z} | Nontrivial (Q z.1)}.Finite ∧
      ∀ z : {z : X // P z}, FiniteDimensional k (Q z.1) := by
  intro Bz Q φ
  classical
  have hle : ∀ z : X, Submodule.span k (B : Set K) ≤ Bz z := fun z =>
    Submodule.span_mono (fun b hb => Set.mem_mul.mpr ⟨b, hb, 1, ⟨1, map_one _⟩, mul_one b⟩)
  have hBz : ∀ z : {z : X // P z}, Bz z.1 = locBSub k (𝔪 z) B := fun z =>
    span_mul_range_eq_locBSub k (𝔪 z) B (R z.1)
  have hO : ∀ z : {z : X // P z}, Submodule.span k (Set.range (algebraMap (R z.1) K)) = locSub k
    (𝔪 z) :=
    fun z => span_range_eq_locSub k (𝔪 z) (R z.1)
  have hQeq : ∀ (z : {z : X // P z}) (x y : ↥(Bz z.1)),
      (Submodule.Quotient.mk x : Q z.1) = Submodule.Quotient.mk y ↔ (x : K) - y ∈ locSub k (𝔪 z)
        (K := K) := by
    intro z x y
    rw [Submodule.Quotient.eq, Submodule.mem_comap, ← hO z]
    rfl
  have hφ : ∀ (b : ↥(Submodule.span k (B : Set K))) (z : {z : X // P z}),
      φ b z = Submodule.Quotient.mk ⟨b, hle z.1 b.2⟩ := fun _ _ => rfl
  obtain ⟨d, hd0, hdB⟩ := exists_denominator B hB
  choose N hN using fun z : {z : X // P z} => exists_pow_forall_mul_mem hdim (𝔪 z) hd0
  have key : ∀ (z : {z : X // P z}) {x : A}, x ∈ 𝔪 z ^ N z → ∀ {b : K}, b ∈ B →
      algebraMap A K x * b ∈ locSub k (𝔪 z) (K := K) :=
    fun z x hx b hb => mul_mem_locSub_of k (𝔪 z) B hdB (hN z) hx hb
  have hT : {z : {z : X // P z} | d ∈ 𝔪 z}.Finite := by
    have hfin := (finite_setOf_isMaximal_mem hdim hd0).preimage (f := 𝔪) h𝔪.injOn
    exact hfin.subset fun z hz => ⟨inferInstance, hz⟩
  have htriv : ∀ z : {z : X // P z}, d ∉ 𝔪 z → ∀ x : ↥(Bz z.1), (x : K) ∈ locSub k (𝔪 z) (K := K)
    := by
    intro z hz x
    have hx : (x : K) ∈ locBSub k (𝔪 z) B := by rw [← hBz z]; exact x.2
    obtain ⟨b, hb, s, hs, e⟩ := hx
    obtain ⟨c, hc⟩ := hdB b hb
    refine ⟨c, d * s, fun h => ((inferInstance : (𝔪 z).IsMaximal).isPrime.mem_or_mem h).elim hz
      hs, ?_⟩
    have hd' : algebraMap A K d ≠ 0 := fun h => hd0 ((injective_iff_map_eq_zero _).mp
      (IsFractionRing.injective A K) d h)
    rw [e, ← hc, map_mul, mul_inv, ← mul_assoc, mul_comm (algebraMap A K d) b, mul_assoc b,
      mul_inv_cancel₀ hd', mul_one]
  have hsub : ∀ z : {z : X // P z}, d ∉ 𝔪 z → Subsingleton (Q z.1) := by
    intro z hz
    refine ⟨fun x y => ?_⟩
    induction x using Submodule.Quotient.induction_on with | _ x =>
    induction y using Submodule.Quotient.induction_on with | _ y =>
    exact (hQeq z x y).mpr (sub_mem (htriv z hz x) (htriv z hz y))
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro y
    have hrep : ∀ z : {z : X // P z}, ∃ b : K, b ∈ B ∧ ∃ s : A, s ∉ 𝔪 z ∧
        ∃ x : ↥(Bz z.1), Submodule.Quotient.mk x = y z ∧ (x : K) = b * (algebraMap A K s)⁻¹ := by
      intro z
      obtain ⟨x, hx⟩ := Submodule.Quotient.mk_surjective _ (y z)
      have hx' : (x : K) ∈ locBSub k (𝔪 z) B := by rw [← hBz z]; exact x.2
      obtain ⟨b, hb, s, hs, e⟩ := hx'
      exact ⟨b, hb, s, hs, x, hx, e⟩
    choose bz hbz sz hsz xz hxz hxbs using hrep
    let T : Finset {z : X // P z} := hT.toFinset
    have hTmem : ∀ z, z ∈ T ↔ d ∈ 𝔪 z := fun z => by simp [T]
    have hcop : Pairwise (Function.onFun IsCoprime fun z : ↥T => 𝔪 z.1 ^ N z.1) := by
      intro z w hzw
      have hne : 𝔪 z.1 ≠ 𝔪 w.1 := fun h => hzw (Subtype.ext (h𝔪 h))
      exact (Ideal.isCoprime_iff_add.mpr (by
        rw [Ideal.add_eq_sup, Ideal.one_eq_top]
        exact (inferInstance : (𝔪 z.1).IsMaximal).coprime_of_ne inferInstance hne)).pow
    have he : ∀ z : ↥T, ∃ e : A, ∀ w : ↥T, e - (if w = z then 1 else 0) ∈ 𝔪 w.1 ^ N w.1 :=
      fun z => Ideal.exists_forall_sub_mem_ideal hcop _
    choose e he using he
    choose t ht using fun z : {z : X // P z} => exists_mul_sub_one_mem_pow (𝔪 z) (hsz z) (N z)
    let bsum : K := ∑ z : ↥T, algebraMap A K (e z * t z.1) * bz z.1
    have hbsumB : bsum ∈ B := B.sum_mem fun z _ => B.mul_mem (B.algebraMap_mem _) (hbz z.1)
    refine ⟨⟨bsum, Submodule.subset_span hbsumB⟩, funext fun w => ?_⟩
    rw [hφ, ← hxz w, hQeq]
    by_cases hw : d ∈ 𝔪 w
    · let w' : ↥T := ⟨w, (hTmem w).mpr hw⟩
      have hsplit : bsum - xz w = (∑ z ∈ Finset.univ.erase w', algebraMap A K (e z * t z.1) * bz
        z.1) +
          (algebraMap A K (e w' * t w * sz w - 1) * bz w * (algebraMap A K (sz w))⁻¹) := by
        have hs0 := algebraMap_ne_zero (K := K) (𝔪 w) (hsz w)
        change (∑ z : ↥T, algebraMap A K (e z * t z.1) * bz z.1) - _ = _
        rw [hxbs w, ← Finset.add_sum_erase _ _ (Finset.mem_univ w')]
        simp only [map_sub, map_mul, map_one]
        field_simp
        ring
      rw [hsplit]
      refine add_mem (Submodule.sum_mem _ fun z hz => ?_) ?_
      · have hzw : z ≠ w' := Finset.ne_of_mem_erase hz
        have hez : e z ∈ 𝔪 w ^ N w := by simpa [ite_eq_right hzw.symm] using he z w'
        rw [map_mul, mul_assoc]
        exact key w hez (B.mul_mem (B.algebraMap_mem _) (hbz z.1))
      · refine mul_inv_mem_locSub k (𝔪 w) (key w ?_ (hbz w)) (hsz w)
        have h1 : e w' - 1 ∈ 𝔪 w ^ N w := by simpa using he w' w'
        have h2 := ht w
        have : e w' * t w * sz w - 1 = (e w' - 1) * (t w * sz w) + (t w * sz w - 1) := by ring
        rw [this]
        exact add_mem (Ideal.mul_mem_right _ _ h1) h2
    · exact sub_mem (htriv w hw ⟨bsum, hle w.1 (Submodule.subset_span hbsumB)⟩) (htriv w hw (xz w))
  · ext b
    rw [LinearMap.mem_ker, Submodule.mem_comap, Submodule.mem_iInf, funext_iff]
    refine forall_congr' fun z => ?_
    rw [Pi.zero_apply, hφ, Submodule.Quotient.mk_eq_zero, Submodule.mem_comap]
    rfl
  · refine hT.subset fun z hz => ?_
    by_contra h
    exact (not_nontrivial_iff_subsingleton.mpr (hsub z h)) hz
  · intro z
    obtain ⟨S, hS⟩ := hB.fg_top
    let Λ : (↥S → A) →ₗ[k] K :=
      ∑ i : ↥S, ((LinearMap.mulRight k ((i : ↥B) : K)).comp ((Algebra.linearMap A
        K).restrictScalars k)).comp
        (LinearMap.proj i)
    have hΛ : ∀ g : ↥S → A, Λ g = ∑ i : ↥S, algebraMap A K (g i) * ((i : ↥B) : K) := by
      intro g
      simp [Λ, LinearMap.sum_apply]
    have hΛB : ∀ g : ↥S → A, Λ g ∈ B := fun g => by
      rw [hΛ]; exact B.sum_mem fun i _ => B.mul_mem (B.algebraMap_mem _) (i : ↥B).2
    let f : (↥S → A) →ₗ[k] Q z.1 :=
      ((LinearMap.proj z).comp φ).comp (Λ.codRestrict (Submodule.span k (B : Set K)) fun g =>
        Submodule.subset_span (hΛB g))
    have hf : ∀ g : ↥S → A, f g = Submodule.Quotient.mk ⟨Λ g, hle z.1 (Submodule.subset_span (hΛB
      g))⟩ :=
      fun g => rfl
    refine finite_of_surjective_of_smul_pow_le (𝔪 z) (hres _ inferInstance) (N z) f ?_ ?_
    · intro q
      obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ q
      have hx : (x : K) ∈ locBSub k (𝔪 z) B := by rw [← hBz z]; exact x.2
      obtain ⟨b, hb, s, hs, e⟩ := hx
      obtain ⟨t, ht⟩ := exists_mul_sub_one_mem_pow (𝔪 z) hs (N z)
      have hrange : Set.range (fun i : ↥S => (i : ↥B)) = (S : Set ↥B) := by ext; simp
      have hsurj := (span_range_eq_top_iff_surjective_fintypeLinearCombination (R := A)
        (v := fun i : ↥S => (i : ↥B))).mp (by rw [hrange]; exact hS)
      obtain ⟨g, hg⟩ := hsurj ⟨b, hb⟩
      have hgb : Λ g = b := by
        have := congrArg Subtype.val hg
        simp only [Fintype.linearCombination_apply, AddSubmonoidClass.coe_finsetSum,
          Algebra.smul_def] at this
        rw [hΛ]
        exact this
      refine ⟨fun i => t * g i, ?_⟩
      rw [hf, hQeq]
      have hΛt : Λ (fun i => t * g i) = algebraMap A K t * b := by
        rw [← hgb, hΛ, hΛ, Finset.mul_sum]
        refine Finset.sum_congr rfl fun i _ => ?_
        rw [map_mul, mul_assoc]
      change Λ (fun i => t * g i) - (x : K) ∈ _
      rw [hΛt, e]
      have hs0 := algebraMap_ne_zero (K := K) (𝔪 z) hs
      have : algebraMap A K t * b - b * (algebraMap A K s)⁻¹ =
          algebraMap A K (t * s - 1) * b * (algebraMap A K s)⁻¹ := by
        simp only [map_sub, map_mul, map_one]
        field_simp
        try ring
      rw [this]
      exact mul_inv_mem_locSub k (𝔪 z) (key z ht hb) hs
    · intro g hg
      rw [hf, Submodule.Quotient.mk_eq_zero, Submodule.mem_comap, hO z]
      change Λ g ∈ locSub k (𝔪 z)
      rw [hΛ]
      exact Submodule.sum_mem _ fun i _ => key z (hg i) (i : ↥B).2