Module

Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Proj Presentation subset support zero Scheme Ideal or disjoint

Imports9

Imported by3

theorem

map_app_one

L49 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint.P2mWs11C3.map_app_one

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs11C3
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem map_app_one (s : 𝟙_ X.Modules ⟶ M) {U W : X.Opens} (i : W ⟶ U) :
    M.presheaf.map i.op (s.app U (toUnitSection U 1)) = s.app W (toUnitSection W 1)

theorem

isFrameOn_smul_of_isUnit

L63 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint.P2mWs11C3.isFrameOn_smul_of_isUnit

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs11C3
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem isFrameOn_smul_of_isUnit {U : X.Opens} {σ : Γ(M, U)} {V : X.Opens} (h : IsFrameOn σ V)
    (W : X.Opens) (hWU : W ≤ U) (hWV : W ≤ V) (g : Γ(X, W)) (hg : IsUnit g) :
    IsFrameOn (g • M.presheaf.map (homOfLE hWU).op σ : Γ(M, W)) W

theorem

subset_support_zeroSchemeIdeal_or_disjoint

L105 ↗

AlgebraicGeometry.Scheme.Modules.ProjPresentation.subset_support_zeroSchemeIdeal_or_disjoint

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_ProjPresentation_subset_support_zeroSchemeIdeal_or_disjoint in
open P2mWs11C3 _root_.AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem Scheme.Modules.ProjPresentation.subset_support_zeroSchemeIdeal_or_disjoint
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
      [IsProper t]
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) {N : ℕ} (𝔓 : M.ProjPresentation t N)
    (Z : Set X) (hZ : IsClosed Z) (hZ' : IsIrreducible Z)
    (y : Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) k)) (_hy : IsClosed ({y} : Set _))
    (hZy : Z ⊆ 𝔓.toProj.base ⁻¹' {y}) (s : 𝟙_ X.Modules ⟶ M) :
    Z ⊆ (Scheme.Modules.zeroSchemeIdeal s).support ∨ Disjoint Z (Scheme.Modules.zeroSchemeIdeal
      s).support

Module documentation

Scheme Modules Proj Presentation subset support zero Scheme Ideal or disjoint

Declarations

map_app_one

isFrameOn_smul_of_isUnit

subset_support_zeroSchemeIdeal_or_disjoint