NYLL
Module

SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.lean

Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
10 declarations indexed from sourceView source ↗

Module documentation

Small Extension is Pic Deformation Cocycle unit pullback Unit Iso zero

Imports6
Imported by2

Declarations

lemma

congr_unit_hom

L41 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.congr_unit_hom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
section coh
variable {T' T : Scheme.{u}}
Lean source · statement
lemma congr_unit_hom {f f' : T' ⟶ T} (H : f = f') :
    (pullbackCongr H).hom.app (SheafOfModules.unit T.ringCatSheaf) ≫ (pullbackUnitIso f').hom =
      (pullbackUnitIso f).hom
lemma

congr_unit_inv

L47 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.congr_unit_inv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
section coh
variable {T' T : Scheme.{u}}
Lean source · statement
lemma congr_unit_inv {f f' : T' ⟶ T} (H : f = f') :
    (pullbackCongr H).inv.app (SheafOfModules.unit T.ringCatSheaf) ≫ (pullbackUnitIso f).hom =
      (pullbackUnitIso f').hom
lemma

comp_inv_map_unit

L53 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.comp_inv_map_unit
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
section coh
variable {T' T : Scheme.{u}}
Lean source · statement
lemma comp_inv_map_unit {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (pullbackComp f g).inv.app (SheafOfModules.unit Z.ringCatSheaf) ≫
      (Scheme.Modules.pullback f).map (pullbackUnitIso g).hom ≫ (pullbackUnitIso f).hom =
      (pullbackUnitIso (f ≫ g)).hom
def

canTriv

L65 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.canTriv
Documentation

The canonical Čech trivialization of the unit module on the ordered affine cover.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
def canTriv (𝒰 : X.OrderedAffineCover) :
    CechTrivialisation 𝒰 (SheafOfModules.unit X.ringCatSheaf)
lemma

canTriv_restrict

L68 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.canTriv_restrict
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
lemma canTriv_restrict (𝒰 : X.OrderedAffineCover) {a : 𝒰.ι} {W : X.Opens} (h : W ≤ 𝒰.U a) :
    (canTriv 𝒰).restrict h = pullbackUnitIso W.ι
lemma

uAS_eq_one_of_eq_refl

L79 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.uAS_eq_one_of_eq_refl
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
lemma uAS_eq_one_of_eq_refl {Y : Scheme.{u}} (W : Y.Opens)
    (e : SheafOfModules.unit ((W : Scheme.{u})).ringCatSheaf ≅ SheafOfModules.unit ((W :
      Scheme.{u})).ringCatSheaf)
    (h : e = Iso.refl _) : unitAutSection W e = 1
lemma

uAS_symm_trans

L86 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.uAS_symm_trans
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
lemma uAS_symm_trans {Y : Scheme.{u}} (W : Y.Opens) {A : ((W : Scheme.{u})).Modules}
    (e : A ≅ SheafOfModules.unit ((W : Scheme.{u})).ringCatSheaf) :
    unitAutSection W (e.symm ≪≫ e) = 1
lemma

canTriv_transition

L91 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.canTriv_transition
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
lemma canTriv_transition (𝒰 : X.OrderedAffineCover) (s : 𝒰.Idx 1) : (canTriv 𝒰).transition s = 1
lemma

canTriv_comap

L96 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero.UnitClassZero.canTriv_comap
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UnitClassZero
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
lemma canTriv_comap (𝒰 : X.OrderedAffineCover) {X₀ : Scheme.{u}} (g : X₀ ⟶ X) [IsAffineHom g] (a :
  𝒰.ι) :
    (canTriv 𝒰).comap g a =
      (Scheme.Modules.pullback ((𝒰.comap g).U a).ι).mapIso (pullbackUnitIso g) ≪≫
        pullbackUnitIso ((𝒰.comap g).U a).ι
theorem

isPicDeformationCocycle_unit_pullbackUnitIso_zero

L115 ↗
AlgebraicGeometry.SmallExtension.isPicDeformationCocycle_unit_pullbackUnitIso_zero
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.SmallExtension.isPicDeformationCocycle_unit_pullbackUnitIso_zero
    {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
    (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ι : V →ₗ[B₁] B₁)
    {X X₀ Xk : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁))
    (fk : Xk ⟶ Spec (CommRingCat.of k)) (i : Xk ⟶ X) [IsAffineHom i]
    (g : X₀ ⟶ X) [IsAffineHom g] (𝒰 : X.OrderedAffineCover) :
    SmallExtension.IsPicDeformationCocycle V ι f fk i g 𝒰 (SheafOfModules.unit X.ringCatSheaf)
      (Scheme.Modules.pullbackUnitIso g) 0

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