PuncturedSpectrumNormalizationFinite.lean

theorem puncturedSpectrum_nonempty_dimension_two
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    Nonempty (Scheme.puncturedSpectrum R)

theorem puncturedSpectrumInclusion_isOpenImmersion :
    IsOpenImmersion (Scheme.puncturedSpectrumInclusion R)

def puncturedSpectrumGenericMorphism
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    Spec (.of (Spec (.of R)).functionField) ⟶ Scheme.puncturedSpectrum R

theorem puncturedSpectrumGenericMorphism_comp_inclusion
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    puncturedSpectrumGenericMorphism R hdim ≫
        Scheme.puncturedSpectrumInclusion R =
      (Spec (.of R)).genericExtensionMorphism
        (Spec (.of R)).functionField

def puncturedSpectrumGenericFiber
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    FiniteEtale (Spec (.of (Spec (.of R)).functionField))

def puncturedSpectrumGenericFiberToCover
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    (puncturedSpectrumGenericFiber R hdim W).left ⟶ W.left

theorem puncturedSpectrumGenericFiberToCover_comp
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    puncturedSpectrumGenericFiberToCover R hdim W ≫ W.hom =
      (puncturedSpectrumGenericFiber R hdim W).hom ≫
        puncturedSpectrumGenericMorphism R hdim

theorem puncturedSpectrumGenericMorphism_denseRange
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    DenseRange (puncturedSpectrumGenericMorphism R hdim)

theorem puncturedSpectrumGenericFiberToCover_appTop_injective
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    Function.Injective
      (puncturedSpectrumGenericFiberToCover R hdim W).appTop.hom

def puncturedSpectrumGenericFiberAlgebra
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    Algebra (Spec (.of R)).functionField
      Γ((puncturedSpectrumGenericFiber R hdim W).left, ⊤)

theorem puncturedSpectrumGenericFiber_sections_etale
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    letI := puncturedSpectrumGenericFiberAlgebra R hdim W
    Algebra.Etale (Spec (.of R)).functionField
      Γ((puncturedSpectrumGenericFiber R hdim W).left, ⊤) := by
  let K : Type u := (Spec (.of R)).functionField
  let G := puncturedSpectrumGenericFiber R hdim W
  let f : G.left ⟶ Spec (.of K) := G.hom
  let : Algebra K Γ(G.left, ⊤) :=
    puncturedSpectrumGenericFiberAlgebra R hdim W
  let : IsFiniteEtale f := G.prop
  let : IsFinite f := G.prop.toIsFinite
  let : IsAffineHom f := G.prop.toIsFinite.toIsAffineHom
  let : IsAffine G.left := isAffine_of_isAffineHom f
  have hf : f.appTop.hom.Etale := by
    rw [← HasRingHomProperty.iff_of_isAffine
      (P := @AlgebraicGeometry.Etale)]
    exact G.prop.toEtale
  change (f.appTop.hom.comp
    (Scheme.ΓSpecIso (.of K)).inv.hom).Etale
  exact RingHom.Etale.respectsIso.right f.appTop.hom
    (Scheme.ΓSpecIso (.of K)).commRingCatIsoToRingEquiv.symm hf

theorem puncturedSpectrumGenericFiber_sections_decomposition
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    let K : Type u := (Spec (.of R)).functionField
    let C := Γ((puncturedSpectrumGenericFiber R hdim W).left, ⊤)
    letI := puncturedSpectrumGenericFiberAlgebra R hdim W
    ∃ (I : Type u) (_ : Finite I) (L : I → Type u)
      (_ : ∀ i, Field (L i)) (_ : ∀ i, Algebra K (L i))
      (_ : C ≃ₐ[K] ∀ i, L i),
      ∀ i, Module.Finite K (L i) ∧ Algebra.IsSeparable K (L i) := by
  let K : Type u := (Spec (.of R)).functionField
  let G := puncturedSpectrumGenericFiber R hdim W
  let C := Γ(G.left, ⊤)
  let : Algebra K C := puncturedSpectrumGenericFiberAlgebra R hdim W
  let : Algebra.Etale K C :=
    puncturedSpectrumGenericFiber_sections_etale R hdim W
  exact (Algebra.Etale.iff_exists_algEquiv_prod K C).mp inferInstance

theorem genericExtensionMorphism_appTop_eq_germ :
    let X := Spec (.of R)
    let K : Type u := X.functionField
    letI : IsIntegral X := inferInstance
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by simp⟩⟩
    (X.genericExtensionMorphism K).appTop.hom =
      (Scheme.ΓSpecIso (.of K)).inv.hom.comp
        (X.germToFunctionField ⊤).hom := by
  let X := Spec (.of R)
  let K : Type u := X.functionField
  let : IsIntegral X := inferInstance
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by simp⟩⟩
  ext r
  let e : Γ(Spec (.of K), ⊤) ≃+* K :=
    (Scheme.ΓSpecIso (.of K)).commRingCatIsoToRingEquiv
  change (X.genericExtensionMorphism K).appTop.hom r =
    e.symm (X.germToFunctionField ⊤ r)
  apply e.injective
  rw [e.apply_symm_apply]
  change e ((X.genericExtensionMorphism K).app ⊤ r) =
    X.germToFunctionField ⊤ r
  have h := X.genericExtensionSectionsIso_hom_app K ⊤ r
  change e ((X.genericExtensionMorphism K).app ⊤ r) =
    algebraMap K K (X.germToFunctionField ⊤ r) at h
  simpa using h

theorem puncturedSpectrumGenericFiberToCover_appTop_comp
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    let X := Spec (.of R)
    let K : Type u := X.functionField
    let G := puncturedSpectrumGenericFiber R hdim W
    let q := puncturedSpectrumGenericFiberToCover R hdim W
    let f := puncturedSpectrumCoverToSpec R W
    letI : IsIntegral X := inferInstance
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by simp⟩⟩
    q.appTop.hom.comp f.appTop.hom =
      (G.hom.appTop.hom.comp (Scheme.ΓSpecIso (.of K)).inv.hom).comp
        (X.germToFunctionField ⊤).hom := by
  let X := Spec (.of R)
  let K : Type u := X.functionField
  let G := puncturedSpectrumGenericFiber R hdim W
  let η := puncturedSpectrumGenericMorphism R hdim
  let q := puncturedSpectrumGenericFiberToCover R hdim W
  let f := puncturedSpectrumCoverToSpec R W
  let : IsIntegral X := inferInstance
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by simp⟩⟩
  dsimp only
  have hs : q ≫ f =
      (puncturedSpectrumGenericFiber R hdim W).hom ≫
        X.genericExtensionMorphism K := by
    calc
      q ≫ f = (q ≫ W.hom) ≫ Scheme.puncturedSpectrumInclusion R := by
        simp only [f, puncturedSpectrumCoverToSpec, Category.assoc]
      _ = ((puncturedSpectrumGenericFiber R hdim W).hom ≫
          puncturedSpectrumGenericMorphism R hdim) ≫
          Scheme.puncturedSpectrumInclusion R := by
        exact congrArg
          (fun t ↦ t ≫ Scheme.puncturedSpectrumInclusion R)
          (puncturedSpectrumGenericFiberToCover_comp R hdim W)
      _ = (puncturedSpectrumGenericFiber R hdim W).hom ≫
          X.genericExtensionMorphism K := by
        exact congrArg
          (fun t ↦ (puncturedSpectrumGenericFiber R hdim W).hom ≫ t)
          (puncturedSpectrumGenericMorphism_comp_inclusion R hdim)
  rw [← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop, hs]
  change (puncturedSpectrumGenericFiber R hdim W).hom.appTop.hom.comp
      (X.genericExtensionMorphism K).appTop.hom = _
  rw [genericExtensionMorphism_appTop_eq_germ (R := R)]
  rfl

theorem puncturedSpectrumNormalizationExtension_integralClosure_finite
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    let f := puncturedSpectrumCoverToSpec R W
    letI : Algebra Γ(Spec (.of R), ⊤) Γ(W.left, ⊤) :=
      f.appTop.hom.toAlgebra
    Module.Finite Γ(Spec (.of R), ⊤)
      (integralClosure Γ(Spec (.of R), ⊤) Γ(W.left, ⊤)) := by
  let X := Spec (.of R)
  let K : Type u := X.functionField
  let G := puncturedSpectrumGenericFiber R hdim W
  let q := puncturedSpectrumGenericFiberToCover R hdim W
  let f := puncturedSpectrumCoverToSpec R W
  let A : Type u := Γ(X, ⊤)
  let B : Type u := Γ(W.left, ⊤)
  let C : Type u := Γ(G.left, ⊤)
  let : IsIntegrallyClosed R :=
    EtaleFundamentalGroups.SpecialLocalPurity.isIntegrallyClosed_of_isRegularLocalRing_dimension_two
      hdim
  let : IsIntegral X := inferInstance
  let : IsNormalIntegral X := inferInstance
  let : IsLocallyNoetherian X := inferInstance
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by simp⟩⟩
  let : IsNoetherianRing A :=
    IsLocallyNoetherian.component_noetherian
      (⟨⊤, isAffineOpen_top X⟩ : X.affineOpens)
  let : IsIntegrallyClosed A :=
    IsNormalIntegral.affine_isIntegrallyClosed ⊤ (isAffineOpen_top X)
  let : Algebra A K := (X.germToFunctionField ⊤).hom.toAlgebra
  let : IsFractionRing A K :=
    functionField_isFractionRing_of_isAffineOpen X ⊤
      (isAffineOpen_top X)
  let : Algebra A B := f.appTop.hom.toAlgebra
  let : Algebra K C := puncturedSpectrumGenericFiberAlgebra R hdim W
  let : Algebra A C :=
    ((algebraMap K C).comp (algebraMap A K)).toAlgebra
  let : Algebra B C := q.appTop.hom.toAlgebra
  let : IsScalarTower A K C := IsScalarTower.of_algebraMap_eq' rfl
  let : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (by
    change (G.hom.appTop.hom.comp
        (Scheme.ΓSpecIso (.of K)).inv.hom).comp
          (X.germToFunctionField ⊤).hom =
      q.appTop.hom.comp f.appTop.hom
    exact (puncturedSpectrumGenericFiberToCover_appTop_comp R hdim W).symm)
  obtain ⟨I, hI, L, hLField, hLAlgebra, e, hL⟩ :=
    puncturedSpectrumGenericFiber_sections_decomposition R hdim W
  let : Finite I := hI
  let (i : I) : Field (L i) := hLField i
  let (i : I) : Algebra K (L i) := hLAlgebra i
  let (i : I) : Module.Finite K (L i) := (hL i).1
  let (i : I) : Algebra.IsSeparable K (L i) := (hL i).2
  let (i : I) : Algebra A (L i) :=
    ((algebraMap K (L i)).comp (algebraMap A K)).toAlgebra
  let (i : I) : IsScalarTower A K (L i) :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : Algebra A (∀ i, L i) := Pi.algebra (R := A) I L
  let : Algebra K (∀ i, L i) := Pi.algebra (R := K) I L
  let : IsScalarTower A K (∀ i, L i) := inferInstance
  let eA : C ≃ₐ[A] (∀ i, L i) := e.restrictScalars A
  let qA : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
  let φ : B →ₐ[A] (∀ i, L i) := eA.toAlgHom.comp qA
  have hφ : Function.Injective φ := by
    intro x y hxy
    apply puncturedSpectrumGenericFiberToCover_appTop_injective R hdim W
    have hq : algebraMap B C x = algebraMap B C y := eA.injective hxy
    change q.appTop.hom x = q.appTop.hom y at hq
    exact hq
  let φInt := φ.mapIntegralClosure
  have hφInt : Function.Injective φInt := by
    intro x y hxy
    apply Subtype.ext
    apply hφ
    exact congrArg Subtype.val hxy
  let (i : I) : Module.Finite A (integralClosure A (L i)) :=
    IsIntegralClosure.finite A K (L i) (integralClosure A (L i))
  let : Module.Finite A (∀ i, integralClosure A (L i)) := inferInstance
  let : Module.Finite A (integralClosure A (∀ i, L i)) :=
    Module.Finite.equiv
      (EtaleFundamentalGroups.integralClosurePiAlgEquiv L).symm.toLinearEquiv
  exact Module.Finite.of_injective φInt.toLinearMap hφInt

theorem puncturedSpectrumNormalizationExtensionHom_isFinite
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) :
    IsFinite (puncturedSpectrumNormalizationExtensionHom R W)