Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.toImage_app

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : ↑Y.affineOpens),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.toImage f)
      ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.imageι f).base).obj ↑U) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.ker f).subschemeObjIso U).hom
      (CommRingCat.ofHom
        (Ideal.Quotient.lift ((AlgebraicGeometry.Scheme.Hom.ker f).ideal U)
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U)) ⋯))

Defined in: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Cited by: 1 results in Mathlib
Foundations: Depth 215 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites67

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
RingHomstatement and proof · cited by 10,189
CategoryTheory.Functor.mapproof · cited by 8,698
Oppositestatement · cited by 8,081
CategoryTheory.Iso.homstatement and proof · cited by 7,684
Set.Elemstatement and proof · cited by 7,166
CategoryTheory.Iso.invproof · cited by 6,514
CategoryTheory.Category.assocproof · cited by 6,433
Idealstatement · cited by 4,748

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.Hom.toImage_app_injectiveproof · cited by 1