OpenCoverSquareBoundary.lean

theorem exists_open_cover_curveModel_square_boundary
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F]
    (M : CurveModel K F) {X : Scheme}
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (j : X ⟶ M.C) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
    (W : FiniteEtale X) [IsConnected W] :
    let : IsIntegral W.left := isIntegral_left_of_isConnected_finiteEtale W
    let cW : W.left ⟶ Spec (.of K) := W.hom ≫ j ≫ M.toBase
    let : Algebra K W.left.functionField := (baseToFunctionField cW).toAlgebra
    ∃ (N : CurveModel K W.left.functionField)
      (d : N.C ⟶ M.C) (k : W.left ⟶ N.C),
      d ≫ M.toBase = N.toBase ∧ IsFinite d ∧ IsOpenImmersion k ∧
      k ≫ d = W.hom ≫ j ∧
      ∀ y : N.C, y ∉ Set.range k ↔ d y ∉ Set.range j := by
  intro hIntegral cW algW
  obtain ⟨N, d, hd, hfinite, e, he⟩ :=
    exists_curveModel_iso_open_cover_normalization M j W
  let i := FiniteEtale.connectedCoverCompactificationInclusion j W
  let k : W.left ⟶ N.C := i ≫ e.hom
  have : IsOpenImmersion i :=
    FiniteEtale.connectedCoverCompactificationInclusion_isOpenImmersion j W
  have hk : IsOpenImmersion k := by dsimp only [k]; infer_instance
  refine ⟨N, d, k, hd, hfinite, hk, ?_, ?_⟩
  · dsimp only [k]
    rw [Category.assoc, he]
    exact FiniteEtale.connectedCoverCompactificationInclusion_comp j W
  · intro y
    obtain ⟨z, rfl⟩ := e.hom.homeomorph.surjective y
    have hr : e.hom z ∈ Set.range k ↔ z ∈ Set.range i := by
      constructor
      · rintro ⟨w, hw⟩
        refine ⟨w, e.hom.homeomorph.injective ?_⟩
        exact hw
      · rintro ⟨w, rfl⟩
        exact ⟨w, rfl⟩
    have hdpoint : d (e.hom z) =
        (FiniteEtale.connectedCoverGenericComposite W ≫ j).fromNormalization z :=
      congrArg (fun f => f z) he
    change e.hom z ∉ Set.range k ↔ d (e.hom z) ∉ Set.range j
    rw [hr, hdpoint]
    exact FiniteEtale.not_mem_range_connectedCoverCompactificationInclusion j W z

theorem surjective_finite_extension_of_open_square
    {X Y M N : Scheme} [IsIntegral M] [Nonempty X]
    (j : X ⟶ M) [IsOpenImmersion j]
    (f : Y ⟶ X) (hf : Function.Surjective f)
    (k : Y ⟶ N) (d : N ⟶ M) [IsFinite d]
    (hsquare : k ≫ d = f ≫ j) : Function.Surjective d