Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullbackSpecIso_unit

theorem

pullbackSpecIso_unit

AlgebraicGeometry.tilde.pullbackSpecIso_unit

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullbackSpecIso_unit
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct

Lean source · statement

theorem _root_.AlgebraicGeometry.tilde.pullbackSpecIso_unit {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))

tilde_pullbackSpecIso_unit.lean

Module documentation

Compatibility of affine pullback with adjunction units

pullbackSpecIso_unit

Module documentation

Compatibility of affine pullback with adjunction units

Declarations

pullbackSpecIso_unit