Module

Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field

14 declarations indexed from sourceView source ↗

Module documentation

Global sections after base change from a field

Degree-zero Cech cohomology computes global sections and supplies the base-change comparison used in the final statement.

Imports6

Imported by3

def

coverOfCompact

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.coverOfCompact

Documentation

A finite ordered affine cover obtained from the canonical affine cover.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField

Lean source · statement

def coverOfCompact (X : Scheme.{u}) [CompactSpace X] : X.OrderedAffineCover

def

toCochain

L58 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.toCochain

Documentation

The degree-zero Cech cochain obtained by restricting a global section.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · full declaration

def toCochain :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
    Γ(M, ⊤) →ₗ[R] (OModulePresheaf.ofModules π M).cochain K 0 :=
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
  LinearMap.pi fun s => (OModulePresheaf.ofModules π M).res (le_top : K.inter s ≤ ⊤)

theorem

toCochain_apply

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.toCochain_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · statement

theorem toCochain_apply (x : Γ(M, ⊤)) (s : K.Idx 0) :
    toCochain π M K x s = M.presheaf.map (homOfLE (le_top : K.inter s ≤ ⊤)).op x

theorem

toCochain_apply'

L67 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.toCochain_apply'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · full declaration

theorem toCochain_apply' (x : Γ(M, ⊤)) (s : K.Idx 0) :
    toCochain π M K x s = (OModulePresheaf.ofModules π M).res (le_top : K.inter s ≤ ⊤)
      (show (OModulePresheaf.ofModules π M).obj ⊤ from x) := rfl

theorem

d_toCochain

L71 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.d_toCochain

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · statement

theorem d_toCochain (x : Γ(M, ⊤)) :
    (OModulePresheaf.ofModules π M).d K 0 (toCochain π M K x) = 0

theorem

toCochain_mem

L84 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.toCochain_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · statement

theorem toCochain_mem (x : Γ(M, ⊤)) : toCochain π M K x ∈ (OModulePresheaf.ofModules π M).H0 K

theorem

toCochain_injective

L87 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.toCochain_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · statement

theorem toCochain_injective : Function.Injective (toCochain π M K)

theorem

exists_toCochain_eq

L93 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.exists_toCochain_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · statement

theorem exists_toCochain_eq (c : (OModulePresheaf.ofModules π M).cochain K 0)
    (hc : c ∈ (OModulePresheaf.ofModules π M).H0 K) : ∃ x : Γ(M, ⊤), toCochain π M K x = c

def

H0Equiv

L99 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.H0Equiv

Documentation

Degree-zero Cech cocycles identify with global sections of the module.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section H0
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)

Lean source · full declaration

def H0Equiv :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
    (OModulePresheaf.ofModules π M).H0 K ≃ₗ[R] Γ(M, ⊤) :=
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
  (LinearEquiv.ofBijective (LinearMap.codRestrict ((OModulePresheaf.ofModules π M).H0 K)
      (toCochain π M K) (toCochain_mem π M K))
    ⟨fun x y h => toCochain_injective π M K (congrArg Subtype.val h),
     fun ⟨c, hc⟩ => by
      obtain ⟨x, rfl⟩ := exists_toCochain_eq π M K c hc
      exact ⟨x, rfl⟩⟩).symm

def

sectionsEquivOfIso

L117 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.sectionsEquivOfIso

Documentation

The linear equivalence on global sections induced by a module isomorphism.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section Transport
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) {M N : V.Modules}

Lean source · full declaration

def sectionsEquivOfIso (e : M ≅ N) :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π N ⊤
    Γ(M, ⊤) ≃ₗ[R] Γ(N, ⊤) :=
  let := Scheme.TwoAffineOpenCover.algebraOfHom π ⊤
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π N ⊤
  { toFun := fun x => Scheme.Modules.Hom.app e.hom ⊤ x
    invFun := fun y => Scheme.Modules.Hom.app e.inv ⊤ y
    map_add' := fun x y => map_add _ x y
    map_smul' := fun r x => by
      change Scheme.Modules.Hom.app e.hom ⊤ ((algebraMap R Γ(V, ⊤) r) • x)
        = (algebraMap R Γ(V, ⊤) r) • Scheme.Modules.Hom.app e.hom ⊤ x
      exact Scheme.Modules.Hom.app_smul _ _ _
    left_inv := fun x => by
      change (Scheme.Modules.Hom.app e.hom ⊤ ≫ Scheme.Modules.Hom.app e.inv ⊤) x = x
      rw [← Scheme.Modules.Hom.comp_app, e.hom_inv_id, Scheme.Modules.Hom.id_app]; rfl
    right_inv := fun y => by
      change (Scheme.Modules.Hom.app e.inv ⊤ ≫ Scheme.Modules.Hom.app e.hom ⊤) y = y
      rw [← Scheme.Modules.Hom.comp_app, e.inv_hom_id, Scheme.Modules.Hom.id_app]; rfl }

def

unitSectionsEquiv

L139 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.unitSectionsEquiv

Documentation

Global sections of the unit module identify with functions on the scheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section Transport
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) {M N : V.Modules}

Lean source · full declaration

def unitSectionsEquiv :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π (SheafOfModules.unit V.ringCatSheaf) ⊤
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π ⊤
    Γ(SheafOfModules.unit V.ringCatSheaf, ⊤) ≃ₗ[R] Γ(V, ⊤) :=
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π (SheafOfModules.unit V.ringCatSheaf) ⊤
  let := Scheme.TwoAffineOpenCover.algebraOfHom π ⊤
  { toFun := fun x => (show Γ(V, ⊤) from x)
    invFun := fun y => (show Γ(SheafOfModules.unit V.ringCatSheaf, ⊤) from y)
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }

theorem

bijective_algebraMap_of_linearEquiv

L154 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.bijective_algebraMap_of_linearEquiv

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField

Lean source · statement

theorem bijective_algebraMap_of_linearEquiv {A S : Type*} [CommRing A] [CommRing S] [Algebra A S]
    (e : S ≃ₗ[A] A) : Function.Bijective (algebraMap A S)

theorem

main

L191 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field.P2mH0BaseChangeField.main

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
  TensorProduct
namespace P2mH0BaseChangeField
section Main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover

Lean source · full declaration

theorem main (k : Type u) [Field k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [QuasiCompact π]
    (hX : letI := Scheme.TwoAffineOpenCover.algebraOfHom π ⊤
      Function.Bijective (algebraMap k Γ(X, ⊤)))
    (A : Type u) [CommRing A] [Algebra k A] :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom
      (Limits.pullback.snd π (Scheme.TwoAffineOpenCover.specMap k A)) ⊤
    Function.Bijective (algebraMap A Γ(Limits.pullback π (Scheme.TwoAffineOpenCover.specMap k A),
      ⊤)) := by
  have : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace π
  let 𝒰 := coverOfCompact X
  let 𝒪 : X.Modules := SheafOfModules.unit X.ringCatSheaf
  let p₁ := Limits.pullback.fst π (specMap k A)
  let p₂ := Limits.pullback.snd π (specMap k A)
  have htriv : ∀ x : X, ∃ V : X.Opens, x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj 𝒪 ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
        :=
    fun x => ⟨⊤, trivial, ⟨Scheme.Modules.pullbackUnitIso _⟩⟩
  obtain ⟨-, hflat⟩ := OModulePresheaf.nonempty_cech_baseChange_equiv_of_locallyTrivial π 𝒰 𝒪
    htriv A
  obtain ⟨⟨e1⟩, -⟩ := hflat inferInstance
  let := Scheme.TwoAffineOpenCover.algebraOfHom π ⊤
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π 𝒪 ⊤
  let := Scheme.TwoAffineOpenCover.algebraOfHom p₂ ⊤
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom p₂ ((Scheme.Modules.pullback p₁).obj 𝒪) ⊤
  let := Scheme.TwoAffineOpenCover.moduleSectionsOfHom p₂
    (SheafOfModules.unit (Limits.pullback π (specMap k A)).ringCatSheaf) ⊤
  let e2 : (OModulePresheaf.ofModules π 𝒪).H0 𝒰 ≃ₗ[k] k :=
    (H0Equiv π 𝒪 𝒰).trans ((unitSectionsEquiv π).trans
      (LinearEquiv.ofBijective (Algebra.linearMap k Γ(X, ⊤)) hX).symm)
  let e3 : A ⊗[k] (OModulePresheaf.ofModules π 𝒪).H0 𝒰 ≃ₗ[A] A :=
    (e2.baseChange k A _ _).trans (AlgebraTensorModule.rid k A A)
  let e4 := (H0Equiv p₂ ((Scheme.Modules.pullback p₁).obj 𝒪) (𝒰.baseChange π A)).trans
    ((sectionsEquivOfIso p₂ (Scheme.Modules.pullbackUnitIso p₁)).trans (unitSectionsEquiv p₂))
  exact bijective_algebraMap_of_linearEquiv (e4.symm.trans (e1.trans e3))

theorem

bijective_algebraMap_sections_baseChange_of_bijective_of_field

L234 ↗

AlgebraicGeometry.Scheme.bijective_algebraMap_sections_baseChange_of_bijective_of_field

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_algebraMap_sections_baseChange_of_bijective_of_field
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in

Lean source · full declaration

theorem
  _root_.AlgebraicGeometry.Scheme.bijective_algebraMap_sections_baseChange_of_bijective_of_field
    (k : Type u) [Field k] {X : Scheme.{u}} (π : X ⟶ Spec (CommRingCat.of k))
    [IsSeparated π] [QuasiCompact π]
    (hX : letI := Scheme.TwoAffineOpenCover.algebraOfHom π ⊤
      Function.Bijective (algebraMap k Γ(X, ⊤)))
    (A : Type u) [CommRing A] [Algebra k A] :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom
      (Limits.pullback.snd π (Scheme.TwoAffineOpenCover.specMap k A)) ⊤
    Function.Bijective (algebraMap A Γ(Limits.pullback π (Scheme.TwoAffineOpenCover.specMap k A),
      ⊤)) :=
  P2mH0BaseChangeField.main k π hX A

Module documentation

Global sections after base change from a field

Declarations