@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.specCommMonAlgPullbackObjXIso {R S : CommRingCat} (M : CommMonCat) (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) : (((commMonAlg ↑R).op.comp ((bialgSpec R).comp (CategoryTheory.Over.pullback Sf).mapMon)).obj (Opposite.op M)).X ≅ (((commMonAlg ↑S).op.comp (bialgSpec S)).obj (Opposite.op M)).X

Equations

• AlgebraicGeometry.Scheme.specCommMonAlgPullbackObjXIso M f Sf H = CategoryTheory.Over.isoMk ⋯.isoPullback.symm ⋯

def AlgebraicGeometry.Scheme.specCommMonAlgPullback {R S : CommRingCat} (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) : (commMonAlg ↑R).op.comp ((bialgSpec R).comp (CategoryTheory.Over.pullback Sf).mapMon) ≅ (commMonAlg ↑S).op.comp (bialgSpec S)

The spectrum of a commutative algebra functor commutes with base change.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.specCommMonAlgPullback_inv_app_hom_left_fst {R S : CommRingCat} (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) (M : CommMonCatᵒᵖ) : CategoryTheory.CategoryStruct.comp ((specCommMonAlgPullback f Sf H).inv.app M).hom.left (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (MonoidAlgebra ↑R ↑(Opposite.unop M))))) Sf) = Spec.map (CommRingCat.ofHom (MonoidAlgebra.mapRangeRingHom (↑(Opposite.unop M)) (CommRingCat.Hom.hom f)))

@[simp]

theorem AlgebraicGeometry.Scheme.specCommMonAlgPullback_inv_app_hom_left_fst_assoc {R S : CommRingCat} (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) (M : CommMonCatᵒᵖ) {Z : Scheme} (h : Spec { carrier := MonoidAlgebra ↑R ↑(Opposite.unop M), commRing := MonoidAlgebra.commRing } ⟶ Z) : CategoryTheory.CategoryStruct.comp ((specCommMonAlgPullback f Sf H).inv.app M).hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (MonoidAlgebra ↑R ↑(Opposite.unop M))))) Sf) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (MonoidAlgebra.mapRangeRingHom (↑(Opposite.unop M)) (CommRingCat.Hom.hom f)))) h

@[simp]

theorem AlgebraicGeometry.Scheme.specCommMonAlgPullback_inv_app_hom_left_snd {R S : CommRingCat} (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) (M : CommMonCatᵒᵖ) : CategoryTheory.CategoryStruct.comp ((specCommMonAlgPullback f Sf H).inv.app M).hom.left (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (MonoidAlgebra ↑R ↑(Opposite.unop M))))) Sf) = Spec.map (CommRingCat.ofHom (algebraMap ↑S ↑(Opposite.unop ((commBialgCatEquivComonCommAlgCat ↑S).functor.leftOp.obj ((commMonAlg ↑S).op.obj M)).X)))

@[simp]

theorem AlgebraicGeometry.Scheme.specCommMonAlgPullback_inv_app_hom_left_snd_assoc {R S : CommRingCat} (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) (M : CommMonCatᵒᵖ) {Z : Scheme} (h : Spec S ⟶ Z) : CategoryTheory.CategoryStruct.comp ((specCommMonAlgPullback f Sf H).inv.app M).hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (MonoidAlgebra ↑R ↑(Opposite.unop M))))) Sf) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap ↑S ↑(Opposite.unop ((commBialgCatEquivComonCommAlgCat ↑S).functor.leftOp.obj ((commMonAlg ↑S).op.obj M)).X)))) h

def AlgebraicGeometry.Scheme.specCommGrpAlgPullback {R S : CommRingCat} (f : R ⟶ S) (Sf : Spec S ⟶ Spec R) (H : Sf = Spec.map f) : (commGrpAlg ↑R).op.comp ((hopfSpec R).comp (CategoryTheory.Over.pullback Sf).mapGrp) ≅ (commGrpAlg ↑S).op.comp (hopfSpec S)

The spectrum of a group algebra functor commutes with base change.

Equations

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