Module

TwoAffineOpenCoverKaehler.lean

Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverKaehler

80 declarations indexed from sourceView source ↗

Module documentation

Kähler differentials and their Čech data on a two-affine-open cover.

Imports2

Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverH1BaseChange
Mathlib.RingTheory.Kaehler.Basic

Imported by9

def

mapOfRingHom

L33 ↗

KaehlerDifferential.mapOfRingHom

Documentation

The semilinear map on Kähler differentials induced by compatible ring homomorphisms.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]

Lean source · statement

def mapOfRingHom (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp
  τ) :
    Ω[A⁄R] →ₛₗ[τ] Ω[B⁄S]

theorem

mapOfRingHom_D

L55 ↗

KaehlerDifferential.mapOfRingHom_D

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)

Lean source · statement

theorem mapOfRingHom_D (a : A) : mapOfRingHom τ φ h (D R A a) = D S B (φ a)

theorem

mapOfRingHom_smul

L67 ↗

KaehlerDifferential.mapOfRingHom_smul

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)

Lean source · statement

theorem mapOfRingHom_smul (a : A) (ω : Ω[A⁄R]) : mapOfRingHom τ φ h (a • ω) = φ a • mapOfRingHom τ
  φ h ω

theorem

mapOfRingHom_smul_D

L80 ↗

KaehlerDifferential.mapOfRingHom_smul_D

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)

Lean source · statement

theorem mapOfRingHom_smul_D (a a' : A) : mapOfRingHom τ φ h (a • D R A a') = φ a • D S B (φ a')

theorem

addMonoidHom_ext_smul_D

L85 ↗

KaehlerDifferential.addMonoidHom_ext_smul_D

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)
omit [Algebra S B] in

Lean source · statement

theorem addMonoidHom_ext_smul_D {M : Type*} [AddCommGroup M] {f g : Ω[A⁄R] →+ M}
    (hfg : ∀ a a' : A, f (a • D R A a') = g (a • D R A a')) : f = g

theorem

mapOfRingHom_congr

L93 ↗

KaehlerDifferential.mapOfRingHom_congr

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)

Lean source · statement

theorem mapOfRingHom_congr {τ τ' : R →+* S} {φ φ' : A →+* B} (hφ : φ = φ')
    (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ) (h' : φ'.comp (algebraMap R A) =
      (algebraMap S B).comp τ')
    (ω : Ω[A⁄R]) : mapOfRingHom τ φ h ω = mapOfRingHom τ' φ' h' ω

theorem

mapOfRingHom_id

L105 ↗

KaehlerDifferential.mapOfRingHom_id

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)
omit [Algebra S B] in

Lean source · statement

theorem mapOfRingHom_id (h : (RingHom.id A).comp (algebraMap R A) = (algebraMap R A).comp
  (RingHom.id R))
    (ω : Ω[A⁄R]) : mapOfRingHom (RingHom.id R) (RingHom.id A) h ω = ω

theorem

mapOfRingHom_comp_apply

L115 ↗

KaehlerDifferential.mapOfRingHom_comp_apply

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)

Lean source · statement

theorem mapOfRingHom_comp_apply {T : Type*} {C : Type*} [CommRing T] [CommRing C] [Algebra T C]
    (υ : S →+* T) (ψ : B →+* C) (h₂ : ψ.comp (algebraMap S B) = (algebraMap T C).comp υ)
    (h₃ : (ψ.comp φ).comp (algebraMap R A) = (algebraMap T C).comp (υ.comp τ)) (ω : Ω[A⁄R]) :
    mapOfRingHom υ ψ h₂ (mapOfRingHom τ φ h ω) = mapOfRingHom (υ.comp τ) (ψ.comp φ) h₃ ω

theorem

mapOfRingHom_apply_eq_map

L127 ↗

KaehlerDifferential.mapOfRingHom_apply_eq_map

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace KaehlerDifferential
variable {R : Type*} {S : Type*} {A : Type*} {B : Type*} [CommRing R] [CommRing S] [CommRing A]
  [CommRing B]
  [Algebra R A] [Algebra S B]
variable (τ : R →+* S) (φ : A →+* B) (h : φ.comp (algebraMap R A) = (algebraMap S B).comp τ)

Lean source · statement

theorem mapOfRingHom_apply_eq_map [Algebra R S] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    [IsScalarTower R S B] [SMulCommClass S A B] (hφ : algebraMap A B = φ) (ω : Ω[A⁄R]) :
    mapOfRingHom τ φ h ω = KaehlerDifferential.map R S A B ω

theorem

ρ0_comp_algebraMap_eq_comp_id

L144 ↗

TwoChartCech.Cover.ρ0_comp_algebraMap_eq_comp_id

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem ρ0_comp_algebraMap_eq_comp_id : 𝒰.ρ0.toRingHom.comp (algebraMap R 𝒰.A0) = (algebraMap R
  𝒰.A01).comp (RingHom.id R)

theorem

ρ1_comp_algebraMap_eq_comp_id

L147 ↗

TwoChartCech.Cover.ρ1_comp_algebraMap_eq_comp_id

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem ρ1_comp_algebraMap_eq_comp_id : 𝒰.ρ1.toRingHom.comp (algebraMap R 𝒰.A1) = (algebraMap R
  𝒰.A01).comp (RingHom.id R)

def

kaehler

L152 ↗

TwoChartCech.Cover.kaehler

Documentation

Kähler differential modules and restriction maps on the two affine charts.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · full declaration

def kaehler : Sections.{u, v, v} 𝒰 where
  M0 := Ω[𝒰.A0⁄R]
  M1 := Ω[𝒰.A1⁄R]
  M01 := Ω[𝒰.A01⁄R]
  r0 := KaehlerDifferential.mapOfRingHom (RingHom.id R) 𝒰.ρ0.toRingHom
    𝒰.ρ0_comp_algebraMap_eq_comp_id
  r1 := KaehlerDifferential.mapOfRingHom (RingHom.id R) 𝒰.ρ1.toRingHom
    𝒰.ρ1_comp_algebraMap_eq_comp_id
  r0_smul a m := KaehlerDifferential.mapOfRingHom_smul _ _ 𝒰.ρ0_comp_algebraMap_eq_comp_id a m
  r1_smul a m := KaehlerDifferential.mapOfRingHom_smul _ _ 𝒰.ρ1_comp_algebraMap_eq_comp_id a m

theorem

kaehler_M0

L163 ↗

TwoChartCech.Cover.kaehler_M0

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_M0 : 𝒰.kaehler.M0 = Ω[𝒰.A0⁄R]

theorem

kaehler_M1

L164 ↗

TwoChartCech.Cover.kaehler_M1

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_M1 : 𝒰.kaehler.M1 = Ω[𝒰.A1⁄R]

theorem

kaehler_M01

L165 ↗

TwoChartCech.Cover.kaehler_M01

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_M01 : 𝒰.kaehler.M01 = Ω[𝒰.A01⁄R]

theorem

kaehler_r0_smul_D

L167 ↗

TwoChartCech.Cover.kaehler_r0_smul_D

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_r0_smul_D (a s : 𝒰.A0) :
    𝒰.kaehler.r0 (a • KaehlerDifferential.D R 𝒰.A0 s) = 𝒰.ρ0 a • KaehlerDifferential.D R 𝒰.A01
      (𝒰.ρ0 s)

theorem

kaehler_r1_smul_D

L171 ↗

TwoChartCech.Cover.kaehler_r1_smul_D

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_r1_smul_D (a s : 𝒰.A1) :
    𝒰.kaehler.r1 (a • KaehlerDifferential.D R 𝒰.A1 s) = 𝒰.ρ1 a • KaehlerDifferential.D R 𝒰.A01
      (𝒰.ρ1 s)

theorem

kaehler_r0_D

L175 ↗

TwoChartCech.Cover.kaehler_r0_D

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_r0_D (s : 𝒰.A0) : 𝒰.kaehler.r0 (KaehlerDifferential.D R 𝒰.A0 s) =
  KaehlerDifferential.D R 𝒰.A01 (𝒰.ρ0 s)

theorem

kaehler_r1_D

L178 ↗

TwoChartCech.Cover.kaehler_r1_D

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_r1_D (s : 𝒰.A1) : 𝒰.kaehler.r1 (KaehlerDifferential.D R 𝒰.A1 s) =
  KaehlerDifferential.D R 𝒰.A01 (𝒰.ρ1 s)

theorem

kaehler_cechDiff_D

L182 ↗

TwoChartCech.Cover.kaehler_cechDiff_D

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R] (𝒰 : Cover.{u, v} R)

Lean source · statement

theorem kaehler_cechDiff_D (s₀ : 𝒰.A0) (s₁ : 𝒰.A1) :
    𝒰.kaehler.cechDiff (KaehlerDifferential.D R 𝒰.A0 s₀, KaehlerDifferential.D R 𝒰.A1 s₁) =
      KaehlerDifferential.D R 𝒰.A01 (𝒰.structureSheaf.cechDiff (s₀, s₁))

abbrev

kaehlerSections

L198 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerSections

Documentation

The two-chart Čech section data for Kähler differentials.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))

Lean source · statement

abbrev kaehlerSections : TwoChartCech.Sections (𝒱.cover c)

def

ringHom0

L206 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom0

Documentation

The ring homomorphism on sections of the first chart.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def ringHom0 : (𝒱.cover c).A0 →+* (𝒲.cover c').A0

def

ringHom1

L208 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom1

Documentation

The ring homomorphism on sections of the second chart.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def ringHom1 : (𝒱.cover c).A1 →+* (𝒲.cover c').A1

def

ringHom01

L210 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom01

Documentation

The ring homomorphism on sections of the chart overlap.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def ringHom01 : (𝒱.cover c).A01 →+* (𝒲.cover c').A01

theorem

ringHom0_apply

L213 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom0_apply

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem ringHom0_apply (x : (𝒱.cover c).A0) : f.ringHom0 x = f.map0 x

theorem

ringHom1_apply

L214 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom1_apply

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem ringHom1_apply (x : (𝒱.cover c).A1) : f.ringHom1 x = f.map1 x

theorem

ringHom01_apply

L215 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom01_apply

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem ringHom01_apply (x : (𝒱.cover c).A01) : f.ringHom01 x = f.map01 x

theorem

ringHom0_comp_algebraMap

L217 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom0_comp_algebraMap

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem ringHom0_comp_algebraMap : f.ringHom0.comp (algebraMap R (𝒱.cover c).A0) = (algebraMap S
  (𝒲.cover c').A0).comp τ

theorem

ringHom1_comp_algebraMap

L220 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom1_comp_algebraMap

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem ringHom1_comp_algebraMap : f.ringHom1.comp (algebraMap R (𝒱.cover c).A1) = (algebraMap S
  (𝒲.cover c').A1).comp τ

theorem

ringHom01_comp_algebraMap

L223 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.ringHom01_comp_algebraMap

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem ringHom01_comp_algebraMap :
    f.ringHom01.comp (algebraMap R (𝒱.cover c).A01) = (algebraMap S (𝒲.cover c').A01).comp τ

def

kaehlerMap0

L228 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap0

Documentation

The induced semilinear map on differentials on the first chart.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def kaehlerMap0 : Ω[(𝒱.cover c).A0⁄R] →ₛₗ[τ] Ω[(𝒲.cover c').A0⁄S]

def

kaehlerMap1

L232 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap1

Documentation

The induced semilinear map on differentials on the second chart.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def kaehlerMap1 : Ω[(𝒱.cover c).A1⁄R] →ₛₗ[τ] Ω[(𝒲.cover c').A1⁄S]

def

kaehlerMap01

L236 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap01

Documentation

The induced semilinear map on differentials on the chart overlap.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def kaehlerMap01 : Ω[(𝒱.cover c).A01⁄R] →ₛₗ[τ] Ω[(𝒲.cover c').A01⁄S]

theorem

kaehlerMap0_smul_D

L239 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap0_smul_D

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap0_smul_D (a s : (𝒱.cover c).A0) :
    f.kaehlerMap0 (a • KaehlerDifferential.D R _ s) = f.map0 a • KaehlerDifferential.D S _ (f.map0
      s)

theorem

kaehlerMap1_smul_D

L243 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap1_smul_D

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap1_smul_D (a s : (𝒱.cover c).A1) :
    f.kaehlerMap1 (a • KaehlerDifferential.D R _ s) = f.map1 a • KaehlerDifferential.D S _ (f.map1
      s)

theorem

kaehlerMap01_smul_D

L247 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap01_smul_D

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap01_smul_D (a s : (𝒱.cover c).A01) :
    f.kaehlerMap01 (a • KaehlerDifferential.D R _ s) = f.map01 a • KaehlerDifferential.D S _
      (f.map01 s)

theorem

kaehlerMap01_r0

L252 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap01_r0

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap01_r0 (ω : Ω[(𝒱.cover c).A0⁄R]) :
    f.kaehlerMap01 ((𝒱.kaehlerSections c).r0 ω) = (𝒲.kaehlerSections c').r0 (f.kaehlerMap0 ω)

theorem

kaehlerMap01_r1

L263 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap01_r1

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap01_r1 (ω : Ω[(𝒱.cover c).A1⁄R]) :
    f.kaehlerMap01 ((𝒱.kaehlerSections c).r1 ω) = (𝒲.kaehlerSections c').r1 (f.kaehlerMap1 ω)

theorem

kaehlerMap01_cechDiff

L274 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap01_cechDiff

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap01_cechDiff (s : Ω[(𝒱.cover c).A0⁄R] × Ω[(𝒱.cover c).A1⁄R]) :
    f.kaehlerMap01 ((𝒱.kaehlerSections c).cechDiff s) =
      (𝒲.kaehlerSections c').cechDiff (f.kaehlerMap0 s.1, f.kaehlerMap1 s.2)

theorem

range_kaehler_cechDiff_le_comap

L281 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.range_kaehler_cechDiff_le_comap

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem range_kaehler_cechDiff_le_comap :
    LinearMap.range (𝒱.kaehlerSections c).cechDiff ≤
      (LinearMap.range (𝒲.kaehlerSections c').cechDiff).comap f.kaehlerMap01

theorem

kaehlerMap_mem_H0

L288 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap_mem_H0

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerMap_mem_H0 (x : (𝒱.kaehlerSections c).H0) :
    (f.kaehlerMap0 x.val.1, f.kaehlerMap1 x.val.2) ∈ (𝒲.kaehlerSections c').H0

def

kaehlerH0map

L293 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerH0map

Documentation

The induced semilinear map on degree-zero Čech cohomology of differentials.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · full declaration

def kaehlerH0map : (𝒱.kaehlerSections c).H0 →ₛₗ[τ] (𝒲.kaehlerSections c').H0 where
  toFun x := ⟨(f.kaehlerMap0 x.val.1, f.kaehlerMap1 x.val.2), f.kaehlerMap_mem_H0 x⟩
  map_add' x y := by
    apply Subtype.ext
    change (f.kaehlerMap0 (x.val.1 + y.val.1), f.kaehlerMap1 (x.val.2 + y.val.2)) =
      (f.kaehlerMap0 x.val.1 + f.kaehlerMap0 y.val.1, f.kaehlerMap1 x.val.2 + f.kaehlerMap1 y.val.2)
    rw [map_add, map_add]
  map_smul' r x := by
    apply Subtype.ext
    change (f.kaehlerMap0 (r • x.val.1), f.kaehlerMap1 (r • x.val.2)) =
      (τ r • f.kaehlerMap0 x.val.1, τ r • f.kaehlerMap1 x.val.2)
    rw [LinearMap.map_smulₛₗ, LinearMap.map_smulₛₗ]

theorem

kaehlerH0map_apply_coe

L306 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerH0map_apply_coe

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerH0map_apply_coe (x : (𝒱.kaehlerSections c).H0) :
    (f.kaehlerH0map x).val = (f.kaehlerMap0 x.val.1, f.kaehlerMap1 x.val.2)

def

kaehlerH1map

L311 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerH1map

Documentation

The induced semilinear map on degree-one Čech cohomology of differentials.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

def kaehlerH1map : (𝒱.kaehlerSections c).H1 →ₛₗ[τ] (𝒲.kaehlerSections c').H1

theorem

kaehlerH1map_mk

L314 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerH1map_mk

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')

Lean source · statement

theorem kaehlerH1map_mk (η : Ω[(𝒱.cover c).A01⁄R]) :
    f.kaehlerH1map (Submodule.Quotient.mk η) = Submodule.Quotient.mk (f.kaehlerMap01 η)

theorem

kaehlerMap0_congr

L323 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap0_congr

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem kaehlerMap0_congr {f : HomOver τ 𝒱 c 𝒲 c'} {g : HomOver τ' 𝒱 c 𝒲 c'} (hfg : f.hom = g.hom)
    (ω : Ω[(𝒱.cover c).A0⁄R]) : f.kaehlerMap0 ω = g.kaehlerMap0 ω

theorem

kaehlerMap1_congr

L327 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap1_congr

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem kaehlerMap1_congr {f : HomOver τ 𝒱 c 𝒲 c'} {g : HomOver τ' 𝒱 c 𝒲 c'} (hfg : f.hom = g.hom)
    (ω : Ω[(𝒱.cover c).A1⁄R]) : f.kaehlerMap1 ω = g.kaehlerMap1 ω

theorem

kaehlerMap01_congr

L331 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerMap01_congr

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem kaehlerMap01_congr {f : HomOver τ 𝒱 c 𝒲 c'} {g : HomOver τ' 𝒱 c 𝒲 c'} (hfg : f.hom = g.hom)
    (ω : Ω[(𝒱.cover c).A01⁄R]) : f.kaehlerMap01 ω = g.kaehlerMap01 ω

theorem

kaehlerH0map_congr

L336 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerH0map_congr

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem kaehlerH0map_congr {f : HomOver τ 𝒱 c 𝒲 c'} {g : HomOver τ' 𝒱 c 𝒲 c'} (hfg : f.hom = g.hom)
    (x : (𝒱.kaehlerSections c).H0) : f.kaehlerH0map x = g.kaehlerH0map x

theorem

kaehlerH1map_congr

L339 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.kaehlerH1map_congr

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem kaehlerH1map_congr {f : HomOver τ 𝒱 c 𝒲 c'} {g : HomOver τ' 𝒱 c 𝒲 c'} (hfg : f.hom = g.hom)
    (x : (𝒱.kaehlerSections c).H1) : f.kaehlerH1map x = g.kaehlerH1map x

theorem

id_appLE

L344 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_appLE

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_appLE (U : X.Opens) (h : U ≤ (𝟙 X : X ⟶ X) ⁻¹ᵁ U) : (𝟙 X : X ⟶ X).appLE U U h = 𝟙 _

theorem

id_ringHom0

L350 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_ringHom0

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_ringHom0 : (HomOver.id 𝒱 c).ringHom0 = RingHom.id _

theorem

id_ringHom1

L353 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_ringHom1

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_ringHom1 : (HomOver.id 𝒱 c).ringHom1 = RingHom.id _

theorem

id_ringHom01

L356 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_ringHom01

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_ringHom01 : (HomOver.id 𝒱 c).ringHom01 = RingHom.id _

theorem

id_kaehlerMap0

L360 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_kaehlerMap0

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_kaehlerMap0 (ω : Ω[(𝒱.cover c).A0⁄R]) : (HomOver.id 𝒱 c).kaehlerMap0 ω = ω

theorem

id_kaehlerMap1

L363 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_kaehlerMap1

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_kaehlerMap1 (ω : Ω[(𝒱.cover c).A1⁄R]) : (HomOver.id 𝒱 c).kaehlerMap1 ω = ω

theorem

id_kaehlerMap01

L366 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_kaehlerMap01

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_kaehlerMap01 (ω : Ω[(𝒱.cover c).A01⁄R]) : (HomOver.id 𝒱 c).kaehlerMap01 ω = ω

theorem

id_kaehlerH0map

L370 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_kaehlerH0map

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_kaehlerH0map (x : (𝒱.kaehlerSections c).H0) : (HomOver.id 𝒱 c).kaehlerH0map x = x

theorem

id_kaehlerH1map

L372 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.id_kaehlerH1map

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem id_kaehlerH1map (x : (𝒱.kaehlerSections c).H1) : (HomOver.id 𝒱 c).kaehlerH1map x = x

theorem

comp_ringHom0

L376 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_ringHom0

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_ringHom0 (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') :
    (g.comp f).ringHom0 = g.ringHom0.comp f.ringHom0

theorem

comp_ringHom1

L381 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_ringHom1

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_ringHom1 (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') :
    (g.comp f).ringHom1 = g.ringHom1.comp f.ringHom1

theorem

comp_ringHom01

L386 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_ringHom01

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_ringHom01 (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') :
    (g.comp f).ringHom01 = g.ringHom01.comp f.ringHom01

theorem

comp_kaehlerMap0

L393 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_kaehlerMap0

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_kaehlerMap0 (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') (ω : Ω[(𝒱.cover
  c).A0⁄R]) :
    (g.comp f).kaehlerMap0 ω = g.kaehlerMap0 (f.kaehlerMap0 ω)

theorem

comp_kaehlerMap1

L399 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_kaehlerMap1

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_kaehlerMap1 (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') (ω : Ω[(𝒱.cover
  c).A1⁄R]) :
    (g.comp f).kaehlerMap1 ω = g.kaehlerMap1 (f.kaehlerMap1 ω)

theorem

comp_kaehlerMap01

L405 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_kaehlerMap01

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_kaehlerMap01 (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') (ω : Ω[(𝒱.cover
  c).A01⁄R]) :
    (g.comp f).kaehlerMap01 ω = g.kaehlerMap01 (f.kaehlerMap01 ω)

theorem

comp_kaehlerH0map

L412 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_kaehlerH0map

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_kaehlerH0map (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') (x :
  (𝒱.kaehlerSections c).H0) :
    (g.comp f).kaehlerH0map x = g.kaehlerH0map (f.kaehlerH0map x)

theorem

comp_kaehlerH1map

L416 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.HomOver.comp_kaehlerH1map

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
namespace HomOver
variable {S : Type u} [CommRing S] {τ : R →+* S} {𝒱} {c} {Y : Scheme.{u}} {𝒲 : Y.TwoAffineOpenCover}
  {c' : Y ⟶ Spec (.of S)} (f : HomOver τ 𝒱 c 𝒲 c')
section Functoriality
variable {τ' : R →+* S} {T : Type u} [CommRing T] {υ : S →+* T} {Z : Scheme.{u}} {𝒳 :
  Z.TwoAffineOpenCover}
  {c'' : Z ⟶ Spec (.of T)}

Lean source · statement

theorem comp_kaehlerH1map (g : HomOver υ 𝒲 c' 𝒳 c'') (f : HomOver τ 𝒱 c 𝒲 c') (x :
  (𝒱.kaehlerSections c).H1) :
    (g.comp f).kaehlerH1map x = g.kaehlerH1map (f.kaehlerH1map x)

abbrev

kaehlerH0baseChangeMap

L431 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH0baseChangeMap

Documentation

The scalar-extension map on degree-zero Čech cohomology of differentials.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]

Lean source · statement

abbrev kaehlerH0baseChangeMap :
    (𝒱.kaehlerSections c).H0 →ₛₗ[algebraMap R A]
      ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R A))).H0

abbrev

kaehlerH1baseChangeMap

L437 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH1baseChangeMap

Documentation

The scalar-extension map on degree-one Čech cohomology of differentials.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]

Lean source · statement

abbrev kaehlerH1baseChangeMap :
    (𝒱.kaehlerSections c).H1 →ₛₗ[algebraMap R A]
      ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R A))).H1

abbrev

kaehlerH0stageMap

L444 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH0stageMap

Documentation

The map on degree-zero cohomology induced by a map between coefficient algebras.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in

Lean source · statement

abbrev kaehlerH0stageMap (g : A →ₐ[R] B) :
    ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R A))).H0 →ₛₗ[g.toRingHom]
      ((𝒱.pullback c B).kaehlerSections (pullback.snd c (specMap R B))).H0

abbrev

kaehlerH1stageMap

L451 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH1stageMap

Documentation

The map on degree-one cohomology induced by a map between coefficient algebras.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in

Lean source · statement

abbrev kaehlerH1stageMap (g : A →ₐ[R] B) :
    ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R A))).H1 →ₛₗ[g.toRingHom]
      ((𝒱.pullback c B).kaehlerSections (pullback.snd c (specMap R B))).H1

theorem

stage_comp_baseChange_hom

L458 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.stage_comp_baseChange_hom

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem stage_comp_baseChange_hom (g : A →ₐ[R] B) :
    ((HomOver.stage 𝒱 c g).comp (HomOver.baseChange 𝒱 c A)).hom = (HomOver.baseChange 𝒱 c B).hom

theorem

stage_id_hom

L462 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.stage_id_hom

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem stage_id_hom :
    (HomOver.stage 𝒱 c (AlgHom.id R A)).hom = (HomOver.id (𝒱.pullback c A) (pullback.snd c
      (specMap R A))).hom

theorem

stage_comp_stage_hom

L472 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.stage_comp_stage_hom

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem stage_comp_stage_hom (g : A →ₐ[R] B) (g' : B →ₐ[R] B') :
    ((HomOver.stage 𝒱 c g').comp (HomOver.stage 𝒱 c g)).hom = (HomOver.stage 𝒱 c (g'.comp g)).hom

theorem

kaehlerH0stageMap_kaehlerH0baseChangeMap

L483 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH0stageMap_kaehlerH0baseChangeMap

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem kaehlerH0stageMap_kaehlerH0baseChangeMap (g : A →ₐ[R] B) (x : (𝒱.kaehlerSections c).H0) :
    kaehlerH0stageMap 𝒱 c g (kaehlerH0baseChangeMap 𝒱 c A x) = kaehlerH0baseChangeMap 𝒱 c B x

theorem

kaehlerH1stageMap_kaehlerH1baseChangeMap

L489 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH1stageMap_kaehlerH1baseChangeMap

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem kaehlerH1stageMap_kaehlerH1baseChangeMap (g : A →ₐ[R] B) (x : (𝒱.kaehlerSections c).H1) :
    kaehlerH1stageMap 𝒱 c g (kaehlerH1baseChangeMap 𝒱 c A x) = kaehlerH1baseChangeMap 𝒱 c B x

theorem

kaehlerH0stageMap_id

L496 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH0stageMap_id

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem kaehlerH0stageMap_id (x : ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R
  A))).H0) :
    kaehlerH0stageMap 𝒱 c (AlgHom.id R A) x = x

theorem

kaehlerH1stageMap_id

L500 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH1stageMap_id

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem kaehlerH1stageMap_id (x : ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R
  A))).H1) :
    kaehlerH1stageMap 𝒱 c (AlgHom.id R A) x = x

theorem

kaehlerH0stageMap_comp

L505 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH0stageMap_comp

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem kaehlerH0stageMap_comp (g : A →ₐ[R] B) (g' : B →ₐ[R] B')
    (x : ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R A))).H0) :
    kaehlerH0stageMap 𝒱 c g' (kaehlerH0stageMap 𝒱 c g x) = kaehlerH0stageMap 𝒱 c (g'.comp g) x

theorem

kaehlerH1stageMap_comp

L512 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.kaehlerH1stageMap_comp

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
  R))
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B]
variable {A} in
variable {A} in
variable {A} {B' : Type u} [CommRing B'] [Algebra R B']

Lean source · statement

theorem kaehlerH1stageMap_comp (g : A →ₐ[R] B) (g' : B →ₐ[R] B')
    (x : ((𝒱.pullback c A).kaehlerSections (pullback.snd c (specMap R A))).H1) :
    kaehlerH1stageMap 𝒱 c g' (kaehlerH1stageMap 𝒱 c g x) = kaehlerH1stageMap 𝒱 c (g'.comp g) x

Module documentation

Declarations