Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : CommRingCat}
  (h :
    (AlgebraicGeometry.Scheme.Hom.normalization f).presheaf.obj
        (Opposite.op ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.fromNormalization f) U) h =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap ↑(Y.presheaf.1 (Opposite.op U))
          ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))))))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU).inv h)

Defined in

Mathlib.AlgebraicGeometry.Normalization

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparated