NYLL
Module

Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
10 declarations indexed from sourceView source ↗

Module documentation

Base-change equivalences for two-chart Cech cohomology of locally trivial module sheaves.

Imports7
Imported by5

Declarations

def

pairMap

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.pairMap
Documentation

Apply the two chartwise base-change equivalences to the tensor product of the pair of section modules.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
Lean source · statement
def pairMap : A ⊗[R] (S.M0 × S.M1) →ₗ[A] T.M0 × T.M1
theorem

pairMap_apply

L55 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.pairMap_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
Lean source · statement
theorem pairMap_apply (x : A ⊗[R] (S.M0 × S.M1)) :
    pairMap S T e0 e1 x = (e0 (TensorProduct.prodRight R A A _ _ x).1, e1 (TensorProduct.prodRight
      R A A _ _ x).2)
theorem

pairMap_bijective

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.pairMap_bijective
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
Lean source · statement
theorem pairMap_bijective : Function.Bijective (pairMap S T e0 e1)
theorem

e01_cechDiff_baseChange

L77 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.e01_cechDiff_baseChange
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
variable (e01 : A ⊗[R] S.M01 ≃ₗ[A] T.M01)
  (h0 : ∀ x, e01 ((S.r0.baseChange A) x) = T.r0 (e0 x)) (h1 : ∀ x, e01 ((S.r1.baseChange A) x) =
    T.r1 (e1 x))
include h0 h1 in
Lean source · statement
theorem e01_cechDiff_baseChange (x : A ⊗[R] (S.M0 × S.M1)) :
    e01 ((S.cechDiff.baseChange A) x) = T.cechDiff (pairMap S T e0 e1 x)
theorem

mem_ker_baseChange_iff

L91 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.mem_ker_baseChange_iff
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
variable (e01 : A ⊗[R] S.M01 ≃ₗ[A] T.M01)
  (h0 : ∀ x, e01 ((S.r0.baseChange A) x) = T.r0 (e0 x)) (h1 : ∀ x, e01 ((S.r1.baseChange A) x) =
    T.r1 (e1 x))
include h0 h1 in
Lean source · statement
theorem mem_ker_baseChange_iff (x : A ⊗[R] (S.M0 × S.M1)) :
    x ∈ LinearMap.ker (S.cechDiff.baseChange A) ↔ pairMap S T e0 e1 x ∈ T.H0
theorem

nonempty_kerEquivH0

L97 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.nonempty_kerEquivH0
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
variable (e01 : A ⊗[R] S.M01 ≃ₗ[A] T.M01)
  (h0 : ∀ x, e01 ((S.r0.baseChange A) x) = T.r0 (e0 x)) (h1 : ∀ x, e01 ((S.r1.baseChange A) x) =
    T.r1 (e1 x))
include h0 h1 in
Lean source · statement
theorem nonempty_kerEquivH0 : Nonempty (T.H0 ≃ₗ[A] LinearMap.ker (S.cechDiff.baseChange A))
theorem

nonempty_cokerEquivH1

L110 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.nonempty_cokerEquivH1
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
variable (e01 : A ⊗[R] S.M01 ≃ₗ[A] T.M01)
  (h0 : ∀ x, e01 ((S.r0.baseChange A) x) = T.r0 (e0 x)) (h1 : ∀ x, e01 ((S.r1.baseChange A) x) =
    T.r1 (e1 x))
include h0 h1 in
Lean source · statement
theorem nonempty_cokerEquivH1 :
    Nonempty (((A ⊗[R] S.M01) ⧸ LinearMap.range (S.cechDiff.baseChange A)) ≃ₗ[A] T.H1)
theorem

nonempty_coker_baseChange_equiv

L122 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.nonempty_coker_baseChange_equiv
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
variable (e01 : A ⊗[R] S.M01 ≃ₗ[A] T.M01)
  (h0 : ∀ x, e01 ((S.r0.baseChange A) x) = T.r0 (e0 x)) (h1 : ∀ x, e01 ((S.r1.baseChange A) x) =
    T.r1 (e1 x))
Lean source · statement
theorem nonempty_coker_baseChange_equiv {C0 C1 : Type u} [AddCommGroup C0] [Module R C0]
    [AddCommGroup C1] [Module R C1]
    (d : C0 →ₗ[R] C1) :
    Nonempty (((A ⊗[R] C1) ⧸ LinearMap.range (d.baseChange A)) ≃ₗ[A] A ⊗[R] (C1 ⧸ LinearMap.range
      d))
theorem

nonempty_ker_baseChange_equiv_of_flat

L138 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial.TwoChartCech.Sections.BC.nonempty_ker_baseChange_equiv_of_flat
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
namespace Sections
open _root_.TwoChartCech.Sections
namespace BC
open _root_.TwoChartCech.Sections
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
variable {𝒰 : TwoChartCech.Cover.{u, u} R} {𝒰A : TwoChartCech.Cover.{u, u} A}
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (T : TwoChartCech.Sections.{u, u, u} 𝒰A)
variable (e0 : A ⊗[R] S.M0 ≃ₗ[A] T.M0) (e1 : A ⊗[R] S.M1 ≃ₗ[A] T.M1)
variable (e01 : A ⊗[R] S.M01 ≃ₗ[A] T.M01)
  (h0 : ∀ x, e01 ((S.r0.baseChange A) x) = T.r0 (e0 x)) (h1 : ∀ x, e01 ((S.r1.baseChange A) x) =
    T.r1 (e1 x))
Lean source · statement
theorem nonempty_ker_baseChange_equiv_of_flat {C0 C1 : Type u} [AddCommGroup C0] [Module R C0]
    [AddCommGroup C1]
    [Module R C1] (d : C0 →ₗ[R] C1) [Module.Flat R A] :
    Nonempty (LinearMap.ker (d.baseChange A) ≃ₗ[A] A ⊗[R] LinearMap.ker d)
theorem

exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial

L159 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open AlgebraicGeometry.Scheme.TwoAffineOpenCover in
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open Scheme_TwoAffineOpenCover_exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem exists_cech_sectionsOf_baseChange_equiv_of_locallyTrivial
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    (A : Type u) [CommRing A] [Algebra R A] :
    Nonempty (((𝒱.pullback c A).sectionsOf (Limits.pullback.snd c
      (Scheme.TwoAffineOpenCover.specMap R A))
        ((Scheme.Modules.pullback (Limits.pullback.fst c (Scheme.TwoAffineOpenCover.specMap R
          A))).obj M)).H1
      ≃ₗ[A] A ⊗[R] (𝒱.sectionsOf c M).H1) ∧
    Nonempty (((𝒱.pullback c A).sectionsOf (Limits.pullback.snd c
      (Scheme.TwoAffineOpenCover.specMap R A))
        ((Scheme.Modules.pullback (Limits.pullback.fst c (Scheme.TwoAffineOpenCover.specMap R
          A))).obj M)).H0
      ≃ₗ[A] LinearMap.ker ((𝒱.sectionsOf c M).cechDiff.baseChange A)) ∧
    (Module.Flat R A →
      Nonempty (((𝒱.pullback c A).sectionsOf (Limits.pullback.snd c
        (Scheme.TwoAffineOpenCover.specMap R A))
        ((Scheme.Modules.pullback (Limits.pullback.fst c (Scheme.TwoAffineOpenCover.specMap R
          A))).obj M)).H0
      ≃ₗ[A] A ⊗[R] (𝒱.sectionsOf c M).H0))

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