Integral.lean

theorem irreducibleSpace_of_connectedSpace_of_irreducible_openCover
    {A I : Type*} [TopologicalSpace A] [ConnectedSpace A]
    (U : I → TopologicalSpace.Opens A)
    (hcover : (⨆ i, U i) = ⊤)
    (hU : ∀ i, IrreducibleSpace (U i)) : IrreducibleSpace A

theorem isIntegral_of_isFiniteEtale_of_isAffine_of_connectedSpace
    {X Y : Scheme.{u}} (f : Y ⟶ X) [IsFiniteEtale f]
    [IsIntegral X] [IsNormalIntegral X] [IsAffine X]
    [ConnectedSpace Y] : IsIntegral Y

theorem isIntegral_connectedComponent_of_isFiniteEtale_of_isAffine
    {X Y : Scheme.{u}} (f : Y ⟶ X) [IsFiniteEtale f]
    [IsIntegral X] [IsNormalIntegral X] [IsAffine X]
    [Finite (_root_.ConnectedComponents Y)]
    (i : _root_.ConnectedComponents Y) :
    IsIntegral (Y.connectedComponents.X i)

theorem isIntegral_left_of_isConnected_finiteEtale
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] : IsIntegral Y.left

theorem isLocallyNoetherian_left_finiteEtale
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (Y : FiniteEtale X) : IsLocallyNoetherian Y.left

theorem isNormalIntegral_left_of_isConnected_finiteEtale
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] :
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    IsNormalIntegral Y.left := by
  classical
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  apply IsNormalIntegral.of_stalks Y.left
  intro y
  have hAffine :
      ∃ U : X.Opens, IsAffineOpen U ∧ Y.hom.base y ∈ U ∧ U ≤ ⊤ :=
    exists_isAffineOpen_mem_and_subset
      (X := X) (U := ⊤) (x := Y.hom.base y) (by simp)
  let U : X.Opens := Classical.choose hAffine
  have hUaffine : IsAffineOpen U :=
    (Classical.choose_spec hAffine).1
  have hyU : Y.hom.base y ∈ U :=
    (Classical.choose_spec hAffine).2.1
  have hUnonempty : Nonempty U := ⟨⟨Y.hom.base y, hyU⟩⟩
  let V : Y.left.Opens := Y.hom ⁻¹ᵁ U
  have hyV : y ∈ V := hyU
  have hrestrEtale : IsFiniteEtale (Y.hom ∣_ U) := by
    exact MorphismProperty.of_isPullback
      (isPullback_morphismRestrict Y.hom U).flip Y.2
  have hfiniteComponents :
      Finite (_root_.ConnectedComponents V) := by
    let : Nonempty U := hUnonempty
    let : IsAffine U := hUaffine
    let A : FiniteEtale U :=
      @FiniteEtale.mk _ _ (Y.hom ∣_ U) hrestrEtale
    change Finite (_root_.ConnectedComponents A.left)
    infer_instance
  let v : V := ⟨y, hyV⟩
  let i : _root_.ConnectedComponents V :=
    _root_.ConnectedComponents.mk v
  let C : (V : Scheme).OpenCover :=
    letI : Finite (_root_.ConnectedComponents V) := hfiniteComponents
    (V : Scheme).connectedComponents
  let Z : Scheme.{u} := C.X i
  let c : Z ⟶ V := C.f i
  have hcOpen : IsOpenImmersion c := by
    let : Finite (_root_.ConnectedComponents V) := hfiniteComponents
    dsimp only [c, C, Scheme.connectedComponents]
    exact (Scheme.connCompOpen (X := (V : Scheme)) i).instIsOpenImmersionι
  have hcClosed : IsClosedImmersion c := by
    dsimp only [c]
    infer_instance
  let g : Z ⟶ U := c ≫ (Y.hom ∣_ U)
  have hcFiniteEtale : IsFiniteEtale c :=
    { toIsFinite := inferInstance
      toEtale := inferInstance }
  have hgFiniteEtale : IsFiniteEtale g := by
    dsimp only [g]
    exact MorphismProperty.comp_mem @IsFiniteEtale
      c (Y.hom ∣_ U) hcFiniteEtale hrestrEtale
  have hZintegral : IsIntegral Z := by
    let : Nonempty U := hUnonempty
    let : IsAffine U := hUaffine
    let hUint : IsIntegral U := isIntegral_of_isOpenImmersion U.ι
    let : IsIntegral U := hUint
    let hUnormal : IsNormalIntegral U := inferInstance
    let : Finite (_root_.ConnectedComponents V) := hfiniteComponents
    change IsIntegral ((V : Scheme).connectedComponents.X i)
    exact @isIntegral_connectedComponent_of_isFiniteEtale_of_isAffine
      U V (Y.hom ∣_ U) hrestrEtale hUint hUnormal hUaffine
      hfiniteComponents i
  have hZnormal : @IsNormalIntegral Z hZintegral := by
    let : Nonempty U := hUnonempty
    let : IsAffine U := hUaffine
    let : IsIntegral U := isIntegral_of_isOpenImmersion U.ι
    let : IsNormalIntegral U := inferInstance
    let : IsIntegral Z := hZintegral
    let : IsFiniteEtale g := hgFiniteEtale
    let : IsAffine Z := isAffine_of_isAffineHom g
    let R := Γ(U, ⊤)
    let T := Γ(Z, ⊤)
    let K := (U : Scheme).functionField
    let : Nonempty (⊤ : (U : Scheme).Opens) :=
      ⟨⟨Classical.choice hUnonempty, trivial⟩⟩
    let : Algebra R T := g.appTop.hom.toAlgebra
    let : Module.Finite R T := by
      rw [← RingHom.finite_algebraMap]
      exact g.finite_appTop
    have hgEtale : g.appTop.hom.Etale := by
      rw [← HasRingHomProperty.iff_of_isAffine
        (P := @AlgebraicGeometry.Etale)]
      infer_instance
    let : Algebra.Etale R T := hgEtale.toAlgebra
    let : IsIntegrallyClosed R :=
      IsNormalIntegral.affine_isIntegrallyClosed ⊤ (isAffineOpen_top U)
    let : Algebra R K := (U : Scheme).affineExtensionAlgebra ⊤ K
    let : IsFractionRing R K :=
      functionField_isFractionRing_of_isAffineOpen (U : Scheme) ⊤
        (isAffineOpen_top (U : Scheme))
    let : ConnectedSpace (PrimeSpectrum T) := by
      change ConnectedSpace (Spec (.of T))
      exact Z.isoSpec.hom.homeomorph.connectedSpace_iff.mp inferInstance
    let : IsIntegrallyClosed T :=
      finiteEtale_isIntegrallyClosed_of_connectedSpace_primeSpectrum
        (R := R) (T := T) (K := K)
    exact IsNormalIntegral.of_isAffine Z
  let j : Z ⟶ Y.left := c ≫ V.ι
  have hjOpen : IsOpenImmersion j := by
    dsimp only [j]
    exact MorphismProperty.comp_mem @IsOpenImmersion
      c V.ι hcOpen inferInstance
  let z : Z := by
    dsimp only [Z, C]
    refine ⟨v, ?_⟩
    change _root_.ConnectedComponents.mk v ∈
      ({i} : Set (_root_.ConnectedComponents V))
    exact Set.mem_singleton _
  let : IsIntegral Z := hZintegral
  let : IsNormalIntegral Z := hZnormal
  let : IsOpenImmersion j := hjOpen
  have hzNormal : IsIntegrallyClosed (Z.presheaf.stalk z) :=
    IsNormalIntegral.stalk_isIntegrallyClosed z
  let e : Z.presheaf.stalk z ≃+* Y.left.presheaf.stalk (j z) :=
    (asIso (j.stalkMap z)).symm.commRingCatIsoToRingEquiv
  have hjz : j z = y := rfl
  have htarget :=
    (@IsIntegrallyClosed.of_equiv
      (Z.presheaf.stalk z) (Y.left.presheaf.stalk (j z))
      _ _ e hzNormal)
  rw [hjz] at htarget
  exact htarget

theorem pullback_obj_isConnected_of_isOpenImmersion
    {X U : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    (Y : FiniteEtale X) [IsConnected Y] :
    IsConnected ((FiniteEtale.pullback j).obj Y)