Module

ProjSpaceCech_GradedModule_Hom_secMap_bijective_of_saturated.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_secMap_bijective_of_saturated

4 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Graded Module Hom sec Map bijective of saturated

Imports3

Imported by2

theorem

secMap_mk

L45 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective.ProjSpaceCech.GradedModule.Hom.secMap_mk

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SecMapSat
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.secMap_mk (φ : GradedModule.Hom D₁ D₂) (I : Finset (Fin (n + 1)))
    (x : GradedModule.Frac D₁ I) :
    GradedModule.Hom.secMap φ I (GradedModule.sec.mk D₁ I x)
      = GradedModule.sec.mk D₂ I ⟨x.denExp, x.hden, φ.toLinearMap x.num, φ.mem_grade _ _ x.hnum⟩

theorem

secMap_surjective_of_saturated

L52 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective.ProjSpaceCech.GradedModule.Hom.secMap_surjective_of_saturated

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SecMapSat
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.secMap_surjective_of_saturated (φ : GradedModule.Hom D₁ D₂)
    (hsat : ∀ (j : Fin (n + 1)) (e : ℤ), ∀ m ∈ D₂.grade e,
      ∃ k : ℕ, ∃ m' ∈ D₁.grade (e + k), φ.toLinearMap m' = (D₂.xMul j ^ k) m)
    (I : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    Function.Surjective (GradedModule.Hom.secMap φ I)

theorem

secMap_bijective_of_saturated'

L79 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective.ProjSpaceCech.GradedModule.Hom.secMap_bijective_of_saturated'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SecMapSat
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.secMap_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 : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    Function.Bijective (GradedModule.Hom.secMap φ I)

theorem

secMap_bijective_of_saturated

L92 ↗

ProjSpaceCech.GradedModule.Hom.secMap_bijective_of_saturated

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedSecMapBijective
universe u
noncomputable section
open Finset Function MvPolynomial

Lean source · statement

theorem _root_.ProjSpaceCech.GradedModule.Hom.secMap_bijective_of_saturated {R : Type u}
  [CommRing R] {n : ℕ} {D₁ D₂ : ProjSpaceCech.GradedModule R n} (φ :
  ProjSpaceCech.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 : Finset (Fin (n + 1))) (hI : I.Nonempty) :
    Function.Bijective (ProjSpaceCech.GradedModule.Hom.secMap φ I)

Module documentation

Proj Space Cech Graded Module Hom sec Map bijective of saturated

Declarations

secMap_mk

secMap_surjective_of_saturated

secMap_bijective_of_saturated'

secMap_bijective_of_saturated