Theorems · Definition · commutative algebra
IsLocalRing.ResidueField.map
{R : Type u_1} →
{S : Type u_2} →
[inst : CommRing R] →
[inst_1 : IsLocalRing R] →
[inst_2 : CommRing S] →
[inst_3 : IsLocalRing S] →
(f : R →+* S) → [IsLocalHom f] → IsLocalRing.ResidueField R →+* IsLocalRing.ResidueField SThe map on residue fields induced by a local homomorphism between local rings
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- RingHom.compproof · cited by 899
- Ideal.Quotient.mkproof · cited by 610
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealproof · cited by 297
- IsLocalRing.ResidueFieldstatement · cited by 156
- IsLocalHomstatement and proof · cited by 100
- Ideal.Quotient.liftproof · cited by 19
Cited by21
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.residueFieldMapproof · cited by 28
- AlgebraicGeometry.LocallyRingedSpace.residueFieldMapproof · cited by 10
- Ideal.ResidueField.mapproof · cited by 8
- IsLocalRing.ResidueField.mapEquivproof · cited by 5
- AlgebraicGeometry.LocallyRingedSpace.evaluation_naturalityproof · cited by 4
- IsLocalRing.ResidueField.map_compstatement · cited by 3
- IsLocalRing.ResidueField.map_idstatement · cited by 3
- IsLocalRing.ResidueField.map_residuestatement · cited by 2
- IsLocalRing.ResidueField.map.congr_simpstatement and proof · cited by 2
- IsLocalRing.ResidueField.map_comp_residuestatement · cited by 1
- AdicCompletion.residueField_map_bijectivestatement · cited by 1
- AdicCompletion.residueField_map_bijective_of_fgstatement and proof · cited by 1