Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_lift_of_germInjective_aux

∀ {X : AlgebraicGeometry.Scheme} {R A : CommRingCat} {U : X.Opens} {x : ↥X} (hxU : x ∈ U) (φ : A ⟶ X.presheaf.stalk x)
  (φRA : R ⟶ A) (φRX : R ⟶ X.presheaf.obj (Opposite.op U)),
  (CommRingCat.Hom.hom φRA).FiniteType →
    CategoryTheory.CategoryStruct.comp φRA φ = CategoryTheory.CategoryStruct.comp φRX (X.presheaf.germ U x hxU) →
      ∃ V,
        ∃ (hxV : x ∈ V), V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range

Defined in

Mathlib.AlgebraicGeometry.SpreadingOut

Cited by

1 results in Mathlib

Foundations

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