NYLL
Module

Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.lean

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

Module documentation

Scheme Opens isAffineOpen and finite aeval of twoChart right

Two-chart pole data makes the right coordinate chart affine and its polynomial evaluation map finite, through the proper coordinate morphism and its field fibres.

Imports9
Imported by4

Declarations

abbrev

baseRingHom

L56 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.AlgebraicGeometry.Scheme.Opens.baseRingHom
Documentation

The base-ring homomorphism to global sections of the open subscheme induced by its structural morphism.

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_right
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

L62 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.AlgebraicGeometry.Scheme.Opens.toSpecPolynomial
Documentation

The map from the open subscheme to the affine line defined by evaluating the polynomial variable at the given 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_right
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

L68 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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_right.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_right
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_right.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_right
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_right.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_right
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_right.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_right
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_right.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_right
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_right.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_right
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

L244 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L268 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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_right.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_right
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_right.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_right
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_right.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_right
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_right.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_right
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

L391 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.AlgebraicGeometry.Scheme.Opens.bcSection
Documentation

The section on the inverse-image open obtained by pulling back the given section along the base-change 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_right
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

L399 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L450 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L460 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L471 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L503 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.AlgebraicGeometry.fibreField
Documentation

The fraction field of the quotient by the prime ideal represented by the given base point.

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_right
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

L505 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L516 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L545 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L630 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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

L649 ↗
AlgebraicCurves.Models.Gluing.Proofs.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right.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_right
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_right

L675 ↗
AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_right
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_right
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_right.AlgebraicGeometry in
with_weak_namespace Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right
open _root_.Polynomial in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_right
    {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 = ⊤) (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) :=
  AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_right_impl c U V f g
    hcov hVU hfg hft

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