NYLL
Module

Scheme_Modules_pullbackComp_hom_app_comp_pullbackUnitIso_hom.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackComp_hom_app_comp_pullbackUnitIso_hom
7 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules pullback Comp hom app comp pullback Unit Iso hom

Imports6
Imported by8

Declarations

def

unitHom

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition.AlgebraicGeometry.Scheme.Modules.unitHom
Documentation

The canonical morphism from the unit module to the pushforward of the unit module, induced by the scheme morphism on functions.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
Lean source · statement
def unitHom : @Quiver.Hom Y.Modules _ (SheafOfModules.unit Y.ringCatSheaf)
    ((pushforward f).obj (SheafOfModules.unit X.ringCatSheaf))
theorem

unitHom_app

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition.AlgebraicGeometry.Scheme.Modules.unitHom_app
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
Lean source · statement
theorem unitHom_app (U : Y.Opens) (x : Γ(SheafOfModules.unit Y.ringCatSheaf, U)) :
    (unitHom f).app U x = f.app U x
theorem

homEquiv_pullbackUnitIso_hom

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition.AlgebraicGeometry.Scheme.Modules.homEquiv_pullbackUnitIso_hom
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
Lean source · statement
theorem homEquiv_pullbackUnitIso_hom :
    (pullbackPushforwardAdjunction f).homEquiv _ _ (pullbackUnitIso f).hom = unitHom f
theorem

unitHom_comp

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition.AlgebraicGeometry.Scheme.Modules.unitHom_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
Lean source · statement
theorem unitHom_comp :
    unitHom (f ≫ g) = unitHom g ≫ (pushforward g).map (unitHom f) ≫
      (pushforwardComp f g).hom.app (SheafOfModules.unit X.ringCatSheaf)
theorem

homEquiv_comp_map_pullbackUnitIso

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition.AlgebraicGeometry.Scheme.Modules.homEquiv_comp_map_pullbackUnitIso
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
Lean source · statement
theorem homEquiv_comp_map_pullbackUnitIso :
    ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f)).homEquiv _ _
        ((pullback f).map (pullbackUnitIso g).hom ≫ (pullbackUnitIso f).hom) =
      unitHom g ≫ (pushforward g).map (unitHom f)
theorem

pullbackUnitIso_comp

L101 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition.AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
Lean source · statement
theorem pullbackUnitIso_comp :
    (pullbackComp f g).hom.app (SheafOfModules.unit Z.ringCatSheaf) ≫ (pullbackUnitIso (f ≫
      g)).hom =
      (pullback f).map (pullbackUnitIso g).hom ≫ (pullbackUnitIso f).hom
theorem

pullbackComp_hom_app_comp_pullbackUnitIso_hom

L147 ↗
AlgebraicGeometry.Scheme.Modules.pullbackComp_hom_app_comp_pullbackUnitIso_hom
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitComposition
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.pullbackComp_hom_app_comp_pullbackUnitIso_hom {X Y
  Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (Scheme.Modules.pullbackComp f g).hom.app (SheafOfModules.unit Z.ringCatSheaf) ≫
        (Scheme.Modules.pullbackUnitIso (f ≫ g)).hom =
      (Scheme.Modules.pullback f).map (Scheme.Modules.pullbackUnitIso g).hom ≫
        (Scheme.Modules.pullbackUnitIso f).hom

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