NYLL
Module

ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
18 declarations indexed from sourceView source ↗

Module documentation

Proj Space forall H0 twist exists is Homogeneous of base Change field

Imports18
Imported by1

Declarations

theorem

preimage_pullbackChart

L63 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.preimage_pullbackChart
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
omit [IsAffineHom ι] [IsAffineHom ι'] in
Lean source · statement
theorem preimage_pullbackChart (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (j : Fin (n + 1)) :
    e ⁻¹ᵁ ProjSpace.pullbackChart ι j = ProjSpace.pullbackChart ι' j
theorem

preimage_inter

L68 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.preimage_inter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem preimage_inter (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) {i : ℕ} (s :
  (ProjSpace.stdCoverPullback ι).Idx i) :
    e ⁻¹ᵁ (ProjSpace.stdCoverPullback ι).inter s = (ProjSpace.stdCoverPullback ι').inter s
theorem

X_eq_mvMapGraded_mul_one

L80 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.X_eq_mvMapGraded_mul_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem X_eq_mvMapGraded_mul_one (i : Fin (n + 1)) :
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) B) = (ProjSpace.mvMapGraded A B n)
      (MvPolynomial.X i) * 1
theorem

one_mem_zero

L85 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.one_mem_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem one_mem_zero : (1 : MvPolynomial (Fin (n + 1)) B) ∈ (MvPolynomial.homogeneousSubmodule (Fin
  (n + 1)) B) 0
def

toB

L90 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.toB
Documentation

The coordinate localization map induced by the coefficient base change.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
def toB (i : Fin (n + 1)) : Away 𝒜A (MvPolynomial.X i) →+* Away 𝒜B (MvPolynomial.X i)
theorem

toB_ratio

L95 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.toB_ratio
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem toB_ratio (i j : Fin (n + 1)) : toB (A := A) B i (ProjSpace.ratio A n i j) =
  ProjSpace.ratio B n i j
theorem

restrictFun_app_pullAway

L103 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.restrictFun_app_pullAway
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
omit [IsAffineHom ι] [IsAffineHom ι'] in
Lean source · statement
theorem restrictFun_app_pullAway (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (i : Fin (n + 1))
    (a : Away 𝒜A (MvPolynomial.X i)) {W' : Z'.Opens}
    (h₁ : W' ≤ e ⁻¹ᵁ ProjSpace.pullbackChart ι i) (h₂ : W' ≤ ProjSpace.pullbackChart ι' i) :
    ProjSpace.restrictFun h₁ ((e.app (ProjSpace.pullbackChart ι i)).hom
        ((ι.app (Proj.basicOpen 𝒜A (MvPolynomial.X i))).hom ((Proj.awayToSection 𝒜A (MvPolynomial.X
          i)).hom a)))
      = ProjSpace.restrictFun h₂ ((ι'.app (Proj.basicOpen 𝒜B (MvPolynomial.X i))).hom
          ((Proj.awayToSection 𝒜B (MvPolynomial.X i)).hom (toB (A := A) B i a)))
theorem

restrictFun_app_frameUnit

L165 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.restrictFun_app_frameUnit
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
omit [IsAffineHom ι] [IsAffineHom ι'] in
Lean source · statement
theorem restrictFun_app_frameUnit (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (i j : Fin (n + 1))
  {W' : Z'.Opens}
    (h₁ : W' ≤ e ⁻¹ᵁ ProjSpace.pullbackChart ι i) (h₂ : W' ≤ ProjSpace.pullbackChart ι' i) :
    ProjSpace.restrictFun h₁ ((e.app (ProjSpace.pullbackChart ι i)).hom (ProjSpace.frameUnit ι i j))
      = ProjSpace.restrictFun h₂ (ProjSpace.frameUnit ι' i j)
theorem

restrictFun_app_eq

L173 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.restrictFun_app_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem restrictFun_app_eq {U V : Z.Opens} (hVU : V ≤ U) {W' : Z'.Opens} (h₁ : W' ≤ e ⁻¹ᵁ V) (h₂ :
  W' ≤ e ⁻¹ᵁ U)
    (x : Γ(Z, U)) :
    ProjSpace.restrictFun h₁ ((e.app V).hom (ProjSpace.restrictFun hVU x)) = ProjSpace.restrictFun
      h₂ ((e.app U).hom x)
theorem

toB_mkDeg

L185 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.toB_mkDeg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem toB_mkDeg (i : Fin (n + 1)) (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF :
  F.IsHomogeneous d) :
    toB (A := A) B i (HomogeneousLocalization.mk
        { deg := d
          num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
          den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
            (MvPolynomial.isHomogeneous_X_pow i d)⟩
          den_mem := ⟨d, rfl⟩ } : Away 𝒜A (MvPolynomial.X i)) =
      (HomogeneousLocalization.mk
        { deg := d
          num := ⟨MvPolynomial.map (algebraMap A B) F,
            (MvPolynomial.mem_homogeneousSubmodule d _).mpr (hF.map (algebraMap A B))⟩
          den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
            (MvPolynomial.isHomogeneous_X_pow i d)⟩
          den_mem := ⟨d, rfl⟩ } : Away 𝒜B (MvPolynomial.X i))
def

chartVal

L228 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.chartVal
Documentation

The section on a pulled-back projective chart obtained from the homogeneous polynomial.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Theta
variable {n : ℕ} {k : Type u} [Field k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ιk] (d : ℕ)
Lean source · statement
def chartVal (F : MvPolynomial (Fin (n + 1)) k) (hF : F.IsHomogeneous d) (i : Fin (n
  + 1)) :
    Γ(Zk, ProjSpace.pullbackChart ιk i)
theorem

isHomogeneous_of_mem

L240 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.isHomogeneous_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Theta
variable {n : ℕ} {k : Type u} [Field k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ιk] (d : ℕ)
Lean source · statement
theorem isHomogeneous_of_mem (F : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)) :
    (F : MvPolynomial (Fin (n + 1)) k).IsHomogeneous d
def

vertex

L245 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.vertex
Documentation

The degree-zero Cech index corresponding to the selected standard projective chart.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Theta
variable {n : ℕ} {k : Type u} [Field k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ιk] (d : ℕ)
Lean source · statement
def vertex (i : Fin (n + 1)) : (ProjSpace.stdCoverPullback ιk).Idx 0
theorem

chart_le_inter_vertex

L249 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.chart_le_inter_vertex
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Theta
variable {n : ℕ} {k : Type u} [Field k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ιk] (d : ℕ)
Lean source · statement
theorem chart_le_inter_vertex (i : Fin (n + 1)) :
    ProjSpace.pullbackChart ιk i ≤ (ProjSpace.stdCoverPullback ιk).inter (vertex ιk i) ⊓
      ProjSpace.pullbackChart ιk i
theorem

exists_theta

L254 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.exists_theta
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section Theta
variable {n : ℕ} {k : Type u} [Field k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ιk] (d : ℕ)
Lean source · statement
theorem exists_theta :
    ∃ Θ : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d) →ₗ[k]
        ↥((ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk d).H0 (ProjSpace.stdCoverPullback ιk)),
      ∀ (F : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d))
        (s : (ProjSpace.stdCoverPullback ιk).Idx 0) (i : Fin (n + 1)),
        ((Θ F : (ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk d).cochain (ProjSpace.stdCoverPullback
          ιk) 0) s).val i =
          ProjSpace.restrictFun
            (inf_le_right : (ProjSpace.stdCoverPullback ιk).inter s ⊓ ProjSpace.pullbackChart ιk i
              ≤ ProjSpace.pullbackChart ιk i)
            (chartVal ιk d F (isHomogeneous_of_mem d F) i)
theorem

eq_zero_of_one_tmul_eq_zero

L296 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.eq_zero_of_one_tmul_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section LinAlg
variable {k : Type u} [Field k] (K : Type u) [Field K] [Algebra k K] {V : Type u} [AddCommGroup V]
  [Module k V]
Lean source · statement
theorem eq_zero_of_one_tmul_eq_zero (v : V) (h : (1 : K) ⊗ₜ[k] v = 0) : v = 0
theorem

mem_of_one_tmul_mem_baseChange

L307 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field.RM6Sol.mem_of_one_tmul_mem_baseChange
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace RM6Sol
section LinAlg
variable {k : Type u} [Field k] (K : Type u) [Field K] [Algebra k K] {V : Type u} [AddCommGroup V]
  [Module k V]
Lean source · statement
theorem mem_of_one_tmul_mem_baseChange (W : Submodule k V) (v : V)
    (h : (1 : K) ⊗ₜ[k] v ∈ W.baseChange K) : v ∈ W
theorem

forall_H0_twist_exists_isHomogeneous_of_baseChange_field

L331 ↗
AlgebraicGeometry.ProjSpace.forall_H0_twist_exists_isHomogeneous_of_baseChange_field
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_forall_H0_twist_exists_isHomogeneous_of_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.forall_H0_twist_exists_isHomogeneous_of_baseChange_field
    {k : Type u} [Field k] {n : ℕ} {Z : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ι]
    (K : Type u) [Field K] [Algebra k K] {Z' : Scheme.{u}}
    (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) K)) [IsAffineHom ι']
    (e : Z' ⟶ Z)
    (hpb : IsPullback e (ι' ≫ ProjSpace.π K n) (ι ≫ ProjSpace.π k n) (Spec.map (CommRingCat.ofHom
      (algebraMap k K))))
    (hcomp : e ≫ ι = ι' ≫ ProjSpace.map k K n) (d : ℕ)
    (hK : ∀ c ∈ (ProjSpace.twist (ι' ≫ ProjSpace.π K n) ι' d).H0 (ProjSpace.stdCoverPullback ι'),
        ∃ (F : MvPolynomial (Fin (n + 1)) K) (hF : F.IsHomogeneous d),
          ∀ (s : (ProjSpace.stdCoverPullback ι').Idx 0) (i : Fin (n + 1)),
            (c s).val i =
              ProjSpace.restrictFun
                  (inf_le_right : (ProjSpace.stdCoverPullback ι').inter s ⊓ ProjSpace.pullbackChart
                    ι' i ≤
                    ProjSpace.pullbackChart ι' i)
                  (ι'.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) K)
                    (MvPolynomial.X i))
              (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) K)
                (MvPolynomial.X i)
                (HomogeneousLocalization.mk
                  { deg := d
                    num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                    den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i d)⟩
                    den_mem := ⟨d, rfl⟩ })))) :
    ∀ c ∈ (ProjSpace.twist (ι ≫ ProjSpace.π k n) ι d).H0 (ProjSpace.stdCoverPullback ι),
        ∃ (F : MvPolynomial (Fin (n + 1)) k) (hF : F.IsHomogeneous d),
          ∀ (s : (ProjSpace.stdCoverPullback ι).Idx 0) (i : Fin (n + 1)),
            (c s).val i =
              ProjSpace.restrictFun
                  (inf_le_right : (ProjSpace.stdCoverPullback ι).inter s ⊓ ProjSpace.pullbackChart
                    ι i ≤
                    ProjSpace.pullbackChart ι i)
                  (ι.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
                    (MvPolynomial.X i))
              (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
                (MvPolynomial.X i)
                (HomogeneousLocalization.mk
                  { deg := d
                    num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                    den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i d)⟩
                    den_mem := ⟨d, rfl⟩ })))

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