Units for affine pullback on the bounded-above projective locus

This file specializes the generic identity comparison to extension of scalars along the identity ring morphism.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPullbackIdIso (R : CommRingCat) : affineBoundedAboveProjectiveHomotopyPullback (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (CategoryTheory.BoundedAboveProjectiveHomotopyCategory (ModuleCat ↑R))

Pullback along the identity ring morphism is the identity on the bounded-above projective homotopy locus.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveDerivedPullbackIdIso (R : CommRingCat) : affineBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (CategoryTheory.BoundedAboveProjectiveDerivedCategory (ModuleCat ↑R))

Pullback along the identity ring morphism is the identity on the bounded-above projective derived locus.

Equations

• One or more equations did not get rendered due to their size.