Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.hom_ext

∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} {f g : X ⟶ AlgebraicGeometry.AffineSpace n S},
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.AffineSpace n S ↘ S) =
      CategoryTheory.CategoryStruct.comp g (AlgebraicGeometry.AffineSpace n S ↘ S) →
    (∀ (i : n),
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
            (AlgebraicGeometry.AffineSpace.coord S i) =
          (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop g))
            (AlgebraicGeometry.AffineSpace.coord S i)) →
      f = g

Defined in

Mathlib.AlgebraicGeometry.AffineSpace

Cited by

8 results in Mathlib

Foundations

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