Theorems · Theorem · commutative algebra
RingHom.comap_ker
∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] (f : S →+* R)
(g : T →+* S), Ideal.comap g (RingHom.ker f) = RingHom.ker (f.comp g)- Defined in
- Mathlib.RingTheory.Ideal.Maps
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, 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.
- Semiringstatement and proof · cited by 13,802
- RingHomstatement and proof · cited by 10,189
- Idealstatement and proof · cited by 4,748
- Bot.botproof · cited by 4,720
- RingHom.compstatement and proof · cited by 899
- Ideal.comapstatement and proof · cited by 443
- RingHom.kerstatement and proof · cited by 363
- Ideal.comap_comapproof · cited by 27
- RingHom.ker_eq_comap_botproof · cited by 23
Cited by16
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.ker_applyproof · cited by 14
- AlgebraicGeometry.Scheme.Hom.support_kerproof · cited by 6
- AlgebraicGeometry.Scheme.Hom.le_ker_compproof · cited by 5
- RingHom.ker_equiv_compproof · cited by 3
- RingHom.ker_comp_of_injectiveproof · cited by 3
- AlgHom.comap_kerproof · cited by 2
- Ideal.ker_quotientMap_mkproof · cited by 1
- Algebra.Extension.cotangentComplex_comp_h1CotangentEquivCotangentproof · cited by 1
- Algebra.TensorProduct.map_kerproof · cited by 1
- AlgebraicGeometry.Scheme.ker_of_isAffineproof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTopproof · cited by 1