Module

ProjSpaceCechGradedModule.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCechGradedModule

77 declarations indexed from sourceView source ↗

Module documentation

Cech sections and cohomology of graded modules for projective space. Fraction sections, presentations and maps supply the coordinate-chart complexes.

Imports8

Mathlib.Tactic.Positivity.Finset
Mathlib.Algebra.MvPolynomial.Basic
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.Tactic.Ring
Mathlib.Tactic.Abel
Lean.Elab.Tactic.NormCast
Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCechTwist

Imported by25

structure

GradedModule

L40 ↗

ProjSpaceCech.GradedModule

Documentation

A graded module equipped with commuting coordinate operators of degree one.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)

Lean source · full declaration

structure GradedModule where
  /-- The underlying module carrier. -/
  M : Type u
  /-- The additive commutative group on the carrier. -/
  [acg : AddCommGroup M]
  /-- The coefficient ring module structure. -/
  [modR : Module R M]
  /-- The submodule of elements in each integer degree. -/
  grade : ℤ → Submodule R M
  /-- Multiplication by each homogeneous coordinate. -/
  xMul : Fin (n + 1) → M →ₗ[R] M
  /-- Each coordinate operator raises degree by one. -/
  xMul_mem_grade : ∀ (j : Fin (n + 1)) (d : ℤ), ∀ m ∈ grade d, xMul j m ∈ grade (d + 1)
  /-- The coordinate operators commute. -/
  xMul_comm : ∀ (j k : Fin (n + 1)), xMul j ∘ₗ xMul k = xMul k ∘ₗ xMul j

theorem

xMul_pow_commute

L61 ↗

ProjSpaceCech.GradedModule.xMul_pow_commute

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.xMul_pow_commute (j k : Fin (n + 1)) (a b : ℕ) :
    Commute (D.xMul j ^ a) (D.xMul k ^ b)

def

monMul

L70 ↗

ProjSpaceCech.GradedModule.monMul

Documentation

The endomorphism given by multiplying by the indicated powers of the commuting coordinate operators.

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

def GradedModule.monMul (a : Fin (n + 1) → ℕ) : D.M →ₗ[R] D.M

theorem

monMul_congr

L74 ↗

ProjSpaceCech.GradedModule.monMul_congr

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_congr {a b : Fin (n + 1) → ℕ} (h : ∀ j, a j = b j) (m : D.M) :
    GradedModule.monMul D a m = GradedModule.monMul D b m

theorem

noncommProd_one

L78 ↗

ProjSpaceCech.GradedModule.noncommProd_one

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.noncommProd_one (s : Finset (Fin (n + 1)))
    (f : Fin (n + 1) → (D.M →ₗ[R] D.M)) (hc : _) (hf : ∀ j ∈ s, f j = 1) :
    s.noncommProd f hc = 1

theorem

monMul_zero

L90 ↗

ProjSpaceCech.GradedModule.monMul_zero

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_zero :
    GradedModule.monMul D 0 = LinearMap.id

theorem

monMul_add

L94 ↗

ProjSpaceCech.GradedModule.monMul_add

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_add (a b : Fin (n + 1) → ℕ) :
    GradedModule.monMul D (a + b)
      = GradedModule.monMul D a * GradedModule.monMul D b

theorem

monMul_add_apply

L102 ↗

ProjSpaceCech.GradedModule.monMul_add_apply

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_add_apply (a b : Fin (n + 1) → ℕ) (m : D.M) :
    GradedModule.monMul D (a + b) m
      = GradedModule.monMul D a (GradedModule.monMul D b m)

theorem

monMul_single

L107 ↗

ProjSpaceCech.GradedModule.monMul_single

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_single (j : Fin (n + 1)) (k : ℕ) :
    GradedModule.monMul D (Pi.single j k) = D.xMul j ^ k

theorem

xMul_pow_mem_grade

L119 ↗

ProjSpaceCech.GradedModule.xMul_pow_mem_grade

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.xMul_pow_mem_grade (j : Fin (n + 1)) (k : ℕ) (d : ℤ) :
    ∀ m ∈ D.grade d, (D.xMul j ^ k) m ∈ D.grade (d + k)

theorem

monMul_mem_grade

L130 ↗

ProjSpaceCech.GradedModule.monMul_mem_grade

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_mem_grade (a : Fin (n + 1) → ℕ) (d : ℤ) :
    ∀ m ∈ D.grade d, GradedModule.monMul D a m ∈ D.grade (d + ∑ j, (a j : ℤ))

theorem

monMul_commute

L151 ↗

ProjSpaceCech.GradedModule.monMul_commute

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_commute (a b : Fin (n + 1) → ℕ) :
    Commute (GradedModule.monMul D a) (GradedModule.monMul D b)

theorem

monMul_commute_apply

L157 ↗

ProjSpaceCech.GradedModule.monMul_commute_apply

Source context 9 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Carrier
variable (R : Type u) [CommRing R] (n : ℕ)
attribute [instance] GradedModule.acg GradedModule.modR
variable {R n}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.monMul_commute_apply (a b : Fin (n + 1) → ℕ) (m : D.M) :
    GradedModule.monMul D a (GradedModule.monMul D b m)
      = GradedModule.monMul D b (GradedModule.monMul D a m)

structure

Frac

L171 ↗

ProjSpaceCech.GradedModule.Frac

Documentation

A homogeneous degree zero fraction whose denominator is supported on the selected chart.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

structure GradedModule.Frac where
  /-- The exponent of each coordinate in the denominator. -/
  denExp : Fin (n + 1) → ℕ
  /-- Coordinates outside the chart occur with exponent zero. -/
  hden : ∀ j ∉ I, denExp j = 0
  /-- The homogeneous numerator. -/
  num : D.M
  /-- The numerator degree equals the total denominator degree. -/
  hnum : num ∈ D.grade (∑ j, (denExp j : ℤ))

theorem

supp_add

L181 ↗

ProjSpaceCech.GradedModule.Frac.supp_add

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.Frac.supp_add {a b : Fin (n + 1) → ℕ}
    (ha : ∀ j ∉ I, a j = 0) (hb : ∀ j ∉ I, b j = 0) :
    ∀ j ∉ I, (a + b) j = 0

def

Rel

L187 ↗

ProjSpaceCech.GradedModule.Frac.Rel

Documentation

Equality of two homogeneous fractions after multiplication by a common denominator.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

def GradedModule.Frac.Rel (x y : GradedModule.Frac D I) : Prop

theorem

refl

L191 ↗

ProjSpaceCech.GradedModule.Frac.Rel.refl

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.Frac.Rel.refl (x : GradedModule.Frac D I) :
    GradedModule.Frac.Rel D I x x

theorem

symm

L195 ↗

ProjSpaceCech.GradedModule.Frac.Rel.symm

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.Frac.Rel.symm {x y : GradedModule.Frac D I}
    (h : GradedModule.Frac.Rel D I x y) : GradedModule.Frac.Rel D I y x

theorem

trans

L200 ↗

ProjSpaceCech.GradedModule.Frac.Rel.trans

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.Frac.Rel.trans {x y z : GradedModule.Frac D I}
    (hxy : GradedModule.Frac.Rel D I x y) (hyz : GradedModule.Frac.Rel D I y z) :
    GradedModule.Frac.Rel D I x z

instance

setoid

L220 ↗

ProjSpaceCech.GradedModule.Frac.setoid

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

instance GradedModule.Frac.setoid : Setoid (GradedModule.Frac D I) where
  r := GradedModule.Frac.Rel D I
  iseqv := ⟨GradedModule.Frac.Rel.refl D I, GradedModule.Frac.Rel.symm D I,
    GradedModule.Frac.Rel.trans D I⟩

def

sec

L226 ↗

ProjSpaceCech.GradedModule.sec

Documentation

Homogeneous degree zero fractions supported on the selected coordinate chart.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

def GradedModule.sec : Type u

def

mk

L229 ↗

ProjSpaceCech.GradedModule.sec.mk

Documentation

The class of a homogeneous fraction in the chart section module.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

def GradedModule.sec.mk (x : GradedModule.Frac D I) : GradedModule.sec D I

theorem

sec_mk_eq

L231 ↗

ProjSpaceCech.GradedModule.sec_mk_eq

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.sec_mk_eq {x y : GradedModule.Frac D I} :
    GradedModule.sec.mk D I x = GradedModule.sec.mk D I y
      ↔ GradedModule.Frac.Rel D I x y

instance

instZero

L236 ↗

ProjSpaceCech.GradedModule.sec.instZero

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

instance GradedModule.sec.instZero : Zero (GradedModule.sec D I)

instance

instAdd

L239 ↗

ProjSpaceCech.GradedModule.sec.instAdd

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

instance GradedModule.sec.instAdd : Add (GradedModule.sec D I) where
  add := Quotient.map₂
    (fun x y => ⟨x.denExp + y.denExp, GradedModule.Frac.supp_add I x.hden y.hden,
      GradedModule.monMul D y.denExp x.num + GradedModule.monMul D x.denExp y.num, by
        have hx := GradedModule.monMul_mem_grade D y.denExp _ x.num x.hnum
        have hy := GradedModule.monMul_mem_grade D x.denExp _ y.num y.hnum
        refine Submodule.add_mem _ ?_ ?_
        · convert hx using 2
          simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]
        · convert hy using 2
          simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]; ring⟩)
    (by
      rintro ⟨a, ha, m, hm⟩ ⟨a', ha', m', hm'⟩ ⟨c, hc, heqc⟩
        ⟨b, hb, p, hp⟩ ⟨b', hb', p', hp'⟩ ⟨c', hc', heqc'⟩
      refine ⟨c + c', GradedModule.Frac.supp_add I hc hc', ?_⟩
      simp only [map_add]
      have key1 : GradedModule.monMul D (c + c' + (a' + b'))
          (GradedModule.monMul D b m)
        = GradedModule.monMul D (c + c' + (a + b)) (GradedModule.monMul D b' m') := by
        rw [← GradedModule.monMul_add_apply, ← GradedModule.monMul_add_apply,
          GradedModule.monMul_congr D (b := c' + b' + b + (c + a'))
            (fun j => by simp only [Pi.add_apply]; omega) m,
          GradedModule.monMul_congr D (b := c' + b' + b + (c + a))
            (fun j => by simp only [Pi.add_apply]; omega) m',
          GradedModule.monMul_add_apply (a := c' + b' + b) (b := c + a'),
          GradedModule.monMul_add_apply (a := c' + b' + b) (b := c + a), heqc]
      have key2 : GradedModule.monMul D (c + c' + (a' + b'))
          (GradedModule.monMul D a p)
        = GradedModule.monMul D (c + c' + (a + b)) (GradedModule.monMul D a' p') := by
        rw [← GradedModule.monMul_add_apply, ← GradedModule.monMul_add_apply,
          GradedModule.monMul_congr D (b := c + a' + a + (c' + b'))
            (fun j => by simp only [Pi.add_apply]; omega) p,
          GradedModule.monMul_congr D (b := c + a' + a + (c' + b))
            (fun j => by simp only [Pi.add_apply]; omega) p',
          GradedModule.monMul_add_apply (a := c + a' + a) (b := c' + b'),
          GradedModule.monMul_add_apply (a := c + a' + a) (b := c' + b), heqc']
      rw [key1, key2])

instance

instNeg

L277 ↗

ProjSpaceCech.GradedModule.sec.instNeg

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

instance GradedModule.sec.instNeg : Neg (GradedModule.sec D I) where
  neg := Quotient.map (fun x => ⟨x.denExp, x.hden, -x.num, by simpa using neg_mem x.hnum⟩)
    (by rintro ⟨a, ha, m, hm⟩ ⟨a', ha', m', hm'⟩ ⟨c, hc, heq⟩;
        exact ⟨c, hc, by simp [map_neg, heq]⟩)

instance

instSMul

L282 ↗

ProjSpaceCech.GradedModule.sec.instSMul

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

instance GradedModule.sec.instSMul : SMul R (GradedModule.sec D I) where
  smul r := Quotient.map (fun x => ⟨x.denExp, x.hden, r • x.num, Submodule.smul_mem _ r x.hnum⟩)
    (by rintro ⟨a, ha, m, hm⟩ ⟨a', ha', m', hm'⟩ ⟨c, hc, heq⟩;
        exact ⟨c, hc, by simp only [map_smul, heq]⟩)

theorem

sec_mk_smul

L287 ↗

ProjSpaceCech.GradedModule.sec_mk_smul

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.sec_mk_smul (r : R) (x : GradedModule.Frac D I) :
    r • GradedModule.sec.mk D I x
      = GradedModule.sec.mk D I
          ⟨x.denExp, x.hden, r • x.num, Submodule.smul_mem _ r x.hnum⟩

theorem

sec_mk_neg

L293 ↗

ProjSpaceCech.GradedModule.sec_mk_neg

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

theorem GradedModule.sec_mk_neg (x : GradedModule.Frac D I) :
    -GradedModule.sec.mk D I x
      = GradedModule.sec.mk D I
          ⟨x.denExp, x.hden, -x.num, by simpa using neg_mem x.hnum⟩ := by
  rfl

theorem

sec_mk_zero_num

L299 ↗

ProjSpaceCech.GradedModule.sec_mk_zero_num

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

theorem GradedModule.sec_mk_zero_num (a : Fin (n + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0) :
    GradedModule.sec.mk D I ⟨a, ha, 0, by simp⟩ = 0 := by
  refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
  simp

theorem

sec_mk_congr

L304 ↗

ProjSpaceCech.GradedModule.sec_mk_congr

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.sec_mk_congr {a a' : Fin (n + 1) → ℕ} (ha : ∀ j ∉ I, a j = 0)
    (ha' : ∀ j ∉ I, a' j = 0) (haa : a = a') {m : D.M} (hm : m ∈ D.grade (∑ j, (a j : ℤ))) :
    GradedModule.sec.mk D I ⟨a, ha, m, hm⟩
      = GradedModule.sec.mk D I ⟨a', ha', m, haa ▸ hm⟩

instance

instAddCommGroup

L310 ↗

ProjSpaceCech.GradedModule.sec.instAddCommGroup

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

instance GradedModule.sec.instAddCommGroup : AddCommGroup (GradedModule.sec D I) where
  add_assoc := by
    rintro ⟨x⟩ ⟨y⟩ ⟨z⟩
    refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp only [zero_add, map_add, ← GradedModule.monMul_add_apply]
    rw [show x.denExp + y.denExp + z.denExp = x.denExp + (y.denExp + z.denExp) from
        add_assoc _ _ _,
      add_assoc]
    refine congrArg₂ (· + ·) ?_ (congrArg₂ (· + ·) ?_ ?_) <;>
      exact GradedModule.monMul_congr D (fun j => congrFun (by abel) j) _
  zero_add := by
    rintro ⟨x⟩
    refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp [GradedModule.monMul_zero]
  add_zero := by
    rintro ⟨x⟩
    refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp [GradedModule.monMul_zero]
  neg_add_cancel := by
    rintro ⟨x⟩
    refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp
  add_comm := by
    rintro ⟨x⟩ ⟨y⟩
    refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    dsimp only
    rw [zero_add, zero_add, show x.denExp + y.denExp = y.denExp + x.denExp from add_comm _ _,
      add_comm (GradedModule.monMul D y.denExp x.num)]
  nsmul := nsmulRec
  zsmul := zsmulRec

instance

instModule

L341 ↗

ProjSpaceCech.GradedModule.sec.instModule

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

instance GradedModule.sec.instModule : Module R (GradedModule.sec D I) where
  one_smul := by
    rintro ⟨x⟩
    exact (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, by simp⟩
  mul_smul r s := by
    rintro ⟨x⟩
    exact (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, by simp [mul_smul]⟩
  smul_zero r := by
    exact (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, by simp⟩
  smul_add r := by
    rintro ⟨x⟩ ⟨y⟩
    exact (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, by simp [smul_add]⟩
  add_smul r s := by
    rintro ⟨x⟩
    refine (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp only [zero_add, map_add, map_smul, ← GradedModule.monMul_add_apply, add_smul]
  zero_smul := by
    rintro ⟨x⟩
    exact (GradedModule.sec_mk_eq D I).mpr ⟨0, fun _ _ => rfl, by simp⟩

theorem

sec_mk_add

L361 ↗

ProjSpaceCech.GradedModule.sec_mk_add

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.sec_mk_add (a : Fin (n + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0)
    {m m' : D.M} (hm : m ∈ D.grade (∑ j, (a j : ℤ))) (hm' : m' ∈ D.grade (∑ j, (a j : ℤ))) :
    GradedModule.sec.mk D I ⟨a, ha, m + m', Submodule.add_mem _ hm hm'⟩
      = GradedModule.sec.mk D I ⟨a, ha, m, hm⟩
        + GradedModule.sec.mk D I ⟨a, ha, m', hm'⟩

def

secMkAt

L370 ↗

ProjSpaceCech.GradedModule.secMkAt

Documentation

The linear map from homogeneous numerators with a fixed denominator to chart sections.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

def GradedModule.secMkAt (a : Fin (n + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0) :
    D.grade (∑ j, (a j : ℤ)) →ₗ[R] GradedModule.sec D I where
  toFun m := GradedModule.sec.mk D I ⟨a, ha, m.1, m.2⟩
  map_add' m m' := GradedModule.sec_mk_add D I a ha m.2 m'.2
  map_smul' r m := by
    simp only [RingHom.id_apply, GradedModule.sec_mk_smul]; rfl

def

secIncl

L378 ↗

ProjSpaceCech.GradedModule.secIncl

Documentation

The restriction of homogeneous fractions along an inclusion of coordinate index sets.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

def GradedModule.secIncl {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J) :
    GradedModule.sec D I →ₗ[R] GradedModule.sec D J where
  toFun := Quotient.map
    (fun x => ⟨x.denExp, fun j hj => x.hden j (fun h => hj (hIJ h)), x.num, x.hnum⟩)
    (fun _ _ ⟨c, hc, heq⟩ => ⟨c, fun j hj => hc j (fun h => hj (hIJ h)), heq⟩)
  map_add' := by
    rintro ⟨x⟩ ⟨y⟩
    exact (GradedModule.sec_mk_eq D J).mpr ⟨0, fun _ _ => rfl, by simp⟩
  map_smul' := by
    rintro r ⟨x⟩
    exact (GradedModule.sec_mk_eq D J).mpr ⟨0, fun _ _ => rfl, by simp⟩

theorem

secIncl_mk

L390 ↗

ProjSpaceCech.GradedModule.secIncl_mk

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · full declaration

theorem GradedModule.secIncl_mk {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J)
    (x : GradedModule.Frac D I) :
    GradedModule.secIncl D hIJ (GradedModule.sec.mk D I x)
      = GradedModule.sec.mk D J
          ⟨x.denExp, fun j hj => x.hden j (fun h => hj (hIJ h)), x.num, x.hnum⟩ := by
  rfl

theorem

secIncl_trans

L397 ↗

ProjSpaceCech.GradedModule.secIncl_trans

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradSec
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n) (I : Finset (Fin (n + 1)))

Lean source · statement

theorem GradedModule.secIncl_trans {I J K : Finset (Fin (n + 1))} (hIJ : I ⊆ J)
    (hJK : J ⊆ K) :
    (GradedModule.secIncl D hJK).comp (GradedModule.secIncl D hIJ)
      = GradedModule.secIncl D (hIJ.trans hJK)

abbrev

cochain

L412 ↗

ProjSpaceCech.GradedModule.cochain

Documentation

Alternating Cech cochains of the graded module on the standard coordinate cover.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

abbrev GradedModule.cochain (i : ℕ) : Type u

def

faceRes

L416 ↗

ProjSpaceCech.GradedModule.faceRes

Documentation

The restriction map from a face chart to its containing Cech chart.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

def GradedModule.faceRes {i : ℕ} (s : Idx n (i + 1)) (j : Fin (i + 2)) :
    GradedModule.sec D (Idx.img n (Idx.face n s j))
      →ₗ[R] GradedModule.sec D (Idx.img n s)

def

d

L422 ↗

ProjSpaceCech.GradedModule.d

Documentation

The alternating sum of face restrictions defining the Cech differential.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

def GradedModule.d (i : ℕ) :
    GradedModule.cochain D i →ₗ[R] GradedModule.cochain D (i + 1)

theorem

d_apply

L427 ↗

ProjSpaceCech.GradedModule.d_apply

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.d_apply (i : ℕ) (f : GradedModule.cochain D i)
    (s : Idx n (i + 1)) :
    GradedModule.d D i f s
      = ∑ j : Fin (i + 2), (-1 : R) ^ (j : ℕ) •
          GradedModule.faceRes D s j (f (Idx.face n s j))

def

H

L436 ↗

ProjSpaceCech.GradedModule.H

Documentation

The kernel in degree zero and the kernel modulo the preceding image in positive degrees.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · full declaration

def GradedModule.H : ℕ → Type u
  | 0 => LinearMap.ker (GradedModule.d D 0)
  | (i + 1) =>
      LinearMap.ker (GradedModule.d D (i + 1)) ⧸
        (LinearMap.range (GradedModule.d D i)).comap
          (LinearMap.ker (GradedModule.d D (i + 1))).subtype

instance

addCommGroup

L443 ↗

ProjSpaceCech.GradedModule.H.addCommGroup

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

instance GradedModule.H.addCommGroup (i : ℕ) : AddCommGroup (GradedModule.H D i)

instance

module

L449 ↗

ProjSpaceCech.GradedModule.H.module

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

instance GradedModule.H.module (i : ℕ) : Module R (GradedModule.H D i)

theorem

subsingleton_cohomology_of_lt

L455 ↗

ProjSpaceCech.GradedModule.subsingleton_cohomology_of_lt

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section GradAltC
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.subsingleton_cohomology_of_lt {i : ℕ} (hi : n < i) :
    Subsingleton (GradedModule.H D i)

theorem

secIncl_irrel

L472 ↗

ProjSpaceCech.GradedModule.secIncl_irrel

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section SecInclIrrel
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)

Lean source · statement

theorem GradedModule.secIncl_irrel {I J : Finset (Fin (n + 1))} (h₁ h₂ : I ⊆ J) :
    GradedModule.secIncl D h₁ = GradedModule.secIncl D h₂

def

freeGrade

L483 ↗

ProjSpaceCech.GradedModule.freeGrade

Documentation

The homogeneous component of the polynomial ring in the indicated integer degree.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)

Lean source · statement

def GradedModule.freeGrade (d : ℤ) : Submodule R (MvPolynomial (Fin (n + 1)) R)

theorem

freeGrade_of_nonneg

L486 ↗

ProjSpaceCech.GradedModule.freeGrade_of_nonneg

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)

Lean source · statement

theorem GradedModule.freeGrade_of_nonneg {d : ℤ} (hd : 0 ≤ d) :
    GradedModule.freeGrade R n d
      = MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R d.toNat

def

freeXMul

L492 ↗

ProjSpaceCech.GradedModule.freeXMul

Documentation

Multiplication by one coordinate variable as a polynomial linear endomorphism.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)

Lean source · full declaration

def GradedModule.freeXMul (j : Fin (n + 1)) :
    MvPolynomial (Fin (n + 1)) R →ₗ[R] MvPolynomial (Fin (n + 1)) R where
  toFun p := X j * p
  map_add' p q := mul_add _ p q
  map_smul' r p := by simp only [RingHom.id_apply]; exact mul_smul_comm r (X j) p

def

free

L499 ↗

ProjSpaceCech.GradedModule.free

Documentation

The graded module of homogeneous polynomials with coordinate multiplication.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)

Lean source · full declaration

def GradedModule.free : GradedModule R n where
  M := MvPolynomial (Fin (n + 1)) R
  grade := GradedModule.freeGrade R n
  xMul := GradedModule.freeXMul R n
  xMul_mem_grade j d m hm := by
    by_cases hd : 0 ≤ d
    · rw [GradedModule.freeGrade_of_nonneg R n hd] at hm
      rw [GradedModule.freeGrade_of_nonneg R n (by omega : (0:ℤ) ≤ d + 1)]
      have hdeg : (d + 1).toNat = 1 + d.toNat := by omega
      rw [hdeg, mem_homogeneousSubmodule]
      exact (isHomogeneous_X R j).mul hm
    · simp only [GradedModule.freeGrade, hd, ite_false, Submodule.mem_bot] at hm
      simp [GradedModule.freeXMul, hm]
  xMul_comm j k := by
    refine LinearMap.ext fun p => ?_
    change (X j : MvPolynomial (Fin (n + 1)) R) * (X k * p) = X k * (X j * p)
    ring

def

shift

L520 ↗

ProjSpaceCech.GradedModule.shift

Documentation

The graded module obtained by shifting all degrees by the specified integer.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · full declaration

def GradedModule.shift (D : GradedModule R n) (d₀ : ℤ) :
    GradedModule R n where
  M := D.M
  grade d := D.grade (d + d₀)
  xMul := D.xMul
  xMul_mem_grade j d m hm := by
    have h := D.xMul_mem_grade j (d + d₀) m hm
    convert h using 2; ring
  xMul_comm := D.xMul_comm

def

pi

L531 ↗

ProjSpaceCech.GradedModule.pi

Documentation

The finite product of graded modules with componentwise grading and coordinate operators.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · full declaration

def GradedModule.pi {ι : Type} [Fintype ι] (D : ι → GradedModule R n) :
    GradedModule R n where
  M := ∀ k, (D k).M
  grade d := Submodule.pi Set.univ (fun k => (D k).grade d)
  xMul j := LinearMap.pi (fun k => (D k).xMul j ∘ₗ LinearMap.proj k)
  xMul_mem_grade j d m hm := by
    intro k _
    exact (D k).xMul_mem_grade j d (m k) (hm k (Set.mem_univ k))
  xMul_comm j k := by
    refine LinearMap.ext fun m => funext fun l => ?_
    exact LinearMap.congr_fun ((D l).xMul_comm j k) (m l)

def

quot

L544 ↗

ProjSpaceCech.GradedModule.quot

Documentation

The graded quotient by a submodule preserved by every coordinate operator.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · full declaration

def GradedModule.quot (D : GradedModule R n) (K : Submodule R D.M)
    (hstab : ∀ j, ∀ m ∈ K, D.xMul j m ∈ K) : GradedModule R n where
  M := D.M ⧸ K
  grade d := (D.grade d).map K.mkQ
  xMul j := K.mapQ K (D.xMul j) (fun m hm => hstab j m hm)
  xMul_mem_grade j d := by
    rintro _ ⟨m, hm, rfl⟩; exact ⟨D.xMul j m, D.xMul_mem_grade j d m hm, rfl⟩
  xMul_comm j k := by
    refine LinearMap.ext fun z => ?_
    obtain ⟨m, rfl⟩ := K.mkQ_surjective z
    exact congrArg K.mkQ (LinearMap.congr_fun (D.xMul_comm j k) m)

theorem

free_monMul_apply

L556 ↗

ProjSpaceCech.GradedModule.free_monMul_apply

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · statement

theorem GradedModule.free_monMul_apply (a : Fin (n + 1) → ℕ)
    (p : MvPolynomial (Fin (n + 1)) R) :
    GradedModule.monMul (GradedModule.free R n) a p = (∏ j, X j ^ a j) * p

theorem

free_monMul_injective

L579 ↗

ProjSpaceCech.GradedModule.free_monMul_injective

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Instances
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · statement

theorem GradedModule.free_monMul_injective (a : Fin (n + 1) → ℕ) :
    Function.Injective (GradedModule.monMul (GradedModule.free R n) a)

abbrev

FD

L604 ↗

ProjSpaceCech.GradedModule.FD

Documentation

The free polynomial graded module shifted by the indicated integer.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section FD
variable (R : Type u) [CommRing R] (n : ℕ)

Lean source · statement

abbrev GradedModule.FD (d₀ : ℤ) : GradedModule R n

theorem

isHomogeneous_prod_X_pow

L609 ↗

ProjSpaceCech.GradedModule.isHomogeneous_prod_X_pow

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section FD
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · statement

theorem GradedModule.isHomogeneous_prod_X_pow (e : Fin (n + 1) → ℕ) :
    (∏ j, (X j : MvPolynomial (Fin (n + 1)) R) ^ e j).IsHomogeneous (∑ j, e j)

theorem

prod_X_pow_mem_freeGrade

L613 ↗

ProjSpaceCech.GradedModule.prod_X_pow_mem_freeGrade

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section FD
variable (R : Type u) [CommRing R] (n : ℕ)
variable {R n}

Lean source · statement

theorem GradedModule.prod_X_pow_mem_freeGrade (e : Fin (n + 1) → ℕ) :
    (∏ j, (X j : MvPolynomial (Fin (n + 1)) R) ^ e j)
      ∈ GradedModule.freeGrade R n (∑ j, (e j : ℤ))

def

sub

L627 ↗

ProjSpaceCech.GradedModule.sub

Documentation

The graded module obtained by intersecting each grade with a coordinate-stable submodule.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section SubMod
variable {R : Type u} [CommRing R] {n : ℕ}

Lean source · full declaration

def GradedModule.sub (D : GradedModule R n) (K : Submodule R D.M)
    (hstab : ∀ j, ∀ m ∈ K, D.xMul j m ∈ K) : GradedModule R n where
  M := D.M
  grade d := D.grade d ⊓ K
  xMul := D.xMul
  xMul_mem_grade j d m hm :=
    ⟨D.xMul_mem_grade j d m hm.1, hstab j m hm.2⟩
  xMul_comm := D.xMul_comm

structure

Hom

L643 ↗

ProjSpaceCech.GradedModule.Hom

Documentation

A linear map preserving grades and commuting with coordinate multiplication.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}

Lean source · full declaration

structure GradedModule.Hom (D₁ D₂ : GradedModule R n) where
  /-- The underlying linear map. -/
  toLinearMap : D₁.M →ₗ[R] D₂.M
  /-- The map preserves every integer grade. -/
  mem_grade : ∀ d m, m ∈ D₁.grade d → toLinearMap m ∈ D₂.grade d
  /-- The map commutes with each coordinate operator. -/
  xMul_comm : ∀ j, toLinearMap ∘ₗ D₁.xMul j = D₂.xMul j ∘ₗ toLinearMap

theorem

map_monMul

L653 ↗

ProjSpaceCech.GradedModule.Hom.map_monMul

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · statement

theorem GradedModule.Hom.map_monMul (φ : GradedModule.Hom D₁ D₂) (a : Fin (n + 1) → ℕ)
    (m : D₁.M) :
    φ.toLinearMap (GradedModule.monMul D₁ a m) = GradedModule.monMul D₂ a (φ.toLinearMap m)

def

secMap

L675 ↗

ProjSpaceCech.GradedModule.Hom.secMap

Documentation

The linear map on fraction sections induced by a graded module homomorphism.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · full declaration

def GradedModule.Hom.secMap (φ : GradedModule.Hom D₁ D₂) (I : Finset (Fin (n + 1))) :
    GradedModule.sec D₁ I →ₗ[R] GradedModule.sec D₂ I where
  toFun := Quotient.map
    (fun x => ⟨x.denExp, x.hden, φ.toLinearMap x.num, φ.mem_grade _ _ x.hnum⟩)
    (fun _ _ ⟨c, hc, heq⟩ => ⟨c, hc, by
      rw [← GradedModule.Hom.map_monMul, ← GradedModule.Hom.map_monMul, heq]⟩)
  map_add' := by
    rintro ⟨x⟩ ⟨y⟩
    refine (GradedModule.sec_mk_eq _ I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp only [zero_add, map_add, GradedModule.Hom.map_monMul]
  map_smul' := by
    rintro r ⟨x⟩
    refine (GradedModule.sec_mk_eq _ I).mpr ⟨0, fun _ _ => rfl, ?_⟩
    simp only [zero_add, map_smul, RingHom.id_apply]

theorem

secMap_incl

L690 ↗

ProjSpaceCech.GradedModule.Hom.secMap_incl

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · statement

theorem GradedModule.Hom.secMap_incl (φ : GradedModule.Hom D₁ D₂)
    {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J) :
    (GradedModule.secIncl D₂ hIJ).comp (GradedModule.Hom.secMap φ I)
      = (GradedModule.Hom.secMap φ J).comp (GradedModule.secIncl D₁ hIJ)

def

cochainMap

L697 ↗

ProjSpaceCech.GradedModule.Hom.cochainMap

Documentation

The componentwise map on Cech cochains induced by a graded module homomorphism.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · statement

def GradedModule.Hom.cochainMap (φ : GradedModule.Hom D₁ D₂) (i : ℕ) :
    GradedModule.cochain D₁ i →ₗ[R] GradedModule.cochain D₂ i

theorem

cochainMap_comm

L702 ↗

ProjSpaceCech.GradedModule.Hom.cochainMap_comm

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · statement

theorem GradedModule.Hom.cochainMap_comm (φ : GradedModule.Hom D₁ D₂) (i : ℕ) :
    (GradedModule.d D₂ i).comp (GradedModule.Hom.cochainMap φ i)
      = (GradedModule.Hom.cochainMap φ (i + 1)).comp (GradedModule.d D₁ i)

def

cochainMapKer

L715 ↗

ProjSpaceCech.GradedModule.Hom.cochainMapKer

Documentation

The restriction of the cochain map to the kernel of the differential.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · statement

def GradedModule.Hom.cochainMapKer (φ : GradedModule.Hom D₁ D₂) (i : ℕ) :
    ↥(LinearMap.ker (GradedModule.d D₁ i))
      →ₗ[R] ↥(LinearMap.ker (GradedModule.d D₂ i))

def

HMap

L724 ↗

ProjSpaceCech.GradedModule.Hom.HMap

Documentation

The induced linear map on the graded module Cech cohomology.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section Hom
variable {R : Type u} [CommRing R] {n : ℕ}
variable {D₁ D₂ : GradedModule R n}

Lean source · full declaration

def GradedModule.Hom.HMap (φ : GradedModule.Hom D₁ D₂) :
    (i : ℕ) → GradedModule.H D₁ i →ₗ[R] GradedModule.H D₂ i
  | 0 => GradedModule.Hom.cochainMapKer φ 0
  | (j + 1) => Submodule.mapQ _ _ (GradedModule.Hom.cochainMapKer φ (j + 1)) fun x hx => by
      obtain ⟨g, hg⟩ := hx
      exact ⟨GradedModule.Hom.cochainMap φ j g, by
        rw [← LinearMap.comp_apply, GradedModule.Hom.cochainMap_comm, LinearMap.comp_apply, hg];
        rfl⟩

structure

Presentation

L740 ↗

ProjSpaceCech.GradedModule.Presentation

Documentation

A finite degreewise surjective presentation by shifted free polynomial graded modules.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}

Lean source · full declaration

structure GradedModule.Presentation (D : GradedModule R n) where
  /-- The index type of the presentation generators. -/
  J : Type
  /-- The finite enumeration of the generator indices. -/
  [fJ : Fintype J]
  /-- The degree shift of each generator. -/
  d₀ : J → ℤ
  /-- The graded homomorphism from the shifted free source. -/
  hom : GradedModule.Hom (GradedModule.pi (fun k => GradedModule.FD R n (d₀ k))) D
  /-- Every homogeneous element lifts to an element of the same degree. -/
  surj : ∀ d, ∀ m ∈ D.grade d,
    ∃ m' ∈ (GradedModule.pi (fun k => GradedModule.FD R n (d₀ k))).grade d,
      hom.toLinearMap m' = m

abbrev

IsFG

L757 ↗

ProjSpaceCech.GradedModule.IsFG

Documentation

Existence of a finite presentation by shifted free polynomial graded modules.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}
attribute [instance] GradedModule.Presentation.fJ

Lean source · statement

abbrev GradedModule.IsFG (D : GradedModule R n) : Prop

abbrev

F

L760 ↗

ProjSpaceCech.GradedModule.Presentation.F

Documentation

The finite product of shifted free graded modules appearing in the presentation.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}
attribute [instance] GradedModule.Presentation.fJ

Lean source · statement

abbrev GradedModule.Presentation.F {D : GradedModule R n} (σ : GradedModule.Presentation D) :
    GradedModule R n

abbrev

K

L765 ↗

ProjSpaceCech.GradedModule.Presentation.K

Documentation

The kernel submodule of the presentation map.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}
attribute [instance] GradedModule.Presentation.fJ

Lean source · statement

abbrev GradedModule.Presentation.K {D : GradedModule R n} (σ : GradedModule.Presentation D) :
    Submodule R σ.F.M

theorem

K_xMul_stable

L768 ↗

ProjSpaceCech.GradedModule.Presentation.K_xMul_stable

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}
attribute [instance] GradedModule.Presentation.fJ

Lean source · statement

theorem GradedModule.Presentation.K_xMul_stable {D : GradedModule R n} (σ :
    GradedModule.Presentation D)
    (j : Fin (n + 1)) : ∀ m ∈ σ.K, σ.F.xMul j m ∈ σ.K

abbrev

ker

L776 ↗

ProjSpaceCech.GradedModule.Presentation.ker

Documentation

The presentation kernel with its induced grading and coordinate multiplication.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}
attribute [instance] GradedModule.Presentation.fJ

Lean source · statement

abbrev GradedModule.Presentation.ker {D : GradedModule R n} (σ : GradedModule.Presentation D) :
    GradedModule R n

def

kerIncl

L781 ↗

ProjSpaceCech.GradedModule.Presentation.kerIncl

Documentation

The graded inclusion of the presentation kernel into its free source.

Source context 7 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section IsFG
variable {R : Type u} [CommRing R] {n : ℕ}
attribute [instance] GradedModule.Presentation.fJ

Lean source · full declaration

def GradedModule.Presentation.kerIncl {D : GradedModule R n} (σ : GradedModule.Presentation D) :
    GradedModule.Hom σ.ker σ.F where
  toLinearMap := LinearMap.id
  mem_grade _ _ hm := hm.1
  xMul_comm _ := rfl

def

shift

L794 ↗

ProjSpaceCech.GradedModule.Hom.shift

Documentation

The same graded homomorphism after shifting both source and target degrees.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section HomShift
variable {R : Type u} [CommRing R] {n : ℕ} {D₁ D₂ : GradedModule R n}

Lean source · full declaration

def GradedModule.Hom.shift (φ : GradedModule.Hom D₁ D₂) (d₀ : ℤ) :
    GradedModule.Hom (GradedModule.shift D₁ d₀) (GradedModule.shift D₂ d₀) where
  toLinearMap := φ.toLinearMap
  mem_grade d m hm := φ.mem_grade (d + d₀) m hm
  xMul_comm j := φ.xMul_comm j

theorem

shift_toLinearMap

L800 ↗

ProjSpaceCech.GradedModule.Hom.shift_toLinearMap

Source context 6 commands

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

noncomputable section
universe u
open Finset Function MvPolynomial
namespace ProjSpaceCech
section HomShift
variable {R : Type u} [CommRing R] {n : ℕ} {D₁ D₂ : GradedModule R n}

Lean source · statement

theorem GradedModule.Hom.shift_toLinearMap (φ : GradedModule.Hom D₁ D₂) (d₀ : ℤ) :
    (φ.shift d₀).toLinearMap = φ.toLinearMap

Module documentation

Declarations