Module

tilde_pullbackSpecIso_hom_app_top_unit_toOpen.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullbackSpecIso_hom_app_top_unit_toOpen

2 declarations indexed from sourceView source ↗

Module documentation

Pullback of sections represented by module elements

The affine pullback comparison sends a module element represented as a section to the section represented by its scalar extension.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesTildePullback

Imported by4

theorem

pullbackSpecIso_unit_aux

L39 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullbackSpecIso_hom_app_top_unit_toOpen.AlgebraicGeometry.tilde.pullbackSpecIso_unit_aux

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullbackSpecIso_hom_app_top_unit_toOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.tilde in

Lean source · statement

theorem AlgebraicGeometry.tilde.pullbackSpecIso_unit_aux {R S : CommRingCat.{u}} (φ : R ⟶ S) (M :
  ModuleCat.{u} R) :
    ((tilde.adjunction (R := R)).comp
        (Scheme.Modules.pullbackPushforwardAdjunction (Spec.map φ))).unit.app M ≫
      (Scheme.Modules.pushforward (Spec.map φ) ⋙ moduleSpecΓFunctor (R := R)).map
        (tilde.pullbackSpecIso φ M).hom ≫
      (Scheme.Modules.pushforwardSpecCompΓIso φ).hom.app (tilde ((ModuleCat.extendScalars φ.hom).obj
          M)) =
    (ModuleCat.extendRestrictScalarsAdj φ.hom).unit.app M ≫
      (ModuleCat.restrictScalars φ.hom).map
        ((tilde.adjunction (R := S)).unit.app ((ModuleCat.extendScalars φ.hom).obj M))

theorem

pullbackSpecIso_hom_app_top_unit_toOpen

L65 ↗

AlgebraicGeometry.tilde.pullbackSpecIso_hom_app_top_unit_toOpen

Source context 7 commands