NYLL
Module

ProjectivePresentationBaseChange.lean

Nyll.SchemeTheory.Modules.ProjectivePresentationBaseChange
19 declarations indexed from sourceView source ↗

Module documentation

Base change of a projective presentation by pulling back its presenting sections and morphism. The chart ratios and pullback square give the compatibility of the resulting presentation.

Imports5
Imported by7

Declarations

def

toProj'

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.toProj'
Documentation

The projective presentation morphism obtained from the pullback square.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
def toProj' : X' ⟶ Proj 𝒜A
lemma

toProj'_map

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.toProj'_map
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
lemma toProj'_map : toProj' sq 𝔓 ≫ ProjSpace.map R A N = p ≫ 𝔓.toProj
lemma

toProj'_π

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.toProj'_π
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
lemma toProj'_π : toProj' sq 𝔓 ≫ ProjSpace.π A N = f'
lemma

isPullback_toProj'

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.isPullback_toProj'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
lemma isPullback_toProj' : IsPullback p (toProj' sq 𝔓) 𝔓.toProj (ProjSpace.map R A N)
lemma

preimage_chart

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.preimage_chart
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
lemma preimage_chart (i : Fin (N + 1)) :
    toProj' sq 𝔓 ⁻¹ᵁ Proj.basicOpen 𝒜A (MvPolynomial.X i) =
      p ⁻¹ᵁ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i))
abbrev

σ'

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.σ'
Documentation

The presenting sections pulled back through the adjunction unit.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
abbrev σ' (i : Fin (N + 1)) : Γ((Modules.pullback p).obj M, ⊤)
lemma

presheaf_map_congr

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.presheaf_map_congr
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 in
Lean source · statement
lemma presheaf_map_congr {Z : Scheme.{u}} (G : TopCat.Presheaf Ab Z) {U V : Z.Opens}
    (k₁ k₂ : op U ⟶ op V) (z : G.obj (op U)) : G.map k₁ z = G.map k₂ z
def

eta

L93 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.eta
Documentation

The pullback of a module section through the adjunction unit.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
def eta (U : X.Opens) (m : Γ(M, U)) : Γ((Modules.pullback p).obj M, p ⁻¹ᵁ U)
lemma

eta_smul

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.eta_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 f in
Lean source · statement
lemma eta_smul (U : X.Opens) (r : Γ(X, U)) (m : Γ(M, U)) :
    eta (p := p) U (r • m) = p.app U r • eta (p := p) U m
lemma

eta_resTop

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.eta_resTop
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 f in
Lean source · statement
lemma eta_resTop (U : X.Opens) (m : Γ(M, ⊤)) :
    eta (p := p) U (M.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op m) =
      ((Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : p ⁻¹ᵁ U ≤ ⊤)).op
        (eta (p := p) ⊤ m)
lemma

ratio_pulled

L111 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.ratio_pulled
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
lemma ratio_pulled (i j : Fin (N + 1)) :
    (p.app (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i))
        (𝔓.toProj.app (Proj.basicOpen 𝒜R (MvPolynomial.X i))
          (Proj.awayToSection _ (MvPolynomial.X i) (ProjSpace.ratio R N i j)))) •
      ((Modules.pullback p).obj M).presheaf.map
        (homOfLE (le_top : p ⁻¹ᵁ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i)) ≤ ⊤)).op
          (σ' 𝔓 (p := p) i) =
      ((Modules.pullback p).obj M).presheaf.map
        (homOfLE (le_top : p ⁻¹ᵁ (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i)) ≤ ⊤)).op
          (σ' 𝔓 (p := p) j)
lemma

awayToSection_mk_congr

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.awayToSection_mk_congr
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 in
Lean source · statement
lemma awayToSection_mk_congr (s t : MvPolynomial (Fin (N + 1)) A) (hst : s = t)
    (hs : s ∈ 𝒜A 1) (ht : t ∈ 𝒜A 1) (a b : MvPolynomial (Fin (N + 1)) A) (hab : a = b)
    (ha : a ∈ 𝒜A (1 • 1)) (hb : b ∈ 𝒜A (1 • 1)) (E : Proj.basicOpen 𝒜A s = Proj.basicOpen 𝒜A t) :
    (Proj 𝒜A).presheaf.map (eqToHom E).op (Proj.awayToSection 𝒜A t (Away.mk 𝒜A ht 1 b hb)) =
      Proj.awayToSection 𝒜A s (Away.mk 𝒜A hs 1 a ha)
lemma

presheaf_map_congr'

L165 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.presheaf_map_congr'
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 in
Lean source · statement
lemma presheaf_map_congr' {Z : Scheme.{u}} (G : TopCat.Presheaf CommRingCat Z) {U V : Z.Opens}
    (k₁ k₂ : op U ⟶ op V) (z : G.obj (op U)) : G.map k₁ z = G.map k₂ z
lemma

presheaf_map_map_eq

L169 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.presheaf_map_map_eq
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 in
Lean source · statement
lemma presheaf_map_map_eq {Z : Scheme.{u}} {U V W : Z.Opens}
    (k₁ : op U ⟶ op V) (k₂ : op V ⟶ op W) (k : op U ⟶ op W) (z : Γ(Z, U)) :
    Z.presheaf.map k₂ (Z.presheaf.map k₁ z) = Z.presheaf.map k z
lemma

map_app_ratio

L175 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.map_app_ratio
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq 𝔓 f f' p in
Lean source · statement
lemma map_app_ratio (i j : Fin (N + 1)) :
    (ProjSpace.map R A N).app (Proj.basicOpen 𝒜R (MvPolynomial.X i))
        (Proj.awayToSection 𝒜R (MvPolynomial.X i) (ProjSpace.ratio R N i j)) =
      (Proj 𝒜A).presheaf.map (eqToHom (ProjSpace.map_preimage_basicOpen_X R A N i)).op
        (Proj.awayToSection 𝒜A (MvPolynomial.X i) (ProjSpace.ratio A N i j))
lemma

toProj'_app_ratio

L205 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.toProj'_app_ratio
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · statement
lemma toProj'_app_ratio (i j : Fin (N + 1)) :
    (toProj' sq 𝔓).app (Proj.basicOpen 𝒜A (MvPolynomial.X i))
        (Proj.awayToSection 𝒜A (MvPolynomial.X i) (ProjSpace.ratio A N i j)) =
      X'.presheaf.map (eqToHom (preimage_chart sq 𝔓 i)).op
        (p.app (𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i))
          (𝔓.toProj.app (Proj.basicOpen 𝒜R (MvPolynomial.X i))
            (Proj.awayToSection 𝒜R (MvPolynomial.X i) (ProjSpace.ratio R N i j))))
lemma

resTop_eq

L241 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.resTop_eq
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
omit sq in
Lean source · statement
lemma resTop_eq {O O' : X'.Opens} (h : O = O') (m : Γ((Modules.pullback p).obj M, ⊤)) :
    ((Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : O ≤ ⊤)).op m =
      ((Modules.pullback p).obj M).presheaf.map (eqToHom h).op
        (((Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : O' ≤ ⊤)).op m)
def

baseChange

L253 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback.AlgebraicGeometry.Scheme.Modules.PresBC.baseChange
Documentation

The projective presentation obtained by pulling back its sections and morphism.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace PresBC
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A
Lean source · full declaration
def baseChange : ((Modules.pullback p).obj M).ProjPresentation f' N where
  σ := σ' 𝔓
  toProj := toProj' sq 𝔓
  toProj_π := toProj'_π sq 𝔓
  frame := fun i V hV =>
    bijective_smul_unit_app_of_bijective_smul p M (𝔓.σ i)
      (V := 𝔓.toProj ⁻¹ᵁ Proj.basicOpen 𝒜R (MvPolynomial.X i)) (𝔓.frame i) V
      (hV.trans (preimage_chart sq 𝔓 i).le)
  app_ratio_smul := fun i j => by
    rw [toProj'_app_ratio, resTop_eq (preimage_chart sq 𝔓 i), resTop_eq (preimage_chart sq 𝔓 i),
      ← Modules.map_smul, ratio_pulled]
theorem

exists_baseChange_of_isPullback

L269 ↗
AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_baseChange_of_isPullback
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_baseChange_of_isPullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
open Opposite TopologicalSpace HomogeneousLocalization
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_baseChange_of_isPullback
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X X' : Scheme.{u}}
    {f : X ⟶ Spec (.of R)} {f' : X' ⟶ Spec (.of A)} {p : X' ⟶ X}
    (sq : IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))))
    {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) :
    ∃ 𝔓' : ((Scheme.Modules.pullback p).obj M).ProjPresentation f' N,
      (∀ i, 𝔓'.σ i =
        (((Scheme.Modules.pullbackPushforwardAdjunction p).unit.app M).app ⊤) (𝔓.σ i)) ∧
      𝔓'.toProj ≫ ProjSpace.map R A N = p ≫ 𝔓.toProj ∧
      IsPullback p 𝔓'.toProj 𝔓.toProj (ProjSpace.map R A N)

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