SmoothProperCurve_finrank_levelSet_field_of_twoChartPoleDatum.lean

theorem finite_aeval_baseChange {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
  (f : A)
    (hfin : (Polynomial.aeval f : R[X] →ₐ[R] A).toRingHom.Finite)
    (L : Type u) [CommRing L] [Algebra R L] :
    (Polynomial.aeval ((1 : L) ⊗ₜ[R] f) : L[X] →ₐ[L] L ⊗[R] A).toRingHom.Finite

theorem isLocalization_away_of_eq_basicOpen {U W : C.Opens} (hU : IsAffineOpen U) (f : Γ(C, U))
    (hW : W ≤ U) (h : W = C.basicOpen f) :
    letI := (C.presheaf.map (homOfLE hW).op).hom.toAlgebra
    IsLocalization.Away f Γ(C, W) := by
  subst h
  exact hU.isLocalization_basicOpen f

theorem isLocalization_away_baseChange {U W : C.Opens} (hU : IsAffineOpen U) (f : Γ(C, U))
    (hW : W ≤ U) (h : W = C.basicOpen f) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c W
    letI := (Algebra.TensorProduct.map (AlgHom.id L L)
      (Scheme.TwoAffineOpenCover.restrictAlgHom c hW)).toRingHom.toAlgebra
    IsLocalization.Away ((1 : L) ⊗ₜ[R] f) (L ⊗[R] Γ(C, W)) := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom c U
  let := Scheme.TwoAffineOpenCover.algebraOfHom c W
  let algUW : Algebra Γ(C, U) Γ(C, W) := (C.presheaf.map (homOfLE hW).op).hom.toAlgebra
  have : IsScalarTower R Γ(C, U) Γ(C, W) := IsScalarTower.of_algebraMap_eq fun r =>
    ((Scheme.TwoAffineOpenCover.restrictAlgHom c hW).commutes r).symm
  have : IsLocalization.Away f Γ(C, W) := isLocalization_away_of_eq_basicOpen hU f hW h
  have hρ : Scheme.TwoAffineOpenCover.restrictAlgHom c hW = IsScalarTower.toAlgHom R Γ(C, U) Γ(C,
    W) := by
    ext x; rfl
  let alg : Algebra (L ⊗[R] Γ(C, U)) (L ⊗[R] Γ(C, W)) :=
    (Algebra.TensorProduct.map (AlgHom.id L L)
      (Scheme.TwoAffineOpenCover.restrictAlgHom c hW)).toRingHom.toAlgebra
  have H : (algebraMap (L ⊗[R] (C.presheaf.obj (Opposite.op U))) (L ⊗[R] (C.presheaf.obj
    (Opposite.op W)))).comp
        Algebra.TensorProduct.includeRight.toRingHom =
      Algebra.TensorProduct.includeRight.toRingHom.comp
        (algebraMap (C.presheaf.obj (Opposite.op U)) (C.presheaf.obj (Opposite.op W))) := by
    ext t
    change (Algebra.TensorProduct.map (AlgHom.id L L) (Scheme.TwoAffineOpenCover.restrictAlgHom c
      hW))
      ((1 : L) ⊗ₜ[R] t) = (1 : L) ⊗ₜ[R] (algebraMap (C.presheaf.obj (Opposite.op U))
        (C.presheaf.obj (Opposite.op W)) t)
    rw [Algebra.TensorProduct.map_tmul]
    rfl
  have hloc := IsLocalization.tensorProduct_tensorProduct_right R L (Submonoid.powers f)
    (C.presheaf.obj (Opposite.op W)) H
  rw [Submonoid.map_powers] at hloc
  exact hloc

theorem finrank_quotient_tmul {R : Type u} [CommRing R] [Nontrivial R] {B : Type u} [CommRing B]
  [Algebra R B] (g : B)
    (L : Type u) [Field L] [Algebra R L] [Module.Free R (B ⧸ Ideal.span {g})] :
    Module.finrank L (L ⊗[R] B ⧸ Ideal.span {(1 : L) ⊗ₜ[R] g}) = Module.finrank R (B ⧸ Ideal.span
      {g})

theorem main
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : NeronModelInfra.SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (U V : C.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hUV : U ⊔ V = ⊤)
    (hUε : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hf : U ⊓ V = C.basicOpen f) (hg : U ⊓ V = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op).hom f *
      (C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g = 1)
    (m : ℕ)
    (hfree : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
      Module.Free R (Γ(C, V) ⧸ Ideal.span {g}))
    (hrank : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
      Module.finrank R (Γ(C, V) ⧸ Ideal.span {g}) = m)
    (hfin : letI := Scheme.TwoAffineOpenCover.algebraOfHom c U;
      (Polynomial.aeval f : Polynomial R →ₐ[R] Γ(C, U)).toRingHom.Finite)
    (hfinV : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
      (Polynomial.aeval g : Polynomial R →ₐ[R] Γ(C, V)).toRingHom.Finite)
    (L : Type u) [Field L] [Algebra R L] (x : L) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    Module.finrank L (L ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : L) ⊗ₜ[R] f - x ⊗ₜ[R] (1 : Γ(C, U))}) = m :=
      by
  let aU := Scheme.TwoAffineOpenCover.algebraOfHom c U
  let aV := Scheme.TwoAffineOpenCover.algebraOfHom c V
  let aW := Scheme.TwoAffineOpenCover.algebraOfHom c (U ⊓ V)
  let ρU := Scheme.TwoAffineOpenCover.restrictAlgHom c (inf_le_left : U ⊓ V ≤ U)
  let ρV := Scheme.TwoAffineOpenCover.restrictAlgHom c (inf_le_right : U ⊓ V ≤ V)
  let φ := Algebra.TensorProduct.map (AlgHom.id L L) ρU
  let ψ := Algebra.TensorProduct.map (AlgHom.id L L) ρV
  have hφ := isLocalization_away_baseChange c L hU f (inf_le_left : U ⊓ V ≤ U) hf
  have hψ := isLocalization_away_baseChange c L hV g (inf_le_right : U ⊓ V ≤ V) hg
  have hab : φ ((1 : L) ⊗ₜ[R] f) * ψ ((1 : L) ⊗ₜ[R] g) = 1 := by
    change (Algebra.TensorProduct.map (AlgHom.id L L) ρU) ((1 : L) ⊗ₜ[R] f) *
      (Algebra.TensorProduct.map (AlgHom.id L L) ρV) ((1 : L) ⊗ₜ[R] g) = 1
    rw [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.map_tmul,
      Algebra.TensorProduct.tmul_mul_tmul]
    change ((AlgHom.id L L) 1 * (AlgHom.id L L) 1) ⊗ₜ[R] ((C.presheaf.map (homOfLE (inf_le_left : U
      ⊓ V ≤ U)).op).hom f *
      (C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g) = 1
    rw [hfg, map_one, one_mul]
    rfl
  have hneU := AlgebraicGeometry.SmoothProperCurve.nontrivial_tensor_sections_of_twoChartPoleDatum
    R c ε U V hU hV hUV hUε f g hf hg hfg L
  have : IsDomain (L ⊗[R] Γ(C, U)) :=
    AlgebraicGeometry.isDomain_tensorProduct_sections_of_geometricallyIntegral c U hU L hneU
  have hinj := AlgebraicGeometry.SmoothProperCurve.injective_aeval_tensor_of_twoChartPoleDatum
    R c ε U V hU hV hUV hUε f g hf hg hfg L hneU
  have ha0 : ((1 : L) ⊗ₜ[R] f : L ⊗[R] Γ(C, U)) ≠ 0 := by
    intro h
    have : (Polynomial.aeval ((1 : L) ⊗ₜ[R] f) : L[X] →ₐ[L] L ⊗[R] Γ(C, U)) X =
        (Polynomial.aeval ((1 : L) ⊗ₜ[R] f) : L[X] →ₐ[L] L ⊗[R] Γ(C, U)) 0 := by
      rw [Polynomial.aeval_X, map_zero, h]
    exact Polynomial.X_ne_zero (hinj this)
  have hφinj : Function.Injective φ := by
    let := φ.toRingHom.toAlgebra
    exact IsLocalization.injective (M := Submonoid.powers ((1 : L) ⊗ₜ[R] f)) _
      (powers_le_nonZeroDivisors_of_noZeroDivisors ha0)
  have : Nontrivial (L ⊗[R] Γ(C, U ⊓ V)) := hφinj.nontrivial
  have hneV : Nontrivial (L ⊗[R] Γ(C, V)) := ψ.toRingHom.domain_nontrivial
  have : IsDomain (L ⊗[R] Γ(C, V)) :=
    AlgebraicGeometry.isDomain_tensorProduct_sections_of_geometricallyIntegral c V hV L hneV
  have hfinD := finite_aeval_baseChange f hfin L
  have hfinE := finite_aeval_baseChange g hfinV L
  have key := Algebra.finrank_quotient_span_sub_eq_of_isLocalization_away_of_mul_eq_one
    φ ψ ((1 : L) ⊗ₜ[R] f) ((1 : L) ⊗ₜ[R] g) hφ hψ hab hfinD hfinE hinj x
  have hx : (algebraMap L (L ⊗[R] Γ(C, U)) x) = x ⊗ₜ[R] (1 : Γ(C, U)) := by
    rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply]
  rw [hx] at key
  rw [key, finrank_quotient_tmul g L, hrank]

theorem _root_.AlgebraicGeometry.SmoothProperCurve.finrank_levelSet_field_of_twoChartPoleDatum
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (U V : C.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hUV : U ⊔ V = ⊤)
    (hUε : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hf : U ⊓ V = C.basicOpen f) (hg : U ⊓ V = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op).hom f *
      (C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g = 1)
    (m : ℕ)
    (hfree : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
      Module.Free R (Γ(C, V) ⧸ Ideal.span {g}))
    (hrank : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
      Module.finrank R (Γ(C, V) ⧸ Ideal.span {g}) = m)
    (hfin : letI := Scheme.TwoAffineOpenCover.algebraOfHom c U;
      (Polynomial.aeval f : Polynomial R →ₐ[R] Γ(C, U)).toRingHom.Finite)
    (hfinV : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
      (Polynomial.aeval g : Polynomial R →ₐ[R] Γ(C, V)).toRingHom.Finite)
    (L : Type u) [Field L] [Algebra R L] (x : L) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    Module.finrank L (L ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : L) ⊗ₜ[R] f - x ⊗ₜ[R] (1 : Γ(C, U))}) = m :=
  U3bRANK.main R c ε U V hU hV hUV hUε f g hf hg hfg m hfree hrank hfin hfinV L x