NYLL
Module

Scheme_OrderedAffineCoverOf_aug_injective.lean

Nyll.SchemeTheory.Cohomology.Cech.Scheme_OrderedAffineCoverOf_aug_injective
6 declarations indexed from sourceView source ↗

Module documentation

Injectivity of the affine-cover augmentation

The augmentation from sections on an open into the degree-zero Cech cochains of its ordered affine cover is injective.

Imports3
Imported by6

Declarations

theorem

res_refl

L51 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.res_refl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section ResHelpers
variable {V : Scheme.{u}}
Lean source · statement
theorem res_refl {O : V.Opens} (h : O ≤ O) (x : Γ(V, O)) :
    (V.presheaf.map (homOfLE h).op).hom x = x
theorem

res_res

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.res_res
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section ResHelpers
variable {V : Scheme.{u}}
Lean source · statement
theorem res_res {O₁ O₂ O₃ : V.Opens} (h12 : O₁ ≤ O₂) (h23 : O₂ ≤ O₃)
    (x : Γ(V, O₃)) :
    (V.presheaf.map (homOfLE h12).op).hom ((V.presheaf.map (homOfLE h23).op).hom x)
      = (V.presheaf.map (homOfLE (h12.trans h23)).op).hom x
theorem

altC_at_eq

L62 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.altC_at_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section ResHelpers
variable {V : Scheme.{u}}
Lean source · statement
theorem altC_at_eq {W : V.Opens} {K : Scheme.OrderedAffineCoverOf W}
    {n : ℕ} (z : K.cochain n) {σ τ : K.Idx n} (h : σ = τ)
    {O : V.Opens} (hσ : O ≤ K.inter σ) (hτ : O ≤ K.inter τ) :
    (V.presheaf.map (homOfLE hσ).op).hom (z σ)
      = (V.presheaf.map (homOfLE hτ).op).hom (z τ)
def

idx0

L75 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.idx0
Documentation

The degree-zero Cech index determined by a single cover member.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section Idx0
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι)
Lean source · statement
def idx0 : K.Idx 0
theorem

aug_injective

L83 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Acyclic.aug_injective
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
namespace Acyclic
open _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section CoverOf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
include π
Lean source · full declaration
theorem aug_injective {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    Function.Injective (K.aug π) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections π
  intro w₁ w₂ hw
  have hcov : W ≤ ⨆ σ : K.Idx 0, K.inter σ :=
    K.iSup_eq.ge.trans (iSup_le fun i => le_iSup_of_le (idx0 K i)
      (le_iInf fun _ => le_rfl))
  exact V.sheaf.eq_of_locally_eq' (K.inter (i := 0)) W
    (fun σ => homOfLE (K.inter_le_base σ)) hcov w₁ w₂ fun σ => congrFun hw σ
theorem

aug_injective

L104 ↗
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.aug_injective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_OrderedAffineCoverOf_aug_injective
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u
with_weak_namespace _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open _root_.AlgebraicGeometry Scheme_OrderedAffineCoverOf_aug_injective.AlgebraicGeometry in
with_weak_namespace Scheme_OrderedAffineCoverOf_aug_injective
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.OrderedAffineCoverOf.aug_injective {R : Type u}
    [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) {W : V.Opens}
    (K : V.OrderedAffineCoverOf W) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections π
    Function.Injective (K.aug π) :=
  Scheme.OrderedAffineCoverOf.Acyclic.aug_injective π K

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