Algebra_finite_maximalSpectrum_and_bijective_localization_of_module_finite.lean

lemma row5_idem_eq_of_isNilpotent_sub {B : Type} [CommRing B] {x y : B}
    (hx : IsIdempotentElem x) (hy : IsIdempotentElem y) (hd : IsNilpotent (x - y)) :
    x = y

lemma row5_exists_completeOrthogonalIdempotents
    (R : Type) [CommRing R] [IsArtinianRing R] [Fintype (MaximalSpectrum R)] :
    ∃ e : MaximalSpectrum R → R, CompleteOrthogonalIdempotents e ∧
      (∀ P : MaximalSpectrum R, e P ∉ P.asIdeal) ∧
      (∀ P Q : MaximalSpectrum R, Q ≠ P → e P ∈ Q.asIdeal)

lemma row5_mapMax_le (P : Ideal A) [P.IsMaximal] :
    (IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A) ≤ P

lemma row5_mem_pow_iff (x : A) (n : ℕ) :
    x ∈ ((IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A)) ^ n ↔
      x ∈ ((IsLocalRing.maximalIdeal 𝒪) ^ n • ⊤ : Submodule 𝒪 A)

lemma row5_isArtinian_quotient :
    IsArtinianRing (A ⧸ (IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A))

def row5_maxSpecEquiv :
    MaximalSpectrum A ≃
      MaximalSpectrum (A ⧸ (IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A)) where
  toFun P :=
    ⟨P.asIdeal.map (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A))), by
      have := P.isMaximal
      rcases Ideal.map_eq_top_or_isMaximal_of_surjective
          (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A)))
          Ideal.Quotient.mk_surjective P.isMaximal with h | h
      · exfalso
        have hcm := Ideal.comap_map_of_surjective
          (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A)))
          Ideal.Quotient.mk_surjective P.asIdeal
        rw [h, Ideal.comap_top, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
          sup_eq_left.mpr (row5_mapMax_le A P.asIdeal)] at hcm
        exact P.isMaximal.ne_top hcm.symm
      · exact h⟩
  invFun Q :=
    ⟨Q.asIdeal.comap (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A))), by
      have := Q.isMaximal
      exact Ideal.comap_isMaximal_of_surjective _ Ideal.Quotient.mk_surjective⟩
  left_inv P := by
    have := P.isMaximal
    refine MaximalSpectrum.ext ?_
    have hcm := Ideal.comap_map_of_surjective
      (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A)))
      Ideal.Quotient.mk_surjective P.asIdeal
    rw [← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
      sup_eq_left.mpr (row5_mapMax_le A P.asIdeal)] at hcm
    exact hcm
  right_inv Q := by
    have := Q.isMaximal
    refine MaximalSpectrum.ext ?_
    exact Ideal.map_comap_of_surjective _ Ideal.Quotient.mk_surjective Q.asIdeal

lemma row5_lift_idempotent (J : Ideal A)
    (hJpow : ∀ (y : A) (n : ℕ), y ∈ J ^ n ↔
      y ∈ ((IsLocalRing.maximalIdeal 𝒪) ^ n • ⊤ : Submodule 𝒪 A))
    (ē : A ⧸ J) (hē : IsIdempotentElem ē) :
    ∃ e : A, IsIdempotentElem e ∧ Ideal.Quotient.mk J e = ē

lemma row5_idem_eq_zero_of_mem (J : Ideal A)
    (hJpow : ∀ (y : A) (n : ℕ), y ∈ J ^ n ↔
      y ∈ ((IsLocalRing.maximalIdeal 𝒪) ^ n • ⊤ : Submodule 𝒪 A))
    (x : A) (hx : IsIdempotentElem x) (hxJ : x ∈ J) : x = 0

lemma row5_finite_maxSpec : Finite (MaximalSpectrum A)

lemma row5_lifted_idempotents [Fintype (MaximalSpectrum A)] :
    ∃ e : MaximalSpectrum A → A, CompleteOrthogonalIdempotents e ∧
      (∀ P : MaximalSpectrum A, e P ∉ P.asIdeal) ∧
      (∀ P Q : MaximalSpectrum A, Q ≠ P → e P ∈ Q.asIdeal)

lemma row5_isLocalization (P : MaximalSpectrum A) (e : A) (he : IsIdempotentElem e)
    (hnot : e ∉ P.asIdeal) (hmem : ∀ Q : MaximalSpectrum A, Q ≠ P → e ∈ Q.asIdeal) :
    IsLocalization P.asIdeal.primeCompl (A ⧸ Ideal.span {1 - e})

theorem _root_.Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite
    {𝒪 : Type} [CommRing 𝒪] [IsLocalRing 𝒪] [IsNoetherianRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]
    (A : Type) [CommRing A] [Algebra 𝒪 A] [Module.Finite 𝒪 A] :
    Finite (MaximalSpectrum A) ∧
    Function.Bijective
      (RingHom.pi fun I : MaximalSpectrum A =>
        algebraMap A (Localization.AtPrime I.asIdeal)) ∧
    (∀ I : MaximalSpectrum A, Module.Finite 𝒪 (Localization.AtPrime I.asIdeal)) ∧
    (∀ I : MaximalSpectrum A,
      IsAdicComplete (IsLocalRing.maximalIdeal (Localization.AtPrime I.asIdeal))
        (Localization.AtPrime I.asIdeal)) := by
  classical
  have hfin : Finite (MaximalSpectrum A) := row5_finite_maxSpec (𝒪 := 𝒪) A
  let : Fintype (MaximalSpectrum A) := Fintype.ofFinite _
  obtain ⟨e, heco, henot, hemem⟩ := row5_lifted_idempotents (𝒪 := 𝒪) A
  have hloc : ∀ P : MaximalSpectrum A,
      IsLocalization P.asIdeal.primeCompl (A ⧸ Ideal.span {1 - e P}) := fun P =>
    row5_isLocalization A P (e P) (heco.idem P) (henot P) fun Q hQ => hemem P Q hQ
  have ψ : ∀ P : MaximalSpectrum A,
      (A ⧸ Ideal.span {1 - e P}) ≃ₐ[A] Localization.AtPrime P.asIdeal := fun P =>
    haveI := hloc P
    IsLocalization.algEquiv P.asIdeal.primeCompl _ _
  have hsurjloc : ∀ P : MaximalSpectrum A,
      Function.Surjective (algebraMap A (Localization.AtPrime P.asIdeal)) := by
    intro P z
    obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective ((ψ P).symm z)
    refine ⟨a, ?_⟩
    have hψ := congrArg (ψ P) ha
    rwa [← Ideal.Quotient.algebraMap_eq, AlgEquiv.commutes,
      AlgEquiv.apply_symm_apply] at hψ
  have hfinloc : ∀ P : MaximalSpectrum A,
      Module.Finite 𝒪 (Localization.AtPrime P.asIdeal) := fun P =>
    Module.Finite.of_surjective (IsScalarTower.toAlgHom 𝒪 A _).toLinearMap (hsurjloc P)
  refine ⟨hfin, ?_, hfinloc, ?_⟩
  · have hΨ := heco.bijective_pi
    have hcomp : ⇑(RingHom.pi fun P : MaximalSpectrum A =>
        algebraMap A (Localization.AtPrime P.asIdeal)) =
        ⇑(RingEquiv.piCongrRight fun P => (ψ P).toRingEquiv) ∘
          ⇑(RingHom.pi fun P : MaximalSpectrum A =>
            Ideal.Quotient.mk (Ideal.span {1 - e P})) := by
      funext a
      funext P
      change algebraMap A (Localization.AtPrime P.asIdeal) a =
        ψ P (Ideal.Quotient.mk (Ideal.span {1 - e P}) a)
      rw [← Ideal.Quotient.algebraMap_eq, AlgEquiv.commutes]
    rw [hcomp]
    exact (RingEquiv.piCongrRight fun P => (ψ P).toRingEquiv).bijective.comp hΨ
  · intro P
    have := hfinloc P
    have : IsLocalHom (algebraMap 𝒪 (Localization.AtPrime P.asIdeal)) := by
      constructor
      intro a ha
      by_contra hna
      have hm : a ∈ IsLocalRing.maximalIdeal 𝒪 := hna
      have h1 : algebraMap 𝒪 A a ∈ P.asIdeal :=
        row5_mapMax_le (𝒪 := 𝒪) A P.asIdeal (Ideal.mem_map_of_mem _ hm)
      have h2 : algebraMap A (Localization.AtPrime P.asIdeal) (algebraMap 𝒪 A a) ∈
          IsLocalRing.maximalIdeal (Localization.AtPrime P.asIdeal) :=
        (IsLocalization.AtPrime.to_map_mem_maximal_iff _ P.asIdeal _).mpr h1
      rw [← IsScalarTower.algebraMap_apply] at h2
      exact h2 ha
    exact IsLocalRing.isAdicComplete_of_module_finite (𝒪 := 𝒪)
      (T := Localization.AtPrime P.asIdeal)