Module

Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit

41 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Unit Cocycle exists comap eq of is Direct Limit

Imports5

Imported by2

theorem

comp_eq

L91 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.comp_eq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem comp_eq (a b : ι) (h : a ≤ b) : (g b).comp (φ a b h) = g a

theorem

comp_eq'

L95 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.comp_eq'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem comp_eq' (a b c : ι) (hab : a ≤ b) (hbc : b ≤ c) : (φ b c hbc).comp (φ a b hab) = φ a c
  (hab.trans hbc)

theorem

spec_comp

L99 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.spec_comp

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem spec_comp (a b : ι) (h : a ≤ b) :
    Spec.map (CommRingCat.ofHom (g b)) ≫ Spec.map (CommRingCat.ofHom (φ a b h)) = Spec.map
      (CommRingCat.ofHom (g a))

theorem

spec_comp'

L105 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.spec_comp'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem spec_comp' (a b c : ι) (hab : a ≤ b) (hbc : b ≤ c) :
    Spec.map (CommRingCat.ofHom (φ b c hbc)) ≫ Spec.map (CommRingCat.ofHom (φ a b hab)) =
      Spec.map (CommRingCat.ofHom (φ a c (hab.trans hbc)))

abbrev

XR

L111 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.XR

Documentation

The base change of the scheme to the limit ring.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

abbrev XR : Scheme.{u}

abbrev

XS

L114 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.XS

Documentation

The base change of the scheme to a later stage of the directed system.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

abbrev XS (j : ι) (h : i ≤ j) : Scheme.{u}

abbrev

prR

L117 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.prR

Documentation

The projection from base change to the limit ring back to the original scheme.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

abbrev prR : XR g i fX ⟶ X

abbrev

prS

L119 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.prS

Documentation

The projection from base change to a later stage back to the original scheme.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

abbrev prS (j : ι) (h : i ≤ j) : XS φ i fX j h ⟶ X

def

cc

L122 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.cc

Documentation

The comparison morphism from the limit base change to a stage base change.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

def cc (j : ι) (h : i ≤ j) : XR g i fX ⟶ XS φ i fX j h

theorem

cc_fst

L127 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.cc_fst

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem cc_fst (j : ι) (h : i ≤ j) : cc φ g hR i fX j h ≫ Limits.pullback.fst _ _ =
  Limits.pullback.fst _ _

theorem

cc_snd

L130 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.cc_snd

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem cc_snd (j : ι) (h : i ≤ j) :
    cc φ g hR i fX j h ≫ Limits.pullback.snd _ _ = Limits.pullback.snd _ _ ≫ Spec.map
      (CommRingCat.ofHom (g j))

theorem

cc_unique

L135 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.cc_unique

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem cc_unique (j : ι) (h : i ≤ j) (c : XR g i fX ⟶ XS φ i fX j h)
    (h1 : c ≫ Limits.pullback.fst _ _ = Limits.pullback.fst _ _)
    (h2 : c ≫ Limits.pullback.snd _ _ = Limits.pullback.snd _ _ ≫ Spec.map (CommRingCat.ofHom (g
      j))) :
    c = cc φ g hR i fX j h

def

dd

L146 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.dd

Documentation

The transition morphism between two stage base changes.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

def dd (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) : XS φ i fX l (hk.trans hkl) ⟶ XS φ i fX k hk

theorem

dd_fst

L152 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.dd_fst

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem dd_fst (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) : dd φ i fX k l hk hkl ≫ Limits.pullback.fst _
  _ = Limits.pullback.fst _ _

theorem

dd_snd

L156 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.dd_snd

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem dd_snd (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) :
    dd φ i fX k l hk hkl ≫ Limits.pullback.snd _ _ = Limits.pullback.snd _ _ ≫ Spec.map
      (CommRingCat.ofHom (φ k l hkl))

theorem

cc_dd

L161 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.cc_dd

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem cc_dd (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) :
    cc φ g hR i fX l (hk.trans hkl) ≫ dd φ i fX k l hk hkl = cc φ g hR i fX k hk

theorem

dd_dd

L168 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.dd_dd

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem dd_dd (k l m : ι) (hk : i ≤ k) (hkl : k ≤ l) (hlm : l ≤ m) :
    dd φ i fX l m (hk.trans hkl) hlm ≫ dd φ i fX k l hk hkl = dd φ i fX k m hk (hkl.trans hlm)

abbrev

castO

L175 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.castO

Documentation

The map on sections induced by equality of the underlying opens.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

abbrev castO {Y : Scheme.{u}} {U V : Y.Opens} (e : U = V) : Γ(Y, V) →+* Γ(Y, U)

theorem

castO_castO

L179 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.castO_castO

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem castO_castO {Y : Scheme.{u}} {U V W : Y.Opens} (e : U = V) (e' : V = W) (x : Γ(Y, W)) :
    castO e (castO e' x) = castO (e.trans e') x

theorem

castO_rfl

L185 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.castO_rfl

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem castO_rfl {Y : Scheme.{u}} {U : Y.Opens} (x : Γ(Y, U)) : castO (rfl : U = U) x = x

theorem

pre_cc

L189 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.pre_cc

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem pre_cc (j : ι) (h : i ≤ j) (V : X.Opens) :
    prR g i fX ⁻¹ᵁ V = cc φ g hR i fX j h ⁻¹ᵁ (prS φ i fX j h ⁻¹ᵁ V)

theorem

pre_dd

L194 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.pre_dd

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem pre_dd (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) (V : X.Opens) :
    prS φ i fX l (hk.trans hkl) ⁻¹ᵁ V = dd φ i fX k l hk hkl ⁻¹ᵁ (prS φ i fX k hk ⁻¹ᵁ V)

theorem

app_castO

L199 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.app_castO

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · full declaration

theorem app_castO {Y Z : Scheme.{u}} (f : Y ⟶ Z) {U V : Z.Opens} (e : U = V) (y : Γ(Z, V)) :
    f.app U (castO e y) = castO (show f ⁻¹ᵁ U = f ⁻¹ᵁ V by rw [e]) (f.app V y) := by
  subst e
  rw [castO_rfl, castO_rfl]

theorem

comp_app_apply

L205 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.comp_app_apply

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem comp_app_apply {Y Z T : Scheme.{u}} (f : Y ⟶ Z) (h : Z ⟶ T) (U : T.Opens) (y : Γ(T, U)) :
    (f ≫ h).app U y = f.app (h ⁻¹ᵁ U) (h.app U y)

def

val

L210 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.val

Documentation

The map on sections from a stage base change to the limit base change.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

def val (k : ι) (hk : i ≤ k) (V : X.Opens) : Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ V) →+* Γ(XR g i
  fX, prR g i fX ⁻¹ᵁ V)

def

push

L216 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.push

Documentation

The transition map on sections between stage base changes.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

def push (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) (V : X.Opens) :
    Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ V) →+* Γ(XS φ i fX l (hk.trans hkl), prS φ i fX l
      (hk.trans hkl) ⁻¹ᵁ V)

theorem

val_push

L221 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.val_push

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem val_push (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) (V : X.Opens) (t : Γ(XS φ i fX k hk, prS φ i
  fX k hk ⁻¹ᵁ V)) :
    val φ g hR i fX l (hk.trans hkl) V (push φ i fX k l hk hkl V t) = val φ g hR i fX k hk V t

theorem

app_rO

L254 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.app_rO

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem app_rO {Y Z : Scheme.{u}} (f : Y ⟶ Z) {U U' : Z.Opens} (hU : U' ≤ U) (y : Γ(Z, U)) :
    GlueOfCocycle.rO (Scheme.Hom.preimage_mono f hU) (f.app U y) = f.app U' (GlueOfCocycle.rO hU y)

theorem

rO_castO

L262 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.rO_castO

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem rO_castO {Y : Scheme.{u}} {U V U' V' : Y.Opens} (e : U = V) (e' : U' = V') (hU : U' ≤ U)
  (hV : V' ≤ V)
    (y : Γ(Y, V)) : GlueOfCocycle.rO hU (castO e y) = castO e' (GlueOfCocycle.rO hV y)

theorem

val_rO

L268 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.val_rO

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR

Lean source · statement

theorem val_rO (k : ι) (hk : i ≤ k) {V V' : X.Opens} (hV : V' ≤ V) (t : Γ(XS φ i fX k hk, prS φ i
  fX k hk ⁻¹ᵁ V)) :
    val φ g hR i fX k hk V' (GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ hV) t) =
      GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ hV) (val φ g hR i fX k hk V t)

theorem

push_rO

L277 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.push_rO

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem push_rO (k l : ι) (hk : i ≤ k) (hkl : k ≤ l) {V V' : X.Opens} (hV : V' ≤ V)
    (t : Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ V)) :
    push φ i fX k l hk hkl V' (GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ hV) t) =
      GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ hV) (push φ i fX k l hk hkl V t)

theorem

push_push

L286 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.push_push

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem push_push (k l m : ι) (hk : i ≤ k) (hkl : k ≤ l) (hlm : l ≤ m) (V : X.Opens)
    (t : Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ V)) :
    push φ i fX l m (hk.trans hkl) hlm V (push φ i fX k l hk hkl V t) = push φ i fX k m hk
      (hkl.trans hlm) V t

theorem

castO_injective

L325 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.castO_injective

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
omit hR in

Lean source · statement

theorem castO_injective {Y : Scheme.{u}} {U V : Y.Opens} (e : U = V) : Function.Injective (castO e)

theorem

exists_val_eq

L331 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.exists_val_eq

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
variable [Nonempty ι] [IsDirected ι (· ≤ ·)]

Lean source · statement

theorem exists_val_eq [QuasiCompact fX] [QuasiSeparated fX] (V : X.Opens) (hV : IsCompact (V : Set
  X))
    (s : Γ(XR g i fX, prR g i fX ⁻¹ᵁ V)) :
    ∃ (k : ι) (hk : i ≤ k) (t : Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ V)), val φ g hR i fX k hk V t
      = s

theorem

exists_push_eq

L340 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.exists_push_eq

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
variable [Nonempty ι] [IsDirected ι (· ≤ ·)]

Lean source · statement

theorem exists_push_eq [QuasiCompact fX] [QuasiSeparated fX] (V : X.Opens) (hV : IsCompact (V : Set
  X))
    (k : ι) (hk : i ≤ k) (t t' : Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ V))
    (h : val φ g hR i fX k hk V t = val φ g hR i fX k hk V t') :
    ∃ (l : ι) (hkl : k ≤ l), push φ i fX k l hk hkl V t = push φ i fX k l hk hkl V t'

theorem

exists_cover

L354 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.exists_cover

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Setup
variable {ι : Type u} [Preorder ι]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i)))
include hR
variable [Nonempty ι] [IsDirected ι (· ≤ ·)]

Lean source · statement

theorem exists_cover [QuasiCompact fX] [QuasiSeparated fX] {κ : Type u} (W : κ → X.Opens)
    (hcov : (⨆ k, prR g i fX ⁻¹ᵁ W k) = ⊤) :
    ∃ (k : ι) (hk : i ≤ k), ∀ (l : ι) (hkl : k ≤ l), (⨆ q, prS φ i fX l (hk.trans hkl) ⁻¹ᵁ W q) = ⊤

abbrev

l12

L379 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.l12

Documentation

The inclusion of a triple intersection in its first two factors.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Main
variable {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX] [QuasiSeparated
    fX]

Lean source · statement

abbrev l12 {κ : Type u} (W : κ → X.Opens) (a b c : κ) : W a ⊓ W b ⊓ W c ≤ W a ⊓ W b

abbrev

l23

L382 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.l23

Documentation

The inclusion of a triple intersection in its last two factors.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Main
variable {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX] [QuasiSeparated
    fX]

Lean source · statement

abbrev l23 {κ : Type u} (W : κ → X.Opens) (a b c : κ) : W a ⊓ W b ⊓ W c ≤ W b ⊓ W c

abbrev

l13

L385 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.l13

Documentation

The inclusion of a triple intersection in its first and last factors.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Main
variable {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX] [QuasiSeparated
    fX]

Lean source · statement

abbrev l13 {κ : Type u} (W : κ → X.Opens) (a b c : κ) : W a ⊓ W b ⊓ W c ≤ W a ⊓ W c

theorem

main

L389 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit.AlgebraicGeometry.CocycleFil.main

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
noncomputable section
namespace AlgebraicGeometry
namespace CocycleFil
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
section Main
variable {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
  {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
  [DirectedSystem G fun i j h => ⇑(φ i j h)]
  {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
  (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
  (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX] [QuasiSeparated
    fX]
include hR in

Lean source · full declaration

theorem main {κ : Type u} [Finite κ] (W : κ → X.Opens) (hW : ∀ k, IsCompact (W k : Set X))
    (hcov : (⨆ k, prR g i fX ⁻¹ᵁ W k) = ⊤)
    (gc : UnitCocycle fun k => prR g i fX ⁻¹ᵁ W k) :
    ∃ (j : ι) (hij : i ≤ j) (cu : ∀ a b, Γ(XS φ i fX j hij, prS φ i fX j hij ⁻¹ᵁ (W a ⊓ W b))),
      (∀ a, cu a a = 1) ∧
      (∀ a b c, GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ (l12 W a b c)) (cu a b) *
          GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ (l23 W a b c)) (cu b c) =
        GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ (l13 W a b c)) (cu a c)) ∧
      (⨆ k, prS φ i fX j hij ⁻¹ᵁ W k) = ⊤ ∧
      ∀ a b, val φ g hR i fX j hij (W a ⊓ W b) (cu a b) =
        (show Γ(XR g i fX, prR g i fX ⁻¹ᵁ (W a ⊓ W b)) from gc.u a b) := by
  classical
  have : Fintype κ := Fintype.ofFinite κ
  have : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated fX
  have hW2 : ∀ a b, IsCompact ((W a ⊓ W b : X.Opens) : Set X) := fun a b =>
    (hW a).inter_of_isOpen (hW b) (W a).isOpen (W b).isOpen
  have hW3 : ∀ a b c, IsCompact ((W a ⊓ W b ⊓ W c : X.Opens) : Set X) := fun a b c =>
    (hW2 a b).inter_of_isOpen (hW c) (W a ⊓ W b).isOpen (W c).isOpen
  have A : ∀ a b, ∃ (k : ι) (hk : i ≤ k) (t : Γ(XS φ i fX k hk, prS φ i fX k hk ⁻¹ᵁ (W a ⊓ W b))),
      val φ g hR i fX k hk (W a ⊓ W b) t = (show Γ(XR g i fX, prR g i fX ⁻¹ᵁ (W a ⊓ W b)) from gc.u
        a b) :=
    fun a b => exists_val_eq φ g hR i fX (W a ⊓ W b) (hW2 a b) _
  choose jab hjab t ht using A
  obtain ⟨j₁, hj₁⟩ := Finset.exists_le (insert i (Finset.univ.image fun p : κ × κ => jab p.1 p.2))
  have hij₁ : i ≤ j₁ := hj₁ i (Finset.mem_insert_self _ _)
  have hjab₁ : ∀ a b, jab a b ≤ j₁ := fun a b =>
    hj₁ _ (Finset.mem_insert_of_mem (Finset.mem_image_of_mem (fun p : κ × κ => jab p.1 p.2)
      (Finset.mem_univ (a, b))))
  let u : ∀ a b, Γ(XS φ i fX j₁ hij₁, prS φ i fX j₁ hij₁ ⁻¹ᵁ (W a ⊓ W b)) := fun a b =>
    push φ i fX (jab a b) j₁ (hjab a b) (hjab₁ a b) (W a ⊓ W b) (t a b)
  have hu : ∀ a b, val φ g hR i fX j₁ hij₁ (W a ⊓ W b) (u a b) =
      (show Γ(XR g i fX, prR g i fX ⁻¹ᵁ (W a ⊓ W b)) from gc.u a b) := fun a b =>
    (val_push φ g hR i fX (jab a b) j₁ (hjab a b) (hjab₁ a b) (W a ⊓ W b) (t a b)).trans (ht a b)
  have B : ∀ a, ∃ (l : ι) (hl : j₁ ≤ l), push φ i fX j₁ l hij₁ hl (W a ⊓ W a) (u a a) = 1 := by
    intro a
    obtain ⟨l, hl, h⟩ := exists_push_eq φ g hR i fX (W a ⊓ W a) (hW2 a a) j₁ hij₁ (u a a) 1 (by
      rw [hu, map_one]; exact gc.refl a)
    exact ⟨l, hl, by rw [h, map_one]⟩
  choose la hla hB using B
  have C : ∀ a b c, ∃ (l : ι) (hl : j₁ ≤ l),
      push φ i fX j₁ l hij₁ hl (W a ⊓ W b ⊓ W c)
        (GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ (l12 W a b c)) (u a b) *
          GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ (l23 W a b c)) (u b c)) =
      push φ i fX j₁ l hij₁ hl (W a ⊓ W b ⊓ W c)
        (GlueOfCocycle.rO (Scheme.Hom.preimage_mono _ (l13 W a b c)) (u a c)) := by
    intro a b c
    apply exists_push_eq φ g hR i fX (W a ⊓ W b ⊓ W c) (hW3 a b c)
    rw [map_mul, val_rO, val_rO, val_rO, hu, hu, hu]
    · exact gc.cocycle a b c
    all_goals first
      | exact l12 W a b c
      | exact l23 W a b c
      | exact l13 W a b c
  choose labc hlabc hC using C
  obtain ⟨jc, hijc, hcovS⟩ := exists_cover φ g hR i fX W hcov
  obtain ⟨j₂, hj₂⟩ := Finset.exists_le ({j₁, jc} : Finset ι)
  have hj₁₂ : j₁ ≤ j₂ := hj₂ _ (by simp)
  have hjc₂ : jc ≤ j₂ := hj₂ _ (by simp)
  obtain ⟨js, hjs⟩ := Finset.exists_le (insert j₂ ((Finset.univ.image la) ∪ (Finset.univ.image fun
    p : κ × κ × κ => labc p.1 p.2.1 p.2.2)))
  have hj₂s : j₂ ≤ js := hjs _ (Finset.mem_insert_self _ _)
  have hj₁s : j₁ ≤ js := hj₁₂.trans hj₂s
  have hlas : ∀ a, la a ≤ js := fun a =>
    hjs _ (Finset.mem_insert_of_mem (Finset.mem_union_left _ (Finset.mem_image_of_mem la
      (Finset.mem_univ a))))
  have hlabcs : ∀ a b c, labc a b c ≤ js := fun a b c =>
    hjs _ (Finset.mem_insert_of_mem (Finset.mem_union_right _
      (Finset.mem_image_of_mem (fun p : κ × κ × κ => labc p.1 p.2.1 p.2.2) (Finset.mem_univ (a, b,
        c)))))
  let cu : ∀ a b, Γ(XS φ i fX js (hij₁.trans hj₁s), prS φ i fX js (hij₁.trans hj₁s) ⁻¹ᵁ (W a ⊓ W
    b)) := fun a b =>
    push φ i fX j₁ js hij₁ hj₁s (W a ⊓ W b) (u a b)
  refine ⟨js, hij₁.trans hj₁s, cu, fun a => ?_, fun a b c => ?_, hcovS js (hjc₂.trans hj₂s), fun a
    b => ?_⟩
  · change push φ i fX j₁ js hij₁ hj₁s (W a ⊓ W a) (u a a) = 1
    rw [← push_push φ i fX j₁ (la a) js hij₁ (hla a) (hlas a), hB a, map_one]
  · change GlueOfCocycle.rO _ (push φ i fX j₁ js hij₁ hj₁s _ (u a b)) * GlueOfCocycle.rO _ (push φ
      i fX j₁ js hij₁ hj₁s _ (u b c)) =
      GlueOfCocycle.rO _ (push φ i fX j₁ js hij₁ hj₁s _ (u a c))
    rw [← push_rO φ i fX j₁ js hij₁ hj₁s (l12 W a b c), ← push_rO φ i fX j₁ js hij₁ hj₁s (l23 W a b
      c),
      ← push_rO φ i fX j₁ js hij₁ hj₁s (l13 W a b c), ← map_mul,
      ← push_push φ i fX j₁ (labc a b c) js hij₁ (hlabc a b c) (hlabcs a b c), hC a b c, push_push]
  · exact (val_push φ g hR i fX j₁ js hij₁ hj₁s (W a ⊓ W b) (u a b)).trans (hu a b)

theorem

exists_comap_eq_of_isDirectLimit

L481 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.exists_comap_eq_of_isDirectLimit

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_UnitCocycle_exists_comap_eq_of_isDirectLimit
attribute [-instance] TwoChartCech.Sections.M0_moduleA TwoChartCech.Sections.M1_module
  TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra TwoChartCech.Cover.A1_commRing
  TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
  TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
  TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
  TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA TwoChartCech.Sections.M0_module
  TwoChartCech.Sections.M1_moduleA TwoChartCech.Sections.M1_addCommGroup
  TwoChartCech.Cover.A01_commRing TwoChartCech.Sections.M01_tower
  CoherentBaseChange.TwoTermComplex.C0_module CoherentBaseChange.TwoTermComplex.C0_addCommGroup
  CoherentBaseChange.TwoTermComplex.C1_module CoherentBaseChange.TwoTermComplex.C1_addCommGroup
  CoherentBaseChange.TwoTermComplex.C0_free CoherentBaseChange.TwoTermComplex.C1_finite
  CoherentBaseChange.TwoTermComplex.C0_finite CoherentBaseChange.TwoTermComplex.C1_free
attribute [-simp] AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
  AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
  TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
  TwoChartCech.Sections.mk.sizeOf_spec TwoChartCech.Cover.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r0_apply TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
  TwoChartCech.Cover.lineBundle_r1_apply CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
  CoherentBaseChange.TwoTermComplex.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
open AlgebraicGeometry.CocycleFil _root_.AlgebraicGeometry.Scheme.Modules in

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Scheme.Modules.UnitCocycle.exists_comap_eq_of_isDirectLimit
    {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    {G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
    [DirectedSystem G fun i j h => ⇑(φ i j h)]
    {R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
    (hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
    (i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX]
      [QuasiSeparated fX]
    {κ : Type u} [Finite κ] (W : κ → X.Opens) (hW : ∀ k, IsCompact (W k : Set X))
    (hcov : (⨆ k, (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i)))) ⁻¹ᵁ W k) = ⊤)
    (gc : Scheme.Modules.UnitCocycle fun k => (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom
      (g i)))) ⁻¹ᵁ W k) :
    ∃ (j : ι) (hij : i ≤ j) (c : Scheme.Modules.UnitCocycle fun k => (Limits.pullback.fst fX
      (Spec.map (CommRingCat.ofHom (φ i j hij)))) ⁻¹ᵁ W k),
      (⨆ k, (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j hij)))) ⁻¹ᵁ W k) = ⊤ ∧
      ∀ (cX : Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i))) ⟶ Limits.pullback fX
        (Spec.map (CommRingCat.ofHom (φ i j hij)))),
        cX ≫ Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j hij))) =
          Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i))) →
        cX ≫ Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (φ i j hij))) =
          Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (g i))) ≫ Spec.map (CommRingCat.ofHom
          (g j)) →
        ∀ (a b : κ)
          (e : (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i)))) ⁻¹ᵁ W a ⊓
            (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i)))) ⁻¹ᵁ W b =
            cX ⁻¹ᵁ ((Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j hij)))) ⁻¹ᵁ W a) ⊓
              cX ⁻¹ᵁ ((Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j hij)))) ⁻¹ᵁ W b)),
          (Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i)))).presheaf.map (eqToHom e).op
            ((c.comap cX).u a b) = gc.u a b := by
  obtain ⟨j, hij, cu, hrefl, hcoc, hcovj, hval⟩ := AlgebraicGeometry.CocycleFil.main φ g hR i fX W
    hW hcov gc
  refine ⟨j, hij, { u := fun a b => cu a b, refl := hrefl, cocycle := hcoc }, hcovj,
    fun cX h1 h2 a b e => ?_⟩
  obtain rfl := AlgebraicGeometry.CocycleFil.cc_unique φ g hR i fX j hij cX h1 h2
  exact hval a b

Module documentation

Scheme Modules Unit Cocycle exists comap eq of is Direct Limit

Declarations