Module

Scheme_Modules_pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Modules pullback Unit Iso hom app pullback Local Section to Unit Section

Imports3

Imported by6

theorem

pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection

L31 ↗

AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection
    {X Y : Scheme.{u}} (φ : X ⟶ Y) (U : Y.Opens) (g : Γ(Y, U)) :
    (Scheme.Modules.pullbackUnitIso φ).hom.app (φ ⁻¹ᵁ U)
        (Scheme.Modules.pullbackLocalSection φ (Scheme.Modules.toUnitSection U g)) =
      Scheme.Modules.toUnitSection (φ ⁻¹ᵁ U) (φ.app U g)

Module documentation

Scheme Modules pullback Unit Iso hom app pullback Local Section to Unit Section

Declarations

pullbackUnitIso_hom_app_pullbackLocalSection_toUnitSection