Module

Scheme_Modules_unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules unit Aut Section pullback Unit Iso conj opens I eq app one

Imports6

Imported by2

theorem

unit_app_one_res

L35 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one.UASRestrict.unit_app_one_res

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace UASRestrict

Lean source · statement

theorem unit_app_one_res {Y : Scheme.{u}}
    (ψ : SheafOfModules.unit Y.ringCatSheaf ≅ SheafOfModules.unit Y.ringCatSheaf)
    {U V : Y.Opens} (i : V ⟶ U) :
    (Y.presheaf.map i.op).hom ((ψ.hom.val.app (op U)).hom (1 : Y.presheaf.obj (op U))) =
      (ψ.hom.val.app (op V)).hom (1 : Y.presheaf.obj (op V))

theorem

unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one

L47 ↗

AlgebraicGeometry.Scheme.Modules.unitAutSection_pullbackUnitIso_conj_opensI_eq_app_one