Module

ProjSpace_isCoherent_twist_and_flat.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_isCoherent_twist_and_flat

12 declarations indexed from sourceView source ↗

Module documentation

Proj Space is Coherent twist and flat

Imports6

Imported by3

def

smallFuns

L58 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.smallFuns

Documentation

Functions whose basic opens are contained in one of the pullback charts.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)

Lean source · statement

def smallFuns : Set Γ(X, U.1)

theorem

span_smallFuns

L60 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.span_smallFuns

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)

Lean source · statement

theorem span_smallFuns [IsAffineHom φ] : Ideal.span (smallFuns φ U) = ⊤

instance

moduleU

L76 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.moduleU

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)
section Local
variable (f : Γ(X, U.1))

Lean source · statement

instance moduleU : Module Γ(X, U.1) ((twist π φ m).obj (X.basicOpen f))

instance

isScalarTower_U

L79 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.isScalarTower_U

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)
section Local
variable (f : Γ(X, U.1))

Lean source · statement

instance isScalarTower_U : IsScalarTower Γ(X, U.1) Γ(X, X.basicOpen f) ((twist π φ m).obj
  (X.basicOpen f))

instance

isLocalization_U

L83 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.isLocalization_U

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)
section Local
variable (f : Γ(X, U.1))

Lean source · statement

instance isLocalization_U : IsLocalization.Away f Γ(X, X.basicOpen f)

theorem

isLocalizedModule_res

L86 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.isLocalizedModule_res

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)
section Local
variable (f : Γ(X, U.1))

Lean source · statement

theorem isLocalizedModule_res [IsSeparated π] [IsAffineHom φ] :
    IsLocalizedModule.Away f ((twist π φ m).resₗ (X.basicOpen_le f) :
      (twist π φ m).obj U.1 →ₗ[Γ(X, U.1)] (twist π φ m).obj (X.basicOpen f))

theorem

finite_local

L93 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.finite_local

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)
section Local
variable (f : Γ(X, U.1))
variable {f}

Lean source · statement

theorem finite_local {j : Fin (N + 1)} (hf : X.basicOpen f ≤ pullbackChart φ j) :
    Module.Finite Γ(X, X.basicOpen f) ((twist π φ m).obj (X.basicOpen f))

theorem

flat_local

L99 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.flat_local

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)
section Local
variable (f : Γ(X, U.1))
variable {f}

Lean source · statement

theorem flat_local {j : Fin (N + 1)} (hf : X.basicOpen f ≤ pullbackChart φ j) :
    Module.Flat Γ(X, U.1) ((twist π φ m).obj (X.basicOpen f))

theorem

finite

L110 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.finite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)

Lean source · statement

theorem finite [IsSeparated π] [IsAffineHom φ] : Module.Finite Γ(X, U.1) ((twist π φ m).obj U.1)

theorem

flat

L120 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.flat

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)

Lean source · statement

theorem flat [IsSeparated π] [IsAffineHom φ] : Module.Flat Γ(X, U.1) ((twist π φ m).obj U.1)

theorem

main

L130 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat.P2mTwistCohFlat.main

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistCohFlat
open AlgebraicGeometry.ProjSpace AlgebraicGeometry.OModulePresheaf
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
  (U : X.affineOpens)

Lean source · statement

theorem main [IsSeparated π] [IsAffineHom φ] : (twist π φ m).IsCoherent ∧ ∀ U : X.affineOpens,
  Module.Flat Γ(X, U.1) ((twist π φ m).obj U.1)

theorem

isCoherent_twist_and_flat

L141 ↗

AlgebraicGeometry.ProjSpace.isCoherent_twist_and_flat

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isCoherent_twist_and_flat
attribute [-simp] AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] P2mTwistCohFlat.moduleU
attribute [local instance] P2mTwistCohFlat.isScalarTower_U
attribute [local instance] P2mTwistCohFlat.isLocalization_U

Lean source · statement

theorem _root_.AlgebraicGeometry.ProjSpace.isCoherent_twist_and_flat
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (π : X ⟶ Spec (.of A)) [IsSeparated π]
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (m : ℕ) :
    (ProjSpace.twist π φ m).IsCoherent ∧
      ∀ U : X.affineOpens, Module.Flat Γ(X, U.1) ((ProjSpace.twist π φ m).obj U.1)

Module documentation

Proj Space is Coherent twist and flat

Declarations