Scheme_IdealSheafData_comap_injective_of_flat_of_surjective.lean

theorem ker_algebraMap_eq_map_ker
    (R B C P : Type*) [CommRing R] [CommRing B] [CommRing C] [CommRing P]
    [Algebra R B] [Algebra R C] [Algebra B P] [Algebra C P] [Algebra R P]
    [IsScalarTower R B P] [IsScalarTower R C P] [Algebra.IsPushout R B C P]
    (hC : Function.Surjective (algebraMap R C)) :
    RingHom.ker (algebraMap B P) = (RingHom.ker (algebraMap R C)).map (algebraMap R B)

theorem ker_eq_map_ker_of_isPushout {R B C P : CommRingCat.{u}} {f : R ⟶ B} {g : R ⟶ C}
    {inl : B ⟶ P} {inr : C ⟶ P} (h : IsPushout f g inl inr)
    (hg : Function.Surjective g.hom) :
    RingHom.ker inl.hom = (RingHom.ker g.hom).map f.hom

theorem ideal_comap_top [IsAffine X] [IsAffine Y] (I : X.IdealSheafData) (f : Y ⟶ X) :
    (I.comap f).ideal ⟨⊤, isAffineOpen_top Y⟩ =
      (I.ideal ⟨⊤, isAffineOpen_top X⟩).map f.appTop.hom

theorem ideal_comap_of_le (I : X.IdealSheafData) (f : Y ⟶ X) (U : X.affineOpens)
    (V : Y.affineOpens) (hVU : (V : Y.Opens) ≤ f ⁻¹ᵁ (U : X.Opens)) :
    (I.comap f).ideal V = (I.ideal U).map (f.appLE U V hVU).hom

theorem ideal_comap_of_isAffineHom (I : X.IdealSheafData) (f : Y ⟶ X) [IsAffineHom f]
    (U : X.affineOpens) :
    (I.comap f).ideal ⟨f ⁻¹ᵁ U, U.2.preimage f⟩ = (I.ideal U).map (f.app U).hom

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.comap_injective_of_flat_of_surjective
    {X Y : Scheme.{u}} (π : Y ⟶ X) [Flat π] [Surjective π] :
    Function.Injective fun I : X.IdealSheafData => I.comap π := by
  intro I J h
  change I.comap π = J.comap π at h
  refine Scheme.IdealSheafData.ext (funext fun U => ?_)
  have hU : IsAffineOpen (U : X.Opens) := U.2
  apply Ideal.eq_of_localization_maximal
  intro P hP
  let 𝔭 : PrimeSpectrum Γ(X, U) := ⟨P, hP.isPrime⟩
  obtain ⟨y, hy⟩ := π.surjective (hU.fromSpec 𝔭)
  have hyU : y ∈ π ⁻¹ᵁ (U : X.Opens) := by
    change π y ∈ (U : X.Opens)
    rw [hy, ← SetLike.mem_coe, ← hU.range_fromSpec]
    exact Set.mem_range_self 𝔭
  obtain ⟨_, ⟨V, hV, rfl⟩, hyV, hVU⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open hyU (π ⁻¹ᵁ (U : X.Opens)).isOpen
  have hφ : (π.appLE U V hVU).hom.Flat := Flat.flat_appLE π hU hV hVU
  let 𝔮 : PrimeSpectrum Γ(Y, V) := hV.primeIdealOf ⟨y, hyV⟩
  have h𝔮 : P = 𝔮.asIdeal.comap (π.appLE U V hVU).hom := by
    have h1 := IsAffineOpen.comap_primeIdealOf_appLE (U : X.Opens) hU V hV hVU hyV
    have h2 : hU.primeIdealOf ⟨π y, hVU hyV⟩ = 𝔭 :=
      hU.fromSpec.isOpenEmbedding.injective (by rw [IsAffineOpen.fromSpec_primeIdealOf]; exact hy)
    exact (congrArg PrimeSpectrum.asIdeal (h1.trans h2)).symm
  have hIJ : (I.ideal U).map (π.appLE U V hVU).hom = (J.ideal U).map (π.appLE U V hVU).hom := by
    rw [← Scheme.IdealSheafData.ideal_comap_of_le I π U ⟨V, hV⟩ hVU,
      ← Scheme.IdealSheafData.ideal_comap_of_le J π U ⟨V, hV⟩ hVU, h]
  let ψ := Localization.localRingHom P 𝔮.asIdeal (π.appLE U V hVU).hom h𝔮
  have hψ : ψ.Flat := RingHom.Flat.localRingHom hφ 𝔮.asIdeal P h𝔮
  let := ψ.toAlgebra
  have : Module.Flat (Localization.AtPrime P) (Localization.AtPrime 𝔮.asIdeal) := hψ
  have : IsLocalHom (algebraMap (Localization.AtPrime P) (Localization.AtPrime 𝔮.asIdeal)) :=
    show IsLocalHom ψ from inferInstance
  have : Module.FaithfullyFlat (Localization.AtPrime P) (Localization.AtPrime 𝔮.asIdeal) :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  suffices hloc : ((I.ideal U).map (algebraMap _ (Localization.AtPrime P))).map
        (algebraMap (Localization.AtPrime P) (Localization.AtPrime 𝔮.asIdeal)) =
      ((J.ideal U).map (algebraMap _ (Localization.AtPrime P))).map
        (algebraMap (Localization.AtPrime P) (Localization.AtPrime 𝔮.asIdeal)) by
    have := congrArg
      (Ideal.comap (algebraMap (Localization.AtPrime P) (Localization.AtPrime 𝔮.asIdeal))) hloc
    rwa [Ideal.comap_map_eq_self_of_faithfullyFlat,
      Ideal.comap_map_eq_self_of_faithfullyFlat] at this
  have hcomm : ψ.comp (algebraMap Γ(X, U) (Localization.AtPrime P)) =
      (algebraMap Γ(Y, V) (Localization.AtPrime 𝔮.asIdeal)).comp (π.appLE U V hVU).hom :=
    RingHom.ext fun x => Localization.localRingHom_to_map P 𝔮.asIdeal _ h𝔮 x
  rw [Ideal.map_map, Ideal.map_map, RingHom.algebraMap_toAlgebra, hcomm, ← Ideal.map_map,
    ← Ideal.map_map, hIJ]