NYLL
Module

Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.lean

Nyll.AlgebraicCurves.Models.Gluing.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
27 declarations indexed from sourceView source ↗

Module documentation

Coordinate maps from two-chart pole data

Two-chart pole data makes the coordinate map proper and finite, yields an affine open chart, and provides the base-change comparisons used to test transcendence on fibres.

Imports9
Imported by3

Declarations

abbrev

baseRingHom

L55 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.baseRingHom
Documentation

The base-ring map to the sections of the open subscheme, through the scheme structure map.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
abbrev Scheme.Opens.baseRingHom (U : C.Opens) : k →+* Γ((U : Scheme.{u}), ⊤)
abbrev

toSpecPolynomial

L60 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial
Documentation

The map to the affine polynomial line determined by the coordinate section.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
abbrev Scheme.Opens.toSpecPolynomial (U : C.Opens) (s : Γ(C, U)) :
    (U : Scheme.{u}) ⟶ Spec (CommRingCat.of k[X])
theorem

toSpecPolynomial_comp_C

L66 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial_comp_C
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.toSpecPolynomial_comp_C (U : C.Opens) (s : Γ(C, U)) :
    Scheme.Opens.toSpecPolynomial c U s ≫ Spec.map (CommRingCat.ofHom (Polynomial.C : k →+* k[X])) =
      U.ι ≫ c
theorem

comp_appTop'

L90 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.comp_appTop'
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section general
open IsLocalRing
open scoped _root_.AlgebraicGeometry.Scheme in
Lean source · statement
theorem Scheme.comp_appTop' {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).appTop = g.appTop ≫ f.appTop
theorem

stalkClosedPointTo_germ_top

L94 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.stalkClosedPointTo_germ_top
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section general
open IsLocalRing
open scoped _root_.AlgebraicGeometry.Scheme in
Lean source · statement
theorem Scheme.stalkClosedPointTo_germ_top {Y : Scheme.{u}} {R : CommRingCat.{u}} [IsLocalRing R]
    (f : Spec R ⟶ Y) (t : Γ(Y, ⊤)) :
    (Scheme.stalkClosedPointTo f).hom (Y.presheaf.germ ⊤ (f.base (closedPoint R)) trivial t) =
      (Scheme.ΓSpecIso R).hom (f.appTop t)
theorem

ι_app_self_apply

L105 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.ι_app_self_apply
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section general
open IsLocalRing
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.ι_app_self_apply {X : Scheme.{u}} (U : X.Opens) (s : Γ(X, U)) :
    U.ι.app U s = (U : Scheme.{u}).presheaf.map (eqToHom U.ι_preimage_self).op
      (U.topIso.inv s)
theorem

toSpecPolynomial_appTop_X

L115 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial_appTop_X
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.toSpecPolynomial_appTop_X (U : C.Opens) (s : Γ(C, U)) :
    (Scheme.Opens.toSpecPolynomial c U s).appTop
      ((Scheme.ΓSpecIso (CommRingCat.of k[X])).inv X) = U.topIso.inv s
theorem

ΓSpecIso_appTop_topIso_inv_eq

L128 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.ΓSpecIso_appTop_topIso_inv_eq
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.ΓSpecIso_appTop_topIso_inv_eq (U : C.Opens) (s : Γ(C, U))
    {R K : Type u} [CommRing R] [Field K] [Algebra R K]
    {i₁ : Spec (.of K) ⟶ (U : Scheme.{u})} {i₂ : Spec (.of R) ⟶ Spec (.of k[X])}
    (w : i₁ ≫ Scheme.Opens.toSpecPolynomial c U s =
      Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂) :
    (Scheme.ΓSpecIso (.of K)).hom (i₁.appTop (U.topIso.inv s)) =
      algebraMap R K ((Scheme.ΓSpecIso (.of R)).hom
        (i₂.appTop ((Scheme.ΓSpecIso (CommRingCat.of k[X])).inv X)))
theorem

valuativeCriterion_existence_toSpecPolynomial_of_twoChart

L149 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.valuativeCriterion_existence_toSpecPolynomial_of_twoChart
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
open IsLocalRing in
Lean source · statement
theorem Scheme.Opens.valuativeCriterion_existence_toSpecPolynomial_of_twoChart
    [IsProper c] (U V W : C.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (hUVW : ∀ x : C, x ∈ U → x ∈ V →
      x ∈ W)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : W = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE hWU).op).hom f *
      (C.presheaf.map (homOfLE hWV).op).hom g = 1) :
    ValuativeCriterion.Existence (Scheme.Opens.toSpecPolynomial c U f)
theorem

isProper_toSpecPolynomial_of_twoChart

L243 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.isProper_toSpecPolynomial_of_twoChart
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.isProper_toSpecPolynomial_of_twoChart
    [IsProper c] (U V W : C.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (hUVW : ∀ x : C, x ∈ U → x ∈ V →
      x ∈ W)
    (hU : IsAffineOpen U) (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : W = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE hWU).op).hom f *
      (C.presheaf.map (homOfLE hWV).op).hom g = 1) :
    IsProper (Scheme.Opens.toSpecPolynomial c U f)
theorem

finite_eval₂RingHom_of_twoChart

L267 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.finite_eval₂RingHom_of_twoChart
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.finite_eval₂RingHom_of_twoChart
    [IsProper c] (U V W : C.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (hUVW : ∀ x : C, x ∈ U → x ∈ V →
      x ∈ W)
    (hU : IsAffineOpen U) (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : W = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE hWU).op).hom f *
      (C.presheaf.map (homOfLE hWV).op).hom g = 1) :
    (Polynomial.eval₂RingHom (Scheme.Opens.baseRingHom c U) (U.topIso.inv f)).Finite
theorem

ι_appTop_comp_topIso_hom

L301 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.ι_appTop_comp_topIso_hom
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.ι_appTop_comp_topIso_hom {X : Scheme.{u}} (U : X.Opens) :
    U.ι.appTop ≫ U.topIso.hom = X.presheaf.map (homOfLE le_top).op
theorem

topIso_hom_comp_baseRingHom

L308 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.topIso_hom_comp_baseRingHom
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.topIso_hom_comp_baseRingHom (U : C.Opens) :
    U.topIso.hom.hom.comp (Scheme.Opens.baseRingHom c U) =
      (Scheme.TwoAffineOpenCover.algebraOfHom c U).algebraMap
theorem

finite_aeval_of_twoChart

L320 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.finite_aeval_of_twoChart
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · full declaration
theorem Scheme.Opens.finite_aeval_of_twoChart
    [IsProper c] (U V W : C.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (hUVW : ∀ x : C, x ∈ U → x ∈ V →
      x ∈ W)
    (hU : IsAffineOpen U) (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : W = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE hWU).op).hom f *
      (C.presheaf.map (homOfLE hWV).op).hom g = 1) :
    let _ := Scheme.TwoAffineOpenCover.algebraOfHom c U
    (Polynomial.aeval f : k[X] →ₐ[k] Γ(C, U)).toRingHom.Finite := by
  let _ := Scheme.TwoAffineOpenCover.algebraOfHom c U
  have h := Scheme.Opens.finite_eval₂RingHom_of_twoChart c U V W hWU hWV hUVW hU f g hcov hUV hfg
  have hiso : (U.topIso.hom.hom : Γ((U : Scheme.{u}), ⊤) →+* Γ(C, U)).Finite :=
    RingHom.Finite.of_surjective _ (fun y => ⟨U.topIso.inv.hom y, by
      rw [← CommRingCat.comp_apply, Iso.inv_hom_id]; rfl⟩)
  have hcomp := hiso.comp h
  convert hcomp using 1
  refine Polynomial.ringHom_ext (fun r => ?_) ?_
  · change (Polynomial.aeval f : k[X] →ₐ[k] Γ(C, U)) (Polynomial.C r) = _
    rw [Polynomial.aeval_C, RingHom.comp_apply, Polynomial.coe_eval₂RingHom, Polynomial.eval₂_C,
      ← RingHom.comp_apply, Scheme.Opens.topIso_hom_comp_baseRingHom]
  · change (Polynomial.aeval f : k[X] →ₐ[k] Γ(C, U)) Polynomial.X = _
    rw [Polynomial.aeval_X, RingHom.comp_apply, Polynomial.coe_eval₂RingHom, Polynomial.eval₂_X,
      ← CommRingCat.comp_apply, Iso.inv_hom_id]
    rfl
theorem

isProper_toSpecPolynomial_of_twoChart'

L354 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.isProper_toSpecPolynomial_of_twoChart'
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.isProper_toSpecPolynomial_of_twoChart' [IsNoetherianRing k]
    [IsProper c] (U V W : C.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (hUVW : ∀ x : C, x ∈ U → x ∈ V →
      x ∈ W)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : W = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE hWU).op).hom f *
      (C.presheaf.map (homOfLE hWV).op).hom g = 1) :
    IsProper (Scheme.Opens.toSpecPolynomial c U f)
def

bcSection

L390 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.bcSection
Documentation

The coordinate section on the pulled-back open obtained from the restricted projection.

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section BaseChangeSquare
variable {k' : Type u} [CommRing k'] (ρ : k →+* k')
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
def Scheme.Opens.bcSection (U : C.Opens) (f : Γ(C, U)) :
    Γ(pullback c (Spec.map (CommRingCat.ofHom ρ)), (pullback.fst c (Spec.map
      (CommRingCat.ofHom ρ))) ⁻¹ᵁ U)
theorem

resLE_toSpecPolynomial

L398 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.resLE_toSpecPolynomial
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section BaseChangeSquare
variable {k' : Type u} [CommRing k'] (ρ : k →+* k')
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.resLE_toSpecPolynomial (U : C.Opens) (f : Γ(C, U)) :
    (pullback.fst c (Spec.map (CommRingCat.ofHom ρ))).resLE U _ le_rfl ≫
        Scheme.Opens.toSpecPolynomial c U f =
      Scheme.Opens.toSpecPolynomial (pullback.snd c (Spec.map (CommRingCat.ofHom ρ)))
          ((pullback.fst c (Spec.map (CommRingCat.ofHom ρ))) ⁻¹ᵁ U)
          (Scheme.Opens.bcSection c ρ U f) ≫
        Spec.map (CommRingCat.ofHom (Polynomial.mapRingHom ρ))
theorem

topIso_inv_resLE_appTop_topIso_hom

L447 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.topIso_inv_resLE_appTop_topIso_hom
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section BaseChangeSquare
variable {k' : Type u} [CommRing k'] (ρ : k →+* k')
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.topIso_inv_resLE_appTop_topIso_hom {X Y : Scheme.{u}} (ι : X ⟶ Y) (U :
  Y.Opens) :
    U.topIso.inv ≫ (ι.resLE U (ι ⁻¹ᵁ U) le_rfl).appTop ≫ (ι ⁻¹ᵁ U).topIso.hom = ι.app U
theorem

bcSection_eq

L457 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.bcSection_eq
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
section BaseChangeSquare
variable {k' : Type u} [CommRing k'] (ρ : k →+* k')
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · statement
theorem Scheme.Opens.bcSection_eq (U : C.Opens) (f : Γ(C, U)) :
    Scheme.Opens.bcSection c ρ U f = ((pullback.fst c (Spec.map
      (CommRingCat.ofHom ρ))).app U).hom f
theorem

SpecMap_mapRingHom_injective_of_quotient

L468 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.SpecMap_mapRingHom_injective_of_quotient
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {k : Type u} [CommRing k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem SpecMap_mapRingHom_injective_of_quotient (I : Ideal k) [I.IsPrime] :
    Function.Injective (Spec.map (CommRingCat.ofHom
      (Polynomial.mapRingHom (algebraMap k (FractionRing (k ⧸ I)))))).base
abbrev

fibreField

L500 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.fibreField
Documentation

The fraction field of the residue-domain quotient at the chosen base prime.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open IsLocalRing
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
Lean source · statement
abbrev fibreField (y : PrimeSpectrum R) : Type u
theorem

mem_range_SpecMap_fibreField

L502 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.mem_range_SpecMap_fibreField
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open IsLocalRing
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem mem_range_SpecMap_fibreField (y : PrimeSpectrum R) :
    (y : Spec (CommRingCat.of R)) ∈ Set.range (Spec.map (CommRingCat.ofHom
      (algebraMap R (fibreField y)))).base
theorem

transcendental_germToFunctionField_of_sections

L513 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.transcendental_germToFunctionField_of_sections
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open IsLocalRing
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
theorem transcendental_germToFunctionField_of_sections {K : Type u} [Field K] {X : Scheme.{u}}
  [IsIntegral X]
    (cK : X ⟶ Spec (CommRingCat.of K)) (U : X.Opens) [Nonempty U] (s : Γ(X, U))
    (hs : letI := Scheme.TwoAffineOpenCover.algebraOfHom cK U; Transcendental K s) :
    let _ := (AlgebraicCurve.baseToFunctionField cK).toAlgebra
    Transcendental K ((X.germToFunctionField U).hom s) := by
  let _ := Scheme.TwoAffineOpenCover.algebraOfHom cK U
  let _ := (AlgebraicCurve.baseToFunctionField cK).toAlgebra
  let θ : Γ(X, U) →ₐ[K] X.functionField :=
    { (X.germToFunctionField U).hom with
      commutes' := fun k => by
        change (X.germToFunctionField U).hom ((cK.appLE ⊤ U le_top).hom ((Scheme.ΓSpecIso
          (.of K)).inv.hom k)) =
          (X.presheaf.germ ⊤ (genericPoint X) trivial).hom (cK.appTop.hom ((Scheme.ΓSpecIso
            (.of K)).inv.hom k))
        dsimp only [Scheme.Hom.appLE]
        erw [CommRingCat.comp_apply]
        change (X.presheaf.map (homOfLE le_top).op ≫ X.presheaf.germ U (genericPoint X) _).hom _ = _
        rw [TopCat.Presheaf.germ_res]
        rfl }
  have hθ : Function.Injective θ := germ_injective_of_isIntegral X _ _
  rw [transcendental_iff_injective] at hs ⊢
  intro p q hpq
  apply hs
  apply hθ
  change aeval (θ s) p = aeval (θ s) q at hpq
  simpa only [Polynomial.aeval_algHom_apply] using hpq
theorem

isAffineOpen_and_finite_aeval_of_twoChart_of_le

L542 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_of_le
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open IsLocalRing
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · full declaration
theorem Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_of_le [IsNoetherianRing R]
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (U V W : C.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (hUVW : ∀ x : C, x ∈ U → x ∈ V → x ∈ W)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : W = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE hWU).op).hom f *
      (C.presheaf.map (homOfLE hWV).op).hom g = 1)
    (hft : ∀ (K : Type u) [Field K] [Algebra R K],
      let _ := Scheme.TwoAffineOpenCover.algebraOfHom
        (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
        ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ U);
      Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app U).hom f)) :
    IsAffineOpen U ∧
      (letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
       (Polynomial.aeval f : R[X] →ₐ[R] Γ(C, U)).toRingHom.Finite) := by
  let _ := Scheme.Opens.isProper_toSpecPolynomial_of_twoChart' c U V W hWU hWV hUVW f g hcov hUV hfg
  set φ := Scheme.Opens.toSpecPolynomial c U f with hφ
  have hqf : LocallyQuasiFinite φ := by
    refine LocallyQuasiFinite.of_finite_preimage_singleton φ (fun p => ?_)
    set y : PrimeSpectrum R := (Spec.map (CommRingCat.ofHom (Polynomial.C :
      R →+* R[X]))).base p with hy
    set κ := fibreField y
    set ρ : R →+* κ := algebraMap R κ with hρ
    set ξ := Spec.map (CommRingCat.ofHom ρ) with hξ
    set ι := pullback.fst c ξ with hι
    set c' := pullback.snd c ξ with hc'
    set U' := ι ⁻¹ᵁ U with hU'
    set r := ι.resLE U U' le_rfl with hr
    let _ : IsIntegral (pullback c ξ) := SmoothProperCurve.isIntegral_pullback_Spec_field R c ξ
    set φ' := Scheme.Opens.toSpecPolynomial c' U' (Scheme.Opens.bcSection c ρ U f) with hφ'
    set πX := Spec.map (CommRingCat.ofHom (Polynomial.mapRingHom ρ)) with hπX
    have hsq : r ≫ φ = φ' ≫ πX := Scheme.Opens.resLE_toSpecPolynomial c ρ U f
    have hlift : ∀ u : (U : Scheme.{u}), φ.base u = p → ∃ u' : (U' : Scheme.{u}), r.base u' =
      u := by
      intro u hu
      have hcu : c.base (U.ι.base u) = y := by
        have key : (Scheme.Opens.toSpecPolynomial c U f ≫
            Spec.map (CommRingCat.ofHom (Polynomial.C : R →+* R[X]))).base u = (U.ι ≫
              c).base u := by
          rw [Scheme.Opens.toSpecPolynomial_comp_C c U f]
        change (U.ι ≫ c).base u = (Spec.map (CommRingCat.ofHom (Polynomial.C : R →+* R[X]))).base p
        rw [← key, ← hu]
        rfl
      have hmem : U.ι.base u ∈ Set.range ι.base := by
        rw [hι, Scheme.Pullback.range_fst]
        change c.base (U.ι.base u) ∈ Set.range ξ.base
        rw [hcu]; exact mem_range_SpecMap_fibreField y
      obtain ⟨x', hx'⟩ := hmem
      have hx'U : x' ∈ U' := by change ι.base x' ∈ U; rw [hx']; exact u.2
      refine ⟨⟨x', hx'U⟩, ?_⟩
      apply U.ι.isOpenEmbedding.injective
      change (r ≫ U.ι).base ⟨x', hx'U⟩ = U.ι.base u
      rw [hr, Scheme.Hom.resLE_comp_ι]
      exact hx'
    by_cases hne : Nonempty U'
    · let _ := hne
      have hs : letI := (AlgebraicCurve.baseToFunctionField c').toAlgebra
          Transcendental κ ((pullback c ξ).germToFunctionField U'
            (Scheme.Opens.bcSection c ρ U f)) := by
        rw [Scheme.Opens.bcSection_eq]
        exact transcendental_germToFunctionField_of_sections c' U' _ (hft κ)
      have hQ : ∀ p', (φ'.base ⁻¹' {p'}).Finite := fun p' =>
        Scheme.Opens.finite_preimage_singleton_toSpecPolynomial c' U'
          (Scheme.Opens.bcSection c ρ U f) hs p'
      have hS : (πX.base ⁻¹' {p}).Finite :=
        Set.Subsingleton.finite fun a ha b hb =>
          SpecMap_mapRingHom_injective_of_quotient y.asIdeal (ha.trans hb.symm)
      refine ((hS.biUnion fun p' _ => hQ p').image r.base).subset ?_
      intro u hu
      obtain ⟨u', rfl⟩ := hlift u hu
      refine ⟨u', Set.mem_biUnion (x := φ'.base u') ?_ rfl, rfl⟩
      change (φ' ≫ πX).base u' = p
      rw [← hsq]
      exact hu
    · convert Set.finite_empty
      ext u
      simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_empty_iff_false, iff_false]
      intro hu
      obtain ⟨u', -⟩ := hlift u hu
      exact hne ⟨⟨u'.1, u'.2⟩⟩
  let _ : IsFinite φ := IsFinite.of_isProper_of_locallyQuasiFinite φ
  have hUaff : IsAffine (U : Scheme.{u}) := isAffine_of_isAffineHom φ
  exact ⟨hUaff, Scheme.Opens.finite_aeval_of_twoChart c U V W hWU hWV hUVW hUaff f g hcov hUV hfg⟩
theorem

isAffineOpen_and_finite_aeval_of_twoChart_impl

L627 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_impl
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open IsLocalRing
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · full declaration
theorem Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_impl [IsNoetherianRing R]
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : 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)
    (hft : ∀ (K : Type u) [Field K] [Algebra R K],
      let _ := Scheme.TwoAffineOpenCover.algebraOfHom
        (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
        ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ U);
      Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app U).hom f)) :
    IsAffineOpen U ∧
      (letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
       (Polynomial.aeval f : R[X] →ₐ[R] Γ(C, U)).toRingHom.Finite) :=
  Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_of_le c U V
    (U ⊓ V) inf_le_left inf_le_right
    (fun _ hu hv => ⟨hu, hv⟩) f g hcov hUV hfg hft
theorem

isAffineOpen_and_finite_aeval_of_twoChart_right_impl

L646 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_right_impl
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open IsLocalRing
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Opens in
Lean source · full declaration
theorem Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_right_impl [IsNoetherianRing R]
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hVU : U ⊓ V = C.basicOpen f)
    (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)
    (hft : ∀ (K : Type u) [Field K] [Algebra R K],
      let _ := Scheme.TwoAffineOpenCover.algebraOfHom
        (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
        ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ V);
      Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app V).hom g)) :
    IsAffineOpen V ∧
      (letI := Scheme.TwoAffineOpenCover.algebraOfHom c V
       (Polynomial.aeval g : R[X] →ₐ[R] Γ(C, V)).toRingHom.Finite) :=
  Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_of_le c V U
    (U ⊓ V) inf_le_right inf_le_left
    (fun _ hv hu => ⟨hu, hv⟩) g f (by rw [sup_comm]; exact hcov) hVU
      (by rw [mul_comm]; exact hfg) hft
theorem

isAffineOpen_and_finite_aeval_of_twoChart

L672 ↗
AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open CategoryTheory CategoryTheory.Limits _root_.AlgebraicGeometry in
with_weak_namespace _root_.AlgebraicCurves.Models.Gluing.Proofs
open Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart.AlgebraicGeometry in
with_weak_namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
open _root_.Polynomial in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart
    {R : Type u} [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec
      (CommRingCat.of R))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
    (hcov : U ⊔ V = ⊤) (hUV : 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)
    (hft : ∀ (K : Type u) [Field K] [Algebra R K],
      let _ := Scheme.TwoAffineOpenCover.algebraOfHom
        (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
        ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ U);
      Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app U).hom f)) :
    IsAffineOpen U ∧
      (letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
       (Polynomial.aeval f : R[X] →ₐ[R] Γ(C, U)).toRingHom.Finite) :=
  AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_impl c U V f g hcov
    hUV hfg hft

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.