NYLL
Module

ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
17 declarations indexed from sourceView source ↗

Module documentation

Proj Space finite projective H0 twist of ker base Change of is Pullback

Imports19
Imported by1

Declarations

theorem

preimage_pullbackChart

L65 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L70 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L82 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L87 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L92 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L97 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L105 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L167 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L175 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L187 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
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

L230 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
section Theta
variable {n : ℕ} {k : Type u} [CommRing 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

L242 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
section Theta
variable {n : ℕ} {k : Type u} [CommRing 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

L247 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
section Theta
variable {n : ℕ} {k : Type u} [CommRing 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

L251 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
section Theta
variable {n : ℕ} {k : Type u} [CommRing 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

L256 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.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_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
section Theta
variable {n : ℕ} {k : Type u} [CommRing 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

exists_kerEquiv

L295 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback.K4ISol.exists_kerEquiv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace K4ISol
section KerEquiv
Lean source · statement
theorem exists_kerEquiv {R : Type*} [CommRing R] {M M' N N' : Type*}
    [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup N] [Module R N]
    [AddCommGroup N'] [Module R N']
    (e₀ : M ≃ₗ[R] M') {e₁ : N ≃ₗ[R] N'} (f : M →ₗ[R] N) (f' : M' →ₗ[R] N')
    (h : e₁.toLinearMap ∘ₗ f = f' ∘ₗ e₀.toLinearMap) :
    ∃ η : LinearMap.ker f ≃ₗ[R] LinearMap.ker f', ∀ x : LinearMap.ker f, (η x : M') = e₀ (x : M)
theorem

finite_projective_H0_twist_of_ker_baseChange_of_isPullback

L316 ↗
AlgebraicGeometry.ProjSpace.finite_projective_H0_twist_of_ker_baseChange_of_isPullback
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_finite_projective_H0_twist_of_ker_baseChange_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
Lean source · statement
theorem
  _root_.AlgebraicGeometry.ProjSpace.finite_projective_H0_twist_of_ker_baseChange_of_isPullback
    {A₀ : Type u} [CommRing A₀] {n : ℕ} {Z₀ : Scheme.{u}}
    (ι₀ : Z₀ ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A₀)) [IsClosedImmersion ι₀]
    (A : Type u) [CommRing A] [Algebra A₀ A] {Z : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
    (g : Z ⟶ Z₀)
    (hpb : IsPullback g (ι ≫ ProjSpace.π A n) (ι₀ ≫ ProjSpace.π A₀ n) (Spec.map (CommRingCat.ofHom
      (algebraMap A₀ A))))
    (hcomp : g ≫ ι₀ = ι ≫ ProjSpace.map A₀ A n) (d : ℕ)
    (Θ₀ : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A₀ d) →ₗ[A₀] (ProjSpace.twist (ι₀ ≫
      ProjSpace.π A₀ n) ι₀ d).cochain (ProjSpace.stdCoverPullback ι₀) 0)
    (hΘ₀ : ∀ (F : MvPolynomial (Fin (n + 1)) A₀) (hF : F.IsHomogeneous d) (s :
      (ProjSpace.stdCoverPullback ι₀).Idx 0) (i : Fin (n + 1)),
      (Θ₀ ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩ 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)) A₀)
            (MvPolynomial.X i)))
                (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A₀)
                  (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⟩ }))))
    (r : ℕ)
    (hfin : Module.Finite A (LinearMap.ker (((ProjSpace.twist (ι₀ ≫ ProjSpace.π A₀ n) ι₀ d).d
      (ProjSpace.stdCoverPullback ι₀) 0).baseChange A)))
    (hproj : Module.Projective A (LinearMap.ker (((ProjSpace.twist (ι₀ ≫ ProjSpace.π A₀ n) ι₀ d).d
      (ProjSpace.stdCoverPullback ι₀) 0).baseChange A)))
    (hrank : ∀ 𝔮 : PrimeSpectrum A,
      Module.rankAtStalk (LinearMap.ker (((ProjSpace.twist (ι₀ ≫ ProjSpace.π A₀ n) ι₀ d).d
        (ProjSpace.stdCoverPullback ι₀) 0).baseChange A)) 𝔮 = r)
    (hgen : LinearMap.ker (((ProjSpace.twist (ι₀ ≫ ProjSpace.π A₀ n) ι₀ d).d
      (ProjSpace.stdCoverPullback ι₀) 0).baseChange A) ≤ LinearMap.range (Θ₀.baseChange A)) :
    Module.Finite A ((ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).H0 (ProjSpace.stdCoverPullback ι))
      ∧
    Module.Projective A ((ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).H0 (ProjSpace.stdCoverPullback
      ι)) ∧
    (∀ 𝔮 : PrimeSpectrum A, Module.rankAtStalk (↥((ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).H0
      (ProjSpace.stdCoverPullback ι))) 𝔮 = r) ∧
    (∀ c ∈ (ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).H0 (ProjSpace.stdCoverPullback ι),
      ∃ (F : MvPolynomial (Fin (n + 1)) A) (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)) A)
                (MvPolynomial.X i)))
                (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)
                  (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.