NYLL
Module

Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
13 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible zero Scheme Ideal tensor Hom

Imports10
Imported by2

Declarations

theorem

app_naturality

L48 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.app_naturality
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
theorem app_naturality {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (k : V ⟶ U) (m : Γ(M, U)) :
    φ.app V (M.presheaf.map k.op m) = N.presheaf.map k.op (φ.app U m)
theorem

restrictFunctorIsoPullback_hom_app_app

L52 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.restrictFunctorIsoPullback_hom_app_app
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · full declaration
theorem restrictFunctorIsoPullback_hom_app_app {Y : Scheme.{u}} (j : Y ⟶ X) [IsOpenImmersion j]
    (M : X.Modules) (W : Y.Opens) (m : Γ(M, j ''ᵁ W)) :
    ((restrictFunctorIsoPullback j).hom.app M).app W (show Γ(M.restrict j, W) from m)
      = ((Scheme.Modules.pullback j).obj M).presheaf.map (eqToHom (j.preimage_image_eq W).symm).op
          (pullbackLocalSection j m) := by
  have h := Adjunction.unit_leftAdjointUniq_hom_app (restrictAdjunction j)
    (Scheme.Modules.pullbackPushforwardAdjunction j) M
  have h' := CategoryTheory.ConcreteCategory.congr_hom
    (congrArg (fun k => Scheme.Modules.Hom.app k (j ''ᵁ W)) h) m
  change ((restrictFunctorIsoPullback j).hom.app M).app (j ⁻¹ᵁ j ''ᵁ W)
      ((M.restrict j).presheaf.map (eqToHom (j.preimage_image_eq W)).op (show Γ(M.restrict j, W)
        from m))
    = pullbackLocalSection j m at h'
  rw [app_naturality] at h'
  rw [← h', ← CategoryTheory.comp_apply, ← Functor.map_comp, ← op_comp, eqToHom_trans, eqToHom_refl,
    op_id, CategoryTheory.Functor.map_id]
  rfl
def

τL

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.τL
Documentation

The restriction trivialization induced by the given pullback trivialization of the first module.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
Lean source · statement
def τL : L.restrict U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules
def

τT

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.τT
Documentation

The restriction trivialization of the tensor product induced by the two given pullback trivializations.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
Lean source · statement
def τT : (L ⊗ M).restrict U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules
abbrev

tens

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.tens
Documentation

The tensor product of two unit-module morphisms, precomposed with the inverse left unitor.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
Lean source · statement
abbrev tens : 𝟙_ X.Modules ⟶ L ⊗ M
theorem

tens_app_one

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.tens_app_one
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
omit U eL eM in
Lean source · statement
theorem tens_app_one (V : X.Opens) :
    (tens s s').app V (unitSection V) = tensorSections (s.app V (unitSection V)) (s'.app V
      (unitSection V))
theorem

τL_app_restrictSection

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.τL_app_restrictSection
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
Lean source · statement
theorem τL_app_restrictSection :
    (τL U eL).hom.app ⊤ (restrictSection s U.1)
      = eL.hom.app ⊤ (((Scheme.Modules.pullback U.1.ι).obj L).presheaf.map
          (eqToHom (U.1.ι.preimage_image_eq ⊤).symm).op (pullbackLocalSection U.1.ι (s.app (U.1.ι
            ''ᵁ ⊤) (unitSection _))))
theorem

τT_app_restrictSection

L117 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.τT_app_restrictSection
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
Lean source · full declaration
theorem τT_app_restrictSection :
    (τT U eL eM).hom.app ⊤ (restrictSection (tens s s') U.1)
      = (show Γ((U.1 : Scheme.{u}), (⊤ : (U.1 : Scheme.{u}).Opens)) from
            eL.hom.app ⊤ (((Scheme.Modules.pullback U.1.ι).obj L).presheaf.map
              (eqToHom (U.1.ι.preimage_image_eq ⊤).symm).op (pullbackLocalSection U.1.ι (s.app
                (U.1.ι ''ᵁ ⊤) (unitSection _))))) •
        eM.hom.app ⊤ (((Scheme.Modules.pullback U.1.ι).obj M).presheaf.map
              (eqToHom (U.1.ι.preimage_image_eq ⊤).symm).op (pullbackLocalSection U.1.ι (s'.app
                (U.1.ι ''ᵁ ⊤) (unitSection _)))) := by
  change (λ_ (𝟙_ (U.1 : Scheme.{u}).Modules)).hom.app ⊤ ((eL.hom ⊗ₘ eM.hom).app ⊤
    ((pullbackTensorObjIso U.1.ι L M).hom.app ⊤
    (((restrictFunctorIsoPullback U.1.ι).hom.app (L ⊗ M)).app ⊤ (restrictSection (tens s s')
      U.1)))) = _
  have h0 : restrictSection (tens s s') U.1
      = (show Γ((L ⊗ M).restrict U.1.ι, ⊤) from
          tensorSections (s.app (U.1.ι ''ᵁ ⊤) (unitSection _)) (s'.app (U.1.ι ''ᵁ ⊤) (unitSection
            _))) :=
    tens_app_one s s' _
  rw [h0]
  erw [restrictFunctorIsoPullback_hom_app_app U.1.ι (L ⊗ M) ⊤]
  rw [app_naturality, pullbackTensorObjIso_hom_app_pullbackLocalSection, map_tensorSections,
    tensorHom_app_tensorSections]
  exact leftUnitor_hom_app_tensorSections (X := (U.1 : Scheme.{u}))
    (N := 𝟙_ (U.1 : Scheme.{u}).Modules) (U := ⊤)
    (show Γ((U.1 : Scheme.{u}), (⊤ : (U.1 : Scheme.{u}).Opens)) from
      eL.hom.app ⊤ (((Scheme.Modules.pullback U.1.ι).obj L).presheaf.map
        (eqToHom (U.1.ι.preimage_image_eq ⊤).symm).op
        (pullbackLocalSection U.1.ι (s.app (U.1.ι ''ᵁ ⊤) (unitSection _)))))
    (eM.hom.app ⊤ (((Scheme.Modules.pullback U.1.ι).obj M).presheaf.map
      (eqToHom (U.1.ι.preimage_image_eq ⊤).symm).op
      (pullbackLocalSection U.1.ι (s'.app (U.1.ι ''ᵁ ⊤) (unitSection _)))))
theorem

coeff_tens

L149 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.coeff_tens
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
Lean source · statement
theorem coeff_tens :
    coeff (tens s s') U.1 (τT U eL eM).hom = coeff s U.1 (τL U eL).hom * coeff s' U.1 (τL U eM).hom
theorem

ideal_eq

L157 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.ideal_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
section local_computation
variable {L M : X.Modules} (U : X.affineOpens)
  (eL : (Scheme.Modules.pullback U.1.ι).obj L ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (eM : (Scheme.Modules.pullback U.1.ι).obj M ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
  (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M)
include eL eM in
Lean source · statement
theorem ideal_eq (hL : IsInvertible L) (hM : IsInvertible M) :
    (zeroSchemeIdeal (tens s s')).ideal U = (zeroSchemeIdeal s).ideal U * (zeroSchemeIdeal
      s').ideal U
def

restrictTriv

L169 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.restrictTriv
Documentation

Restricts a pullback trivialization from an open subset to a smaller open subset.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
def restrictTriv {L : X.Modules} {U₀ : X.Opens} {U : X.Opens} (h : U ≤ U₀)
    (e : (Scheme.Modules.pullback U₀.ι).obj L ≅ 𝟙_ (U₀ : Scheme.{u}).Modules) :
    (Scheme.Modules.pullback U.ι).obj L ≅ 𝟙_ (U : Scheme.{u}).Modules
theorem

main

L177 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom.Ws31C4.main
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace Ws31C4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}
Lean source · statement
theorem main {L M : X.Modules} (hL : IsInvertible L) (hM : IsInvertible M)
    (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M) :
    zeroSchemeIdeal ((λ_ (𝟙_ X.Modules)).inv ≫ (s ⊗ₘ s')) = zeroSchemeIdeal s * zeroSchemeIdeal s'
theorem

zeroSchemeIdeal_tensorHom

L200 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.zeroSchemeIdeal_tensorHom
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_zeroSchemeIdeal_tensorHom
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.zeroSchemeIdeal_tensorHom
    {X : Scheme.{u}} {L M : X.Modules} (hL : Scheme.Modules.IsInvertible L) (hM :
      Scheme.Modules.IsInvertible M)
    (s : 𝟙_ X.Modules ⟶ L) (s' : 𝟙_ X.Modules ⟶ M) :
    Scheme.Modules.zeroSchemeIdeal ((λ_ (𝟙_ X.Modules)).inv ≫ (s ⊗ₘ s')) =
      Scheme.Modules.zeroSchemeIdeal s * Scheme.Modules.zeroSchemeIdeal s'

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