Theorems · Theorem · algebraic geometry
AlgebraicGeometry.StructureSheaf.comap_apply
∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
(U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
(V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
(hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier)
(s : ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))) (p : ↥V),
↑((AlgebraicGeometry.StructureSheaf.comap f U V hUV) s) p =
(Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)- Defined in
- Mathlib.AlgebraicGeometry.StructureSheaf
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement · cited by 53,352
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functorstatement · cited by 16,252
- RingHomstatement and proof · cited by 10,189
- Oppositestatement · cited by 8,081
- Set.preimagestatement and proof · cited by 4,946
- Idealstatement · cited by 4,748
- TopCat.carrierstatement and proof · cited by 3,184
- CommRingCatstatement · cited by 2,333
- Opposite.unopstatement · cited by 2,231
Cited by5
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.StructureSheaf.toOpen_comp_comapproof · cited by 3
- AlgebraicGeometry.StructureSheaf.comap_compproof · cited by 1
- AlgebraicGeometry.Spec_Γ_naturalityproof · cited by 1
- AlgebraicGeometry.StructureSheaf.comap_id_eq_mapproof · cited by 1
- AlgebraicGeometry.StructureSheaf.comap_constproof · cited by 0