Module

ProjSpaceCech_GradedModule_HMap_bijective_of_cochainMap_bijective.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_HMap_bijective_of_cochainMap_bijective

2 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Graded Module HMap bijective of cochain Map bijective

Imports2

Imported by3

theorem

HMap_bijective_of_cochainMap_bijective'

L42 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjectiveGradedHMapBijective.ProjSpaceCech.GradedModule.HMap_bijective_of_cochainMap_bijective'

Source context 11 commands

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

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

Lean source · statement

theorem GradedModule.HMap_bijective_of_cochainMap_bijective' (φ : GradedModule.Hom D₁ D₂)
    (h : ∀ i, Function.Bijective (GradedModule.Hom.cochainMap φ i)) (i : ℕ) :
    Function.Bijective (GradedModule.Hom.HMap φ i)

theorem

HMap_bijective_of_cochainMap_bijective

L92 ↗

ProjSpaceCech.GradedModule.HMap_bijective_of_cochainMap_bijective

Source context 5 commands