Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom h)) =
    CategoryTheory.CategoryStruct.comp iV
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) h)

Defined in

Mathlib.AlgebraicGeometry.Normalization

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparatedAlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparatedAlgebraicGeometry.QuasiCompactAlgebraicGeometry.QuasiSeparated