PuncturedSpectrumConnectedLefschetzSource.lean

instance finiteHasAffinePropertyLefschetz : HasAffineProperty
    (@IsFinite : MorphismProperty Scheme.{u}) (affineAnd RingHom.Finite)

theorem connectedSpace_spec_quotient_map_of_finiteDomain_of_maximalAdicComplete
    {C : Type u} [CommRing C] [IsDomain C] [Algebra R C]
    [Module.Finite R C] [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ConnectedSpace
      (Spec (.of (C ⧸ I.map (algebraMap R C))))

theorem connectedSpace_pullback_spec_quotient_of_finiteDomain_of_maximalAdicComplete
    {C : Type u} [CommRing C] [IsDomain C] [Algebra R C]
    [Module.Finite R C] [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ConnectedSpace
      ((Limits.pullback
        (Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (Spec.map (CommRingCat.ofHom (algebraMap R (R ⧸ I))))) : Scheme.{u})

def pullbackIsoOfIsoOver
    {A B X Y : Scheme.{u}} (e : A ≅ B)
    (f : A ⟶ X) (h : B ⟶ X) (g : Y ⟶ X)
    (w : e.hom ≫ h = f) :
    Limits.pullback f g ≅ Limits.pullback h g

theorem connectedSpace_normalizationClosedFiber_of_isFinite_of_isIntegral
    {Z : Scheme.{u}} (z : Z ⟶ Spec (.of R)) [IsFinite z] [IsIntegral Z]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ConnectedSpace
      ((Limits.pullback z
        (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))) : Scheme.{u})

theorem puncturedSpectrumFunctionFieldRingEquiv_apply_germ_source
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (r : Γ(Spec (.of R), ⊤)) :
    let X := Spec (.of R)
    let U := Scheme.puncturedSpectrum R
    let j : U ⟶ X := Scheme.puncturedSpectrumInclusion R
    letI : Nonempty U :=
      Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
    letI : IsOpenImmersion j := by
      dsimp only [j, Scheme.puncturedSpectrumInclusion]
      infer_instance
    letI : IsIntegral U := isIntegral_of_isOpenImmersion j
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by trivial⟩⟩
    letI : Algebra R X.functionField :=
      AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
    letI : Nonempty (⊤ : U.Opens) :=
      ⟨⟨genericPoint U, by trivial⟩⟩
    puncturedSpectrumFunctionFieldRingEquivOfPositiveDimension R hpos
        (X.germToFunctionField ⊤ r) =
      U.germToFunctionField ⊤ (j.appTop r) := by
  dsimp only
  let X := Spec (.of R)
  let U := Scheme.puncturedSpectrum R
  let j : U ⟶ X := Scheme.puncturedSpectrumInclusion R
  let : Nonempty U :=
    Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
  let : IsOpenImmersion j := by
    dsimp only [j, Scheme.puncturedSpectrumInclusion]
    infer_instance
  let : IsIntegral U := isIntegral_of_isOpenImmersion j
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by trivial⟩⟩
  let : Algebra R X.functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
  let : Nonempty (⊤ : U.Opens) :=
    ⟨⟨genericPoint U, by trivial⟩⟩
  let hgen : j (genericPoint U) = genericPoint X :=
    genericPoint_eq_of_isOpenImmersion j
  change j.stalkMap (genericPoint U)
      ((X.presheaf.stalkCongr (.of_eq hgen.symm)).hom
        (X.germToFunctionField ⊤ r)) =
    U.germToFunctionField ⊤ (j.appTop r)
  simp only [TopCat.Presheaf.stalkCongr_hom]
  have htransport :
      X.presheaf.stalkSpecializes
          (Inseparable.of_eq hgen.symm).ge
          (X.presheaf.germ ⊤ (genericPoint X) (by trivial) r) =
        X.presheaf.germ ⊤ (j (genericPoint U)) (by trivial) r := by
    exact DFunLike.congr_fun
      (CommRingCat.hom_ext_iff.mp
        (X.presheaf.germ_stalkSpecializes
          (show genericPoint X ∈ (⊤ : X.Opens) by trivial)
          (Inseparable.of_eq hgen.symm).ge)) r
  rw [htransport]
  exact j.germ_stalkMap_apply (⊤ : X.Opens) (genericPoint U)
    (by trivial) r

theorem specFunctionField_algebraMap_ΓSpecIso_hom_source
    (r : Γ(Spec (.of R), ⊤)) :
    let X := Spec (.of R)
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨genericPoint X, by trivial⟩⟩
    letI : Algebra R X.functionField :=
      AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
    algebraMap R X.functionField ((Scheme.ΓSpecIso (.of R)).hom r) =
      X.germToFunctionField ⊤ r := by
  dsimp only
  let X := Spec (.of R)
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by trivial⟩⟩
  let : Algebra R X.functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
  change X.presheaf.germ ⊤ (genericPoint X) (by trivial)
      ((Scheme.ΓSpecIso (.of R)).inv
        ((Scheme.ΓSpecIso (.of R)).hom r)) =
    X.germToFunctionField ⊤ r
  change X.presheaf.germ ⊤ (genericPoint X) (by trivial)
      ((Scheme.ΓSpecIso (.of R)).inv
        ((Scheme.ΓSpecIso (.of R)).hom r)) =
    X.presheaf.germ ⊤ (genericPoint X) (by trivial) r
  exact congrArg (fun s ↦
    X.presheaf.germ ⊤ (genericPoint X) (by trivial) s)
      (Iso.hom_inv_id_apply (Scheme.ΓSpecIso (.of R)) r)

theorem connectedPuncturedCoverGenericNormalization_isFinite
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W] :
    let U := Scheme.puncturedSpectrum R
    let j : U ⟶ Spec (.of R) := Scheme.puncturedSpectrumInclusion R
    letI : Nonempty U :=
      Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
    letI : IsOpenImmersion j := by
      dsimp only [j, Scheme.puncturedSpectrumInclusion]
      infer_instance
    letI : IsIntegral U := isIntegral_of_isOpenImmersion j
    IsFinite (connectedCoverGenericComposite W ≫ j).fromNormalization := by
  dsimp only
  let X := Spec (.of R)
  let U := Scheme.puncturedSpectrum R
  let j : U ⟶ X := Scheme.puncturedSpectrumInclusion R
  let : Nonempty U :=
    Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim R hpos
  let : IsOpenImmersion j := by
    dsimp only [j, Scheme.puncturedSpectrumInclusion]
    infer_instance
  let : IsIntegral U := isIntegral_of_isOpenImmersion j
  let : IsNormalIntegral U := inferInstance
  let : IsLocallyNoetherian U := inferInstance
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨genericPoint X, by trivial⟩⟩
  let : Nonempty (⊤ : U.Opens) :=
    ⟨⟨genericPoint U, by trivial⟩⟩
  let : Algebra R X.functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of R)
  let K : Type u := U.functionField
  let : Algebra R K :=
    puncturedSpectrumFunctionFieldAlgebraOfPositiveDimension R hpos
  let : IsFractionRing R K :=
    puncturedSpectrumFunctionField_isFractionRing_of_positiveDimension R hpos
  let : IsIntegral W.left :=
    EtaleFundamentalGroups.isIntegral_left_of_isConnected_finiteEtale W
  let L : Type u := W.left.functionField
  let : Algebra K L :=
    EtaleFundamentalGroups.finiteEtaleFunctionFieldAlgebra W
  let : Algebra R L :=
    ((algebraMap K L).comp (algebraMap R K)).toAlgebra
  let : IsScalarTower R K L := IsScalarTower.of_algebraMap_eq' rfl
  let : FiniteDimensional K L :=
    EtaleFundamentalGroups.finiteDimensional_functionField_of_finiteEtale_isConnected W
  let : Algebra.IsSeparable K L :=
    EtaleFundamentalGroups.isSeparable_functionField_of_finiteEtale_isConnected W
  let f : Spec (.of L) ⟶ U := connectedCoverGenericComposite W
  let g : Spec (.of L) ⟶ X := f ≫ j
  let : QuasiCompact g := inferInstance
  let : QuasiSeparated g := inferInstance
  let A : Type u := Γ(X, ⊤)
  let S : Type u := Γ(Spec (.of L), g ⁻¹ᵁ (⊤ : X.Opens))
  let : Algebra A S := g.appTop.hom.toAlgebra
  let eBase : A ≃+* R :=
    (Scheme.ΓSpecIso (.of R)).commRingCatIsoToRingEquiv
  let eAmbientCat : CommRingCat.of S ≅ CommRingCat.of L := by
    change Γ(Spec (.of L), f ⁻¹ᵁ (⊤ : U.Opens)) ≅ .of L
    exact connectedCoverGenericCompositeSectionsIso W
  let eAmbient : S ≃+* L := eAmbientCat.commRingCatIsoToRingEquiv
  have hCompat :
      eAmbient.toRingHom.comp (algebraMap A S) =
        (algebraMap R L).comp eBase.toRingHom := by
    ext a
    change eAmbient (g.appTop a) = algebraMap R L (eBase a)
    change (connectedCoverGenericCompositeSectionsIso W).hom
        (f.appTop (j.appTop a)) = algebraMap R L (eBase a)
    rw [connectedCoverGenericCompositeSectionsIso_hom_appTop]
    change algebraMap K L (U.germToFunctionField ⊤ (j.appTop a)) =
      algebraMap K L (algebraMap R K (eBase a))
    congr 1
    rw [← puncturedSpectrumFunctionFieldRingEquiv_apply_germ_source R hpos a]
    change (puncturedSpectrumFunctionFieldRingEquivOfPositiveDimension R hpos)
        (X.germToFunctionField ⊤ a) =
      (puncturedSpectrumFunctionFieldRingEquivOfPositiveDimension R hpos)
        (algebraMap R X.functionField (eBase a))
    congr 1
    exact (specFunctionField_algebraMap_ΓSpecIso_hom_source R a).symm
  let C : Type u := integralClosure A S
  let CR : Type u := integralClosure R L
  let : Module.Finite R CR :=
    connectedPuncturedCover_integralClosure_finite_of_positiveDimension
      R hpos W
  let : Algebra A CR :=
    EtaleFundamentalGroups.integralClosureBaseRingAlgebra eBase
  let eC : C ≃ₐ[A] CR :=
    EtaleFundamentalGroups.integralClosureAlgEquivOfBaseAndAmbientEquiv
      eBase eAmbient hCompat
  let : Algebra A R := eBase.toRingHom.toAlgebra
  let : IsScalarTower A R CR := IsScalarTower.of_algebraMap_eq' rfl
  let : Module.Finite A R := eBase.finite
  let : Module.Finite A CR := Module.Finite.trans R CR
  let : Module.Finite A C := Module.Finite.equiv eC.symm.toLinearEquiv
  have hfiniteC : (algebraMap A C).Finite := by
    change Module.Finite A C
    infer_instance
  have hApp : g.fromNormalization.appTop.hom.Finite := by
    change (g.fromNormalization.app (⊤ : X.Opens)).hom.Finite
    rw [g.fromNormalization_app (isAffineOpen_top X)]
    exact RingHom.Finite.comp
      (g.normalizationObjIso (isAffineOpen_top X)).symm.commRingCatIsoToRingEquiv.finite
      hfiniteC
  rw [HasAffineProperty.iff_of_isAffine (P := (@IsFinite : MorphismProperty Scheme.{u}))
        (Q := affineAnd RingHom.Finite)]
  exact ⟨isAffine_of_isAffineHom g.fromNormalization, hApp⟩

def connectedPuncturedCoverNormalizationClosedFiber
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) : Over (Spec (.of (R ⧸ I)))

theorem connectedPuncturedCoverNormalizationClosedFiber_hom_isFinite
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) :
    IsFinite
      (connectedPuncturedCoverNormalizationClosedFiber R hpos W I).hom

theorem connectedPuncturedCoverNormalizationClosedFiber_isAffine
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) :
    IsAffine
      (connectedPuncturedCoverNormalizationClosedFiber R hpos W I).left

theorem connectedPuncturedCoverNormalizationClosedFiber_connectedSpace
    [IsAdicComplete (maximalIdeal R) R]
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ConnectedSpace
      (connectedPuncturedCoverNormalizationClosedFiber R hpos W I).left

def connectedPuncturedCoverNormalizationPuncturedFiber
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) : Scheme.{u}

def connectedPuncturedCoverQuotientRestrictionIso
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ((pullback (Scheme.puncturedSpectrumQuotientMorphism R I hI)).obj W).left ≅
      connectedPuncturedCoverNormalizationPuncturedFiber R hpos W I hI

theorem connectedPuncturedCoverQuotientRestriction_connectedSpace_iff
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ConnectedSpace
        ((pullback
          (Scheme.puncturedSpectrumQuotientMorphism R I hI)).obj W).left ↔
      ConnectedSpace
        (connectedPuncturedCoverNormalizationPuncturedFiber
          R hpos W I hI)

theorem connectedPuncturedCoverQuotientRestriction_isConnected_iff
    (hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (W : FiniteEtale (Scheme.puncturedSpectrum R)) [IsConnected W]
    (I : Ideal R) (hI : I ≤ maximalIdeal R)
    [IsLocalRing (R ⧸ I)]
    [ConnectedSpace (Scheme.puncturedSpectrum (R ⧸ I))] :
    IsConnected
        ((pullback
          (Scheme.puncturedSpectrumQuotientMorphism R I hI)).obj W) ↔
      ConnectedSpace
        (connectedPuncturedCoverNormalizationPuncturedFiber
          R hpos W I hI)