NYLL
Module

OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
14 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf nonempty cech Equiv of Modules of iso

Imports1
Imported by11

Declarations

structure

LinIso

L42 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.LinIso
Documentation

A family of linear equivalences on sections commuting with restriction.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · full declaration
structure LinIso (F G : OModulePresheaf π) where
  /-- The linear equivalence on the sections of each open. -/
  app : ∀ U : V.Opens, F.obj U ≃ₗ[R] G.obj U
  /-- The section equivalences commute with restriction maps. -/
  res_app : ∀ {U U' : V.Opens} (h : U ≤ U') (x : F.obj U'), G.res h (app U' x) = app U (F.res h x)
def

cochainEquiv

L51 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.cochainEquiv
Documentation

The pointwise linear equivalence induced on the ordered-cover cochains.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
def cochainEquiv (i : ℕ) : F.cochain K i ≃ₗ[R] G.cochain K i
theorem

cochainEquiv_apply

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.cochainEquiv_apply
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
theorem cochainEquiv_apply (i : ℕ) (c : F.cochain K i) (s : K.Idx i) :
    cochainEquiv φ K i c s = φ.app (K.inter s) (c s)
theorem

d_cochainEquiv

L57 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.d_cochainEquiv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
theorem d_cochainEquiv (i : ℕ) (c : F.cochain K i) :
    G.d K i (cochainEquiv φ K i c) = cochainEquiv φ K (i + 1) (F.d K i c)
theorem

d_comp_cochainEquiv

L64 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.d_comp_cochainEquiv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
theorem d_comp_cochainEquiv (i : ℕ) :
    G.d K i ∘ₗ (cochainEquiv φ K i).toLinearMap = (cochainEquiv φ K (i + 1)).toLinearMap ∘ₗ F.d
      K i
theorem

map_ker

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.map_ker
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
theorem map_ker (i : ℕ) :
    Submodule.map (cochainEquiv φ K i).toLinearMap (LinearMap.ker (F.d K i)) = LinearMap.ker
      (G.d K i)
def

H0Equiv

L84 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.H0Equiv
Documentation

The induced linear equivalence on degree-zero cohomology.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
def H0Equiv : F.H0 K ≃ₗ[R] G.H0 K
def

kerEquiv

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.kerEquiv
Documentation

The linear equivalence on the kernels of corresponding Čech differentials.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
def kerEquiv (i : ℕ) : LinearMap.ker (F.d K (i + 1)) ≃ₗ[R] LinearMap.ker (G.d K (i + 1))
theorem

kerEquiv_apply_coe

L91 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.kerEquiv_apply_coe
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
theorem kerEquiv_apply_coe (i : ℕ) (x : LinearMap.ker (F.d K (i + 1))) :
    ((kerEquiv φ K i x : LinearMap.ker (G.d K (i + 1))) : G.cochain K (i + 1)) = cochainEquiv φ
      K (i + 1) x
theorem

map_boundaries

L95 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.map_boundaries
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
theorem map_boundaries (i : ℕ) :
    Submodule.map (kerEquiv φ K i).toLinearMap
        ((LinearMap.range (F.d K i)).comap (LinearMap.ker (F.d K (i + 1))).subtype)
      = (LinearMap.range (G.d K i)).comap (LinearMap.ker (G.d K (i + 1))).subtype
def

HSuccEquiv

L116 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.HSuccEquiv
Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · statement
def HSuccEquiv (i : ℕ) : F.HSucc K i ≃ₗ[R] G.HSucc K i
theorem

cechFinite_iff

L119 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.cechFinite_iff
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
include φ in
Lean source · statement
theorem cechFinite_iff : F.CechFinite K ↔ G.CechFinite K
def

ofIso

L127 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso.AlgebraicGeometry.OModulePresheaf.IsoTransfer.ofIso
Documentation

The restriction-compatible linear equivalences induced by an isomorphism of scheme modules.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
namespace IsoTransfer
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable {F G : OModulePresheaf π} (φ : LinIso F G) (K : V.OrderedAffineCover)
Lean source · full declaration
def ofIso {M M' : V.Modules} (e : M ≅ M') : LinIso (ofModules π M) (ofModules π M') where
  app U :=
    { toFun := fun x => (e.hom.app U).hom x
      invFun := fun y => (e.inv.app U).hom y
      map_add' := fun x y => (e.hom.app U).hom.map_add x y
      map_smul' := fun r x => by
        exact (congrArg (fun y : (ofModules π M).obj U => (e.hom.app U).hom y)
          (ofModules_algebraMap_smul π M U r x)).trans
          ((Scheme.Modules.Hom.app_smul e.hom
            ((Scheme.TwoAffineOpenCover.algebraOfHom π U).algebraMap r)
            (show Γ(M, U) from x)).trans
            (ofModules_algebraMap_smul π M' U r
              (show (ofModules π M').obj U from (e.hom.app U).hom x)).symm)
      left_inv := fun x => by
        change (e.hom.app U ≫ e.inv.app U).hom x = x
        rw [← Scheme.Modules.Hom.comp_app, e.hom_inv_id, Scheme.Modules.Hom.id_app]; rfl
      right_inv := fun y => by
        change (e.inv.app U ≫ e.hom.app U).hom y = y
        rw [← Scheme.Modules.Hom.comp_app, e.inv_hom_id, Scheme.Modules.Hom.id_app]; rfl }
  res_app {U U'} h x := by
    change (M'.presheaf.map (homOfLE h).op) ((e.hom.app U').hom x) = (e.hom.app U).hom
      ((M.presheaf.map (homOfLE h).op) x)
    have hnat := e.hom.mapPresheaf.naturality (homOfLE h).op
    have hx := ConcreteCategory.congr_hom hnat x
    simp only [Scheme.Modules.mapPresheaf_app] at hx
    exact hx.symm
theorem

nonempty_cechEquiv_ofModules_of_iso

L158 ↗
AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_ofModules_of_iso
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_ofModules_of_iso
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open AlgebraicGeometry.OModulePresheaf.IsoTransfer in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_ofModules_of_iso
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) {M M' : V.Modules} (e : M
      ≅ M')
    (K : V.OrderedAffineCover) :
    Nonempty ((OModulePresheaf.ofModules π M).H0 K ≃ₗ[R] (OModulePresheaf.ofModules π M').H0 K) ∧
      (∀ i : ℕ, Nonempty ((OModulePresheaf.ofModules π M).HSucc K i ≃ₗ[R]
        (OModulePresheaf.ofModules π M').HSucc K i)) ∧
      ((OModulePresheaf.ofModules π M).CechFinite K ↔ (OModulePresheaf.ofModules π
        M').CechFinite K)

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