Module

ProjSpaceCech_GradedModule_Hom_HMap_bijective_of_saturated.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_HMap_bijective_of_saturated

2 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Graded Module Hom HMap bijective of saturated

Imports4

Imported by3

theorem

HMap_bijective_of_saturated'

L47 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjectiveGradedHomHMapBijective.ProjSpaceCech.GradedModule.Hom.HMap_bijective_of_saturated'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjectiveGradedHomHMapBijective
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HMapSat
variable {R : Type u} [CommRing R] {n : ℕ} {D₁ D₂ : GradedModule R n}
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Hom in

Lean source · statement

theorem GradedModule.Hom.HMap_bijective_of_saturated' (φ : GradedModule.Hom D₁ D₂)
    (hinj : Function.Injective φ.toLinearMap)
    (hsat : ∀ (j : Fin (n + 1)) (e : ℤ), ∀ m ∈ D₂.grade e,
      ∃ k : ℕ, ∃ m' ∈ D₁.grade (e + k), φ.toLinearMap m' = (D₂.xMul j ^ k) m) (i : ℕ) :
    Function.Bijective (GradedModule.Hom.HMap φ i)

theorem

HMap_bijective_of_saturated

L59 ↗

ProjSpaceCech.GradedModule.Hom.HMap_bijective_of_saturated

Source context 5 commands