NYLL
Module

Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
16 declarations indexed from sourceView source ↗

Module documentation

Transporting two-chart cohomology along a scheme isomorphism

A scheme isomorphism and a compatible module isomorphism transport a two-affine-open cover and give linear equivalences on its zeroth and first section cohomology.

Imports2
Imported by74

Declarations

theorem

h0h1_of_equiv

L52 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.h0h1_of_equiv
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Generic
variable {R : Type u} [CommRing R] {𝒰 𝒰' : TwoChartCech.Cover.{u, u} R}
  (S : TwoChartCech.Sections.{u, u, u} 𝒰) (S' : TwoChartCech.Sections.{u, u, u} 𝒰')
Lean source · statement
theorem h0h1_of_equiv (g0 : S.M0 ≃ₗ[R] S'.M0) (g1 : S.M1 ≃ₗ[R] S'.M1) (g01 : S.M01 ≃ₗ[R] S'.M01)
    (h0 : ∀ m, S'.r0 (g0 m) = g01 (S.r0 m)) (h1 : ∀ m, S'.r1 (g1 m) = g01 (S.r1 m)) :
    Nonempty (S.H0 ≃ₗ[R] S'.H0) ∧ Nonempty (S.H1 ≃ₗ[R] S'.H1)
def

appEquiv

L87 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.appEquiv
Documentation

The linear equivalence on sections induced by the module isomorphism ψ.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section ModuleIso
variable {R : Type u} [CommRing R] {X' : Scheme.{u}} (𝒱' : X'.TwoAffineOpenCover)
  (x' : X' ⟶ Spec (.of R)) {M' P : X'.Modules} (ψ : M' ≅ P)
Lean source · full declaration
def appEquiv (U : X'.Opens) :
    letI := moduleSectionsOfHom x' M' U; letI := moduleSectionsOfHom x' P U
    Γ(M', U) ≃ₗ[R] Γ(P, U) :=
  letI := moduleSectionsOfHom x' M' U; letI := moduleSectionsOfHom x' P U
  letI := algebraOfHom x' U
  { toFun := fun m => ψ.hom.app U m
    invFun := fun m => ψ.inv.app U m
    map_add' := fun a b => map_add _ a b
    map_smul' := fun r m => by
      change ψ.hom.app U ((algebraMap R Γ(X', U) r) • m) = (algebraMap R Γ(X', U) r) • ψ.hom.app U m
      exact Scheme.Modules.Hom.app_smul _ _ _
    left_inv := fun m => by
      change (ψ.hom.app U ≫ ψ.inv.app U) m = m
      rw [← Scheme.Modules.Hom.comp_app, ψ.hom_inv_id, Scheme.Modules.Hom.id_app]; rfl
    right_inv := fun m => by
      change (ψ.inv.app U ≫ ψ.hom.app U) m = m
      rw [← Scheme.Modules.Hom.comp_app, ψ.inv_hom_id, Scheme.Modules.Hom.id_app]; rfl }
theorem

appEquiv_apply

L105 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.appEquiv_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section ModuleIso
variable {R : Type u} [CommRing R] {X' : Scheme.{u}} (𝒱' : X'.TwoAffineOpenCover)
  (x' : X' ⟶ Spec (.of R)) {M' P : X'.Modules} (ψ : M' ≅ P)
Lean source · full declaration
theorem appEquiv_apply (U : X'.Opens) (m : Γ(M', U)) :
    letI := moduleSectionsOfHom x' M' U; letI := moduleSectionsOfHom x' P U
    appEquiv x' ψ U m = ψ.hom.app U m := rfl
theorem

app_res

L109 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.app_res
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section ModuleIso
variable {R : Type u} [CommRing R] {X' : Scheme.{u}} (𝒱' : X'.TwoAffineOpenCover)
  (x' : X' ⟶ Spec (.of R)) {M' P : X'.Modules} (ψ : M' ≅ P)
Lean source · statement
theorem app_res {U V : X'.Opens} (i : V ⟶ U) (m : Γ(M', U)) :
    ψ.hom.app V (M'.presheaf.map i.op m) = P.presheaf.map i.op (ψ.hom.app U m)
theorem

of_moduleIso

L117 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.of_moduleIso
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section ModuleIso
variable {R : Type u} [CommRing R] {X' : Scheme.{u}} (𝒱' : X'.TwoAffineOpenCover)
  (x' : X' ⟶ Spec (.of R)) {M' P : X'.Modules} (ψ : M' ≅ P)
include ψ in
Lean source · statement
theorem of_moduleIso :
    Nonempty ((𝒱'.sectionsOf x' M').H0 ≃ₗ[R] (𝒱'.sectionsOf x' P).H0) ∧
      Nonempty ((𝒱'.sectionsOf x' M').H1 ≃ₗ[R] (𝒱'.sectionsOf x' P).H1)
def

preimageCover

L140 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.preimageCover
Documentation

The two-affine-open cover obtained by inverse image along the scheme isomorphism φ.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Push
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (.of R)) (x' : X' ⟶ Spec
    (.of R))
  (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M : X.Modules)
Lean source · full declaration
def preimageCover : X.TwoAffineOpenCover where
  U0 := φ.hom ⁻¹ᵁ 𝒱'.U0
  U1 := φ.hom ⁻¹ᵁ 𝒱'.U1
  isAffineOpen_U0 := 𝒱'.isAffineOpen_U0.preimage_of_isIso φ.hom
  isAffineOpen_U1 := 𝒱'.isAffineOpen_U1.preimage_of_isIso φ.hom
  sup_eq_top := by
    change φ.hom ⁻¹ᵁ (𝒱'.U0 ⊔ 𝒱'.U1) = ⊤
    rw [𝒱'.sup_eq_top]; rfl
  isAffineOpen_inf := by
    change IsAffineOpen (φ.hom ⁻¹ᵁ (𝒱'.U0 ⊓ 𝒱'.U1))
    exact 𝒱'.isAffineOpen_inf.preimage_of_isIso φ.hom
theorem

preimageCover_U0

L152 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.preimageCover_U0
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Push
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (.of R)) (x' : X' ⟶ Spec
    (.of R))
  (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M : X.Modules)
Lean source · statement
theorem preimageCover_U0 : (preimageCover φ 𝒱').U0 = φ.hom ⁻¹ᵁ 𝒱'.U0
theorem

preimageCover_U1

L153 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.preimageCover_U1
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Push
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (.of R)) (x' : X' ⟶ Spec
    (.of R))
  (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M : X.Modules)
Lean source · statement
theorem preimageCover_U1 : (preimageCover φ 𝒱').U1 = φ.hom ⁻¹ᵁ 𝒱'.U1
theorem

scalar_eq

L156 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.scalar_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Push
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (.of R)) (x' : X' ⟶ Spec
    (.of R))
  (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M : X.Modules)
include hφ in
Lean source · statement
theorem scalar_eq (U : X'.Opens) (r : R) :
    (algebraOfHom x (φ.hom ⁻¹ᵁ U)).algebraMap r = φ.hom.app U ((algebraOfHom x' U).algebraMap r)
def

pushEquivSections

L166 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.pushEquivSections
Documentation

Identify sections on inverse images with sections of the pushforward module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Push
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (.of R)) (x' : X' ⟶ Spec
    (.of R))
  (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M : X.Modules)
Lean source · full declaration
def pushEquivSections (U : X'.Opens) :
    letI := moduleSectionsOfHom x M (φ.hom ⁻¹ᵁ U)
    letI := moduleSectionsOfHom x' ((Scheme.Modules.pushforward φ.hom).obj M) U
    Γ(M, φ.hom ⁻¹ᵁ U) ≃ₗ[R] Γ((Scheme.Modules.pushforward φ.hom).obj M, U) :=
  letI := moduleSectionsOfHom x M (φ.hom ⁻¹ᵁ U)
  letI := moduleSectionsOfHom x' ((Scheme.Modules.pushforward φ.hom).obj M) U
  { toFun := fun m => (show Γ((Scheme.Modules.pushforward φ.hom).obj M, U) from m)
    invFun := fun m => (show Γ(M, φ.hom ⁻¹ᵁ U) from m)
    map_add' := fun a b => rfl
    map_smul' := fun r m => by
      let := algebraOfHom x (φ.hom ⁻¹ᵁ U); let := algebraOfHom x' U
      change (algebraMap R Γ(X, φ.hom ⁻¹ᵁ U) r) • m
        = (φ.hom.app U (algebraMap R Γ(X', U) r)) • (show Γ(M, φ.hom ⁻¹ᵁ U) from m)
      congr 1
      exact scalar_eq x x' φ hφ U r
    left_inv := fun m => rfl
    right_inv := fun m => rfl }
theorem

of_pushforward

L185 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.of_pushforward
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Push
variable {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (.of R)) (x' : X' ⟶ Spec
    (.of R))
  (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M : X.Modules)
include hφ in
Lean source · statement
theorem of_pushforward :
    Nonempty (((preimageCover φ 𝒱').sectionsOf x M).H0 ≃ₗ[R]
        (𝒱'.sectionsOf x' ((Scheme.Modules.pushforward φ.hom).obj M)).H0) ∧
      Nonempty (((preimageCover φ 𝒱').sectionsOf x M).H1 ≃ₗ[R]
        (𝒱'.sectionsOf x' ((Scheme.Modules.pushforward φ.hom).obj M)).H1)
def

pushEquiv

L213 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.pushEquiv
Documentation

The equivalence of scheme-module categories induced by pushforward along φ and its inverse.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Adj
variable {X X' : Scheme.{u}} (φ : X ≅ X')
Lean source · statement
def pushEquiv : X.Modules ≌ X'.Modules
def

pullbackIsoPushforwardInv

L222 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.pullbackIsoPushforwardInv
Documentation

Identify pullback along φ with pushforward along its inverse using their adjunctions.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Adj
variable {X X' : Scheme.{u}} (φ : X ≅ X')
Lean source · statement
def pullbackIsoPushforwardInv :
    Scheme.Modules.pullback φ.hom ≅ Scheme.Modules.pushforward φ.inv
def

isoPushforward

L228 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.isoPushforward
Documentation

The isomorphism to the pushforward module induced by an isomorphism to the pullback.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Adj
variable {X X' : Scheme.{u}} (φ : X ≅ X')
Lean source · statement
def isoPushforward (M' : X'.Modules) (M : X.Modules)
    (e : M ≅ (Scheme.Modules.pullback φ.hom).obj M') :
    M' ≅ (Scheme.Modules.pushforward φ.hom).obj M
theorem

main

L236 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso.AlgebraicGeometry.Scheme.TwoAffineOpenCover.Trans.main
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace Trans
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem main
    {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of R)) (x' : X' ⟶
        Spec (CommRingCat.of R))
    (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M' : X'.Modules) (M :
        X.Modules)
    (e : M ≅ (Scheme.Modules.pullback φ.hom).obj M') :
    ∃ 𝒱 : X.TwoAffineOpenCover, 𝒱.U0 = φ.hom ⁻¹ᵁ 𝒱'.U0 ∧ 𝒱.U1 = φ.hom ⁻¹ᵁ 𝒱'.U1 ∧
      Nonempty ((𝒱.sectionsOf x M).H0 ≃ₗ[R] (𝒱'.sectionsOf x' M').H0) ∧
      Nonempty ((𝒱.sectionsOf x M).H1 ≃ₗ[R] (𝒱'.sectionsOf x' M').H1)
theorem

exists_linearEquiv_sectionsOf_of_iso

L251 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_linearEquiv_sectionsOf_of_iso
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_exists_linearEquiv_sectionsOf_of_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_linearEquiv_sectionsOf_of_iso
    {R : Type u} [CommRing R] {X X' : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of R)) (x' : X' ⟶
        Spec (CommRingCat.of R))
    (φ : X ≅ X') (hφ : φ.hom ≫ x' = x) (𝒱' : X'.TwoAffineOpenCover) (M' : X'.Modules) (M :
        X.Modules)
    (e : M ≅ (Scheme.Modules.pullback φ.hom).obj M') :
    ∃ 𝒱 : X.TwoAffineOpenCover, 𝒱.U0 = φ.hom ⁻¹ᵁ 𝒱'.U0 ∧ 𝒱.U1 = φ.hom ⁻¹ᵁ 𝒱'.U1 ∧
      Nonempty ((𝒱.sectionsOf x M).H0 ≃ₗ[R] (𝒱'.sectionsOf x' M').H0) ∧
      Nonempty ((𝒱.sectionsOf x M).H1 ≃ₗ[R] (𝒱'.sectionsOf x' M').H1)

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