Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_range

∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  Set.range
      ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H').base) =
    ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

Defined in: Mathlib.Geometry.RingedSpace.OpenImmersion
Cited by: 0 results in Mathlib
Foundations: Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites46

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.objproof · cited by 19,642
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.Functor.mapproof · cited by 8,698
CategoryTheory.Iso.homproof · cited by 7,684
CategoryTheory.Functor.compproof · cited by 6,529
CategoryTheory.Category.assocproof · cited by 6,433
Set.ofPredproof · cited by 6,101
Set.imageproof · cited by 5,609
Set.preimagestatement and proof · cited by 4,946

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.