Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Families.BaseChangeAdjunction

Adjunctions on constructed base-change categories #

Once the derived pullback and pushforward preserve the base-change components, their ambient adjunction restricts to the full subcategories. The same argument first restricts the ambient Dqc adjunction to intrinsic bounded-coherent complexes and then to D_T.

source
theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcLeftDerivedPullback.essSurj_of_adjunction_counit_isIso {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (pull : DqcLeftDerivedPullback f) (push : DqcRightDerivedPushforward f) (adj : pull.functor ⊣ push.functor) (hCounit : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left T)), CategoryTheory.IsIso (adj.counit.app E)) :
pull.functor.EssSurj

A Dqc left-derived pullback is essentially surjective when it has a right adjoint with invertible counit.

source
theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcLeftDerivedPullback.essSurj_of_adjunction_of_fullyFaithful {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (pull : DqcLeftDerivedPullback f) (push : DqcRightDerivedPushforward f) (adj : pull.functor ⊣ push.functor) [push.functor.Full] [push.functor.Faithful] :
pull.functor.EssSurj

A Dqc left-derived pullback with a fully faithful right adjoint is essentially surjective. For a quasi-compact open immersion, this is the formal categorical conclusion once derived pushforward is known to preserve quasicoherent cohomology and remain fully faithful.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackPushforwardAdjunction {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (adj : pull.functor ⊣ push.functor) (hPull : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hPush : DT.PushforwardPreservesQuasicoherentComponent DU P push) :
DT.quasicoherentPullback DU P pull hPull ⊣ DT.quasicoherentPushforward DU P push hPush

An adjunction between the ambient Dqc pullback and pushforward restricts to the constructed quasicoherent base-change components.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedCoherentPullbackPushforwardAdjunction {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (adj : pull.functor ⊣ push.functor) (hPull : pull.PreservesBoundedCoherent) (hPush : push.PreservesBoundedCoherent) :
    pull.boundedFunctor hPull ⊣ push.boundedFunctor hPush

    The ambient Dqc adjunction restricts to intrinsic bounded-coherent complexes when both functors preserve that locus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackPushforwardAdjunction {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (adj : pull.functor ⊣ push.functor) (hPullDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hPushDqc : DT.PushforwardPreservesQuasicoherentComponent DU P push) (hPullBounded : pull.PreservesBoundedCoherent) (hPushBounded : push.PreservesBoundedCoherent) :
      DT.boundedPullback DU P pull hPullDqc hPullBounded ⊣ DT.boundedPushforward DU P push hPushDqc hPushBounded

      The pullback-pushforward adjunction on the constructed bounded base-change categories.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfDetection_essSurj_of_adjunction {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (adj : pull.functor ⊣ push.functor) (hDetect : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))), DU.quasicoherentComponent P E ↔ DT.quasicoherentComponent P (pull.functor.obj E)) [push.functor.Full] [push.functor.Faithful] :
        (DT.quasicoherentPullbackOfDetection DU P pull hDetect).EssSurj

        Lemma 3.18 for the constructed quasicoherent base-change component, reduced to the geometric inputs: a fully faithful right adjoint on Dqc and detection of component membership by pullback.

        source
        theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfDetection_essSurj_of_adjunction {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (adj : pull.functor ⊣ push.functor) (hPull : pull.PreservesBoundedCoherent) (hPush : push.PreservesBoundedCoherent) (hDetect : ∀ (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), DU.boundedComponent P E ↔ DT.boundedComponent P ((pull.boundedFunctor hPull).obj E)) [push.functor.Full] [push.functor.Faithful] :
        (DT.boundedPullbackOfDetection DU P pull hPull hDetect).EssSurj

        Lemma 3.18 for the constructed bounded base-change component. Full faithfulness of the Dqc right adjoint descends to the bounded-coherent restriction, whose counit supplies essential surjectivity before the final membership-detection restriction to D_T.