Theorems · Theorem · algebraic geometry
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
[inst_1 : AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g),
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).hom g = f- Defined in
- Mathlib.AlgebraicGeometry.OpenImmersion
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
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 · cited by 53,352
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Iso.homstatement · cited by 7,684
- Set.rangestatement and proof · cited by 4,705
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- TopCat.carrierstatement · cited by 3,184
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- ContinuousMapstatement · cited by 2,491
- CommRingCatstatement · cited by 2,333
- AlgebraicGeometry.PresheafedSpace.carrierstatement · cited by 2,020
Cited by13
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.isoImage_hom_ιproof · cited by 9
- AlgebraicGeometry.Scheme.isoOfEq_hom_ιproof · cited by 7
- AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ιproof · cited by 6
- AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayιproof · cited by 3
- AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpenproof · cited by 2
- AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ιproof · cited by 2
- AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ιproof · cited by 2
- AlgebraicGeometry.IsZariskiLocalAtSource.mk'proof · cited by 2
- AlgebraicGeometry.basicOpenIsoSpecAway_hom_SpecMapproof · cited by 1
- AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ιproof · cited by 1
- AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac_assocproof · cited by 1