Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint

∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).x))
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.Limits.pullback.fst f g) t) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap g (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).y))
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.Limits.pullback.snd f g) t)

Defined in

Mathlib.AlgebraicGeometry.PullbackCarrier

Cited by

1 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound