ChartFunctionFieldCompatibility.lean

instance (y : Y) (P : Spec (Y.presheaf.stalk y)) :
    P.asIdeal.IsPrime

theorem functionFieldMap_eq_of_eq
    {T R : Scheme.{u}} [IsIntegral T] [IsIntegral R]
    (a b : R ⟶ T) (hab : a = b)
    (ha : DenseRange a) (hb : DenseRange b) :
    a.functionFieldMap ha = b.functionFieldMap hb

def etaleChartLocalizationAlgebra
    (f : Y ⟶ X) (y : Y) (P : Spec (Y.presheaf.stalk y)) :
    Algebra (X.presheaf.stalk (f y))
      (Localization.AtPrime P.asIdeal)

theorem etaleChartLocalization_algebraMap_injective
    [IsIntegral X] (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Spec (Y.presheaf.stalk y))
    (_hVdomain : IsDomain (Localization.AtPrime P.asIdeal)) :
    Function.Injective
      ((algebraMap (Y.presheaf.stalk y)
        (Localization.AtPrime P.asIdeal)).comp
          (f.stalkMap y).hom)

theorem boundaryAwayToSupportComplement_comp_ι_eq_specMap_fromSpecStalk
    (I : X.IdealSheafData) (f : Y ⟶ X) (y : Y)
    (P : Spec (Y.presheaf.stalk y)) {r : ℕ}
    (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hboundary :
      ((I.comap f).stalkIdeal y).map
          (algebraMap (Y.presheaf.stalk y)
            (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r}) :
    boundaryAwayToSupportComplement I f y P t hboundary ≫
        I.supportComplement.ι =
      Spec.map (CommRingCat.ofHom
        ((algebraMap (Localization.AtPrime P.asIdeal)
          (Localization.Away (boundaryProduct t r))).comp
        ((algebraMap (Y.presheaf.stalk y)
          (Localization.AtPrime P.asIdeal)).comp
            (f.stalkMap y).hom))) ≫
        X.fromSpecStalk (f y)

theorem boundaryAwayToSupportComplement_denseRange
    [IsIntegral X]
    (I : X.IdealSheafData) (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Spec (Y.presheaf.stalk y)) {r : ℕ}
    (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hf : boundaryProduct t r ≠ 0)
    (hboundary :
      ((I.comap f).stalkIdeal y).map
          (algebraMap (Y.presheaf.stalk y)
            (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    (hVdomain : IsDomain (Localization.AtPrime P.asIdeal)) :
    DenseRange
      (boundaryAwayToSupportComplement I f y P t hboundary)

theorem boundaryAway_functionFieldMap_comp_ambientStalk
    [IsIntegral X] (I : X.IdealSheafData) [Nonempty I.supportComplement]
    (f : Y ⟶ X) [Etale f] (y : Y)
    (P : Spec (Y.presheaf.stalk y)) {r : ℕ}
    (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hf : boundaryProduct t r ≠ 0)
    (hboundary :
      ((I.comap f).stalkIdeal y).map
          (algebraMap (Y.presheaf.stalk y)
            (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    [IsDomain (Localization.AtPrime P.asIdeal)]
    [IsDomain (Localization.Away (boundaryProduct t r))] :
    let c := boundaryAwayToSupportComplement I f y P t hboundary
    let hc : DenseRange c :=
      boundaryAwayToSupportComplement_denseRange
        I f y P t hf hboundary inferInstance
    (c.functionFieldMap hc).comp
        ((Scheme.Hom.functionFieldRingEquivOfIsOpenImmersion
          I.supportComplement.ι).toRingHom.comp
            (algebraMap (X.presheaf.stalk (f y)) X.functionField)) =
      (StructureSheaf.toStalk
        (CommRingCat.of (Localization.Away (boundaryProduct t r)))
        (genericPoint (Spec (.of (Localization.Away
          (boundaryProduct t r)))))).hom.comp
        ((algebraMap (Localization.AtPrime P.asIdeal)
          (Localization.Away (boundaryProduct t r))).comp
        ((algebraMap (Y.presheaf.stalk y)
          (Localization.AtPrime P.asIdeal)).comp
            (f.stalkMap y).hom)) := by
  dsimp only
  let A := X.presheaf.stalk (f y)
  let B := Y.presheaf.stalk y
  let V := Localization.AtPrime P.asIdeal
  let b := boundaryProduct t r
  let S := Localization.Away b
  let : Algebra S (Spec (.of S)).functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of S)
  let c := boundaryAwayToSupportComplement I f y P t hboundary
  let j := I.supportComplement.ι
  let phi : A →+* S :=
    (algebraMap V S).comp
      ((algebraMap B V).comp (f.stalkMap y).hom)
  have hAV : Function.Injective
      ((algebraMap B V).comp (f.stalkMap y).hom) := by
    exact etaleChartLocalization_algebraMap_injective
      f y P (inferInstance : IsDomain V)
  have hVS : Function.Injective (algebraMap V S) :=
    IsLocalization.injective (M := Submonoid.powers b) S
      (Submonoid.powers_le.mpr
        (mem_nonZeroDivisors_iff_ne_zero.mpr hf))
  have hphi : Function.Injective phi := hVS.comp hAV
  let g : Spec (.of S) ⟶ X :=
    Spec.map (CommRingCat.ofHom phi) ≫ X.fromSpecStalk (f y)
  let hg : DenseRange g :=
    Scheme.Hom.denseRange_specMap_comp_fromSpecStalk_of_injective
      (f y) phi hphi
  have hc : DenseRange c :=
    boundaryAwayToSupportComplement_denseRange
      I f y P t hf hboundary inferInstance
  have hj : DenseRange j :=
    j.isOpenEmbedding.isOpenMap.denseRange_of_isPreirreducibleSpace j
  have hcj : DenseRange (c ≫ j) := by
    change DenseRange (j.base ∘ c.base)
    exact hj.comp hc j.continuous
  have hcanonical : c ≫ j = g := by
    exact boundaryAwayToSupportComplement_comp_ι_eq_specMap_fromSpecStalk
      I f y P t hboundary
  have hfield : (c ≫ j).functionFieldMap hcj =
      g.functionFieldMap hg :=
    functionFieldMap_eq_of_eq (c ≫ j) g hcanonical hcj hg
  calc
    (c.functionFieldMap hc).comp
        ((j.functionFieldRingEquivOfIsOpenImmersion.toRingHom).comp
          (algebraMap A X.functionField)) =
      ((c.functionFieldMap hc).comp (j.functionFieldMap hj)).comp
        (algebraMap A X.functionField) := by
          rw [RingHom.comp_assoc]
          rfl
    _ = ((c ≫ j).functionFieldMap hcj).comp
        (algebraMap A X.functionField) := by
          rw [Scheme.Hom.functionFieldMap_comp_of_denseRange j hj c hc]
    _ = (g.functionFieldMap hg).comp
        (algebraMap A X.functionField) := by rw [hfield]
    _ = (algebraMap S (Spec (.of S)).functionField).comp phi :=
      Scheme.Hom.functionFieldMap_comp_stalkFunctionField_of_injective
        (f y) phi hphi