NYLL
Module

ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
22 declarations indexed from sourceView source ↗

Module documentation

Equivalence between twist Cech cohomology and cohomology of the corresponding shifted free module.

Imports3
Imported by3

Declarations

theorem

toNat_sub_neg_toNat

L44 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.toNat_sub_neg_toNat
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.toNat_sub_neg_toNat (b : ℤ) :
    ((b.toNat : ℤ) - ((-b).toNat : ℤ)) = b
def

Xprod

L50 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.Xprod
Documentation

The product of coordinate variables with the prescribed nonnegative exponents.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.Xprod (e : Fin (n + 1) → ℕ) : MvPolynomial (Fin (n + 1)) R
theorem

Xprod_mem_freeGrade

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.Xprod_mem_freeGrade
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.Xprod_mem_freeGrade (e : Fin (n + 1) → ℕ) {d : ℤ}
    (hd : d = ∑ j, (e j : ℤ)) :
    (GradedModule.Xprod (R := R) e) ∈ GradedModule.freeGrade R n d
def

twistFrac

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.twistFrac
Documentation

The homogeneous fraction representing the specified Laurent monomial in the shifted free module.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
def GradedModule.twistFrac {I : Finset (Fin (n + 1))}
    (b : Twist.Mon n d₀ I) : GradedModule.Frac (GradedModule.FD R n d₀) I where
  denExp j := (- b.1 j).toNat
  hden j hj := by
    have hbj : 0 ≤ b.1 j := by
      by_contra h; exact hj (b.2.2 ((Twist.mem_negSupp n).mpr (not_le.mp h)))
    omega
  num := GradedModule.Xprod (R := R) (fun j => (b.1 j).toNat)
  hnum := by
    refine GradedModule.Xprod_mem_freeGrade _ ?_
    have hb := b.2.1
    have hsum : ∑ j, (((b.1 j).toNat : ℤ) - (((- b.1 j).toNat : ℤ))) = d₀ := by
      simp_rw [GradedModule.toNat_sub_neg_toNat]; exact hb
    rw [Finset.sum_sub_distrib] at hsum
    linarith
def

twistToGradSec

L81 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.twistToGradSec
Documentation

The linear map from monomial twist sections to homogeneous fraction sections.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.twistToGradSec (I : Finset (Fin (n + 1))) :
    Twist.Sec R n d₀ I →ₗ[R] GradedModule.sec (GradedModule.FD R n d₀) I
theorem

twistToGradSec_single

L87 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.twistToGradSec_single
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.twistToGradSec_single (I : Finset (Fin (n + 1)))
    (b : Twist.Mon n d₀ I) (r : R) :
    GradedModule.twistToGradSec d₀ I (Finsupp.single b r)
      = r • GradedModule.sec.mk _ I (GradedModule.twistFrac d₀ b)
theorem

twistToGradSec_incl

L94 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.twistToGradSec_incl
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.twistToGradSec_incl {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J) :
    (GradedModule.secIncl (GradedModule.FD R n d₀) hIJ).comp
        (GradedModule.twistToGradSec d₀ I)
      = (GradedModule.twistToGradSec d₀ J).comp
          (Finsupp.lmapDomain R R (Twist.Mon.incl n d₀ hIJ))
theorem

sec_mk_enlarge

L107 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.sec_mk_enlarge
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.sec_mk_enlarge (I : Finset (Fin (n + 1)))
    (x : GradedModule.Frac (GradedModule.FD R n d₀) I) (c : Fin (n + 1) → ℕ)
    (hc : ∀ j ∉ I, c j = 0) :
    GradedModule.sec.mk _ I x
      = GradedModule.sec.mk _ I
          ⟨c + x.denExp, GradedModule.Frac.supp_add I hc x.hden,
            GradedModule.monMul _ c x.num, by
              have h := GradedModule.monMul_mem_grade (GradedModule.FD R n d₀) c _ x.num x.hnum
              convert h using 2
              simp only [Pi.add_apply, Nat.cast_add, Finset.sum_add_distrib]; ring⟩ := by
  refine (GradedModule.sec_mk_eq _ I).mpr ⟨0, fun _ _ => rfl, ?_⟩
  simp only [zero_add, ← GradedModule.monMul_add_apply]
  exact GradedModule.monMul_congr _ (fun j => by simp [add_comm]) _
theorem

FD_monMul_apply

L122 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.FD_monMul_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.FD_monMul_apply (c : Fin (n + 1) → ℕ)
    (p : MvPolynomial (Fin (n + 1)) R) :
    GradedModule.monMul (GradedModule.FD R n d₀) c p
      = (∏ j, X j ^ c j) * p
theorem

Xprod_mul

L129 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.Xprod_mul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.Xprod_mul (c e : Fin (n + 1) → ℕ) :
    (GradedModule.Xprod (R := R) c) * (GradedModule.Xprod e)
      = GradedModule.Xprod (c + e)
theorem

coeff_Xprod

L137 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.coeff_Xprod
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · full declaration
theorem GradedModule.coeff_Xprod (e : Fin (n + 1) → ℕ) (s : Fin (n + 1) →₀ ℕ) :
    (GradedModule.Xprod (R := R) e).coeff s
      = if s = ∑ j, Finsupp.single j (e j) then 1 else 0 := by
  unfold GradedModule.Xprod
  rw [show (∏ j, (X j : MvPolynomial (Fin (n+1)) R) ^ e j)
      = MvPolynomial.monomial (∑ j, Finsupp.single j (e j)) 1 from by
    rw [MvPolynomial.monomial_sum_one]
    exact Finset.prod_congr rfl fun j _ => MvPolynomial.X_pow_eq_monomial,
    MvPolynomial.coeff_monomial]
  simp only [eq_comm]
theorem

sec_mk_Xprod_eq_twistFrac

L149 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.sec_mk_Xprod_eq_twistFrac
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.sec_mk_Xprod_eq_twistFrac (I : Finset (Fin (n + 1)))
    (a e : Fin (n + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0)
    (hdeg : (GradedModule.Xprod (R := R) e) ∈ (GradedModule.FD R n d₀).grade (∑ j, (a j : ℤ)))
    (b : Twist.Mon n d₀ I) (hb : ∀ j, b.1 j = (e j : ℤ) - (a j : ℤ)) :
    GradedModule.sec.mk (GradedModule.FD R n d₀) I ⟨a, ha, GradedModule.Xprod e, hdeg⟩
      = GradedModule.sec.mk _ I (GradedModule.twistFrac d₀ b)
theorem

secMkAt_FD_injective

L164 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.secMkAt_FD_injective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.secMkAt_FD_injective (I : Finset (Fin (n + 1)))
    (a : Fin (n + 1) → ℕ) (ha : ∀ j ∉ I, a j = 0) :
    Function.Injective (GradedModule.secMkAt (GradedModule.FD R n d₀) I a ha)
theorem

twistToGradSec_injective

L179 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.twistToGradSec_injective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.twistToGradSec_injective (I : Finset (Fin (n + 1))) :
    Function.Injective (GradedModule.twistToGradSec (R := R) (n := n) d₀ I)
theorem

twistToGradSec_surjective

L256 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.twistToGradSec_surjective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.twistToGradSec_surjective (I : Finset (Fin (n + 1))) :
    Function.Surjective (GradedModule.twistToGradSec (R := R) (n := n) d₀ I)
def

secTwistEquiv

L316 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.secTwistEquiv
Documentation

The equivalence between twist sections and fraction sections of the shifted free graded module.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.secTwistEquiv (I : Finset (Fin (n + 1))) :
    Twist.Sec R n d₀ I ≃ₗ[R] GradedModule.sec (GradedModule.FD R n d₀) I
def

cochainTwistEquiv

L324 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.cochainTwistEquiv
Documentation

The componentwise equivalence between twist cochains and shifted free module cochains.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.cochainTwistEquiv (i : ℕ) :
    Twist.cochain R n d₀ i
      ≃ₗ[R] GradedModule.cochain (GradedModule.FD R n d₀) i
theorem

cochainTwistEquiv_comm

L330 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.cochainTwistEquiv_comm
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainTwistEquiv_comm (i : ℕ) :
    (GradedModule.d (GradedModule.FD R n d₀) i).comp
        (GradedModule.cochainTwistEquiv (R := R) (n := n) d₀ i).toLinearMap
      = (GradedModule.cochainTwistEquiv (R := R) (n := n) d₀ (i + 1)).toLinearMap.comp
          (Twist.d R n d₀ i)
theorem

cochainTwistEquiv_ker

L349 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.cochainTwistEquiv_ker
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainTwistEquiv_ker (k : ℕ) :
    (LinearMap.ker (Twist.d R n d₀ k)).map
        (GradedModule.cochainTwistEquiv (R := R) (n := n) d₀ k).toLinearMap
      = LinearMap.ker (GradedModule.d (GradedModule.FD R n d₀) k)
theorem

cochainTwistEquiv_range

L362 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.cochainTwistEquiv_range
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.cochainTwistEquiv_range (k : ℕ) :
    (LinearMap.range (Twist.d R n d₀ k)).map
        (GradedModule.cochainTwistEquiv (R := R) (n := n) d₀ (k + 1)).toLinearMap
      = LinearMap.range (GradedModule.d (GradedModule.FD R n d₀) k)
def

HTwistEquiv

L372 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD.ProjSpaceCech.GradedModule.HTwistEquiv
Documentation

The cohomology equivalence induced by the compatible twist cochain equivalences.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Bridge
variable {R : Type u} [CommRing R] {n : ℕ}
variable (d₀ : ℤ)
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.HTwistEquiv (i : ℕ) :
    Twist.H R n d₀ i ≃ₗ[R] GradedModule.H (GradedModule.FD R n d₀) i
theorem

nonempty_HEquiv_FD

L408 ↗
ProjSpaceCech.GradedModule.nonempty_HEquiv_FD
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_nonempty_HEquiv_FD
universe u
noncomputable section
open Finset Function MvPolynomial
Lean source · statement
theorem _root_.ProjSpaceCech.GradedModule.nonempty_HEquiv_FD (R : Type u) [CommRing R] (n : ℕ) (d₀
    : ℤ) (i : ℕ) :
    Nonempty (ProjSpaceCech.Twist.H R n d₀ i ≃ₗ[R] ProjSpaceCech.GradedModule.H
      (ProjSpaceCech.GradedModule.FD R n d₀) i)

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