NYLL
Module

TwoAffineOpenCoverH1BaseChange.lean

Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverH1BaseChange
32 declarations indexed from sourceView source ↗

Module documentation

Two Affine Open Cover H1Base Change

Imports1
Imported by16

Declarations

structure

HomOver

L30 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver
Documentation

A morphism of two affine covers compatible with the indicated map of base rings.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
Lean source · full declaration
structure HomOver (τ : R →+* S) {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    {Y : Scheme.{u}} (𝒲 : Y.TwoAffineOpenCover) (c' : Y ⟶ Spec (.of S)) where
  /-- The underlying morphism of schemes. -/
  hom : Y ⟶ X
  /-- Compatibility with the structure morphisms to the affine bases. -/
  comm : hom ≫ c = c' ≫ Spec.map (CommRingCat.ofHom τ)
  /-- The first chart maps into the first chart of the target cover. -/
  U0_le : 𝒲.U0 ≤ hom ⁻¹ᵁ 𝒱.U0
  /-- The second chart maps into the second chart of the target cover. -/
  U1_le : 𝒲.U1 ≤ hom ⁻¹ᵁ 𝒱.U1
theorem

inf_le

L46 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.inf_le
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem inf_le : 𝒲.U0 ⊓ 𝒲.U1 ≤ f.hom ⁻¹ᵁ (𝒱.U0 ⊓ 𝒱.U1)
theorem

appLE_algebraMap

L49 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.appLE_algebraMap
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem appLE_algebraMap {U : X.Opens} {V : Y.Opens} (h : V ≤ f.hom ⁻¹ᵁ U) (r : R) :
    (f.hom.appLE U V h).hom ((algebraOfHom c U).algebraMap r) = (algebraOfHom c' V).algebraMap (τ
      r)
def

sectionsMap

L82 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.sectionsMap
Documentation

The semilinear restriction of sections along the morphism on the specified opens.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · full declaration
def sectionsMap {U : X.Opens} {V : Y.Opens} (h : V ≤ f.hom ⁻¹ᵁ U) :
    letI := algebraOfHom c U; letI := algebraOfHom c' V
    Γ(X, U) →ₛₗ[τ] Γ(Y, V) :=
  letI := algebraOfHom c U; letI := algebraOfHom c' V
  { toFun := (f.hom.appLE U V h).hom
    map_add' := fun x y => map_add _ x y
    map_smul' := fun r x => by
      change (f.hom.appLE U V h).hom ((algebraOfHom c U).algebraMap r * x) =
        (algebraOfHom c' V).algebraMap (τ r) * (f.hom.appLE U V h).hom x
      rw [map_mul, appLE_algebraMap] }
def

map0

L94 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map0
Documentation

The induced semilinear map on sections over the first chart.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
def map0 : (𝒱.cover c).A0 →ₛₗ[τ] (𝒲.cover c').A0
def

map1

L97 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map1
Documentation

The induced semilinear map on sections over the second chart.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
def map1 : (𝒱.cover c).A1 →ₛₗ[τ] (𝒲.cover c').A1
def

map01

L100 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map01
Documentation

The induced semilinear map on sections over the chart intersection.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
def map01 : (𝒱.cover c).A01 →ₛₗ[τ] (𝒲.cover c').A01
theorem

map0_apply

L102 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map0_apply
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem map0_apply (x : (𝒱.cover c).A0) : f.map0 x = (f.hom.appLE 𝒱.U0 𝒲.U0 f.U0_le).hom x
theorem

map1_apply

L103 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map1_apply
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem map1_apply (x : (𝒱.cover c).A1) : f.map1 x = (f.hom.appLE 𝒱.U1 𝒲.U1 f.U1_le).hom x
theorem

map01_apply

L104 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map01_apply
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem map01_apply (x : (𝒱.cover c).A01) :
    f.map01 x = (f.hom.appLE (𝒱.U0 ⊓ 𝒱.U1) (𝒲.U0 ⊓ 𝒲.U1) f.inf_le).hom x
theorem

map01_ρ0

L107 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map01_ρ0
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem map01_ρ0 (x : (𝒱.cover c).A0) : f.map01 ((𝒱.cover c).ρ0 x) = (𝒲.cover c').ρ0 (f.map0 x)
theorem

map01_ρ1

L122 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map01_ρ1
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem map01_ρ1 (x : (𝒱.cover c).A1) : f.map01 ((𝒱.cover c).ρ1 x) = (𝒲.cover c').ρ1 (f.map1 x)
theorem

map01_cechDiff

L137 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.map01_cechDiff
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem map01_cechDiff (s : (𝒱.cover c).A0 × (𝒱.cover c).A1) :
    f.map01 ((𝒱.structureSheafSections c).cechDiff s) =
      (𝒲.structureSheafSections c').cechDiff (f.map0 s.1, f.map1 s.2)
theorem

range_cechDiff_le_comap

L145 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.range_cechDiff_le_comap
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem range_cechDiff_le_comap :
    LinearMap.range (𝒱.structureSheafSections c).cechDiff ≤
      (LinearMap.range (𝒲.structureSheafSections c').cechDiff).comap f.map01
def

H1map

L153 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.H1map
Documentation

The induced map on the first Cech cohomology of the structure sheaf.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
def H1map : (𝒱.structureSheafSections c).H1 →ₛₗ[τ] (𝒲.structureSheafSections c').H1
theorem

H1map_mk

L156 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.H1map_mk
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem H1map_mk (y : (𝒱.cover c).A01) :
    f.H1map (Submodule.Quotient.mk y) = Submodule.Quotient.mk (f.map01 y)
theorem

H1map_congr

L159 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.H1map_congr
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem H1map_congr {τ' : R →+* S} {f : HomOver τ 𝒱 c 𝒲 c'} {g : HomOver τ' 𝒱 c 𝒲 c'} (h : f.hom =
  g.hom)
    (x : (𝒱.structureSheafSections c).H1) : f.H1map x = g.H1map x
def

id

L169 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id
Documentation

The identity morphism of an affine cover over its base ring.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · full declaration
def id (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) : HomOver (RingHom.id R) 𝒱 c 𝒱
  c where
  hom := 𝟙 X
  comm := by
    change 𝟙 X ≫ c = c ≫ Spec.map (𝟙 _)
    rw [Spec.map_id, Category.id_comp, Category.comp_id]
  U0_le := le_rfl
  U1_le := le_rfl
theorem

id_H1map

L178 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_H1map
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem id_H1map (x : (𝒱.structureSheafSections c).H1) : (HomOver.id 𝒱 c).H1map x = x
def

comp

L191 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp
Documentation

Composition of morphisms of affine covers over composable base ring maps.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · full declaration
def comp {υ : S →+* T} {Z : Scheme.{u}} {𝒳 : Z.TwoAffineOpenCover} {c'' : Z ⟶ Spec (.of T)}
    (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') : HomOver (υ.comp τ) 𝒱 c 𝒳 c'' where
  hom := g.hom ≫ f.hom
  comm := by
    rw [Category.assoc, f.comm, ← Category.assoc, g.comm, Category.assoc, ← Spec.map_comp]
    rfl
  U0_le := g.U0_le.trans
    (by rw [Scheme.Hom.comp_preimage]; exact Scheme.Hom.preimage_mono _ f.U0_le)
  U1_le := g.U1_le.trans
    (by rw [Scheme.Hom.comp_preimage]; exact Scheme.Hom.preimage_mono _ f.U1_le)
theorem

comp_H1map

L202 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_H1map
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
namespace HomOver
variable {τ : R →+* S} {X : Scheme.{u}} {𝒱 : X.TwoAffineOpenCover} {c : X ⟶ Spec (.of R)}
  {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover} {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
Lean source · statement
theorem comp_H1map {υ : S →+* T} {Z : Scheme.{u}} {𝒳 : Z.TwoAffineOpenCover} {c'' : Z ⟶ Spec (.of
  T)}
    (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') (x : (𝒱.structureSheafSections c).H1) :
    (g.comp f).H1map x = g.H1map (f.H1map x)
def

baseChange

L230 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.baseChange
Documentation

The projection from the affine cover obtained by base change.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
Lean source · full declaration
def HomOver.baseChange :
    HomOver (algebraMap R A) 𝒱 c (𝒱.pullback c A) (pullback.snd c (specMap R A)) where
  hom := pullback.fst c (specMap R A)
  comm := pullback.condition
  U0_le := le_rfl
  U1_le := le_rfl
def

stage

L238 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.stage
Documentation

The morphism between base changed covers induced by an algebra homomorphism.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
Lean source · full declaration
def HomOver.stage (g : A →ₐ[R] B) :
    HomOver g.toRingHom (𝒱.pullback c A) (pullback.snd c (specMap R A))
      (𝒱.pullback c B) (pullback.snd c (specMap R B)) where
  hom := RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom R g)
  comm := pullback.lift_snd _ _ _
  U0_le := (baseChangeSnd_preimage_U0 𝒱 c (RelPicard.LFP.stageHom R g)).ge
  U1_le := (baseChangeSnd_preimage_U1 𝒱 c (RelPicard.LFP.stageHom R g)).ge
def

H1baseChangeMap

L248 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1baseChangeMap
Documentation

The semilinear map on first Cech cohomology induced by base change.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
def H1baseChangeMap : (𝒱.structureSheafSections c).H1 →ₛₗ[algebraMap R A]
    ((𝒱.pullback c A).structureSheafSections (pullback.snd c (specMap R A))).H1
def

H1stageMap

L253 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1stageMap
Documentation

The semilinear map on first Cech cohomology induced by a map of base algebras.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
def H1stageMap (g : A →ₐ[R] B) :
    ((𝒱.pullback c A).structureSheafSections (pullback.snd c (specMap R A))).H1 →ₛₗ[g.toRingHom]
      ((𝒱.pullback c B).structureSheafSections (pullback.snd c (specMap R B))).H1
theorem

baseChange_map01_apply

L258 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.baseChange_map01_apply
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem baseChange_map01_apply (y : (𝒱.cover c).A01) :
    (HomOver.baseChange 𝒱 c A).map01 y = ((pullback.fst c (specMap R A)).app (𝒱.U0 ⊓ 𝒱.U1)).hom y
theorem

H1baseChangeMap_mk

L264 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1baseChangeMap_mk
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem H1baseChangeMap_mk (y : (𝒱.cover c).A01) :
    H1baseChangeMap 𝒱 c A (Submodule.Quotient.mk y) =
      Submodule.Quotient.mk ((HomOver.baseChange 𝒱 c A).map01 y)
theorem

stage_map01_apply

L268 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.stage_map01_apply
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem stage_map01_apply (g : A →ₐ[R] B) (f : ((𝒱.pullback c A).cover (pullback.snd c (specMap R
  A))).A01) :
    (HomOver.stage 𝒱 c g).map01 f =
      ((RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom R g)).appLE
        ((𝒱.pullback c A).U0 ⊓ (𝒱.pullback c A).U1) ((𝒱.pullback c B).U0 ⊓ (𝒱.pullback c B).U1)
        (HomOver.stage 𝒱 c g).inf_le).hom f
theorem

H1stageMap_mk

L275 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1stageMap_mk
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem H1stageMap_mk (g : A →ₐ[R] B) (f : ((𝒱.pullback c A).cover (pullback.snd c (specMap R
  A))).A01) :
    H1stageMap 𝒱 c g (Submodule.Quotient.mk f) = Submodule.Quotient.mk ((HomOver.stage 𝒱 c
      g).map01 f)
theorem

H1stageMap_H1baseChangeMap

L280 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1stageMap_H1baseChangeMap
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem H1stageMap_H1baseChangeMap (g : A →ₐ[R] B) (x : (𝒱.structureSheafSections c).H1) :
    H1stageMap 𝒱 c g (H1baseChangeMap 𝒱 c A x) = H1baseChangeMap 𝒱 c B x
theorem

H1stageMap_id

L285 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1stageMap_id
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem H1stageMap_id (x : ((𝒱.pullback c A).structureSheafSections (pullback.snd c (specMap R
  A))).H1) :
    H1stageMap 𝒱 c (AlgHom.id R A) x = x
theorem

H1stageMap_comp

L298 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1stageMap_comp
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite NeronModelInfra
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {S : Type u} [CommRing S] {T : Type u} [CommRing T]
section BaseChange
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
  {A : Type u} [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
  {B' : Type u} [CommRing B'] [Algebra R B']
variable (A) in
variable (A) in
Lean source · statement
theorem H1stageMap_comp (g : A →ₐ[R] B) (g' : B →ₐ[R] B')
    (x : ((𝒱.pullback c A).structureSheafSections (pullback.snd c (specMap R A))).H1) :
    H1stageMap 𝒱 c g' (H1stageMap 𝒱 c g x) = H1stageMap 𝒱 c (g'.comp g) x

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