Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd

∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  Set.range ⇑(CategoryTheory.Limits.pullback.snd f g) =
    ↑((TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f))

Defined in: Mathlib.AlgebraicGeometry.OpenImmersion
Cited by: 4 results in Mathlib
Foundations: Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AlgebraicGeometry.IsOpenImmersion

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites42

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

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.Functor.mapproof · cited by 8,698
SetLike.coestatement and proof · cited by 8,199
CategoryTheory.Iso.homproof · cited by 7,684
Set.imageproof · cited by 5,609
Set.preimageproof · cited by 4,946
Set.rangestatement and proof · cited by 4,705
CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022

Cited by4

Results whose statement or proof uses this declaration.

AlgebraicGeometry.IsOpenImmersion.isPullbackproof · cited by 4
AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_leftproof · cited by 3
AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullbackproof · cited by 3
AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSndproof · cited by 0