Scheme_TwoAffineOpenCover_bijective_algebraMap_sections_baseChange_of_isReduced.lean

theorem specMap_algebraMap_eq' (U : X.Opens) (hU : IsAffineOpen U) :
    letI := algebraOfHom c U
    Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, U))) = hU.fromSpec ≫ c := by
  let := algebraOfHom c U
  have halg : (algebraMap R Γ(X, U)) = ((Scheme.ΓSpecIso (.of R)).inv ≫ c.appLE ⊤ U le_top).hom :=
      rfl
  rw [halg, CommRingCat.ofHom_hom, Spec.map_comp, ← Scheme.isoSpec_Spec_inv, ←
      IsAffineOpen.fromSpec_top,
    IsAffineOpen.SpecMap_appLE_fromSpec c (isAffineOpen_top (Spec (.of R))) hU (le_top : U ≤ c ⁻¹ᵁ
        ⊤)]

theorem flat_sections [Flat c] (U : X.Opens) (hU : IsAffineOpen U) :
    letI := algebraOfHom c U; Module.Flat R Γ(X, U) := by
  let := algebraOfHom c U
  have hflat : Flat (Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, U)))) := by
    rw [specMap_algebraMap_eq' c U hU]; infer_instance
  exact (HasRingHomProperty.Spec_iff (P := @Flat)).mp hflat

theorem flat_prod' {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    [Module.Flat R M] [Module.Flat R N] : Module.Flat R (M × N)

theorem bijective_algebraMap_of_finrank_eq_one {B : Type u} [CommRing B] [Algebra R B] [IsLocalRing
    R]
    [Module.Finite R B] [Module.Free R B]
    (h1 : Module.finrank (IsLocalRing.ResidueField R) ((IsLocalRing.ResidueField R) ⊗[R] B) = 1) :
    Function.Bijective (algebraMap R B)

theorem bijective_algebraMap_of_forall_finrank_eq_one {B : Type u} [CommRing B] [Algebra R B]
    [Module.Finite R B] [Module.Projective R B]
    (h1 : ∀ 𝔭 : PrimeSpectrum R, Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R]
        B) = 1) :
    Function.Bijective (algebraMap R B)

theorem bijective_algebraMap_sections_baseChange_of_isReduced'
    {R : Type u} [CommRing R] [IsNoetherianRing R] [_root_.IsReduced R]
    {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) [Flat c]
    (hfin : Module.Finite R (𝒱.structureSheafSections c).H0 ∧ Module.Finite R
        (𝒱.structureSheafSections c).H1)
    (hH0 : ∀ (K : Type u) [Field K] [Algebra R K],
      Module.finrank K (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange K)) = 1)
    (A : Type u) [CommRing A] [Algebra R A] :
    letI := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤
    Function.Bijective (algebraMap A Γ(Limits.pullback c (specMap R A), ⊤)) := by
  classical
  let instA := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤
  set S := 𝒱.structureSheafSections c with hS
  have : Module.Flat R (𝒱.cover c).A0 := flat_sections c 𝒱.U0 𝒱.isAffineOpen_U0
  have : Module.Flat R (𝒱.cover c).A1 := flat_sections c 𝒱.U1 𝒱.isAffineOpen_U1
  have : Module.Flat R (𝒱.cover c).A01 := flat_sections c (𝒱.U0 ⊓ 𝒱.U1) 𝒱.isAffineOpen_inf
  have : Module.Flat R (S.M0 × S.M1) := flat_prod'
  have : Module.Flat R S.M01 := inferInstanceAs (Module.Flat R (𝒱.cover c).A01)
  have : Module.Finite R (LinearMap.ker S.cechDiff) := hfin.1
  have : Module.Finite R (S.M01 ⧸ LinearMap.range S.cechDiff) := hfin.2
  obtain ⟨G, ι0, ι1, comm, hG⟩ := TwoChartCech.exists_twoTermComplex_kerMapBaseChange_bijective
      S.cechDiff
  obtain ⟨hproj, hbc, hrank⟩ :=
    TwoChartCech.projective_ker_of_isReduced_of_kerMapBaseChange_bijective G ι0 ι1 comm hG (n := 1)
      (fun 𝔭 => hH0 𝔭.asIdeal.ResidueField)
  let instB := algebraOfHom c ⊤
  let eB : Γ(X, ⊤) ≃ₗ[R] S.H0 := LinearEquiv.ofBijective (𝒱.toH0 c) (toH0_bijective 𝒱 c)
  have : Module.Finite R Γ(X, ⊤) := Module.Finite.equiv eB.symm
  have : Module.Projective R Γ(X, ⊤) := Module.Projective.of_equiv eB.symm
  have hdim : ∀ 𝔭 : PrimeSpectrum R,
      Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R] Γ(X, ⊤)) = 1 := by
    intro 𝔭
    rw [(eB.baseChange R 𝔭.asIdeal.ResidueField _ _).finrank_eq]
    exact hrank 𝔭
  have hB : Function.Bijective (algebraMap R Γ(X, ⊤)) :=
      bijective_algebraMap_of_forall_finrank_eq_one hdim
  obtain ⟨e0, e1, e01, eH0, eH1, he0, he1, he01, heH0, -⟩ := exists_baseChangeIsos_structureSheaf 𝒱
      c A
  have hA : Function.Bijective (letI := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤;
      (𝒱.pullback c A).toH0 (Limits.pullback.snd c (specMap R A))) := toH0_bijective _ _
  let u : S.H0 := 𝒱.toH0 c 1
  have hu : (u : S.M0 × S.M1)
      = ((X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom 1,
          (X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom 1) := toH0_apply_coe 𝒱 c 1
  let eR : R ≃ₗ[R] S.H0 :=
    LinearEquiv.ofBijective ((𝒱.toH0 c) ∘ₗ Algebra.linearMap R Γ(X, ⊤)) ((toH0_bijective 𝒱 c).comp
        hB)
  have heR : eR 1 = u := by
    change 𝒱.toH0 c (algebraMap R Γ(X, ⊤) 1) = 𝒱.toH0 c 1
    rw [RingHom.map_one]
  let ι : A → A ⊗[R] S.H0 := fun a => a ⊗ₜ[R] u
  have hιbij : Function.Bijective ι := by
    have hι : ι = (eR.baseChange R A _ _) ∘ (TensorProduct.rid R A).symm := by
      funext a
      change a ⊗ₜ[R] u = (eR.baseChange R A _ _) ((TensorProduct.rid R A).symm a)
      rw [TensorProduct.rid_symm_apply, LinearEquiv.baseChange_tmul, heR]
    rw [hι]
    exact (eR.baseChange R A _ _).bijective.comp (TensorProduct.rid R A).symm.bijective
  have hE0 : ∀ a : A, e0 (a ⊗ₜ[R] ((X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom 1))
      = algebraMap A ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R A))).A0 a := by
    intro a
    have hsm : ∀ x : (𝒱.cover c).A0, a ⊗ₜ[R] x = a • ((1 : A) ⊗ₜ[R] x) := fun x => by
      rw [TensorProduct.smul_tmul', smul_eq_mul, mul_one]
    let s : (𝒱.cover c).A0 := (X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom 1
    have hs : s = 1 := map_one (X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom
    have hunit : e0 ((1 : A) ⊗ₜ[R] s) = (1 : ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap
        R A))).A0) :=
      (he0 s).trans ((congrArg
        (fun v : (𝒱.cover c).A0 => ((Limits.pullback.fst c (specMap R A)).app 𝒱.U0).hom v) hs).trans
        (map_one ((Limits.pullback.fst c (specMap R A)).app 𝒱.U0).hom))
    exact (congrArg (fun v : A ⊗[R] (𝒱.cover c).A0 => e0 v) (hsm s)).trans
      ((e0.toLinearEquiv.map_smul a ((1 : A) ⊗ₜ[R] s)).trans
        ((congrArg (fun v : ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R A))).A0 => a •
            v) hunit).trans
          ((Algebra.smul_def a (1 : ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R
              A))).A0)).trans (mul_one _))))
  have hE1 : ∀ a : A, e1 (a ⊗ₜ[R] ((X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom 1))
      = algebraMap A ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R A))).A1 a := by
    intro a
    have hsm : ∀ x : (𝒱.cover c).A1, a ⊗ₜ[R] x = a • ((1 : A) ⊗ₜ[R] x) := fun x => by
      rw [TensorProduct.smul_tmul', smul_eq_mul, mul_one]
    let s : (𝒱.cover c).A1 := (X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom 1
    have hs : s = 1 := map_one (X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom
    have hunit : e1 ((1 : A) ⊗ₜ[R] s) = (1 : ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap
        R A))).A1) :=
      (he1 s).trans ((congrArg
        (fun v : (𝒱.cover c).A1 => ((Limits.pullback.fst c (specMap R A)).app 𝒱.U1).hom v) hs).trans
        (map_one ((Limits.pullback.fst c (specMap R A)).app 𝒱.U1).hom))
    exact (congrArg (fun v : A ⊗[R] (𝒱.cover c).A1 => e1 v) (hsm s)).trans
      ((e1.toLinearEquiv.map_smul a ((1 : A) ⊗ₜ[R] s)).trans
        ((congrArg (fun v : ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R A))).A1 => a •
            v) hunit).trans
          ((Algebra.smul_def a (1 : ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R
              A))).A1)).trans (mul_one _))))
  have key : ∀ a : A,
      (letI := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤;
        (𝒱.pullback c A).toH0 (Limits.pullback.snd c (specMap R A))
          (algebraMap A Γ(Limits.pullback c (specMap R A), ⊤) a))
        = eH0 (TwoChartCech.kerBaseChangeHom S.cechDiff A (ι a)) := by
    intro a
    let := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤
    let := algebraOfHom (Limits.pullback.snd c (specMap R A)) (𝒱.pullback c A).U0
    let := algebraOfHom (Limits.pullback.snd c (specMap R A)) (𝒱.pullback c A).U1
    apply Subtype.ext
    rw [heH0, toH0_apply_coe, TwoChartCech.kerBaseChangeHom_apply_coe]
    change _ = (e0 (TensorProduct.prodRight R A A _ _ (((LinearMap.ker
        S.cechDiff).subtype.baseChange A) (a ⊗ₜ[R] u))).1,
      e1 (TensorProduct.prodRight R A A _ _ (((LinearMap.ker S.cechDiff).subtype.baseChange A) (a
          ⊗ₜ[R] u))).2)
    rw [LinearMap.baseChange_tmul, Submodule.subtype_apply, hu]
    let s : S.M0 × S.M1 :=
      ((X.presheaf.map (homOfLE (le_top : 𝒱.U0 ≤ ⊤)).op).hom 1,
        (X.presheaf.map (homOfLE (le_top : 𝒱.U1 ≤ ⊤)).op).hom 1)
    have hp : TensorProduct.prodRight R A A S.M0 S.M1 (a ⊗ₜ[R] s) =
        (a ⊗ₜ[R] s.1, a ⊗ₜ[R] s.2) :=
      TensorProduct.prodRight_tmul R A A S.M0 S.M1 a s
    have hrhs : (e0 (a ⊗ₜ[R] s.1), e1 (a ⊗ₜ[R] s.2)) =
        (algebraMap A ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R A))).A0 a,
          algebraMap A ((𝒱.pullback c A).cover (Limits.pullback.snd c (specMap R A))).A1 a) :=
      Prod.ext (hE0 a) (hE1 a)
    have hright := (congrArg
      (fun v : (A ⊗[R] S.M0) × (A ⊗[R] S.M1) => (e0 v.1, e1 v.2)) hp).trans hrhs
    exact (Prod.ext
      ((restrictAlgHom (Limits.pullback.snd c (specMap R A)) (le_top : (𝒱.pullback c A).U0 ≤
          ⊤)).commutes a)
      ((restrictAlgHom (Limits.pullback.snd c (specMap R A)) (le_top : (𝒱.pullback c A).U1 ≤
          ⊤)).commutes a)).trans
      hright.symm
  have hcomp : (letI := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤;
      ((𝒱.pullback c A).toH0 (Limits.pullback.snd c (specMap R A)))
        ∘ (algebraMap A Γ(Limits.pullback c (specMap R A), ⊤)))
      = eH0 ∘ (TwoChartCech.kerBaseChangeHom S.cechDiff A) ∘ ι := funext key
  have hbij : Function.Bijective (letI := algebraOfHom (Limits.pullback.snd c (specMap R A)) ⊤;
      ((𝒱.pullback c A).toH0 (Limits.pullback.snd c (specMap R A)))
        ∘ (algebraMap A Γ(Limits.pullback c (specMap R A), ⊤))) := by
    rw [hcomp]; exact eH0.bijective.comp ((hbc A).comp hιbij)
  exact (Function.Bijective.of_comp_iff' hA _).mp hbij

theorem bijective_algebraMap_sections_baseChange_of_isReduced
    {R : Type u} [CommRing R] [IsNoetherianRing R] [_root_.IsReduced R]
    {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) [Flat c]
    (hfin : Module.Finite R (𝒱.structureSheafSections c).H0 ∧ Module.Finite R
        (𝒱.structureSheafSections c).H1)
    (hH0 : ∀ (K : Type u) [Field K] [Algebra R K],
      Module.finrank K (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange K)) = 1)
    (A : Type u) [CommRing A] [Algebra R A] :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom
      (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
    Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
        ⊤)) :=
  bijective_algebraMap_sections_baseChange_of_isReduced' 𝒱 c hfin hH0 A