NYLL
Module

OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
59 declarations indexed from sourceView source ↗

Module documentation

Finiteness of unit-presheaf Cech cohomology for a closed immersion into projective space.

Imports5
Imported by3

Declarations

def

canonicalAlg

L50 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.canonicalAlg
Documentation

The algebra of section rings induced by the morphism to the affine base.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section File8
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · statement
def canonicalAlg (W : V.Opens) : Algebra R Γ(V, W)
theorem

canonicalAlg_compat

L53 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.canonicalAlg_compat
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section File8
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
theorem canonicalAlg_compat (W : V.Opens) :
    ∀ c, letI := canonicalAlg π W
      algebraMap R Γ(V, W) c = (V.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom
        (π.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom c)) :=
  fun _ => rfl
def

moduleΓ

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.moduleΓ
Documentation

The section module of the unit module presheaf over the affine base ring.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section File8
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · statement
def moduleΓ (W : V.Opens) : Module R Γ(V, W)
def

resLinearMap

L64 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.resLinearMap
Documentation

Restriction of sections as a linear map over the affine base ring.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section File8
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
def resLinearMap {W₁ W₂ : V.Opens} (h : W₁ ≤ W₂) :
    letI := moduleΓ π W₁; letI := moduleΓ π W₂
    (Γ(V, W₂) : Type u) →ₗ[R] (Γ(V, W₁) : Type u) :=
  (OModulePresheaf.unit π).res h
theorem

resLinearMap_apply

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.resLinearMap_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section File8
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
theorem resLinearMap_apply {W₁ W₂ : V.Opens} (h : W₁ ≤ W₂) (s) :
    letI := moduleΓ π W₁; letI := moduleΓ π W₂
    resLinearMap π h s = (V.presheaf.map (homOfLE h).op).hom s := rfl
def

idxEquiv

L85 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.idxEquiv
Documentation

The equivalence between indices of the pulled back standard cover and projective cochains.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
def idxEquiv (i : ℕ) :
    (ProjSpace.stdCoverPullback ι).Idx i
      ≃ ProjSpaceCech.Idx n i where
  toFun s := ⟨fun k => (s.1 k).down, fun _a _b h => (s.2 h : _)⟩
  invFun s := ⟨fun k => ULift.up (s.1 k), fun _a _b h => (s.2 h : _)⟩
  left_inv _s := Subtype.ext rfl
  right_inv _s := Subtype.ext rfl
theorem

prodX_mem

L93 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.prodX_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem prodX_mem (I : Finset (Fin (n + 1))) :
    (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)) ∈ 𝒜 I.card
theorem

finsetInf_basicOpen

L101 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.finsetInf_basicOpen
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem finsetInf_basicOpen (I : Finset (Fin (n + 1))) :
    (⨅ j ∈ I, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j))
      = ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
          (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))
theorem

altOpen_eq

L111 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.altOpen_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem altOpen_eq (i : ℕ)
    (s : (ProjSpace.stdCoverPullback ι).Idx i) :
    (ProjSpace.stdCoverPullback ι).inter s
      = ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
          (∏ j ∈ ProjSpaceCech.Idx.img n (idxEquiv ι i s),
            (X j : MvPolynomial (Fin (n + 1)) A))
def

testAt

L125 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAt
Documentation

The section obtained from a homogeneous numerator on one standard projective chart.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def testAt (d : ℕ) (j : Fin (n + 1)) (m : 𝒜 d) :
    Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j))
theorem

testAt_mul

L133 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAt_mul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem testAt_mul (d e : ℕ) (j : Fin (n + 1)) (m : 𝒜 d) (z : 𝒜 e)
    (hzm : z.1 * m.1 ∈ 𝒜 (e + d)) :
    testAt ι (e + d) j ⟨z.1 * m.1, hzm⟩
      = (ι.app _).hom ((AlgebraicGeometry.Proj.awayToSection 𝒜 (X j)).hom
          (HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A n j) e z.1
            (by simp)))
        * testAt ι d j m := by
  unfold testAt
  rw [← map_mul, ← map_mul]
  congr 2
  refine HomogeneousLocalization.val_injective _ ?_
  simp only [HomogeneousLocalization.Away.val_mk, HomogeneousLocalization.val_mul,
    Localization.mk_mul]
  congr 1
  ext : 1
  exact (pow_add (X j) e d)
def

J

L151 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.J
Documentation

The graded submodule of homogeneous polynomials whose chart sections vanish after pullback.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def J : Submodule A (ProjSpaceCech.GradedModule.free A n).M
theorem

J_xMul_stable

L192 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.J_xMul_stable
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem J_xMul_stable (k : Fin (n + 1)) :
    ∀ m ∈ J ι, (ProjSpaceCech.GradedModule.free A n).xMul k m
      ∈ J ι
abbrev

Dι

L210 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.Dι
Documentation

The quotient graded module by polynomials vanishing on the closed subscheme.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
abbrev Dι : ProjSpaceCech.GradedModule A n
theorem

J_monMul_stable

L215 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.J_monMul_stable
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem J_monMul_stable (a : Fin (n + 1) → ℕ) :
    ∀ m ∈ J ι,
      ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) a m ∈ J ι
def

mkQHom

L234 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.mkQHom
Documentation

The graded quotient map to the module defined by the closed subscheme.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
def mkQHom :
    ProjSpaceCech.GradedModule.Hom (ProjSpaceCech.GradedModule.free A n) (Dι ι) where
  toLinearMap := (J ι).mkQ
  mem_grade _d m hm := ⟨m, hm, rfl⟩
  xMul_comm _j := LinearMap.ext fun _m => rfl
theorem

testAt_congr

L241 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAt_congr
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem testAt_congr {d d' : ℕ} (hd : d = d') (j : Fin (n + 1))
    {p p' : MvPolynomial (Fin (n + 1)) A} (hp : p ∈ 𝒜 d) (hp' : p' ∈ 𝒜 d') (hpp : p = p') :
    testAt ι d j ⟨p, hp⟩ = testAt ι d' j ⟨p', hp'⟩
theorem

mem_J_homogeneous

L247 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.mem_J_homogeneous
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem mem_J_homogeneous {d : ℕ} {p : MvPolynomial (Fin (n + 1)) A}
    (hp : p ∈ 𝒜 d) :
    p ∈ J ι ↔ ∀ j, testAt ι d j ⟨p, hp⟩ = 0
def

testAtI

L286 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAtI
Documentation

The section represented by a homogeneous numerator on an intersection of standard charts.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def testAtI (I : Finset (Fin (n + 1))) (k : ℕ)
    {m : MvPolynomial (Fin (n + 1)) A} (hm : m ∈ 𝒜 (k * I.card)) :
    Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
theorem

testAtI_prodXpow

L295 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAtI_prodXpow
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem testAtI_prodXpow (I : Finset (Fin (n + 1))) (k e : ℕ)
    {m : MvPolynomial (Fin (n + 1)) A} (hm : m ∈ 𝒜 (k * I.card))
    (hm' : (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)) ^ e * m ∈ 𝒜 ((e + k) * I.card)) :
    testAtI ι I (e + k) hm' = testAtI ι I k hm
theorem

testAtI_add

L306 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAtI_add
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem testAtI_add (I : Finset (Fin (n + 1))) (k : ℕ)
    {m m' : MvPolynomial (Fin (n + 1)) A}
    (hm : m ∈ 𝒜 (k * I.card)) (hm' : m' ∈ 𝒜 (k * I.card)) :
    testAtI ι I k (Submodule.add_mem _ hm hm')
      = testAtI ι I k hm + testAtI ι I k hm'
theorem

testAtI_congr

L318 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAtI_congr
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem testAtI_congr (I : Finset (Fin (n + 1))) {k k' : ℕ} (hk : k = k')
    {m m' : MvPolynomial (Fin (n + 1)) A} (hm : m ∈ 𝒜 (k * I.card)) (hm' : m' ∈ 𝒜 (k' * I.card))
    (hmm : m = m') :
    testAtI ι I k hm = testAtI ι I k' hm'
theorem

prodXpow_eq_monMul

L324 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.prodXpow_eq_monMul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem prodXpow_eq_monMul (I : Finset (Fin (n + 1))) (e : ℕ)
    (p : MvPolynomial (Fin (n + 1)) A) :
    (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)) ^ e * p
      = ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
          (fun j => if j ∈ I then e else 0) p := by
  rw [ProjSpaceCech.GradedModule.free_monMul_apply]
  refine congrArg (· * p) ((Finset.prod_subset (Finset.subset_univ I)
    (fun j _ hj => by rw [ite_eq_right hj, pow_zero])).symm.trans
    ((Finset.prod_congr rfl (fun j hj => by rw [ite_eq_left hj])).trans
      (Finset.prod_pow _ _ _))).symm
def

pad

L336 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.pad
Documentation

The exponent vector used to replace separate denominators by a common product denominator.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def pad (I : Finset (Fin (n + 1))) (a : Fin (n + 1) → ℕ) :
    Fin (n + 1) → ℕ
theorem

pad_add_supp

L340 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.pad_add_supp
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem pad_add_supp (I : Finset (Fin (n + 1))) (a : Fin (n + 1) → ℕ)
    (ha : ∀ j ∉ I, a j = 0) (j : Fin (n + 1)) :
    pad I a j + a j = if j ∈ I then ∑ k, a k else 0 := by
  unfold pad
  by_cases hj : j ∈ I
  · have hle : a j ≤ ∑ k, a k :=
      Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ j)
    simp only [hj, ite_true]; omega
  · simp [hj, ha j hj]
theorem

sum_pad

L350 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.sum_pad
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem sum_pad (I : Finset (Fin (n + 1))) (a : Fin (n + 1) → ℕ)
    (ha : ∀ j ∉ I, a j = 0) :
    ∑ j, pad I a j + ∑ j, a j = (∑ j, a j) * I.card
theorem

secAuxNum_mem

L357 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAuxNum_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem secAuxNum_mem (I : Finset (Fin (n + 1)))
    (x : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I) :
    ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) (pad I x.denExp) x.num
      ∈ 𝒜 ((∑ k, x.denExp k) * I.card)
theorem

prodXpow_mul_mem

L370 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.prodXpow_mul_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem prodXpow_mul_mem (I : Finset (Fin (n + 1))) {d : ℕ} (N : ℕ)
    {p : MvPolynomial (Fin (n + 1)) A} (hp : p ∈ 𝒜 (d * I.card)) :
    (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ N * p ∈ 𝒜 ((N + d) * I.card)
def

secAux

L379 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAux
Documentation

The section represented by a graded fraction after padding its numerator.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def secAux (I : Finset (Fin (n + 1)))
    (x : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I) :
    Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
theorem

secAux_enlarge

L386 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAux_enlarge
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem secAux_enlarge (I : Finset (Fin (n + 1)))
    (z : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I)
    (e : Fin (n + 1) → ℕ) (heI : ∀ j ∉ I, e j = 0) :
    ∃ hm : ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
        (pad I (e + z.denExp) + e) z.num
          ∈ 𝒜 (((∑ k, e k) + ∑ k, z.denExp k) * I.card),
      secAux ι I z
        = testAtI ι I ((∑ k, e k) + ∑ k, z.denExp k) hm
theorem

secAux_wellDef

L412 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAux_wellDef
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem secAux_wellDef (I : Finset (Fin (n + 1)))
    {x y : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I}
    (hxy : ProjSpaceCech.GradedModule.Frac.Rel _ I x y) :
    secAux ι I x = secAux ι I y
theorem

secAux_add

L429 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAux_add
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem secAux_add (I : Finset (Fin (n + 1)))
    (x y : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I) :
    secAux ι I ⟨x.denExp + y.denExp,
        ProjSpaceCech.GradedModule.Frac.supp_add I x.hden y.hden,
        ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) y.denExp x.num
          + ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) x.denExp
            y.num, by
          refine Submodule.add_mem _ ?_ ?_
          · have hx := ProjSpaceCech.GradedModule.monMul_mem_grade _ y.denExp _ x.num x.hnum
            convert hx using 2; simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]
          · have hy := ProjSpaceCech.GradedModule.monMul_mem_grade _ x.denExp _ y.num y.hnum
            convert hy using 2
            simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]; ring⟩
      = secAux ι I x + secAux ι I y := by
  set w₁ : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I :=
    ⟨x.denExp + y.denExp, ProjSpaceCech.GradedModule.Frac.supp_add I x.hden y.hden,
      ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) y.denExp x.num, by
        have hx := ProjSpaceCech.GradedModule.monMul_mem_grade _ y.denExp _ x.num x.hnum
        convert hx using 2; simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]⟩
  set w₂ : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I :=
    ⟨x.denExp + y.denExp, ProjSpaceCech.GradedModule.Frac.supp_add I x.hden y.hden,
      ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) x.denExp y.num, by
        have hy := ProjSpaceCech.GradedModule.monMul_mem_grade _ x.denExp _ y.num y.hnum
        convert hy using 2
        simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]; ring⟩
  rw [secAux_wellDef ι I (x := x) (y := w₁)
      ⟨0, fun _ _ => rfl, by
        dsimp only [w₁]; rw [zero_add, zero_add, ← ProjSpaceCech.GradedModule.monMul_add_apply]⟩,
    secAux_wellDef ι I (x := y) (y := w₂)
      ⟨0, fun _ _ => rfl, by
        dsimp only [w₂]; rw [zero_add, zero_add, ← ProjSpaceCech.GradedModule.monMul_add_apply]
        exact ProjSpaceCech.GradedModule.monMul_congr _ (fun j => add_comm _ _) _⟩,
    show secAux ι I w₁
      = testAtI ι I (∑ k, w₁.denExp k) (secAuxNum_mem I w₁)
      from rfl,
    show secAux ι I w₂
      = testAtI ι I (∑ k, w₂.denExp k) (secAuxNum_mem I w₂)
      from rfl,
    ← testAtI_add ι I _ (secAuxNum_mem I w₁)
      (secAuxNum_mem I w₂)]
  unfold secAux
  exact testAtI_congr ι I rfl _
    (Submodule.add_mem _ (secAuxNum_mem I w₁)
      (secAuxNum_mem I w₂))
    (map_add (ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
      (pad I (x.denExp + y.denExp))) _ _)
theorem

canonicalAlg_eq

L477 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.canonicalAlg_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem canonicalAlg_eq (I : Finset (Fin (n + 1))) (hI : I.Nonempty) (r : A) :
    letI := canonicalAlg (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    (ι.app _).hom ((AlgebraicGeometry.Proj.awayToSection 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))).hom
      ((HomogeneousLocalization.fromZeroRingHom 𝒜 _) (ProjSpace.grad0Equiv A n r)))
      = algebraMap A Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
          (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))) r := by
  rw [canonicalAlg_compat (ι ≫ ProjSpace.π A n)]
  have hawayι : AlgebraicGeometry.Proj.awayι 𝒜 _ (prodX_mem I)
        (Finset.card_pos.mpr hI) ≫ ProjSpace.π A n
      = Spec.map (CommRingCat.ofHom ((HomogeneousLocalization.fromZeroRingHom 𝒜 _).comp
          (ProjSpace.grad0Equiv A n).toRingHom)) := by
    unfold ProjSpace.π
    rw [← Category.assoc, AlgebraicGeometry.Proj.awayι_toSpecZero, ← Spec.map_comp]; rfl
  have hIι : (AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))).ι ≫ ProjSpace.π A n
      = AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 _
        ≫ Spec.map (CommRingCat.ofHom ((HomogeneousLocalization.fromZeroRingHom 𝒜 _).comp
            (ProjSpace.grad0Equiv A n).toRingHom)) := by
    rw [← hawayι, ← AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι 𝒜 _
      (prodX_mem I) (Finset.card_pos.mpr hI),
      ← Category.assoc (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 _),
      ← AlgebraicGeometry.Proj.basicOpenIsoSpec_hom 𝒜 _ (prodX_mem I)
        (Finset.card_pos.mpr hI),
      Iso.hom_inv_id_assoc]
  have hres := (Scheme.ΓSpecIso (.of A)).inv ≫= congrArg Scheme.Hom.appTop hIι
    =≫ (AlgebraicGeometry.Proj.basicOpen 𝒜 (∏ j ∈ I, (X j : _))).topIso.hom
  simp only [Scheme.Hom.comp_appTop, CommRingCat.ofHom_comp, Spec.map_comp,
    Category.assoc] at hres
  rw [← Scheme.ΓSpecIso_inv_naturality_assoc, ← Scheme.ΓSpecIso_inv_naturality_assoc,
    show (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))).appTop
      = (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 _).app ⊤ from rfl,
    AlgebraicGeometry.Proj.basicOpenToSpec_app_top, Category.assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, Category.comp_id, Scheme.Opens.ι_appTop,
    Scheme.Opens.topIso_hom] at hres
  have hres' := congrArg (fun φ => CommRingCat.Hom.hom φ r) hres
  simp only [CommRingCat.hom_comp, RingHom.comp_apply, CommRingCat.hom_ofHom] at hres'
  have hιnat := congrArg (fun φ => CommRingCat.Hom.hom φ
      ((ProjSpace.π A n).appTop.hom ((Scheme.ΓSpecIso (.of A)).inv.hom r)))
    (ι.naturality (homOfLE (le_top :
      AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)) ≤ ⊤)).op)
  simp only [CommRingCat.hom_comp, RingHom.comp_apply] at hιnat
  rw [show ((ι ≫ ProjSpace.π A n).appTop : _)
    = (ProjSpace.π A n).appTop ≫ ι.appTop from rfl, CommRingCat.hom_comp,
    RingHom.comp_apply]
  refine ((congrArg _ (hres'.symm.trans ?_)).trans hιnat).trans
    (congrArg (fun α => (W.presheaf.map α).hom _) (Subsingleton.elim _ _))
  rw [← CommRingCat.comp_apply]
  erw [← (Proj 𝒜).presheaf.map_comp]
  exact congrArg (fun φ => CommRingCat.Hom.hom φ _)
    (congrArg ((Proj 𝒜).presheaf.map) (Subsingleton.elim _ _))
theorem

secAux_smul

L534 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAux_smul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem secAux_smul (I : Finset (Fin (n + 1))) (hI : I.Nonempty) (r : A)
    (x : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n) I) :
    letI := moduleΓ (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    secAux ι I ⟨x.denExp, x.hden, r • x.num, Submodule.smul_mem _ r x.hnum⟩
      = r • secAux ι I x := by
  let := canonicalAlg (ι ≫ ProjSpace.π A n)
    (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
  change _ = algebraMap A _ r * secAux ι I x
  unfold secAux
  rw [testAtI_congr ι I rfl (secAuxNum_mem I
      ⟨x.denExp, x.hden, r • x.num, Submodule.smul_mem _ r x.hnum⟩)
    (Submodule.smul_mem _ r (secAuxNum_mem I x))
    (map_smul _ r x.num)]
  unfold testAtI
  rw [← canonicalAlg_eq ι I hI r, ← map_mul, ← map_mul]
  refine congrArg _ (congrArg _ (HomogeneousLocalization.val_injective _ ?_))
  have hzero : (HomogeneousLocalization.fromZeroRingHom 𝒜
      (Submonoid.powers (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
      (ProjSpace.grad0Equiv A n r)).val = Localization.mk (C r) 1 := rfl
  erw [HomogeneousLocalization.val_mul, HomogeneousLocalization.Away.val_mk,
    hzero, HomogeneousLocalization.Away.val_mk, Localization.mk_mul, smul_eq_C_mul]
  congr 1; ext : 1; simp
def

freeSec

L561 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.freeSec
Documentation

The linear map from localized free graded sections to sections on the closed subscheme.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
def freeSec (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    letI := moduleΓ (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    ProjSpaceCech.GradedModule.sec (ProjSpaceCech.GradedModule.free A n) I
      →ₗ[A] Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))) := by
  letI := moduleΓ (ι ≫ ProjSpace.π A n)
    (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
  exact
  { toFun := Quotient.lift (secAux ι I)
      (fun _ _ => secAux_wellDef ι I)
    map_add' := by rintro ⟨x⟩ ⟨y⟩; exact secAux_add ι I x y
    map_smul' := by rintro r ⟨x⟩; exact secAux_smul ι I hI r x }
theorem

freeSec_surjective

L577 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.freeSec_surjective
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem freeSec_surjective (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    letI := moduleΓ (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    Function.Surjective (freeSec ι I hI) := by
  intro s
  have hUaff : IsAffineOpen (AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))) :=
    AlgebraicGeometry.Proj.isAffineOpen_basicOpen 𝒜 _ (prodX_mem I)
      (Finset.card_pos.mpr hI)
  obtain ⟨t, ht⟩ := ι.app_surjective _ hUaff s
  let z := (AlgebraicGeometry.Proj.basicOpenIsoAway 𝒜 _ (prodX_mem I)
    (Finset.card_pos.mpr hI)).inv t
  obtain ⟨k, m, hm, hmk⟩ :=
    HomogeneousLocalization.Away.mk_surjective 𝒜 (prodX_mem I) z
  have hm' : m ∈ 𝒜 (k * I.card) := by simpa [smul_eq_mul] using hm
  have hsum : (∑ j, if j ∈ I then k else 0) = k * I.card := by
    rw [Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, smul_eq_mul, mul_comm]
  have hcast : (∑ j, ((if j ∈ I then k else 0 : ℕ) : ℤ)) = ((k * I.card : ℕ) : ℤ) := by
    exact_mod_cast hsum
  have hnum : m ∈ (ProjSpaceCech.GradedModule.free A n).grade
      (∑ j, ((if j ∈ I then k else 0 : ℕ) : ℤ)) := by
    change m ∈ ProjSpaceCech.GradedModule.freeGrade A n _
    rw [hcast, ProjSpaceCech.GradedModule.freeGrade_of_nonneg A n (Int.natCast_nonneg _),
      Int.toNat_natCast]
    exact hm'
  refine ⟨ProjSpaceCech.GradedModule.sec.mk _ I
    ⟨fun j => if j ∈ I then k else 0, fun j hj => by simp [hj], m, hnum⟩, ?_⟩
  have hle : k ≤ k * I.card := Nat.le_mul_of_pos_right k (Finset.card_pos.mpr hI)
  have hpad : pad I (fun j => if j ∈ I then k else 0)
      = fun j => if j ∈ I then k * I.card - k else 0 :=
    funext fun j => by unfold pad; by_cases hj : j ∈ I <;> simp [hj, hsum]
  have hnum' :=
    secAuxNum_mem (A := A) I ⟨_, fun j hj => by simp [hj], m, hnum⟩
  change secAux ι I ⟨_, fun j hj => by simp [hj], m, hnum⟩ = s
  unfold secAux
  refine ((testAtI_congr ι I (hsum.trans (Nat.sub_add_cancel hle).symm) hnum'
      (prodXpow_mul_mem I (k * I.card - k) hm') ?_).trans
    ((testAtI_prodXpow ι I k (k * I.card - k) hm' _).trans ?_))
  · dsimp only; rw [hpad, ← prodXpow_eq_monMul]
  · unfold testAtI
    refine (congrArg _ ?_).trans ht
    exact (congrArg _ hmk).trans (congrArg (fun φ => CommRingCat.Hom.hom φ t)
      (AlgebraicGeometry.Proj.basicOpenIsoAway 𝒜 _ (prodX_mem I)
        (Finset.card_pos.mpr hI)).inv_hom_id)
theorem

proj_basicOpen_awayMk

L623 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.proj_basicOpen_awayMk
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem proj_basicOpen_awayMk (j : Fin (n + 1)) {d : ℕ}
    {g : MvPolynomial (Fin (n + 1)) A} (hg : g ∈ 𝒜 d) :
    (Proj 𝒜).basicOpen ((AlgebraicGeometry.Proj.awayToSection 𝒜 (X j)).hom
        (HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A n j) d g
          (by simpa using hg)))
      = AlgebraicGeometry.Proj.basicOpen 𝒜 ((X j : MvPolynomial (Fin (n + 1)) A) * g) := by
  set z := HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A n j) d g
    (by simpa using hg) with hz
  have hkey : ∀ (x : Proj 𝒜) (hxj : x ∈ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j)),
      IsUnit ((Proj 𝒜).presheaf.germ _ x hxj
        ((AlgebraicGeometry.Proj.awayToSection 𝒜 (X j)).hom z))
        ↔ g ∉ x.asHomogeneousIdeal := by
    intro x hxj
    let : x.asHomogeneousIdeal.toIdeal.IsPrime :=
      (show ProjectiveSpectrum 𝒜 from x).isPrime
    have hxj' : (X j : MvPolynomial (Fin (n + 1)) A)
        ∈ x.asHomogeneousIdeal.toIdeal.primeCompl := hxj
    have hgerm := congrArg (fun φ => CommRingCat.Hom.hom φ z)
      (ProjectiveSpectrum.Proj.awayToSection_germ 𝒜 (X j) x hxj)
    simp only [CommRingCat.hom_comp, RingHom.comp_apply, CommRingCat.hom_ofHom] at hgerm
    erw [hgerm]
    have : IsLocalHom (AlgebraicGeometry.Proj.stalkIso' 𝒜 x).toCommRingCatIso.inv.hom :=
      isLocalHom_of_isIso _
    refine (isUnit_map_iff (AlgebraicGeometry.Proj.stalkIso' 𝒜 x).toCommRingCatIso.inv.hom
      _).trans ?_
    rw [← HomogeneousLocalization.isUnit_iff_isUnit_val]
    have hval : (HomogeneousLocalization.mapId 𝒜 (Submonoid.powers_le.mpr hxj') z).val
        = Localization.mk g ⟨(X j : MvPolynomial (Fin (n + 1)) A) ^ d,
            pow_mem hxj' d⟩ := by
      simp only [hz, HomogeneousLocalization.Away.mk, HomogeneousLocalization.mapId]
      rfl
    rw [show Submonoid.powers_le.mpr hxj = Submonoid.powers_le.mpr hxj' from rfl, hval,
      Localization.mk_eq_mk', IsLocalization.AtPrime.isUnit_mk'_iff]
    exact Iff.rfl
  ext x
  simp only [SetLike.mem_coe, AlgebraicGeometry.Proj.basicOpen_mul,
    AlgebraicGeometry.Proj.mem_basicOpen, Opens.mem_inf]
  refine ⟨fun hx => ?_, fun ⟨hxj, hxg⟩ => ?_⟩
  · have hxj : x ∈ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j) := Scheme.basicOpen_le _ _ hx
    exact ⟨hxj, (hkey x hxj).mp ((Scheme.mem_basicOpen _ _ x hxj).mp hx)⟩
  · exact (Scheme.mem_basicOpen _ _ x hxj).mpr ((hkey x hxj).mpr hxg)
theorem

freeSec_ker_le

L665 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.freeSec_ker_le
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem freeSec_ker_le (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    letI := moduleΓ (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    LinearMap.ker (freeSec ι I hI)
      ≤ LinearMap.ker (ProjSpaceCech.GradedModule.Hom.secMap (mkQHom ι) I) := by
  let := moduleΓ (ι ≫ ProjSpace.π A n)
    (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
  rintro z hz
  obtain ⟨x⟩ := z
  have hz' : testAtI ι I (∑ k, x.denExp k)
      (secAuxNum_mem I x) = 0 := hz
  set sa := ∑ k, x.denExp k with hsa
  set m' : MvPolynomial (Fin (n + 1)) A :=
    ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
      (pad I x.denExp) x.num with hm'
  have hm'mem : m' ∈ 𝒜 (sa * I.card) := secAuxNum_mem I x
  have hperj : ∀ j : Fin (n + 1), ∃ N : ℕ,
      testAt ι ((N + sa) * I.card) j
        ⟨(∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ N * m',
          prodXpow_mul_mem I N hm'mem⟩ = 0 := by
    intro j
    set r_j := testAt ι I.card j
      ⟨∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A), prodX_mem I⟩ with hrj
    have hVj : IsAffineOpen (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j)) :=
      (AlgebraicGeometry.Proj.isAffineOpen_basicOpen 𝒜 (X j)
        (ProjSpace.X_mem_one A n j) one_pos).preimage ι
    have hbopen : W.basicOpen r_j
        = ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
            ((X j : MvPolynomial (Fin (n + 1)) A) * ∏ i ∈ I, X i) := by
      rw [hrj]; unfold testAt
      rw [show ((ι.app _).hom _ : Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j)))
            = ι.app (AlgebraicGeometry.Proj.basicOpen 𝒜 (X j))
              ((AlgebraicGeometry.Proj.awayToSection 𝒜 (X j)).hom
                (HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A n j) I.card
                  (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A))
                  (by simpa using prodX_mem I))) from rfl,
        ← Scheme.preimage_basicOpen ι,
        proj_basicOpen_awayMk j (prodX_mem I)]
    have := hVj.isLocalization_basicOpen r_j
    have hres0 : algebraMap Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j))
        Γ(W, W.basicOpen r_j) (testAt ι (sa * I.card) j ⟨m', hm'mem⟩) = 0 := by
      set zm := HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A n j)
        (sa * I.card) m' (by simpa using hm'mem) with hzm
      change (ι.appLE (AlgebraicGeometry.Proj.basicOpen 𝒜 (X j)) (W.basicOpen r_j)
          (W.basicOpen_le r_j)).hom ((AlgebraicGeometry.Proj.awayToSection 𝒜 (X j)).hom zm) = 0
      rw [← Scheme.Hom.appLE_map' ι (W.basicOpen_le r_j) hbopen, CommRingCat.comp_apply]
      refine Eq.trans (congrArg _ ?_) (map_zero _)
      have hle_jV : AlgebraicGeometry.Proj.basicOpen 𝒜
            ((X j : MvPolynomial (Fin (n + 1)) A) * ∏ i ∈ I, X i)
          ≤ AlgebraicGeometry.Proj.basicOpen 𝒜 (X j) :=
        AlgebraicGeometry.Proj.basicOpen_mono 𝒜 _ _ ⟨_, rfl⟩
      rw [show (ι.appLE _ _ (hbopen ▸ W.basicOpen_le r_j) : _)
            = (Proj 𝒜).presheaf.map (homOfLE hle_jV).op
              ≫ ι.app (AlgebraicGeometry.Proj.basicOpen 𝒜 ((X j : _) * ∏ i ∈ I, X i)) by
          rw [Scheme.Hom.app_eq_appLE, Scheme.Hom.map_appLE],
        CommRingCat.comp_apply]
      have hway_j := congrArg (fun φ => CommRingCat.Hom.hom φ zm)
        (AlgebraicGeometry.Proj.awayMap_awayToSection 𝒜
          (prodX_mem I)
          (rfl : (X j : MvPolynomial (Fin (n + 1)) A) * ∏ i ∈ I, X i = X j * ∏ i ∈ I, X i))
      simp only [CommRingCat.hom_comp, RingHom.comp_apply, CommRingCat.hom_ofHom] at hway_j
      erw [← hway_j]
      have hXjg_mem : (X j : MvPolynomial (Fin (n + 1)) A) * ∏ i ∈ I, X i ∈ 𝒜 (1 + I.card) :=
        SetLike.mul_mem_graded (ProjSpace.X_mem_one A n j) (prodX_mem I)
      have hw_mem : (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ (sa * (I.card + 1))
          ∈ 𝒜 ((sa * I.card) • (1 + I.card)) := by
        have hpw :=
          SetLike.pow_mem_graded (sa * (I.card + 1)) (prodX_mem (A := A) I)
        have hdeq : (sa * (I.card + 1)) • I.card = (sa * I.card) • (1 + I.card) := by
          simp only [smul_eq_mul]; ring
        exact hdeq ▸ hpw
      have hprod : HomogeneousLocalization.awayMap 𝒜 (prodX_mem I)
            (rfl : (X j : _) * ∏ i ∈ I, X i = X j * ∏ i ∈ I, X i) zm
          = HomogeneousLocalization.Away.mk 𝒜 hXjg_mem (sa * I.card)
              ((∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ (sa * (I.card + 1))) hw_mem
            * HomogeneousLocalization.awayMap 𝒜 (ProjSpace.X_mem_one A n j)
              (mul_comm (X j : _) (∏ i ∈ I, X i))
              (HomogeneousLocalization.Away.mk 𝒜 (prodX_mem I) sa m'
                (by simpa [smul_eq_mul] using hm'mem)) := by
        refine HomogeneousLocalization.val_injective _ ?_
        simp only [hzm, HomogeneousLocalization.val_mul, HomogeneousLocalization.Away.mk,
          HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_awayMap_mk, Localization.mk_mul]
        rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
        refine ⟨1, ?_⟩
        simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_pow]
        ring_nf
      rw [hprod, map_mul, map_mul]
      refine mul_eq_zero_of_right _ ?_
      have hle_IV : AlgebraicGeometry.Proj.basicOpen 𝒜
            ((X j : MvPolynomial (Fin (n + 1)) A) * ∏ i ∈ I, X i)
          ≤ AlgebraicGeometry.Proj.basicOpen 𝒜 (∏ i ∈ I, (X i : _)) :=
        AlgebraicGeometry.Proj.basicOpen_mono 𝒜 _ _ ⟨_, mul_comm _ _⟩
      have hway_I := congrArg (fun φ => CommRingCat.Hom.hom φ
          (HomogeneousLocalization.Away.mk 𝒜 (prodX_mem I) sa m'
            (by simpa [smul_eq_mul] using hm'mem)))
        (AlgebraicGeometry.Proj.awayMap_awayToSection 𝒜 (ProjSpace.X_mem_one A n j)
          (mul_comm (X j : _) (∏ i ∈ I, X i)))
      simp only [CommRingCat.hom_comp, RingHom.comp_apply, CommRingCat.hom_ofHom] at hway_I
      erw [hway_I]
      have hnat := congrArg (fun φ => CommRingCat.Hom.hom φ
          ((AlgebraicGeometry.Proj.awayToSection 𝒜 (∏ i ∈ I, (X i : _))).hom
            (HomogeneousLocalization.Away.mk 𝒜 (prodX_mem I) sa m'
              (by simpa [smul_eq_mul] using hm'mem))))
        (ι.naturality (homOfLE hle_IV).op)
      simp only [CommRingCat.hom_comp, RingHom.comp_apply] at hnat
      erw [hnat]
      exact (congrArg _ hz').trans (map_zero _)
    obtain ⟨⟨_, N, rfl⟩, hann⟩ :=
      (IsLocalization.map_eq_zero_iff (Submonoid.powers r_j) _ _).mp hres0
    have hann' : r_j ^ N * testAt ι (sa * I.card) j ⟨m', hm'mem⟩ = 0 := hann
    refine ⟨N, ?_⟩
    have hzpow : (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ N ∈ 𝒜 (N * I.card) := by
      have := SetLike.pow_mem_graded N (prodX_mem (A := A) I)
      simpa [smul_eq_mul, mul_comm] using this
    refine (testAt_congr ι (by ring) j
        (prodXpow_mul_mem I N hm'mem)
        (SetLike.mul_mem_graded hzpow hm'mem) rfl).trans ?_
    refine (testAt_mul ι (sa * I.card) (N * I.card) j
        ⟨m', hm'mem⟩ ⟨_, hzpow⟩ (SetLike.mul_mem_graded hzpow hm'mem)).trans ?_
    refine Eq.trans (congrArg₂ (· * ·) ?_ rfl) hann'
    rw [hrj]; unfold testAt; rw [← map_pow, ← map_pow]
    refine congrArg _ (congrArg _ (HomogeneousLocalization.val_injective _ ?_))
    simp only [HomogeneousLocalization.Away.val_mk, HomogeneousLocalization.val_pow]
    rw [Localization.mk_pow]; congr 1; ext : 1
    simp only [SubmonoidClass.coe_pow]
    rw [← pow_mul, Nat.mul_comm]
  choose N hN using hperj
  set Nmax := ∑ i, N i with hNmax
  have hNle : ∀ j, N j ≤ Nmax := fun j =>
    Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ j)
  have hp_mem : (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ Nmax * m'
      ∈ 𝒜 ((Nmax + sa) * I.card) := prodXpow_mul_mem I Nmax hm'mem
  have htestAll : ∀ j, testAt ι ((Nmax + sa) * I.card) j
      ⟨(∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ Nmax * m', hp_mem⟩ = 0 := by
    intro j
    have hsplit :
        (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ Nmax * m'
          = (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ (Nmax - N j)
            * ((∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ (N j) * m') := by
      rw [← mul_assoc, ← pow_add, Nat.sub_add_cancel (hNle j)]
    have hle := hNle j
    have hdeg : (Nmax + sa) * I.card
        = (Nmax - N j) * I.card + (N j + sa) * I.card := by
      rw [← add_mul]; congr 1; omega
    have hzpow : (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ (Nmax - N j)
        ∈ 𝒜 ((Nmax - N j) * I.card) := by
      have := SetLike.pow_mem_graded (Nmax - N j) (prodX_mem (A := A) I)
      simpa [smul_eq_mul, mul_comm] using this
    refine (testAt_congr ι hdeg j hp_mem
        (SetLike.mul_mem_graded hzpow (prodXpow_mul_mem I (N j) hm'mem))
        hsplit).trans ?_
    exact (testAt_mul ι ((N j + sa) * I.card) ((Nmax - N j) * I.card) j
        ⟨_, prodXpow_mul_mem I (N j) hm'mem⟩ ⟨_, hzpow⟩
        (SetLike.mul_mem_graded hzpow (prodXpow_mul_mem I (N j) hm'mem))).trans
      (by rw [hN j, mul_zero])
  have hp_J : (∏ i ∈ I, (X i : MvPolynomial (Fin (n + 1)) A)) ^ Nmax * m'
      ∈ J ι := (mem_J_homogeneous ι hp_mem).mpr htestAll
  refine LinearMap.mem_ker.mpr ((ProjSpaceCech.GradedModule.sec_mk_eq _ I).mpr
    ⟨(fun j => if j ∈ I then Nmax else 0) + pad I x.denExp,
      fun j hj => by simp [hj, pad], ?_⟩)
  simp only [map_zero, add_zero]
  show ProjSpaceCech.GradedModule.monMul (Dι ι) _
    ((mkQHom ι).toLinearMap x.num) = 0
  rw [← ProjSpaceCech.GradedModule.Hom.map_monMul (mkQHom ι)]
  refine (Submodule.Quotient.mk_eq_zero _).mpr ?_
  rw [ProjSpaceCech.GradedModule.monMul_add_apply, ← hm',
    ProjSpaceCech.GradedModule.free_monMul_apply (fun j => if j ∈ I then Nmax else 0),
    show (∏ j, (X j : MvPolynomial (Fin (n + 1)) A) ^ if j ∈ I then Nmax else 0)
        = (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)) ^ Nmax from
      (Finset.prod_subset (Finset.subset_univ I)
        (fun j _ hj => by rw [ite_eq_right hj, pow_zero])).symm.trans
        ((Finset.prod_congr rfl (fun j hj => by rw [ite_eq_left hj])).trans
          (Finset.prod_pow _ _ _))]
  exact hp_J
theorem

testAtI_eq_zero_of_mem_J

L844 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.testAtI_eq_zero_of_mem_J
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem testAtI_eq_zero_of_mem_J (I : Finset (Fin (n + 1))) (hI : I.Nonempty)
    {k : ℕ} {p : MvPolynomial (Fin (n + 1)) A} (hp : p ∈ 𝒜 (k * I.card))
    (hpJ : p ∈ J ι) :
    testAtI ι I k hp = 0
theorem

freeSec_ker_ge

L928 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.freeSec_ker_ge
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem freeSec_ker_ge (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    letI := moduleΓ (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    LinearMap.ker (ProjSpaceCech.GradedModule.Hom.secMap (mkQHom ι) I)
      ≤ LinearMap.ker (freeSec ι I hI) := by
  let := moduleΓ (ι ≫ ProjSpace.π A n)
    (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
  rintro z hz; obtain ⟨x⟩ := z
  obtain ⟨c, hc, heq⟩ := (ProjSpaceCech.GradedModule.sec_mk_eq _ I).mp hz
  simp only [map_zero, add_zero] at heq
  have hmemJ : ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n) c x.num
      ∈ J ι :=
    (Submodule.Quotient.mk_eq_zero _).mp
      ((ProjSpaceCech.GradedModule.Hom.map_monMul (mkQHom ι) c x.num).trans heq)
  obtain ⟨hm, hx1⟩ := secAux_enlarge ι I x c hc
  refine LinearMap.mem_ker.mpr (show secAux ι I x = 0 from hx1.trans ?_)
  refine testAtI_eq_zero_of_mem_J ι I hI hm ?_
  rw [ProjSpaceCech.GradedModule.monMul_add_apply]
  exact J_monMul_stable ι _ _ hmemJ
theorem

gradSecMap_mkQ_surj

L951 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.gradSecMap_mkQ_surj
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem gradSecMap_mkQ_surj (I : Finset (Fin (n + 1))) :
    Function.Surjective (ProjSpaceCech.GradedModule.Hom.secMap (mkQHom ι) I)
def

quotSecEquiv

L960 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.quotSecEquiv
Documentation

The linear equivalence from localized quotient graded sections to subscheme sections.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
def quotSecEquiv (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    letI := moduleΓ (ι ≫ ProjSpace.π A n)
      (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
    ProjSpaceCech.GradedModule.sec (Dι ι) I
      ≃ₗ[A] Γ(W, ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
        (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A))) := by
  letI := moduleΓ (ι ≫ ProjSpace.π A n)
    (ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜
      (∏ j ∈ I, (X j : MvPolynomial (Fin (n + 1)) A)))
  exact LinearEquiv.trans
    (LinearMap.quotKerEquivOfSurjective _ (gradSecMap_mkQ_surj ι I)).symm
    ((Submodule.quotEquivOfEq _ _
        (le_antisymm (freeSec_ker_ge ι I hI)
          (freeSec_ker_le ι I hI))).trans
      (LinearMap.quotKerEquivOfSurjective _ (freeSec_surjective ι I hI)))
theorem

quotSecEquiv_gradSecMap

L977 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.quotSecEquiv_gradSecMap
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem quotSecEquiv_gradSecMap (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    (quotSecEquiv ι I hI).toLinearMap
        ∘ₗ ProjSpaceCech.GradedModule.Hom.secMap (mkQHom ι) I
      = freeSec ι I hI := by
  let : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
  refine LinearMap.ext fun z => ?_
  obtain ⟨y⟩ := z
  change (quotSecEquiv ι I hI)
    (ProjSpaceCech.GradedModule.Hom.secMap (mkQHom ι) I ⟦y⟧) = secAux ι I y
  unfold quotSecEquiv
  erw [LinearEquiv.trans_apply, LinearMap.quotKerEquivOfSurjective_symm_apply,
    LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
    LinearMap.quotKerEquivOfSurjective_apply_mk]
  rfl
theorem

secAux_face

L994 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.secAux_face
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem secAux_face {I I' : Finset (Fin (n + 1))} (hII' : I ⊆ I')
    (_hI : I.Nonempty) (y : ProjSpaceCech.GradedModule.Frac (ProjSpaceCech.GradedModule.free A n)
      I) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    secAux ι I'
        ⟨y.denExp, fun j hj => y.hden j (fun h => hj (hII' h)), y.num, y.hnum⟩
      = resLinearMap (ι ≫ ProjSpace.π A n) (by
          rw [← finsetInf_basicOpen ι,
            ← finsetInf_basicOpen ι]; exact biInf_mono hII')
        (secAux ι I y) := by
  unfold secAux testAtI
  have hsplit : (∏ j ∈ I', (X j : MvPolynomial (Fin (n + 1)) A))
      = (∏ j ∈ I, X j) * ∏ j ∈ I' \ I, X j :=
    (Finset.prod_sdiff hII').symm.trans (mul_comm _ _)
  have hgdeg : (∏ j ∈ I' \ I, (X j : MvPolynomial (Fin (n + 1)) A)) ∈ 𝒜 (I' \ I).card :=
    prodX_mem (A := A) (I' \ I)
  have hway := congrArg (fun φ => CommRingCat.Hom.hom φ
      (HomogeneousLocalization.Away.mk 𝒜 (prodX_mem I) (∑ k, y.denExp k)
        (ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
          (pad I y.denExp) y.num)
        (by
          have hnum := secAuxNum_mem I y
          change @Membership.mem (MvPolynomial (Fin (n + 1)) A)
            (Submodule A (MvPolynomial (Fin (n + 1)) A)) SetLike.instMembership
            (𝒜 ((∑ k, y.denExp k) * I.card))
            (ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
              (pad I y.denExp) y.num) at hnum
          simpa only [smul_eq_mul] using hnum)))
    (AlgebraicGeometry.Proj.awayMap_awayToSection 𝒜 hgdeg hsplit)
  simp only [CommRingCat.hom_comp, RingHom.comp_apply, CommRingCat.hom_ofHom] at hway
  have hnat := congrArg (fun φ => CommRingCat.Hom.hom φ
      ((AlgebraicGeometry.Proj.awayToSection 𝒜 (∏ j ∈ I, (X j : _))).hom
        (HomogeneousLocalization.Away.mk 𝒜 (prodX_mem I) (∑ k, y.denExp k) _
          (by
            have hnum := secAuxNum_mem I y
            change @Membership.mem (MvPolynomial (Fin (n + 1)) A)
              (Submodule A (MvPolynomial (Fin (n + 1)) A)) SetLike.instMembership
              (𝒜 ((∑ k, y.denExp k) * I.card))
              (ProjSpaceCech.GradedModule.monMul (ProjSpaceCech.GradedModule.free A n)
                (pad I y.denExp) y.num) at hnum
            simpa only [smul_eq_mul] using hnum))))
    (ι.naturality (homOfLE (AlgebraicGeometry.Proj.basicOpen_mono 𝒜 _ _ ⟨_, hsplit⟩)).op)
  simp only [CommRingCat.hom_comp, RingHom.comp_apply] at hnat
  change (ι.app _).hom ((AlgebraicGeometry.Proj.awayToSection 𝒜 _).hom _)
    = (W.presheaf.map _).hom ((ι.app _).hom ((AlgebraicGeometry.Proj.awayToSection 𝒜 _).hom _))
  refine (congrArg _ ((congrArg _ ?_).trans hway)).trans
    (hnat.trans (congrArg (fun α => (W.presheaf.map α).hom _) (Subsingleton.elim _ _)))
  refine HomogeneousLocalization.val_injective _ ?_
  simp only [HomogeneousLocalization.Away.mk, HomogeneousLocalization.val_mk,
    HomogeneousLocalization.val_awayMap_mk]
  erw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
  have hpad : ∀ j ∈ I',
      (if j ∈ I then pad I y.denExp j else ∑ k, y.denExp k)
        = pad I' y.denExp j := fun j hj => by
    unfold pad; by_cases hjI : j ∈ I
    · simp [hj, hjI]
    · simp [hj, hjI, y.hden j hjI]
  have hprod : (∏ j, (X j : MvPolynomial (Fin (n + 1)) A) ^ pad I y.denExp j)
        * (∏ j ∈ I' \ I, (X j : MvPolynomial (Fin (n + 1)) A)) ^ (∑ k, y.denExp k)
      = ∏ j, (X j : MvPolynomial (Fin (n + 1)) A) ^ pad I' y.denExp j := by
    rw [← Finset.prod_pow, show (∏ j ∈ I' \ I, (X j : MvPolynomial (Fin (n + 1)) A)
          ^ (∑ k, y.denExp k)) = ∏ j, (X j : MvPolynomial (Fin (n + 1)) A)
          ^ if j ∈ I' \ I then ∑ k, y.denExp k else 0 from
        (Finset.prod_congr rfl fun j hj => by rw [ite_eq_left hj]).trans
          (Finset.prod_subset (I' \ I).subset_univ fun j _ hj => by
            rw [ite_eq_right hj, pow_zero]),
      ← Finset.prod_mul_distrib]
    exact Finset.prod_congr rfl fun j _ => by
      rw [← pow_add]; refine congrArg (X j ^ ·) ?_
      by_cases hjI' : j ∈ I'
      · rw [← hpad j hjI']
        by_cases hjI : j ∈ I <;>
          simp [hjI, hjI', Finset.mem_sdiff, pad]
      · have hjI : j ∉ I := fun h => hjI' (hII' h)
        simp [hjI', hjI, Finset.mem_sdiff, pad]
  refine ⟨1, ?_⟩
  simp only [OneMemClass.coe_one, one_mul]
  erw [ProjSpaceCech.GradedModule.free_monMul_apply,
    ProjSpaceCech.GradedModule.free_monMul_apply]
  rw [← hprod]
  exact congrArg (_ * ·) (mul_right_comm _ _ _)
theorem

quotSecEquiv_face

L1076 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.quotSecEquiv_face
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem quotSecEquiv_face {I I' : Finset (Fin (n + 1))}
    (hII' : I ⊆ I') (hI : I.Nonempty) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    (quotSecEquiv ι I' (hI.mono hII')).toLinearMap
        ∘ₗ ProjSpaceCech.GradedModule.secIncl (Dι ι) hII'
      = (resLinearMap (ι ≫ ProjSpace.π A n) (by
            rw [← finsetInf_basicOpen ι,
              ← finsetInf_basicOpen ι]
            exact biInf_mono hII'))
        ∘ₗ (quotSecEquiv ι I hI).toLinearMap := by
  let : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
  rw [← LinearMap.cancel_right (gradSecMap_mkQ_surj ι I),
    LinearMap.comp_assoc, LinearMap.comp_assoc,
    ProjSpaceCech.GradedModule.Hom.secMap_incl (mkQHom ι) hII', ← LinearMap.comp_assoc,
    quotSecEquiv_gradSecMap ι I' (hI.mono hII'), ← LinearMap.comp_assoc,
    LinearMap.comp_assoc _ (quotSecEquiv ι I hI).toLinearMap,
    quotSecEquiv_gradSecMap ι I hI]
  refine LinearMap.ext fun z => ?_
  obtain ⟨y, rfl⟩ := Quotient.exists_rep z
  exact secAux_face ι hII' hI y
theorem

Dι_isFG

L1098 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.Dι_isFG
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem Dι_isFG : ProjSpaceCech.GradedModule.IsFG (Dι ι)
theorem

altImg_nonempty

L1113 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.altImg_nonempty
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem altImg_nonempty {i : ℕ} (s : ProjSpaceCech.Idx n i) :
    (ProjSpaceCech.Idx.img n s).Nonempty
def

chainFwd

L1118 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainFwd
Documentation

The map from quotient graded cochains to cochains of the pulled back standard cover.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
def chainFwd (i : ℕ) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    ProjSpaceCech.GradedModule.cochain (Dι ι) i
      →ₗ[A] (OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).cochain (ProjSpace.stdCoverPullback ι) i :=
  letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
  LinearMap.pi fun s' =>
    (resLinearMap (ι ≫ ProjSpace.π A n)
        (altOpen_eq ι i s').le)
      ∘ₗ (quotSecEquiv ι
            (ProjSpaceCech.Idx.img n (idxEquiv ι i s'))
            (altImg_nonempty _)).toLinearMap
      ∘ₗ LinearMap.proj (idxEquiv ι i s')
def

chainBwd

L1132 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainBwd
Documentation

The inverse map from cover cochains to quotient graded cochains.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
def chainBwd (i : ℕ) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    (OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).cochain (ProjSpace.stdCoverPullback ι) i
      →ₗ[A] ProjSpaceCech.GradedModule.cochain (Dι ι) i :=
  letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
  LinearMap.pi fun s =>
    (quotSecEquiv ι (ProjSpaceCech.Idx.img n s)
        (altImg_nonempty s)).symm.toLinearMap
      ∘ₗ resLinearMap (ι ≫ ProjSpace.π A n)
          (altOpen_eq ι i ((idxEquiv ι i).symm s)).ge
      ∘ₗ LinearMap.proj ((idxEquiv ι i).symm s)
theorem

chainFwd_apply

L1144 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainFwd_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem chainFwd_apply (i : ℕ)
    (f : ProjSpaceCech.GradedModule.cochain (Dι ι) i)
    (s' : (ProjSpace.stdCoverPullback ι).Idx i) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    chainFwd ι i f s'
      = resLinearMap (ι ≫ ProjSpace.π A n)
          (altOpen_eq ι i s').le
        (quotSecEquiv ι
          (ProjSpaceCech.Idx.img n (idxEquiv ι i s'))
          (altImg_nonempty _) (f (idxEquiv ι i s'))) := rfl
theorem

chainBwd_apply

L1155 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainBwd_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem chainBwd_apply (i : ℕ)
    (g : (OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).cochain (ProjSpace.stdCoverPullback ι) i) (s
      : ProjSpaceCech.Idx n i) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    chainBwd ι i g s
      = (quotSecEquiv ι (ProjSpaceCech.Idx.img n s)
          (altImg_nonempty s)).symm
        (resLinearMap (ι ≫ ProjSpace.π A n)
          (altOpen_eq ι i ((idxEquiv ι i).symm s)).ge
          (g ((idxEquiv ι i).symm s))) := rfl
def

chainEquiv

L1167 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainEquiv
Documentation

The linear equivalence comparing graded cochains and the pulled back standard cover.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def chainEquiv (i : ℕ) :
    ProjSpaceCech.GradedModule.cochain (Dι ι) i
      ≃ₗ[A] (OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).cochain (ProjSpace.stdCoverPullback ι) i
theorem

chainEquiv_apply

L1199 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainEquiv_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · full declaration
theorem chainEquiv_apply (i : ℕ)
    (f : ProjSpaceCech.GradedModule.cochain (Dι ι) i)
    (s' : (ProjSpace.stdCoverPullback ι).Idx i) :
    letI : ∀ U : W.Opens, Module A Γ(W, U) := moduleΓ (ι ≫ ProjSpace.π A n)
    chainEquiv ι i f s'
      = resLinearMap (ι ≫ ProjSpace.π A n)
          (altOpen_eq ι i s').le
        (quotSecEquiv ι
          (ProjSpaceCech.Idx.img n (idxEquiv ι i s'))
          (altImg_nonempty _) (f (idxEquiv ι i s'))) := rfl
theorem

idxEquiv_altFace

L1210 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.idxEquiv_altFace
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem idxEquiv_altFace (i : ℕ)
    (s' : (ProjSpace.stdCoverPullback ι).Idx (i + 1)) (j : Fin (i + 2)) :
    idxEquiv ι i ((ProjSpace.stdCoverPullback ι).face s' j)
      = ProjSpaceCech.Idx.face n (idxEquiv ι (i + 1) s') j
theorem

chainEquiv_comm

L1215 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainEquiv_comm
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem chainEquiv_comm (i : ℕ) :
    (chainEquiv ι (i + 1)).toLinearMap
        ∘ₗ ProjSpaceCech.GradedModule.d (Dι ι) i
      = (OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).d (ProjSpace.stdCoverPullback ι) i
        ∘ₗ (chainEquiv ι i).toLinearMap
def

chainEquivKer

L1244 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.chainEquivKer
Documentation

The induced linear equivalence between the kernels of the two cochain differentials.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
def chainEquivKer (i : ℕ) :
    ↥(LinearMap.ker (ProjSpaceCech.GradedModule.d (Dι ι) i))
      ≃ₗ[A] ↥(LinearMap.ker ((OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).d
        (ProjSpace.stdCoverPullback ι) i))
theorem

gradH_altHF_finite

L1256 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.gradH_altHF_finite
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
Lean source · statement
theorem gradH_altHF_finite [IsNoetherianRing A] (i : ℕ) :
    Module.Finite A ((OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).HSucc
      (ProjSpace.stdCoverPullback ι) i)
theorem

closedImm_allFinite

L1294 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj.AlgebraicGeometry.ProjSpace.ClosedImmCech.closedImm_allFinite
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ClosedImmCech
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Setup
variable {A : Type u} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
variable {W : Scheme.{u}}
  (ι : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
variable [IsNoetherianRing A]
Lean source · statement
theorem closedImm_allFinite :
    (OModulePresheaf.unit (ι ≫ ProjSpace.π A n)).CechFinite (ProjSpace.stdCoverPullback ι)
theorem

cechFinite_unit_of_isClosedImmersion_proj

L1306 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_unit_of_isClosedImmersion_proj
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_unit_of_isClosedImmersion_proj
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial HomogeneousLocalization
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_unit_of_isClosedImmersion_proj {A :
    Type u} [CommRing A] [IsNoetherianRing A] {n : ℕ} {W : AlgebraicGeometry.Scheme.{u}}
    (ι : W ⟶ AlgebraicGeometry.Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
      [AlgebraicGeometry.IsClosedImmersion ι] :
    (AlgebraicGeometry.OModulePresheaf.unit (ι ≫ AlgebraicGeometry.ProjSpace.π A n)).CechFinite
      (AlgebraicGeometry.ProjSpace.stdCoverPullback ι)

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