Scheme_TwoAffineOpenCover_exists_ideal_pullback_cover_ringEquiv_quotient_appLE_of_squareZero.lean

def quotMapEquiv : (A ⧸ (I.map (algebraMap B A))) ≃+* ((B ⧸ I) ⊗[B] A)

theorem quotMapEquiv_mk (a : A) :
    quotMapEquiv I A (Ideal.Quotient.mk _ a) = (1 : B ⧸ I) ⊗ₜ[B] a

theorem exists_ideal_pullback_cover_ringEquiv_quotient_appLE_of_squareZero
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    {B : Type u} [CommRing B] [Algebra R B] (I : Ideal B) (hI : I ^ 2 = ⊥) :
    let 𝒱B := 𝒱.pullback c B
    let cB := Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R B)
    let 𝒱BI := 𝒱.pullback c (B ⧸ I)
    let cBI := Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R (B ⧸ I))
    let σst := RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B
        (B ⧸ I)))
    ∃ (J0 : Ideal (𝒱B.cover cB).A0) (J1 : Ideal (𝒱B.cover cB).A1)
      (J01 : Ideal (𝒱B.cover cB).A01),
      J0 ^ 2 = ⊥ ∧ J1 ^ 2 = ⊥ ∧ J01 ^ 2 = ⊥ ∧
      ∃ (φ0 : (𝒱B.cover cB).A0 ⧸ J0 ≃+* (𝒱BI.cover cBI).A0)
        (φ1 : (𝒱B.cover cB).A1 ⧸ J1 ≃+* (𝒱BI.cover cBI).A1)
        (φ01 : (𝒱B.cover cB).A01 ⧸ J01 ≃+* (𝒱BI.cover cBI).A01),
        (∀ a, φ01 ((Ideal.Quotient.mk J01) ((𝒱B.cover cB).ρ0 a)) =
          (𝒱BI.cover cBI).ρ0 (φ0 ((Ideal.Quotient.mk J0) a))) ∧
        (∀ a, φ01 ((Ideal.Quotient.mk J01) ((𝒱B.cover cB).ρ1 a)) =
          (𝒱BI.cover cBI).ρ1 (φ1 ((Ideal.Quotient.mk J1) a))) ∧
        (∀ a, φ0 ((Ideal.Quotient.mk J0) a) =
          (σst.appLE 𝒱B.U0 𝒱BI.U0
            (Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_U0 𝒱 c
              (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom a) ∧
        (∀ a, φ1 ((Ideal.Quotient.mk J1) a) =
          (σst.appLE 𝒱B.U1 𝒱BI.U1
            (Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_U1 𝒱 c
              (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom a) ∧
        (∀ a, φ01 ((Ideal.Quotient.mk J01) a) =
          (σst.appLE (𝒱B.U0 ⊓ 𝒱B.U1) (𝒱BI.U0 ⊓ 𝒱BI.U1)
            (Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_inf 𝒱 c
              (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom a) := by
  intro 𝒱B cB 𝒱BI cBI σst
  obtain ⟨eR0, eR1, eR01, heR0, heR1, heR01⟩ :=
    exists_stage_baseChangeIsos_structureSheaf 𝒱 c B (B ⧸ I)
  have hmk0 : ∀ a : (𝒱B.cover cB).A0,
      ((quotMapEquiv I (𝒱B.cover cB).A0).trans eR0.toRingEquiv)
        (Ideal.Quotient.mk _ a)
      = (σst.appLE 𝒱B.U0 𝒱BI.U0
          (baseChangeSnd_preimage_U0 𝒱 c (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B
              (B ⧸ I)))).ge).hom a :=
    fun a => by rw [RingEquiv.trans_apply, quotMapEquiv_mk]; exact heR0 a
  have hmk1 : ∀ a : (𝒱B.cover cB).A1,
      ((quotMapEquiv I (𝒱B.cover cB).A1).trans eR1.toRingEquiv)
        (Ideal.Quotient.mk _ a)
      = (σst.appLE 𝒱B.U1 𝒱BI.U1
          (baseChangeSnd_preimage_U1 𝒱 c (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B
              (B ⧸ I)))).ge).hom a :=
    fun a => by rw [RingEquiv.trans_apply, quotMapEquiv_mk]; exact heR1 a
  have hmk01 : ∀ a : (𝒱B.cover cB).A01,
      ((quotMapEquiv I (𝒱B.cover cB).A01).trans eR01.toRingEquiv)
        (Ideal.Quotient.mk _ a)
      = (σst.appLE (𝒱B.U0 ⊓ 𝒱B.U1) (𝒱BI.U0 ⊓ 𝒱BI.U1)
          (baseChangeSnd_preimage_inf 𝒱 c (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B
              (B ⧸ I)))).ge).hom a :=
    fun a => by rw [RingEquiv.trans_apply, quotMapEquiv_mk]; exact heR01 a
  refine ⟨I.map (algebraMap B (𝒱B.cover cB).A0),
          I.map (algebraMap B (𝒱B.cover cB).A1),
          I.map (algebraMap B (𝒱B.cover cB).A01),
          by rw [← Ideal.map_pow, hI, Ideal.map_bot],
          by rw [← Ideal.map_pow, hI, Ideal.map_bot],
          by rw [← Ideal.map_pow, hI, Ideal.map_bot],
          (quotMapEquiv I (𝒱B.cover cB).A0).trans eR0.toRingEquiv,
          (quotMapEquiv I (𝒱B.cover cB).A1).trans eR1.toRingEquiv,
          (quotMapEquiv I (𝒱B.cover cB).A01).trans eR01.toRingEquiv,
          fun a => ?_, fun a => ?_, hmk0, hmk1, hmk01⟩
  · rw [hmk01, hmk0]
    refine (congrArg
      (σst.appLE (𝒱B.U0 ⊓ 𝒱B.U1) (𝒱BI.U0 ⊓ 𝒱BI.U1)
        (baseChangeSnd_preimage_inf 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom
      (cover_ρ0_apply 𝒱B cB a)).trans ?_
    refine Eq.trans ?_ (cover_ρ0_apply 𝒱BI cBI
      ((σst.appLE 𝒱B.U0 𝒱BI.U0
        (baseChangeSnd_preimage_U0 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom a)).symm
    exact congrArg (fun f => f.hom a)
      ((Scheme.Hom.map_appLE σst
        (baseChangeSnd_preimage_inf 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge
        (homOfLE (inf_le_left : 𝒱B.U0 ⊓ 𝒱B.U1 ≤ 𝒱B.U0)).op).trans
      (Scheme.Hom.appLE_map σst
        (baseChangeSnd_preimage_U0 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge
        (homOfLE (inf_le_left : 𝒱BI.U0 ⊓ 𝒱BI.U1 ≤ 𝒱BI.U0)).op).symm)
  · rw [hmk01, hmk1]
    refine (congrArg
      (σst.appLE (𝒱B.U0 ⊓ 𝒱B.U1) (𝒱BI.U0 ⊓ 𝒱BI.U1)
        (baseChangeSnd_preimage_inf 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom
      (cover_ρ1_apply 𝒱B cB a)).trans ?_
    refine Eq.trans ?_ (cover_ρ1_apply 𝒱BI cBI
      ((σst.appLE 𝒱B.U1 𝒱BI.U1
        (baseChangeSnd_preimage_U1 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge).hom a)).symm
    exact congrArg (fun f => f.hom a)
      ((Scheme.Hom.map_appLE σst
        (baseChangeSnd_preimage_inf 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge
        (homOfLE (inf_le_right : 𝒱B.U0 ⊓ 𝒱B.U1 ≤ 𝒱B.U1)).op).trans
      (Scheme.Hom.appLE_map σst
        (baseChangeSnd_preimage_U1 𝒱 c
          (RelPicard.LFP.stageHom R (IsScalarTower.toAlgHom R B (B ⧸ I)))).ge
        (homOfLE (inf_le_right : 𝒱BI.U0 ⊓ 𝒱BI.U1 ≤ 𝒱BI.U1)).op).symm)