NYLL
Module

Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
10 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules geom Fibre H0 Finrank eq of is Pullback

Imports5
Imported by4

Declarations

lemma

map_map

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.map_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma map_map {O₁ O₂ O₃ : Y.Opens} (f : O₂ ⟶ O₁) (g : O₃ ⟶ O₂) (c : Γ(Y, O₁)) :
    Y.presheaf.map g.op (Y.presheaf.map f.op c) = Y.presheaf.map (g ≫ f).op c
lemma

map_irrel

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.map_irrel
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma map_irrel {O₁ O₂ : Y.Opens} (f g : O₂ ⟶ O₁) (c : Γ(Y, O₁)) :
    Y.presheaf.map f.op c = Y.presheaf.map g.op c
lemma

mmap_mmap

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.mmap_mmap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma mmap_mmap (N : Y.Modules) {O₁ O₂ O₃ : Y.Opens} (f : O₂ ⟶ O₁) (g : O₃ ⟶ O₂) (c : Γ(N, O₁)) :
    N.presheaf.map g.op (N.presheaf.map f.op c) = N.presheaf.map (g ≫ f).op c
lemma

mmap_irrel

L80 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.mmap_irrel
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma mmap_irrel (N : Y.Modules) {O₁ O₂ : Y.Opens} (f g : O₂ ⟶ O₁) (c : Γ(N, O₁)) :
    N.presheaf.map f.op c = N.presheaf.map g.op c
lemma

image_top_of_isIso

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.image_top_of_isIso
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma image_top_of_isIso {P₂ P₁ : Scheme.{u}} (θ : P₂ ⟶ P₁) [IsIso θ] : θ ''ᵁ ⊤ = ⊤
def

iUp

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.iUp
Documentation

The inclusion of the top open subset into its image under a scheme isomorphism.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def iUp {P₂ P₁ : Scheme.{u}} (θ : P₂ ⟶ P₁) [IsIso θ] : (⊤ : P₁.Opens) ⟶ θ ''ᵁ ⊤
def

iDown

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.iDown
Documentation

The inclusion of the image of the top open subset into the top open subset.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def iDown {P₂ P₁ : Scheme.{u}} (θ : P₂ ⟶ P₁) [IsIso θ] : θ ''ᵁ ⊤ ⟶ (⊤ : P₁.Opens)
def

restrictTopEquiv

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.restrictTopEquiv
Documentation

The additive equivalence of global sections induced by restriction along a scheme isomorphism.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def restrictTopEquiv {P₂ P₁ : Scheme.{u}} (θ : P₂ ⟶ P₁) [IsIso θ] (N : P₁.Modules) :
    Γ(N.restrict θ, ⊤) ≃+ Γ(N, ⊤)
lemma

restrictTopEquiv_smul

L111 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback.AlgebraicGeometry.Scheme.Modules.H0CartesianAux.restrictTopEquiv_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace H0CartesianAux
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · full declaration
lemma restrictTopEquiv_smul {P₂ P₁ : Scheme.{u}} (θ : P₂ ⟶ P₁) [IsIso θ] (N : P₁.Modules)
    (r : Γ(P₁, ⊤)) (x : Γ(N.restrict θ, ⊤)) :
    restrictTopEquiv θ N ((θ.appLE ⊤ ⊤ (by simp)) r • x) = r • restrictTopEquiv θ N x := by
  change N.presheaf.map (iUp θ).op (((θ.appIso ⊤).inv (θ.appLE ⊤ ⊤
    (by simp) r)) • (show Γ(N, θ ''ᵁ ⊤) from x)) =
    r • N.presheaf.map (iUp θ).op (show Γ(N, θ ''ᵁ ⊤) from x)
  rw [Scheme.Modules.map_smul]
  congr 1
  change (θ.appLE ⊤ ⊤ (by simp) ≫ (θ.appIso ⊤).inv ≫ P₁.presheaf.map (iUp θ).op) r = r
  erw [Scheme.Hom.appLE_appIso_inv_assoc θ (U := ⊤) (V := ⊤) le_top, ← Functor.map_comp, ← op_comp,
    Subsingleton.elim (_ ≫ _) (𝟙 _), op_id,
    CategoryTheory.Functor.map_id]
  rfl
theorem

geomFibreH0Finrank_eq_of_isPullback

L128 ↗
AlgebraicGeometry.Scheme.Modules.geomFibreH0Finrank_eq_of_isPullback
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_eq_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules.H0CartesianAux in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.geomFibreH0Finrank_eq_of_isPullback
    {S S' : Type u} [CommRing S] [CommRing S'] (φ : S →+* S')
    {X A' : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of S)) (f' : A' ⟶ Spec (CommRingCat.of S'))
    (c : A' ⟶ X) (hc : IsPullback c f' f (Spec.map (CommRingCat.ofHom φ)))
    (M : X.Modules) (M' : A'.Modules) (e : (Scheme.Modules.pullback c).obj M ≅ M')
    (K : Type u) [Field K] (sK : S' →+* K) :
    Scheme.Modules.geomFibreH0Finrank f' M' K sK = Scheme.Modules.geomFibreH0Finrank f M K (sK.comp
      φ)

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