NYLL
Module

SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
52 declarations indexed from sourceView source ↗

Module documentation

The projective morphism associated with finite-map data

The two coordinate functions in finite-map data glue to a morphism to the projective line. Its chart preimages are the given affine opens and its projective coordinate sections pull back to the original functions.

Imports2
Imported by2

Declarations

def

awayDesc

L58 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.awayDesc
Documentation

The homogeneous localization map induced by a ring homomorphism and a chosen inverse of the localized element.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section AwayDesc
variable {A B : Type*} [CommRing A] [CommRing B] {σ : Type*} [SetLike σ A] [AddSubgroupClass σ A]
  (𝒜 : ℕ → σ) [GradedRing 𝒜]
Lean source · statement
def awayDesc (χ : A →+* B) (x : A) (v : B) (hv : χ x * v = 1) :
    HomogeneousLocalization.Away 𝒜 x →+* B
theorem

awayDesc_mk

L63 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.awayDesc_mk
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section AwayDesc
variable {A B : Type*} [CommRing A] [CommRing B] {σ : Type*} [SetLike σ A] [AddSubgroupClass σ A]
  (𝒜 : ℕ → σ) [GradedRing 𝒜]
Lean source · statement
theorem awayDesc_mk (χ : A →+* B) (x : A) (v : B) (hv : χ x * v = 1) {d : ℕ} (hx : x ∈ 𝒜 d)
    (n : ℕ) (a : A) (ha : a ∈ 𝒜 (n • d)) :
    awayDesc 𝒜 χ x v hv (Away.mk 𝒜 hx n a ha) = χ a * v ^ n
theorem

awayDesc_fromZeroRingHom

L71 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.awayDesc_fromZeroRingHom
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section AwayDesc
variable {A B : Type*} [CommRing A] [CommRing B] {σ : Type*} [SetLike σ A] [AddSubgroupClass σ A]
  (𝒜 : ℕ → σ) [GradedRing 𝒜]
Lean source · statement
theorem awayDesc_fromZeroRingHom (χ : A →+* B) (x : A) (v : B) (hv : χ x * v = 1) (a : 𝒜 0) :
    awayDesc 𝒜 χ x v hv (fromZeroRingHom 𝒜 _ a) = χ a
theorem

eval₂_smul_of_isHomogeneous

L82 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.eval₂_smul_of_isHomogeneous
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
Lean source · statement
theorem eval₂_smul_of_isHomogeneous {R S : Type*} [CommSemiring R] [CommSemiring S] {τ : Type*}
    {φ : MvPolynomial τ R} {n : ℕ} (hφ : φ.IsHomogeneous n) (i : R →+* S) (u : S) (v : τ → S) :
    MvPolynomial.eval₂ i (u • v) φ = u ^ n * MvPolynomial.eval₂ i v φ
theorem

X_mem

L100 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.X_mem
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem X_mem (j : Fin 2) : (MvPolynomial.X j : MvPolynomial (Fin 2) R) ∈ 𝒜 1
theorem

X_mul_X_mem

L103 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.X_mul_X_mem
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem X_mul_X_mem : (MvPolynomial.X 0 * MvPolynomial.X 1 : MvPolynomial (Fin 2) R) ∈ 𝒜 2
def

χ₀

L107 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₀
Documentation

The polynomial evaluation map for the projective chart with coordinates (1, f).

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def χ₀ (i : R →+* B) (f : B) : MvPolynomial (Fin 2) R →+* B
def

χ₁

L111 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₁
Documentation

The polynomial evaluation map for the projective chart with coordinates (g, 1).

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def χ₁ (i : R →+* B) (g : B) : MvPolynomial (Fin 2) R →+* B
theorem

χ₀_X_zero

L114 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₀_X_zero
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₀_X_zero (i : R →+* B) (f : B) : χ₀ i f (MvPolynomial.X 0) = 1
theorem

χ₀_X_one

L116 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₀_X_one
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₀_X_one (i : R →+* B) (f : B) : χ₀ i f (MvPolynomial.X 1) = f
theorem

χ₁_X_zero

L118 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₁_X_zero
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₁_X_zero (i : R →+* B) (g : B) : χ₁ i g (MvPolynomial.X 0) = g
theorem

χ₁_X_one

L120 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₁_X_one
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₁_X_one (i : R →+* B) (g : B) : χ₁ i g (MvPolynomial.X 1) = 1
theorem

χ₀_C

L122 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₀_C
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₀_C (i : R →+* B) (f : B) (r : R) : χ₀ i f (MvPolynomial.C r) = i r
theorem

χ₁_C

L124 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₁_C
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₁_C (i : R →+* B) (g : B) (r : R) : χ₁ i g (MvPolynomial.C r) = i r
theorem

comp_χ₀

L127 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.comp_χ₀
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem comp_χ₀ {B' : Type u} [CommRing B'] (ρ : B →+* B') (i : R →+* B) (f : B) :
    ρ.comp (χ₀ i f) = χ₀ (ρ.comp i) (ρ f)
theorem

comp_χ₁

L132 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.comp_χ₁
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem comp_χ₁ {B' : Type u} [CommRing B'] (ρ : B →+* B') (i : R →+* B) (g : B) :
    ρ.comp (χ₁ i g) = χ₁ (ρ.comp i) (ρ g)
theorem

χ₁_eq_of_mem

L137 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.χ₁_eq_of_mem
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem χ₁_eq_of_mem (i : R →+* B) (f g : B) (hfg : f * g = 1) {n : ℕ} {a : MvPolynomial (Fin 2) R}
    (ha : a ∈ 𝒜 n) : χ₁ i g a = g ^ n * χ₀ i f a
def

ψ₀

L147 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.ψ₀
Documentation

The degree-zero localization map on the chart where the first homogeneous coordinate is nonzero.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def ψ₀ (i : R →+* B) (f : B) : Away 𝒜 (MvPolynomial.X 0) →+* B
def

ψ₁

L152 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.ψ₁
Documentation

The degree-zero localization map on the chart where the second homogeneous coordinate is nonzero.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def ψ₁ (i : R →+* B) (g : B) : Away 𝒜 (MvPolynomial.X 1) →+* B
def

θ

L157 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.θ
Documentation

The localization map on the intersection of the two projective charts, using g as the inverse of f.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def θ (i : R →+* B) (f g : B) (hfg : f * g = 1) :
    Away 𝒜 (MvPolynomial.X 0 * MvPolynomial.X 1) →+* B
theorem

ψ₀_mk

L161 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.ψ₀_mk
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem ψ₀_mk (i : R →+* B) (f : B) (n : ℕ) (a : MvPolynomial (Fin 2) R) (ha : a ∈ 𝒜 (n • 1)) :
    ψ₀ i f (Away.mk 𝒜 (X_mem 0) n a ha) = χ₀ i f a
theorem

ψ₁_mk

L165 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.ψ₁_mk
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem ψ₁_mk (i : R →+* B) (g : B) (n : ℕ) (a : MvPolynomial (Fin 2) R) (ha : a ∈ 𝒜 (n • 1)) :
    ψ₁ i g (Away.mk 𝒜 (X_mem 1) n a ha) = χ₁ i g a
theorem

θ_mk

L169 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.θ_mk
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem θ_mk (i : R →+* B) (f g : B) (hfg : f * g = 1) (n : ℕ) (a : MvPolynomial (Fin 2) R)
    (ha : a ∈ 𝒜 (n • 2)) :
    θ i f g hfg (Away.mk 𝒜 X_mul_X_mem n a ha) = χ₀ i f a * g ^ n
theorem

comp_ψ₀

L174 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.comp_ψ₀
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem comp_ψ₀ {B' : Type u} [CommRing B'] (ρ : B →+* B') (i : R →+* B) (f : B) :
    ρ.comp (ψ₀ i f) = ψ₀ (ρ.comp i) (ρ f)
theorem

comp_ψ₁

L180 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.comp_ψ₁
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem comp_ψ₁ {B' : Type u} [CommRing B'] (ρ : B →+* B') (i : R →+* B) (g : B) :
    ρ.comp (ψ₁ i g) = ψ₁ (ρ.comp i) (ρ g)
theorem

ψ₀_fromZeroRingHom

L186 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.ψ₀_fromZeroRingHom
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem ψ₀_fromZeroRingHom (i : R →+* B) (f : B) (r : R) (hr : MvPolynomial.C r ∈ 𝒜 0) :
    ψ₀ i f (fromZeroRingHom 𝒜 _ ⟨MvPolynomial.C r, hr⟩) = i r
theorem

ψ₁_fromZeroRingHom

L190 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.ψ₁_fromZeroRingHom
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem ψ₁_fromZeroRingHom (i : R →+* B) (g : B) (r : R) (hr : MvPolynomial.C r ∈ 𝒜 0) :
    ψ₁ i g (fromZeroRingHom 𝒜 _ ⟨MvPolynomial.C r, hr⟩) = i r
theorem

θ_comp_awayMap₀

L194 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.θ_comp_awayMap₀
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem θ_comp_awayMap₀ (i : R →+* B) (f g : B) (hfg : f * g = 1) :
    (θ i f g hfg).comp (awayMap 𝒜 (X_mem 1) (rfl : (MvPolynomial.X 0 * MvPolynomial.X 1 :
      MvPolynomial (Fin 2) R) = _)) = ψ₀ i f
theorem

θ_comp_awayMap₁

L203 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.θ_comp_awayMap₁
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Charts
variable {R : Type u} [CommRing R] {B : Type u} [CommRing B]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem θ_comp_awayMap₁ (i : R →+* B) (f g : B) (hfg : f * g = 1) :
    (θ i f g hfg).comp (awayMap 𝒜 (X_mem 0) (mul_comm _ _ : (MvPolynomial.X 0 * MvPolynomial.X 1 :
      MvPolynomial (Fin 2) R) = _)) = ψ₁ i g
def

iOf

L225 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.iOf
Documentation

The base-ring map on sections of an open, obtained from the structure morphism and the global-sections isomorphism of Spec.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def iOf (W : C.Opens) : R →+* Γ(C, W)
theorem

map_comp_iOf

L228 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.map_comp_iOf
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem map_comp_iOf {W W' : C.Opens} (h : W' ≤ W) :
    (C.presheaf.map (homOfLE h).op).hom.comp (iOf c W) = iOf c W'
def

chart₀

L240 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.chart₀
Documentation

The morphism from the first affine chart to the projective line defined by the coordinates (1, f).

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
Lean source · statement
def chart₀ : Spec Γ(C, U) ⟶ Proj 𝒜
def

chart₁

L245 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.chart₁
Documentation

The morphism from the second affine chart to the projective line defined by the coordinates (g, 1).

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
Lean source · statement
def chart₁ : Spec Γ(C, V) ⟶ Proj 𝒜
theorem

specMap_comp_chart₀

L248 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.specMap_comp_chart₀
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
Lean source · statement
theorem specMap_comp_chart₀
    (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) :
    Spec.map (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op) ≫ chart₀ c U f =
      Spec.map (CommRingCat.ofHom (θ (iOf c (U ⊓ V)) _ _ hfg)) ≫
        Proj.awayι 𝒜 (MvPolynomial.X 0 * MvPolynomial.X 1) X_mul_X_mem two_pos
theorem

specMap_comp_chart₁

L263 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.specMap_comp_chart₁
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
Lean source · statement
theorem specMap_comp_chart₁
    (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) :
    Spec.map (C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op) ≫ chart₁ c V g =
      Spec.map (CommRingCat.ofHom (θ (iOf c (U ⊓ V)) _ _ hfg)) ≫
        Proj.awayι 𝒜 (MvPolynomial.X 0 * MvPolynomial.X 1) X_mul_X_mem two_pos
theorem

exists_of_homOfLE_comp_eq

L278 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.exists_of_homOfLE_comp_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
Lean source · statement
theorem exists_of_homOfLE_comp_eq {Y : Scheme.{u}} (hUV : U ⊔ V = ⊤) (φU : (U : Scheme.{u}) ⟶ Y)
    (φV : (V : Scheme.{u}) ⟶ Y) (h : C.homOfLE inf_le_left ≫ φU = C.homOfLE inf_le_right ≫ φV) :
    ∃ π : C ⟶ Y, U.ι ≫ π = φU ∧ V.ι ≫ π = φV
theorem

exists_fromSpec_comp_eq

L304 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.exists_fromSpec_comp_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Glue
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V))
Lean source · statement
theorem exists_fromSpec_comp_eq (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hUV : U ⊔ V = ⊤)
    (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) :
    ∃ π : C ⟶ Proj 𝒜, hU.fromSpec ≫ π = chart₀ c U f ∧ hV.fromSpec ≫ π = chart₁ c V g
theorem

opens_ext_of_fromSpec

L330 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.opens_ext_of_fromSpec
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
Lean source · statement
theorem opens_ext_of_fromSpec (hUV : U ⊔ V = ⊤) {W₁ W₂ : C.Opens}
    (h₀ : hU.fromSpec ⁻¹ᵁ W₁ = hU.fromSpec ⁻¹ᵁ W₂) (h₁ : hV.fromSpec ⁻¹ᵁ W₁ = hV.fromSpec ⁻¹ᵁ W₂) :
    W₁ = W₂
theorem

hom_ext_of_fromSpec

L341 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.hom_ext_of_fromSpec
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
Lean source · statement
theorem hom_ext_of_fromSpec (hUV : U ⊔ V = ⊤) {Y : Scheme.{u}} {p q : C ⟶ Y}
    (h₀ : hU.fromSpec ≫ p = hU.fromSpec ≫ q) (h₁ : hV.fromSpec ≫ p = hV.fromSpec ≫ q) : p = q
theorem

chart₀_preimage_basicOpen_X_zero

L354 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.chart₀_preimage_basicOpen_X_zero
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
Lean source · statement
theorem chart₀_preimage_basicOpen_X_zero :
    chart₀ c U f ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 0) = ⊤
theorem

chart₁_preimage_basicOpen_X_one

L360 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.chart₁_preimage_basicOpen_X_one
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
Lean source · statement
theorem chart₁_preimage_basicOpen_X_one :
    chart₁ c V g ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 1) = ⊤
theorem

chart₀_preimage_basicOpen_X_one

L366 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.chart₀_preimage_basicOpen_X_one
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
Lean source · statement
theorem chart₀_preimage_basicOpen_X_one :
    chart₀ c U f ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 1) = PrimeSpectrum.basicOpen f
theorem

chart₁_preimage_basicOpen_X_zero

L376 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.chart₁_preimage_basicOpen_X_zero
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
Lean source · statement
theorem chart₁_preimage_basicOpen_X_zero :
    chart₁ c V g ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 0) = PrimeSpectrum.basicOpen g
theorem

preimage_basicOpen_X_zero

L388 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.preimage_basicOpen_X_zero
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem preimage_basicOpen_X_zero (π : C ⟶ Proj 𝒜) (h₀ : hU.fromSpec ≫ π = chart₀ c U f)
    (h₁ : hV.fromSpec ≫ π = chart₁ c V g) (hUV : U ⊔ V = ⊤) (hg : U ⊓ V = C.basicOpen g) :
    π ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 0) = U
theorem

preimage_basicOpen_X_one

L398 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.preimage_basicOpen_X_one
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem preimage_basicOpen_X_one (π : C ⟶ Proj 𝒜) (h₀ : hU.fromSpec ≫ π = chart₀ c U f)
    (h₁ : hV.fromSpec ≫ π = chart₁ c V g) (hUV : U ⊔ V = ⊤) (hf : U ⊓ V = C.basicOpen f) :
    π ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 1) = V
theorem

fromSpec_comp

L408 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.fromSpec_comp
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem fromSpec_comp (W : C.Opens) (hW : IsAffineOpen W) :
    hW.fromSpec ≫ c = Spec.map (CommRingCat.ofHom (iOf c W))
theorem

comp_eq

L414 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.comp_eq
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem comp_eq (π : C ⟶ Proj 𝒜) (h₀ : hU.fromSpec ≫ π = chart₀ c U f)
    (h₁ : hV.fromSpec ≫ π = chart₁ c V g) (hUV : U ⊔ V = ⊤) (p : Proj 𝒜 ⟶ Spec (CommRingCat.of R))
    (e : R →+* (𝒜 0)) (he : ∀ r, (e r : MvPolynomial (Fin 2) R) = MvPolynomial.C r)
    (hp : ∀ j : Fin 2, Proj.awayι 𝒜 (MvPolynomial.X j) (X_mem j) one_pos ≫ p =
      Spec.map (CommRingCat.ofHom ((fromZeroRingHom 𝒜 _).comp e))) :
    π ≫ p = c
theorem

awayToSection_comp_appLE_X_zero

L433 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.awayToSection_comp_appLE_X_zero
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem awayToSection_comp_appLE_X_zero (π : C ⟶ Proj 𝒜) (h₀ : hU.fromSpec ≫ π = chart₀ c U f)
    (hle : U ≤ π ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 0)) :
    Proj.awayToSection 𝒜 (MvPolynomial.X 0) ≫ π.appLE (Proj.basicOpen 𝒜 (MvPolynomial.X 0)) U hle =
      CommRingCat.ofHom (ψ₀ (iOf c U) f)
theorem

awayToSection_comp_appLE_X_one

L448 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.awayToSection_comp_appLE_X_one
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem awayToSection_comp_appLE_X_one (π : C ⟶ Proj 𝒜) (h₁ : hV.fromSpec ≫ π = chart₁ c V g)
    (hle : V ≤ π ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 1)) :
    Proj.awayToSection 𝒜 (MvPolynomial.X 1) ≫ π.appLE (Proj.basicOpen 𝒜 (MvPolynomial.X 1)) V hle =
      CommRingCat.ofHom (ψ₁ (iOf c V) g)
theorem

appLE_awayToSection_X_zero

L463 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.appLE_awayToSection_X_zero
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem appLE_awayToSection_X_zero (π : C ⟶ Proj 𝒜) (h₀ : hU.fromSpec ≫ π = chart₀ c U f)
    (hle : U ≤ π ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 0))
    (h1 : (MvPolynomial.X 1 : MvPolynomial (Fin 2) R) ∈ 𝒜 (1 • 1)) :
    (π.appLE (Proj.basicOpen 𝒜 (MvPolynomial.X 0)) U hle).hom
      ((Proj.awayToSection 𝒜 (MvPolynomial.X 0)).hom (Away.mk 𝒜 (X_mem 0) 1 (MvPolynomial.X 1) h1))
          = f
theorem

appLE_awayToSection_X_one

L473 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.HomProj.appLE_awayToSection_X_one
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
namespace HomProj
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open HomogeneousLocalization
section Consequences
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin 2) R
attribute [local instance] MvPolynomial.gradedAlgebra
variable (U V : C.Opens) (f : Γ(C, U)) (g : Γ(C, V)) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
variable {U V f g hU hV}
Lean source · statement
theorem appLE_awayToSection_X_one (π : C ⟶ Proj 𝒜) (h₁ : hV.fromSpec ≫ π = chart₁ c V g)
    (hle : V ≤ π ⁻¹ᵁ Proj.basicOpen 𝒜 (MvPolynomial.X 1))
    (h0 : (MvPolynomial.X 0 : MvPolynomial (Fin 2) R) ∈ 𝒜 (1 • 1)) :
    (π.appLE (Proj.basicOpen 𝒜 (MvPolynomial.X 1)) V hle).hom
      ((Proj.awayToSection 𝒜 (MvPolynomial.X 1)).hom (Away.mk 𝒜 (X_mem 1) 1 (MvPolynomial.X 0) h0))
          = g
theorem

exists_hom_proj_preimage_basicOpen_eq

L487 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.exists_hom_proj_preimage_basicOpen_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_exists_hom_proj_preimage_basicOpen_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem
    _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.exists_hom_proj_preimage_basicOpen_eq
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} (𝔉 : SmoothProperCurve.FiniteMapData c ε) :
    ∃ (π : C ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin 2) R))
      (hU : π ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R) (MvPolynomial.X 0) =
          𝔉.U)
      (hV : π ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R) (MvPolynomial.X 1) =
          𝔉.V),
      π ≫ ProjSpace.π R 1 = c ∧
      (π.appLE (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R) (MvPolynomial.X 0))
          𝔉.U hU.ge).hom
          ((Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin 2) R) (MvPolynomial.X
              0)).hom (ProjSpace.ratio R 1 0 1)) = 𝔉.f ∧
      (π.appLE (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R) (MvPolynomial.X 1))
          𝔉.V hV.ge).hom
          ((Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin 2) R) (MvPolynomial.X
              1)).hom (ProjSpace.ratio R 1 1 0)) = 𝔉.g

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