NYLL
Module

OModulePresheaf_AffHom_nonempty_H0_equiv_and_HSucc_equiv_of_bijective.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_AffHom_nonempty_H0_equiv_and_HSucc_equiv_of_bijective
11 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf Aff Hom nonempty H0 equiv and HSucc equiv of bijective

Imports1
Imported by8

Declarations

theorem

cochainMap_bijective

L37 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.cochainMap_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
include hφ in
Lean source · statement
theorem cochainMap_bijective (i : ℕ) : Function.Bijective (φ.cochainMap K i)
def

cochainEquiv

L46 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.cochainEquiv
Documentation

The cochain equivalence induced by the given sectionwise bijective morphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
def cochainEquiv (i : ℕ) : F.cochain K i ≃ₗ[R] G.cochain K i
theorem

cochainEquiv_apply

L49 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.cochainEquiv_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
theorem cochainEquiv_apply (i : ℕ) (x : F.cochain K i) : cochainEquiv φ hφ K i x = φ.cochainMap K
  i x
theorem

d_cochainEquiv

L52 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.d_cochainEquiv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
theorem d_cochainEquiv (i : ℕ) (x : F.cochain K i) :
    G.d K i (cochainEquiv φ hφ K i x) = cochainEquiv φ hφ K (i + 1) (F.d K i x)
theorem

map_ker

L57 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.map_ker
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
theorem map_ker (i : ℕ) :
    (LinearMap.ker (F.d K i)).map (cochainEquiv φ hφ K i : F.cochain K i →ₗ[R] G.cochain K i) =
      LinearMap.ker (G.d K i)
def

kerEquiv

L71 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.kerEquiv
Documentation

The induced equivalence of cocycle modules.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
def kerEquiv (i : ℕ) : LinearMap.ker (F.d K i) ≃ₗ[R] LinearMap.ker (G.d K i)
theorem

kerEquiv_coe

L74 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.kerEquiv_coe
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
theorem kerEquiv_coe (i : ℕ) (x : LinearMap.ker (F.d K i)) :
    (kerEquiv φ hφ K i x : G.cochain K i) = φ.cochainMap K i x
theorem

map_bdry

L77 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.map_bdry
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
theorem map_bdry (i : ℕ) :
    ((LinearMap.range (F.d K i)).comap (LinearMap.ker (F.d K (i + 1))).subtype).map
        (kerEquiv φ hφ K (i + 1) : LinearMap.ker (F.d K (i + 1)) →ₗ[R] LinearMap.ker (G.d K (i +
          1))) =
      (LinearMap.range (G.d K i)).comap (LinearMap.ker (G.d K (i + 1))).subtype
def

HSuccEquiv

L99 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.HSuccEquiv
Documentation

The induced linear equivalence on positive-degree Čech cohomology.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
Lean source · statement
def HSuccEquiv (i : ℕ) : F.HSucc K i ≃ₗ[R] G.HSucc K i
theorem

main

L103 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv.P2mCechIso.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechIso
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable {F G : OModulePresheaf π} (φ : AffHom F G) (hφ : ∀ U : V.affineOpens, Function.Bijective
  (φ.app U))
variable (K : V.OrderedAffineCover)
include φ hφ in
Lean source · statement
theorem main :
    Nonempty (F.H0 K ≃ₗ[R] G.H0 K) ∧ ∀ i : ℕ, Nonempty (F.HSucc K i ≃ₗ[R] G.HSucc K i)
theorem

nonempty_H0_equiv_and_HSucc_equiv_of_bijective

L109 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.nonempty_H0_equiv_and_HSucc_equiv_of_bijective
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffHomCohomologyEquiv
universe u
open CategoryTheory AlgebraicGeometry
Lean source · statement
theorem
  _root_.AlgebraicGeometry.OModulePresheaf.AffHom.nonempty_H0_equiv_and_HSucc_equiv_of_bijective
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
    {F G : OModulePresheaf π} (φ : OModulePresheaf.AffHom F G)
    (hφ : ∀ U : V.affineOpens, Function.Bijective (φ.app U)) (K : V.OrderedAffineCover) :
    Nonempty (F.H0 K ≃ₗ[R] G.H0 K) ∧ ∀ i : ℕ, Nonempty (F.HSucc K i ≃ₗ[R] G.HSucc K i)

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