isFinite_and_etale_fromNormalization_kummer_of_isIntegrallyClosed.lean

abbrev Kum (X : Scheme.{u}) [IsIntegral X] (k : ℕ) (g : X.functionField) : Type u

abbrev kumHom (X : Scheme.{u}) [IsIntegral X] (k : ℕ) (g : X.functionField) :
    Spec (CommRingCat.of (Kum X k g)) ⟶ X

theorem kumHom_preimage_eq_top (k : ℕ) (g : X.functionField) {V : X.Opens} (hη : genericPoint X ∈
  V) :
    (kumHom X k g) ⁻¹ᵁ V = ⊤

def secIso (k : ℕ) (g : X.functionField) {V : X.Opens} (hη : genericPoint X ∈ V) :
    Γ(Spec (CommRingCat.of (Kum X k g)), (kumHom X k g) ⁻¹ᵁ V) ≅ CommRingCat.of (Kum X k g)

theorem app_secIso_hom (k : ℕ) (g : X.functionField) {V : X.Opens} (hη : genericPoint X ∈ V) :
    (kumHom X k g).app V ≫ (secIso k g hη).hom =
      X.presheaf.germ V (genericPoint X) hη ≫ CommRingCat.ofHom (algebraMap X.functionField (Kum X
        k g))

theorem isIntegrallyClosed_sections (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x))
    (V : X.affineOpens) (hη : genericPoint X ∈ (V : X.Opens)) : IsIntegrallyClosed Γ(X, (V :
      X.Opens))

def Good (k : ℕ) (g : X.functionField) {r : ℕ} (U : Fin r → X.Opens) (h : Fin r → X.functionField)
    (V : X.affineOpens) : Prop

theorem key {R : Type u} [CommRing R] (f : X ⟶ Spec (CommRingCat.of R))
    (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x))
    (k : ℕ) (hk : IsUnit ((k : ℕ) : R)) (g : X.functionField) (_hg : g ≠ 0)
    {r : ℕ} (U : Fin r → X.Opens) (h : Fin r → X.functionField) (hh : ∀ a, h a ≠ 0)
    (V : X.affineOpens) (hV : Good k g U h V) :
    letI := ((kumHom X k g).app (V : X.Opens)).hom.toAlgebra
    Module.Finite Γ(X, (V : X.Opens)) (integralClosure Γ(X, (V : X.Opens))
        Γ(Spec (CommRingCat.of (Kum X k g)), (kumHom X k g) ⁻¹ᵁ (V : X.Opens))) ∧
    Algebra.Etale Γ(X, (V : X.Opens)) (integralClosure Γ(X, (V : X.Opens))
        Γ(Spec (CommRingCat.of (Kum X k g)), (kumHom X k g) ⁻¹ᵁ (V : X.Opens))) := by
  obtain ⟨hη, a, hVU, v, w, hvw, hgerm⟩ := hV
  let inst := ((kumHom X k g).app (V : X.Opens)).hom.toAlgebra
  have : Nonempty (V : X.Opens) := ⟨⟨_, hη⟩⟩
  have : IsDomain Γ(X, (V : X.Opens)) := IsIntegral.component_integral (V : X.Opens)
  have : IsFractionRing Γ(X, (V : X.Opens)) X.functionField :=
    functionField_isFractionRing_of_isAffineOpen X (V : X.Opens) V.2
  have : IsIntegrallyClosed Γ(X, (V : X.Opens)) := isIntegrallyClosed_sections hnorm V hη
  have hkB : IsUnit ((k : ℕ) : Γ(X, (V : X.Opens))) := by
    have := hk.map ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appTop ≫
      X.presheaf.map (homOfLE (le_top : (V : X.Opens) ≤ ⊤)).op).hom
    simpa using this
  have hvu : IsUnit v := isUnit_iff_exists_inv.mpr ⟨w, hvw⟩
  have hgeq : g = algebraMap Γ(X, (V : X.Opens)) X.functionField v * h a ^ k := by
    have : algebraMap Γ(X, (V : X.Opens)) X.functionField v = g / h a ^ k := hgerm
    rw [this, div_mul_cancel₀ _ (pow_ne_zero _ (hh a))]
  obtain ⟨-, hEt, hFin⟩ :=
    IsIntegrallyClosed.integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
    (B := Γ(X, (V : X.Opens))) (F := X.functionField) k hkB v hvu (h a) (hh a) g hgeq
  let e : Γ(Spec (CommRingCat.of (Kum X k g)), (kumHom X k g) ⁻¹ᵁ (V : X.Opens)) ≃ₐ[Γ(X, (V :
    X.Opens))] Kum X k g :=
    AlgEquiv.ofRingEquiv (f := (secIso k g hη).commRingCatIsoToRingEquiv) (fun s => by
      change ((kumHom X k g).app (V : X.Opens) ≫ (secIso k g hη).hom) s =
        algebraMap X.functionField (Kum X k g) (algebraMap Γ(X, (V : X.Opens)) X.functionField s)
      rw [app_secIso_hom]
      rfl)
  let e' := (AlgEquiv.mapIntegralClosure e).symm
  exact ⟨Module.Finite.equiv e'.toLinearEquiv, Algebra.Etale.of_equiv e'⟩

theorem genericPoint_mem_of_nonempty {V : X.Opens} (hV : Nonempty (V : X.Opens)) : genericPoint X ∈
  V

theorem res_res {A B C : X.Opens} (i : C ⟶ B) (j : B ⟶ A) (s : X.presheaf.obj (Opposite.op A)) :
    X.presheaf.map i.op (X.presheaf.map j.op s) = X.presheaf.map (homOfLE (i.le.trans j.le)).op s

theorem iSup_good_eq_top (k : ℕ) (g : X.functionField) (hg : g ≠ 0)
    {r : ℕ} (U : Fin r → X.Opens) (hU : (⨆ a, U a) = ⊤) (h : Fin r → X.functionField) (hh : ∀ a, h
      a ≠ 0)
    (hdiv : ∀ a (x : X), x ∈ U a →
      g / h a ^ k ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range ∧
      h a ^ k / g ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    (⨆ V : {V : X.affineOpens // Good k g U h V}, ((V : X.affineOpens) : X.Opens)) = ⊤

theorem _root_.AlgebraicGeometry.isFinite_and_etale_fromNormalization_kummer_of_isIntegrallyClosed
    {R : Type u} [CommRing R]
    {X : Scheme.{u}} [IsIntegral X] (f : X ⟶ Spec (CommRingCat.of R))
    (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x))
    (k : ℕ) (hk : IsUnit ((k : ℕ) : R))
    (g : X.functionField) (hg : g ≠ 0)
    (r : ℕ) (U : Fin r → X.Opens) (hU : (⨆ a, U a) = ⊤) (h : Fin r → X.functionField) (hh : ∀ a, h
      a ≠ 0)
    (hdiv : ∀ a (x : X), x ∈ U a →
      g / h a ^ k ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range ∧
      h a ^ k / g ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    let π := (Spec.map (CommRingCat.ofHom (algebraMap X.functionField (AdjoinRoot (Polynomial.X ^ k
      - Polynomial.C g : Polynomial X.functionField)))) ≫
      X.fromSpecStalk (genericPoint X)).fromNormalization
    IsFinite π ∧ AlgebraicGeometry.Etale π := by
  set φ := Spec.map (CommRingCat.ofHom (algebraMap X.functionField
        (AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial X.functionField)))) ≫
      X.fromSpecStalk (genericPoint X) with hφ
  intro π
  change IsFinite φ.fromNormalization ∧ Etale φ.fromNormalization
  have hcov := KFEAux.iSup_good_eq_top k g hg U hU h hh hdiv
  have hAffine : HasAffineProperty (@IsFinite : MorphismProperty Scheme.{u})
      (affineAnd RingHom.Finite) :=
    (HasAffineProperty.affineAnd_iff (@IsFinite : MorphismProperty Scheme.{u})
      RingHom.finite_respectsIso RingHom.finite_localizationPreserves.away
      RingHom.finite_ofLocalizationSpan).mpr (fun {_ _} f => isFinite_iff f)
  have : IsZariskiLocalAtTarget (@IsFinite : MorphismProperty Scheme.{u}) :=
    (HasAffineProperty.iff.mp hAffine).1
  have : IsZariskiLocalAtTarget (@Etale : MorphismProperty Scheme.{u}) :=
    HasRingHomProperty.instIsZariskiLocalAtTarget (@Etale : MorphismProperty Scheme.{u})
  have : MorphismProperty.RespectsIso (@IsFinite : MorphismProperty Scheme.{u}) :=
    HasAffineProperty.instRespectsIsoScheme (P := @IsFinite) (Q := affineAnd RingHom.Finite)
  have : HasAffineProperty (@Etale : MorphismProperty Scheme.{u})
      (sourceAffineLocally RingHom.Etale) :=
    HasRingHomProperty.HasAffineProperty (@Etale : MorphismProperty Scheme.{u})
  have : MorphismProperty.RespectsIso (@Etale : MorphismProperty Scheme.{u}) :=
    HasAffineProperty.instRespectsIsoScheme (P := @Etale) (Q := sourceAffineLocally RingHom.Etale)
  constructor
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsFinite) _ hcov]
    rintro ⟨V, hV⟩
    have : IsOpenImmersion (φ.normalizationOpenCover.f V) :=
      φ.normalizationOpenCover.map_prop V
    let e := IsOpenImmersion.isoOfRangeEq (φ.fromNormalization ⁻¹ᵁ (V : X.Opens)).ι
      (φ.normalizationOpenCover.f V)
      (by simpa using congr($(φ.fromNormalization_preimage V).1))
    rw [← MorphismProperty.cancel_left_of_respectsIso (@IsFinite : MorphismProperty Scheme.{u})
        e.inv,
      ← MorphismProperty.cancel_right_of_respectsIso (@IsFinite : MorphismProperty Scheme.{u})
        _ V.2.isoSpec.hom]
    have : (φ.normalizationDiagramMap.app (.op V)).hom.Finite := by
      let := (φ.app V).hom.toAlgebra
      change (algebraMap Γ(X, (V : X.Opens)) (integralClosure Γ(X, (V : X.Opens))
        Γ(Spec (CommRingCat.of (AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial
          X.functionField))), φ ⁻¹ᵁ (V : X.Opens)))).Finite
      rw [RingHom.finite_algebraMap]
      exact (KFEAux.key f hnorm k hk g hg U h hh V hV).1
    convert! (IsFinite.SpecMap_iff _).mpr this
    have : IsOpenImmersion V.2.fromSpec := V.2.isOpenImmersion_fromSpec
    erw [← cancel_mono V.2.fromSpec]
    have he : e.inv ≫ (φ.fromNormalization ⁻¹ᵁ (V : X.Opens)).ι =
        φ.normalizationOpenCover.f V :=
      IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _
    erw [Category.assoc, Category.assoc, V.2.isoSpec_hom_fromSpec,
      morphismRestrict_ι, ← Category.assoc, he, φ.ι_fromNormalization V]
    rfl
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @Etale) _ hcov]
    rintro ⟨V, hV⟩
    have : IsOpenImmersion (φ.normalizationOpenCover.f V) :=
      φ.normalizationOpenCover.map_prop V
    let e := IsOpenImmersion.isoOfRangeEq (φ.fromNormalization ⁻¹ᵁ (V : X.Opens)).ι
      (φ.normalizationOpenCover.f V)
      (by simpa using congr($(φ.fromNormalization_preimage V).1))
    rw [← MorphismProperty.cancel_left_of_respectsIso (@Etale : MorphismProperty Scheme.{u})
        e.inv,
      ← MorphismProperty.cancel_right_of_respectsIso (@Etale : MorphismProperty Scheme.{u})
        _ V.2.isoSpec.hom]
    have : (φ.normalizationDiagramMap.app (.op V)).hom.Etale := by
      let := (φ.app V).hom.toAlgebra
      change (algebraMap Γ(X, (V : X.Opens)) (integralClosure Γ(X, (V : X.Opens))
        Γ(Spec (CommRingCat.of (AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial
          X.functionField))), φ ⁻¹ᵁ (V : X.Opens)))).Etale
      rw [RingHom.etale_algebraMap]
      exact (KFEAux.key f hnorm k hk g hg U h hh V hV).2
    convert! (HasRingHomProperty.Spec_iff (P := @Etale)).mpr this
    have : IsOpenImmersion V.2.fromSpec := V.2.isOpenImmersion_fromSpec
    erw [← cancel_mono V.2.fromSpec]
    have he : e.inv ≫ (φ.fromNormalization ⁻¹ᵁ (V : X.Opens)).ι =
        φ.normalizationOpenCover.f V :=
      IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _
    erw [Category.assoc, Category.assoc, V.2.isoSpec_hom_fromSpec,
      morphismRestrict_ι, ← Category.assoc, he, φ.ι_fromNormalization V]
    rfl