Module

ProjSpaceCech_GradedModule_Hom_secMap_injective.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Hom_secMap_injective

3 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Graded Module Hom sec Map injective

Imports2

Imported by3

theorem

secMap_mk

L44 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Hom_secMap_injective.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.ProjSpaceCech_GradedModule_Hom_secMap_injective
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SecMapInj
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_injective'

L51 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Hom_secMap_injective.ProjSpaceCech.GradedModule.Hom.secMap_injective'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_Hom_secMap_injective
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SecMapInj
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_injective' (φ : GradedModule.Hom D₁ D₂)
    (hinj : Function.Injective φ.toLinearMap) (I : Finset (Fin (n + 1))) :
    Function.Injective (GradedModule.Hom.secMap φ I)

theorem

secMap_injective

L70 ↗

ProjSpaceCech.GradedModule.Hom.secMap_injective

Source context 5 commands

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

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

Lean source · statement

theorem _root_.ProjSpaceCech.GradedModule.Hom.secMap_injective {R : Type u} [CommRing R] {n : ℕ}
  {D₁ D₂ : ProjSpaceCech.GradedModule R n} (φ : ProjSpaceCech.GradedModule.Hom D₁ D₂)
    (hinj : Function.Injective φ.toLinearMap) (I : Finset (Fin (n + 1))) :
    Function.Injective (ProjSpaceCech.GradedModule.Hom.secMap φ I)

Module documentation

Proj Space Cech Graded Module Hom sec Map injective

Declarations

secMap_mk

secMap_injective'

secMap_injective