Module

Scheme_Modules_ofUnitSection_sectionDual_app.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ofUnitSection_sectionDual_app

5 declarations indexed from sourceView source ↗

Module documentation

The action of a dual section

Evaluating the dual of a module section agrees with the coefficient obtained from the restricted internal-Hom section and the canonical restriction of the tensor unit.

Imports2

Imported by3

abbrev

sVal

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app.AlgebraicGeometry.Scheme.Modules.SectionDualFormula.sVal

Documentation

The section of M obtained by evaluating a morphism from the tensor unit at its unit section.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace SectionDualFormula
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

abbrev sVal (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens) : Γ(M, U)

lemma

map_sVal

L54 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app.AlgebraicGeometry.Scheme.Modules.SectionDualFormula.map_sVal

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace SectionDualFormula
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma map_sVal (s : 𝟙_ X.Modules ⟶ M) {U V : X.Opens} (i : V ⟶ U) :
    M.presheaf.map i.op (sVal s U) = sVal s V

lemma

sectionDual_app

L60 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app.AlgebraicGeometry.Scheme.Modules.SectionDualFormula.sectionDual_app

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace SectionDualFormula
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma sectionDual_app (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens) (t : Γ(Scheme.Modules.dual M, U)) :
    (sectionDual s).app U t = ihomEval M (𝟙_ X.Modules) U (sVal s U) t

theorem

ofUnitSection_sectionDual_app'

L66 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app.AlgebraicGeometry.Scheme.Modules.SectionDualFormula.ofUnitSection_sectionDual_app'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace SectionDualFormula
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem ofUnitSection_sectionDual_app' (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
    (t : Γ(Scheme.Modules.dual M, U)) :
    ofUnitSection U ((sectionDual s).app U t) =
      coeff s U (ihomSectionsEquiv M (𝟙_ X.Modules) U t ≫ (restrictUnitIso' U.ι).hom)

theorem

ofUnitSection_sectionDual_app

L101 ↗

AlgebraicGeometry.Scheme.Modules.ofUnitSection_sectionDual_app

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ofUnitSection_sectionDual_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.ofUnitSection_sectionDual_app
    {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
    (t : Γ(Scheme.Modules.dual M, U)) :
    Scheme.Modules.ofUnitSection U ((Scheme.Modules.sectionDual s).app U t) =
      Scheme.Modules.coeff s U
        (Scheme.Modules.ihomSectionsEquiv M (𝟙_ X.Modules) U t ≫
          (Scheme.Modules.restrictUnitIso' U.ι).hom)

Module documentation

The action of a dual section

Declarations

sVal

map_sVal

sectionDual_app

ofUnitSection_sectionDual_app'

ofUnitSection_sectionDual_app