Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Dqc.AffineKProjectivePseudofunctor

Coherence for the affine bounded-projective pullback lane #

The extension-of-scalars pentagon is first transported to cochain complexes and then through the homotopy quotient. This supplies the main higher coherence equation needed to package the affine supported pullbacks as a pseudofunctor.

source
theorem AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalarsComplex_associativity {R A B C : CommRingCat} (f : R ⟶ A) (g : A ⟶ B) (h : B ⟶ C) :
CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) (CommRingCat.Hom.hom h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom f) (CommRingCat.Hom.hom g)).hom (ModuleCat.extendScalars (CommRingCat.Hom.hom h))) (CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).associator (ModuleCat.extendScalars (CommRingCat.Hom.hom g)) (ModuleCat.extendScalars (CommRingCat.Hom.hom h))).hom (CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).whiskerLeft (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom g) (CommRingCat.Hom.hom h)).inv) (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom f) ((CommRingCat.Hom.hom h).comp (CommRingCat.Hom.hom g))).inv)))) (ComplexShape.up ℤ) = CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars ((CommRingCat.Hom.hom h).comp ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))))) (ComplexShape.up ℤ)

The extension-of-scalars pentagon transported degreewise to cochain complexes.

source
theorem AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalarsComplex_leftUnitality {R A : CommRingCat} (f : R ⟶ A) :
CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (RingHom.id ↑R) (CommRingCat.Hom.hom f)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId ↑R).hom (ModuleCat.extendScalars (CommRingCat.Hom.hom f))) (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).leftUnitor.hom)) (ComplexShape.up ℤ) = CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars ((CommRingCat.Hom.hom f).comp (RingHom.id ↑R)))) (ComplexShape.up ℤ)

The left unit equation for extension of scalars transported degreewise to cochain complexes.

source
theorem AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalarsComplex_rightUnitality {R A : CommRingCat} (f : R ⟶ A) :
CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom f) (RingHom.id ↑A)).hom (CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).whiskerLeft (ModuleCat.extendScalarsId ↑A).hom) (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).rightUnitor.hom)) (ComplexShape.up ℤ) = CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars ((RingHom.id ↑A).comp (CommRingCat.Hom.hom f)))) (ComplexShape.up ℤ)

The right unit equation for extension of scalars transported degreewise to cochain complexes.

source
theorem AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPullback_associativity {R A B C : CommRingCat} (f : R ⟶ A) (g : A ⟶ B) (h : B ⟶ C) :
CategoryTheory.CategoryStruct.comp (affineBoundedAboveProjectiveHomotopyPullbackCompIso (CategoryTheory.CategoryStruct.comp f g) h).symm.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (affineBoundedAboveProjectiveHomotopyPullbackCompIso f g).symm.hom (affineBoundedAboveProjectiveHomotopyPullback h)) (CategoryTheory.CategoryStruct.comp ((affineBoundedAboveProjectiveHomotopyPullback f).associator (affineBoundedAboveProjectiveHomotopyPullback g) (affineBoundedAboveProjectiveHomotopyPullback h)).hom (CategoryTheory.CategoryStruct.comp ((affineBoundedAboveProjectiveHomotopyPullback f).whiskerLeft (affineBoundedAboveProjectiveHomotopyPullbackCompIso g h).hom) (affineBoundedAboveProjectiveHomotopyPullbackCompIso f (CategoryTheory.CategoryStruct.comp g h)).hom))) = CategoryTheory.CategoryStruct.id (affineBoundedAboveProjectiveHomotopyPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h))

The affine compositor on bounded-above projective homotopy representatives satisfies the pentagon equation.

source
theorem AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPullback_leftUnitality {R A : CommRingCat} (f : R ⟶ A) :
CategoryTheory.CategoryStruct.comp (affineBoundedAboveProjectiveHomotopyPullbackCompIso (CategoryTheory.CategoryStruct.id R) f).symm.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (affineBoundedAboveProjectiveHomotopyPullbackIdIso R).hom (affineBoundedAboveProjectiveHomotopyPullback f)) (affineBoundedAboveProjectiveHomotopyPullback f).leftUnitor.hom) = CategoryTheory.CategoryStruct.id (affineBoundedAboveProjectiveHomotopyPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id R) f))

The affine compositor and unit satisfy the left triangle equation on bounded-above projective homotopy representatives.

source
theorem AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPullback_rightUnitality {R A : CommRingCat} (f : R ⟶ A) :
CategoryTheory.CategoryStruct.comp (affineBoundedAboveProjectiveHomotopyPullbackCompIso f (CategoryTheory.CategoryStruct.id A)).symm.hom (CategoryTheory.CategoryStruct.comp ((affineBoundedAboveProjectiveHomotopyPullback f).whiskerLeft (affineBoundedAboveProjectiveHomotopyPullbackIdIso A).hom) (affineBoundedAboveProjectiveHomotopyPullback f).rightUnitor.hom) = CategoryTheory.CategoryStruct.id (affineBoundedAboveProjectiveHomotopyPullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id A)))

The affine compositor and unit satisfy the right triangle equation on bounded-above projective homotopy representatives.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPseudofunctor :
CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCat) CategoryTheory.Cat

Arbitrary affine extension of scalars on bounded-above projective homotopy representatives, packaged with its proved unit, compositor, pentagon, and triangle equations.

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