NYLL
Module

OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
20 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf cech Finrank of Modules pullback eq of is Iso

Imports11
Imported by2

Declarations

theorem

cechEquiv_of_affHom_inverse

L55 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.cechEquiv_of_affHom_inverse
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
Lean source · statement
theorem cechEquiv_of_affHom_inverse
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)} [IsSeparated π]
    {F G : OModulePresheaf π} (φ : AffHom F G) (ψ : AffHom G F)
    (h₁ : ∀ (U : V.affineOpens) (x : F.obj U.1), ψ.app U (φ.app U x) = x)
    (h₂ : ∀ (U : V.affineOpens) (y : G.obj U.1), φ.app U (ψ.app U y) = y)
    (K : V.OrderedAffineCover) :
    Nonempty (F.H0 K ≃ₗ[R] G.H0 K) ∧ ∀ i : ℕ, Nonempty (F.HSucc K i ≃ₗ[R] G.HSucc K i)
abbrev

eU

L93 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.eU
Documentation

The pullback homomorphism on sections over an open subset.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
abbrev eU (U : P'.Opens) : Γ(P', U) →+* Γ(P, Φ ⁻¹ᵁ U)
theorem

eU_eq

L96 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.eU_eq
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
omit [IsIso Φ] in
Lean source · statement
theorem eU_eq (U : P'.Opens) : eU Φ U = (Φ.app U).hom
theorem

eU_bijective

L100 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.eU_bijective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
theorem eU_bijective (U : P'.Opens) : Function.Bijective (eU Φ U)
def

eEquiv

L105 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.eEquiv
Documentation

The section ring equivalence induced by the scheme isomorphism.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
def eEquiv (U : P'.Opens) : Γ(P', U) ≃+* Γ(P, Φ ⁻¹ᵁ U)
theorem

pf_smul

L109 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.pf_smul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
omit [IsIso Φ] in
Lean source · full declaration
theorem pf_smul (U : P'.Opens) (a : Γ(P', U)) (b : (OModulePresheaf.pushforwardUnit π' Φ).obj U) :
    a • b = (show (OModulePresheaf.pushforwardUnit π' Φ).obj U from eU Φ U a * (show Γ(P, Φ ⁻¹ᵁ U)
      from b)) := rfl
def

onePf

L114 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.onePf
Documentation

The unit section of the pushed forward structure sheaf.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
def onePf (U : P'.Opens) : (OModulePresheaf.pushforwardUnit π' Φ).obj U
theorem

eU_mul_onePf

L117 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.eU_mul_onePf
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
omit [IsIso Φ] in
Lean source · statement
theorem eU_mul_onePf (U : P'.Opens) (a : (P'.presheaf.obj (Opposite.op U))) :
    a • onePf π' Φ U = (eU Φ U a : (OModulePresheaf.pushforwardUnit π' Φ).obj U)
def

fwd

L123 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.fwd
Documentation

Send a module section to its tensor product with the unit section.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
def fwd (U : P'.Opens) :
    (OModulePresheaf.ofModules π' N).obj U →ₗ[R] ((OModulePresheaf.pushforwardUnit π' Φ).twist
      N).obj U
theorem

fwd_apply

L138 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.fwd_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
omit [IsIso Φ] in
Lean source · statement
theorem fwd_apply (U : P'.Opens) (m : (OModulePresheaf.ofModules π' N).obj U) :
    fwd π' Φ N U m = (onePf π' Φ U ⊗ₜ[(P'.presheaf.obj (Opposite.op U))] m :
      ((OModulePresheaf.pushforwardUnit π' Φ).twist N).obj U)
theorem

fwd_smul_sections

L143 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.fwd_smul_sections
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
omit [IsIso Φ] in
Lean source · statement
theorem fwd_smul_sections (U : P'.Opens) (a : (P'.presheaf.obj (Opposite.op U))) (m :
  (OModulePresheaf.ofModules π' N).obj U) :
    fwd π' Φ N U (a • m) = a • fwd π' Φ N U m
def

bwdBil

L150 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.bwdBil
Documentation

Evaluate a pushed forward section through the inverse section ring map.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
def bwdBil (U : P'.Opens) :
    (OModulePresheaf.pushforwardUnit π' Φ).obj U →ₗ[(P'.presheaf.obj (Opposite.op U))]
      ((OModulePresheaf.ofModules π' N).obj U →ₗ[(P'.presheaf.obj (Opposite.op U))]
        (OModulePresheaf.ofModules π' N).obj U)
def

bwd

L170 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.bwd
Documentation

Contract the structure sheaf tensor factor through the section ring equivalence.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
def bwd (U : P'.Opens) :
    ((OModulePresheaf.pushforwardUnit π' Φ).twist N).obj U →ₗ[R] (OModulePresheaf.ofModules π'
      N).obj U
theorem

bwd_tmul

L184 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.bwd_tmul
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
theorem bwd_tmul (U : P'.Opens) (b : (OModulePresheaf.pushforwardUnit π' Φ).obj U) (m :
  (OModulePresheaf.ofModules π' N).obj U) :
    bwd π' Φ N U (b ⊗ₜ[(P'.presheaf.obj (Opposite.op U))] m : ((OModulePresheaf.pushforwardUnit π'
      Φ).twist N).obj U) =
      ((eEquiv Φ U).symm b) • m
theorem

bwd_fwd

L192 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.bwd_fwd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
theorem bwd_fwd (U : P'.Opens) (m : (OModulePresheaf.ofModules π' N).obj U) : bwd π' Φ N U (fwd π'
  Φ N U m) = m
theorem

fwd_bwd

L198 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.fwd_bwd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · statement
theorem fwd_bwd (U : P'.Opens) (t : ((OModulePresheaf.pushforwardUnit π' Φ).twist N).obj U) :
    fwd π' Φ N U (bwd π' Φ N U t) = t
def

fwdHom

L214 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.fwdHom
Documentation

The affine presheaf morphism given by tensoring with the unit.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · full declaration
def fwdHom : AffHom (OModulePresheaf.ofModules π' N)
  ((OModulePresheaf.pushforwardUnit π' Φ).twist N) where
  app U := fwd π' Φ N U.1
  app_smul U a m := fwd_smul_sections π' Φ N U.1 a m
  naturality {U U'} h := by
    refine LinearMap.ext fun m => ?_
    change (OModulePresheaf.ofModules π' N).obj U'.1 at m
    rw [LinearMap.comp_apply, LinearMap.comp_apply, fwd_apply, fwd_apply]
    refine Eq.trans ?_ (OModulePresheaf.tensor_res_tmul
      (OModulePresheaf.pushforwardUnit π' Φ) (OModulePresheaf.ofModules π' N)
      h (onePf π' Φ U'.1) m).symm
    congr 1
    symm
    change (P.presheaf.map (homOfLE _).op).hom 1 = 1
    exact map_one _
def

bwdHom

L231 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.bwdHom
Documentation

The inverse affine presheaf morphism given by contracting the tensor factor.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
section twistIso
variable {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R))
  (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules)
Lean source · full declaration
def bwdHom : AffHom ((OModulePresheaf.pushforwardUnit π' Φ).twist N)
  (OModulePresheaf.ofModules π' N) where
  app U := bwd π' Φ N U.1
  app_smul U a t := by
    have hinj : Function.Injective (fwd π' Φ N U.1) :=
      Function.LeftInverse.injective (g := bwd π' Φ N U.1) (bwd_fwd π' Φ N U.1)
    apply hinj
    have hs : ∀ m : (OModulePresheaf.ofModules π' N).obj U.1, fwd π' Φ N U.1 (a • m) = a • fwd π' Φ
      N U.1 m :=
      (fwdHom π' Φ N).app_smul U a
    rw [hs, fwd_bwd, fwd_bwd]
  naturality {U U'} h := by
    refine LinearMap.ext fun t => ?_
    have hinj : Function.Injective (fwd π' Φ N U.1) :=
      Function.LeftInverse.injective (g := bwd π' Φ N U.1) (bwd_fwd π' Φ N U.1)
    apply hinj
    rw [LinearMap.comp_apply, LinearMap.comp_apply, fwd_bwd]
    have hn : fwd π' Φ N U.1 ((OModulePresheaf.ofModules π' N).res h (bwd π' Φ N U'.1 t)) =
        ((OModulePresheaf.pushforwardUnit π' Φ).twist N).res h (fwd π' Φ N U'.1 (bwd π' Φ N U'.1
          t)) :=
      congrArg (fun f => f (bwd π' Φ N U'.1 t)) ((fwdHom π' Φ N).naturality h)
    rw [hn, fwd_bwd]
theorem

cechEquiv_twist_pushforwardUnit_of_isIso

L256 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso.P2mAutInv.cechEquiv_twist_pushforwardUnit_of_isIso
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace P2mAutInv
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.TensorProduct
Lean source · statement
theorem cechEquiv_twist_pushforwardUnit_of_isIso
    {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R)) [IsSeparated
      π']
    (Φ : P ⟶ P') [IsIso Φ] (N : P'.Modules) (𝔚' : P'.OrderedAffineCover) :
    Nonempty (((OModulePresheaf.pushforwardUnit π' Φ).twist N).H0 𝔚' ≃ₗ[R]
      (OModulePresheaf.ofModules π' N).H0 𝔚') ∧
      ∀ i : ℕ, Nonempty (((OModulePresheaf.pushforwardUnit π' Φ).twist N).HSucc 𝔚' i ≃ₗ[R]
        (OModulePresheaf.ofModules π' N).HSucc 𝔚' i)
theorem

cechFinrank_ofModules_pullback_eq_of_isIso

L272 ↗
AlgebraicGeometry.OModulePresheaf.cechFinrank_ofModules_pullback_eq_of_isIso
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinrank_ofModules_pullback_eq_of_isIso
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
universe u
open CategoryTheory AlgebraicGeometry
open P2mAutInv in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinrank_ofModules_pullback_eq_of_isIso
    {R : Type u} [CommRing R] {P P' : Scheme.{u}} (π' : P' ⟶ Spec (CommRingCat.of R)) [IsSeparated
      π']
    (Φ : P ⟶ P') [IsIso Φ]
    (N : P'.Modules) (hN : Scheme.Modules.IsInvertible N)
    (𝔚 : P.OrderedAffineCover) (𝔚' : P'.OrderedAffineCover) (n : ℕ) :
    (OModulePresheaf.ofModules (Φ ≫ π') ((Scheme.Modules.pullback Φ).obj N)).cechFinrank 𝔚 n =
      (OModulePresheaf.ofModules π' N).cechFinrank 𝔚' n

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