Module

SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.lean

Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle

20 declarations indexed from sourceView source ↗

Module documentation

Small Extension sub mem range d of is Pic Deformation Cocycle of is Pic Deformation

Cocycle

Imports16

Imported by2

theorem

uAS_conj_homOfLE

L55 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.uAS_conj_homOfLE

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD

Lean source · statement

theorem uAS_conj_homOfLE {Y : Scheme.{u}} {W U : Y.Opens} (h : W ≤ U)
    (lam : SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (U :
      Scheme.{u}).ringCatSheaf) :
    Scheme.Modules.unitAutSection W
        ((Scheme.Modules.pullbackUnitIso (Y.homOfLE h)).symm ≪≫
          (Scheme.Modules.pullback (Y.homOfLE h)).mapIso lam ≪≫
          Scheme.Modules.pullbackUnitIso (Y.homOfLE h)) =
      (Y.presheaf.map (homOfLE h).op).hom (Scheme.Modules.unitAutSection U lam)

theorem

presheaf_map_map_eq

L78 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.presheaf_map_map_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD

Lean source · statement

theorem presheaf_map_map_eq {Z : Scheme.{u}} {A B C : (Z.Opens)ᵒᵖ} (f : A ⟶ B) (g : B ⟶ C) (h : A ⟶
  C)
    (y : Z.presheaf.obj A) :
    (Z.presheaf.map g).hom ((Z.presheaf.map f).hom y) = (Z.presheaf.map h).hom y

theorem

uAS_conj_morphismRestrict

L84 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.uAS_conj_morphismRestrict

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD

Lean source · statement

theorem uAS_conj_morphismRestrict {X X₀ : Scheme.{u}} (g : X₀ ⟶ X) (U : X.Opens)
    (lam : SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (U :
      Scheme.{u}).ringCatSheaf) :
    Scheme.Modules.unitAutSection (g ⁻¹ᵁ U)
        ((Scheme.Modules.pullbackUnitIso (g ∣_ U)).symm ≪≫
          (Scheme.Modules.pullback (g ∣_ U)).mapIso lam ≪≫
          Scheme.Modules.pullbackUnitIso (g ∣_ U)) =
      (g.app U).hom (Scheme.Modules.unitAutSection U lam)

def

transportR

L106 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.transportR

Documentation

The Čech trivialization modified by the given automorphisms of the unit modules.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

def transportR
    (lam : ∀ a : 𝒱.ι, SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf ≅
      SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) : Scheme.Modules.CechTrivialisation 𝒱 𝓜

theorem

transportR_restrict

L112 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.transportR_restrict

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem transportR_restrict
    (lam : ∀ a : 𝒱.ι, SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf ≅
      SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) {a : 𝒱.ι} {W : Y.Opens} (h : W ≤ 𝒱.U a) :
    (transportR lam τ).restrict h =
      τ.restrict h ≪≫ ((Scheme.Modules.pullbackUnitIso (Y.homOfLE h)).symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE h)).mapIso (lam a) ≪≫ Scheme.Modules.pullbackUnitIso
          (Y.homOfLE h))

theorem

transportR_comap

L144 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.transportR_comap

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem transportR_comap
    (lam : ∀ a : 𝒱.ι, SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf ≅
      SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) {Y' : Scheme.{u}} (g : Y' ⟶ Y) [IsAffineHom g] (a :
      𝒱.ι) :
    (transportR lam τ).comap g a =
      τ.comap g a ≪≫ ((Scheme.Modules.pullbackUnitIso (g ∣_ 𝒱.U a)).symm ≪≫
        (Scheme.Modules.pullback (g ∣_ 𝒱.U a)).mapIso (lam a) ≪≫ Scheme.Modules.pullbackUnitIso (g
          ∣_ 𝒱.U a))

theorem

conj_symm

L178 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.conj_symm

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem conj_symm {Z Z' : Scheme.{u}} (p : Z' ⟶ Z)
    (lam : SheafOfModules.unit Z.ringCatSheaf ≅ SheafOfModules.unit Z.ringCatSheaf) :
    ((Scheme.Modules.pullbackUnitIso p).symm ≪≫ (Scheme.Modules.pullback p).mapIso lam ≪≫
        Scheme.Modules.pullbackUnitIso p).symm =
      (Scheme.Modules.pullbackUnitIso p).symm ≪≫ (Scheme.Modules.pullback p).mapIso lam.symm ≪≫
        Scheme.Modules.pullbackUnitIso p

theorem

uAS_trans'

L191 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.uAS_trans'

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem uAS_trans' {Z : Scheme.{u}} (W : Z.Opens)
    (e₁ e₂ : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    Scheme.Modules.unitAutSection W (e₁ ≪≫ e₂) =
      Scheme.Modules.unitAutSection W e₁ * Scheme.Modules.unitAutSection W e₂

theorem

uAS_mul_uAS_symm

L198 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.uAS_mul_uAS_symm

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem uAS_mul_uAS_symm {Z : Scheme.{u}} (W : Z.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    Scheme.Modules.unitAutSection W e * Scheme.Modules.unitAutSection W e.symm = 1

theorem

transportR_transition

L205 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.transportR_transition

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem transportR_transition
    (lam : ∀ a : 𝒱.ι, SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf ≅
      SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) (s : 𝒱.Idx 1) :
    (transportR lam τ).transition s =
      (Y.presheaf.map (homOfLE (𝒱.inter_le s 0)).op).hom
          (Scheme.Modules.unitAutSection (𝒱.U (s.1 0)) (lam (s.1 0)).symm) *
        τ.transition s *
      (Y.presheaf.map (homOfLE (𝒱.inter_le s 1)).op).hom
          (Scheme.Modules.unitAutSection (𝒱.U (s.1 1)) (lam (s.1 1)))

theorem

transportR_discrepancy

L220 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.transportR_discrepancy

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem transportR_discrepancy
    (lam : ∀ a : 𝒱.ι, SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf ≅
      SheafOfModules.unit ((𝒱.U a : Scheme.{u})).ringCatSheaf)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) {Y' : Scheme.{u}} (g : Y' ⟶ Y) [IsAffineHom g] (a :
      𝒱.ι)
    (φ₀ : (Scheme.Modules.pullback g).obj 𝓜 ≅ SheafOfModules.unit Y'.ringCatSheaf) :
    Scheme.Modules.unitAutSection (g ⁻¹ᵁ 𝒱.U a)
        (((transportR lam τ).comap g a).symm ≪≫
          (Scheme.Modules.pullback (g ⁻¹ᵁ 𝒱.U a).ι).mapIso φ₀ ≪≫
            Scheme.Modules.pullbackUnitIso (g ⁻¹ᵁ 𝒱.U a).ι) =
      (g.app (𝒱.U a)).hom (Scheme.Modules.unitAutSection (𝒱.U a) (lam a).symm) *
        Scheme.Modules.unitAutSection (g ⁻¹ᵁ 𝒱.U a)
          ((τ.comap g a).symm ≪≫
            (Scheme.Modules.pullback (g ⁻¹ᵁ 𝒱.U a).ι).mapIso φ₀ ≪≫
              Scheme.Modules.pullbackUnitIso (g ⁻¹ᵁ 𝒱.U a).ι)

theorem

inter_one_eq_inf

L238 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.inter_one_eq_inf

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem inter_one_eq_inf {Z : Scheme.{u}} (𝒦 : Z.OrderedAffineCover) (s : 𝒦.Idx 1) :
    𝒦.inter s = 𝒦.U (s.1 0) ⊓ 𝒦.U (s.1 1)

theorem

mul_eq_zero_of_mem_map

L247 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.mul_eq_zero_of_mem_map

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem mul_eq_zero_of_mem_map {T' A : Type u} [CommRing T'] [CommRing A] [Algebra T' A]
    (J : Ideal T') (hJ : J * J = ⊥) {x y : A}
    (hx : x ∈ J.map (algebraMap T' A)) (hy : y ∈ J.map (algebraMap T' A)) : x * y = 0

theorem

map_res_mem

L254 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.map_res_mem

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · full declaration

theorem map_res_mem {T' : Type u} [CommRing T'] {Z : Scheme.{u}} (p : Z ⟶ Spec (CommRingCat.of T'))
    (J : Ideal T') {U U' : Z.Opens} (h : U' ≤ U) {x : Γ(Z, U)}
    (hx : letI := algebraOfHom p U; x ∈ J.map (algebraMap T' Γ(Z, U))) :
    letI := algebraOfHom p U'
    (Z.presheaf.map (homOfLE h).op).hom x ∈ J.map (algebraMap T' Γ(Z, U')) := by
  let := algebraOfHom p U
  let := algebraOfHom p U'
  have hc : (algebraMap T' Γ(Z, U')) = (restrictAlgHom p h).toRingHom.comp (algebraMap T' Γ(Z, U))
    :=
    RingHom.ext fun r => ((restrictAlgHom p h).commutes r).symm
  rw [hc, ← Ideal.map_map]
  exact Ideal.mem_map_of_mem _ hx

theorem

mem_map_of_isFibreReading

L267 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.mem_map_of_isFibreReading

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · full declaration

theorem mem_map_of_isFibreReading {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 : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁))
    {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of k)) (i : Xk ⟶ X)
    (U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ : Γ(X, U))
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W)
    (h : IsFibreReading V ι f fk i U W hW δ w) :
    letI := algebraOfHom f U
    δ ∈ Ideal.map (algebraMap B₁ Γ(X, U)) (LinearMap.range ι) := by
  let := algebraOfHom f U
  obtain ⟨n, v, s, hs, -⟩ := h
  rw [← hs]
  refine Submodule.sum_mem _ fun j _ => Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ ⟨v j, rfl⟩)

theorem

eq_of_mul_eq_one_of_mul_eq_one

L281 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.eq_of_mul_eq_one_of_mul_eq_one

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem eq_of_mul_eq_one_of_mul_eq_one {A : Type u} [CommRing A] {x y z : A} (hy : x * y = 1) (hz :
  x * z = 1) :
    y = z

theorem

key_identity

L288 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.key_identity

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

theorem key_identity {A : Type u} [CommRing A] (t ea eb la la' lb lb' ca cb : A)
    (hA : la * la' = 1) (hB : lb * lb' = 1) (hcc : ca * cb = 0)
    (hda : (t * ea * eb - 1) * ca = 0) (hdb : (t * ea * eb - 1) * cb = 0) :
    la' * t * lb * (la * ea * (1 - ca)) * (lb' * eb * (1 + cb)) - 1 =
      (t * ea * eb - 1) + cb + -ca

theorem

res_face_aux

L300 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.res_face_aux

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}
section dzero
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {p : Z ⟶ Spec (.of R)}
  (F : OModulePresheaf p) (K : Z.OrderedAffineCover)

Lean source · statement

theorem res_face_aux (η : ∀ a : K.ι, F.obj (K.U a)) {t : K.Idx 0} {a : K.ι} (h : t.1 0 = a)
    {W : Z.Opens} (hW : W ≤ K.inter t) (hW' : W ≤ K.U a) :
    F.res hW (F.res (K.inter_le t 0) (η (t.1 0))) = F.res hW' (η a)

theorem

d_zero_apply

L305 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle.PicDefWD.d_zero_apply

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PicDefWD
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}
section dzero
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {p : Z ⟶ Spec (.of R)}
  (F : OModulePresheaf p) (K : Z.OrderedAffineCover)

Lean source · full declaration

theorem d_zero_apply (η : ∀ a : K.ι, F.obj (K.U a)) (s : K.Idx 1) :
    F.d K 0 (fun t => F.res (K.inter_le t 0) (η (t.1 0))) s =
      F.res (K.inter_le s 1) (η (s.1 1)) + -F.res (K.inter_le s 0) (η (s.1 0)) := by
  rw [OModulePresheaf.d_apply, Fin.sum_univ_two]
  have h0 : (K.face s 0).1 0 = s.1 1 := congrArg s.1 (by decide)
  have h1 : (K.face s 1).1 0 = s.1 0 := congrArg s.1 (by decide)
  rw [res_face_aux F K η h0 _ (K.inter_le s 1), res_face_aux F K η h1 _ (K.inter_le s 0)]
  simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul, neg_smul]

theorem

sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle

L336 ↗

AlgebraicGeometry.SmallExtension.sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicGeometry.SmallExtension
universe u
open _root_.AlgebraicCurves.Geometry.Picard.Proofs in
open SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle in
open _root_.CategoryTheory in
open _root_.CategoryTheory.Limits in
open _root_.AlgebraicGeometry in
open _root_.IsLocalRing in
open _root_.AlgebraicGeometry.SmallExtension in
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover in
open _root_.Opposite in
open _root_.TopologicalSpace in
open PicDefWD in

Lean source · statement

theorem sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
    {B₁ B₀ : Type u} [CommRing B₁] [IsLocalRing B₁] [CommRing B₀]
    (π : B₁ →+* B₀) (hπ : Function.Surjective π)
    (hsmall : RingHom.ker π * maximalIdeal B₁ = ⊥) (hI : RingHom.ker π ≤ maximalIdeal B₁)
    (V : Type u) [AddCommGroup V] [Module (ResidueField B₁) V] [Module.Finite (ResidueField B₁) V]
    [Module B₁ V] [IsScalarTower B₁ (ResidueField B₁) V]
    (ι : V →ₗ[B₁] B₁) (hι : Function.Injective ι)
    (hιI : LinearMap.range ι = Submodule.restrictScalars B₁ (RingHom.ker π))
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁)) [IsSeparated f] [Flat f]
    {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of B₀)) (g : X₀ ⟶ X) [IsAffineHom g]
    (hg : IsPullback g f₀ f (Spec.map (CommRingCat.ofHom π)))
    {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of (ResidueField B₁))) (i : Xk ⟶ X) [IsAffineHom
      i]
    (hi : IsPullback i fk f (Spec.map (CommRingCat.ofHom (residue B₁))))
    (𝒰 : X.OrderedAffineCover)
    (M : X.Modules) (φ₀ : (Scheme.Modules.pullback g).obj M ≅ SheafOfModules.unit X₀.ringCatSheaf)
    (w w' : Module.Dual (ResidueField B₁) V →ₗ[ResidueField B₁] (OModulePresheaf.unit fk).cochain
      (𝒰.comap i) 1)
    (hw : IsPicDeformationCocycle V ι f fk i g 𝒰 M φ₀ w) (hw' : IsPicDeformationCocycle V ι f fk i
      g 𝒰 M φ₀ w') :
    ∀ ξ : Module.Dual (ResidueField B₁) V,
      w ξ - w' ξ ∈ LinearMap.range ((OModulePresheaf.unit fk).d (𝒰.comap i) 0)

Module documentation

Small Extension sub mem range d of is Pic Deformation Cocycle of is Pic Deformation

Declarations