OpenCoverDegree.lean

theorem finiteCurveFieldMap_eq_actual_functionFieldMap
    {K F E : Type} [Field K] [IsAlgClosed K]
    [Field F] [Field E] [Algebra K F] [Algebra K E]
    (M : CurveModel K F) (N : CurveModel K E)
    (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
    [IsFinite d] (hsurj : Function.Surjective d) (a : F) :
    N.ffEquiv (M.finiteCurveFieldMap N d hd hsurj a) =
      d.functionFieldMap hsurj.denseRange (M.ffEquiv a)

theorem finrankAlong_openCover_eq_actual
    {K F E : Type} [Field K] [IsAlgClosed K]
    [Field F] [Field E] [Algebra K F] [Algebra K E]
    (M : CurveModel K F) (N : CurveModel K E)
    {X : Scheme} [IsIntegral X] [IsNormalIntegral X]
    (j : X ⟶ M.C) [IsOpenImmersion j]
    (W : FiniteEtale X) [IsConnected W]
    (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
    [IsFinite d] (hsurj : Function.Surjective d)
    (k : W.left ⟶ N.C) [IsOpenImmersion k]
    (hsquare : k ≫ d = W.hom ≫ j) :
    let : IsIntegral W.left := isIntegral_left_of_isConnected_finiteEtale W
    let : Algebra X.functionField W.left.functionField := finiteEtaleFunctionFieldAlgebra W
    finrankAlong K (M.finiteCurveFieldMap N d hd hsurj) =
      Module.finrank X.functionField W.left.functionField := by
  intro hIntegral algW
  have : IsIntegral ((Functor.id Scheme).obj W.left) := hIntegral
  have : IsIntegral ((Functor.fromPUnit X).obj W.right) :=
    inferInstanceAs (IsIntegral X)
  let hj : DenseRange j :=
    j.isOpenEmbedding.isOpenMap.denseRange_of_isPreirreducibleSpace j
  let hk : DenseRange k :=
    k.isOpenEmbedding.isOpenMap.denseRange_of_isPreirreducibleSpace k
  let hw : DenseRange W.hom := finiteEtale_hom_denseRange_of_isConnected W
  let φ := M.finiteCurveFieldMap N d hd hsurj
  let : Algebra F E := algebraAlong φ
  have hcomp :
      (k.functionFieldMap hk).comp (d.functionFieldMap hsurj.denseRange) =
        (W.hom.functionFieldMap hw).comp (j.functionFieldMap hj) := by
    rw [functionFieldMap_comp_of_dense d hsurj.denseRange k hk,
      functionFieldMap_comp_of_dense (X := M.C) (Y := X) (Z := W.left) j hj W.hom hw]
    congr 1
  refine Algebra.finrank_eq_of_equiv_equiv
    (M.ffEquiv.trans j.functionFieldRingEquivOfIsOpenImmersion)
    (N.ffEquiv.trans k.functionFieldRingEquivOfIsOpenImmersion) ?_
  ext a
  change W.hom.functionFieldMap hw (j.functionFieldMap hj (M.ffEquiv a)) =
    k.functionFieldMap hk (N.ffEquiv (φ a))
  rw [finiteCurveFieldMap_eq_actual_functionFieldMap M N d hd hsurj a]
  exact (DFunLike.congr_fun hcomp (M.ffEquiv a)).symm