Theorems · Definition · commutative algebra
KaehlerDifferential.ideal
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Ideal (TensorProduct R S S)
The kernel of the multiplication map S ⊗[R] S →ₐ[R] S.
- Defined in
- Mathlib.RingTheory.Kaehler.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Algebrastatement and proof · cited by 11,388
- Idealstatement · cited by 4,748
- TensorProductstatement · cited by 2,545
- RingHom.kerproof · cited by 363
- Algebra.TensorProduct.lmul'proof · cited by 28
Cited by23
Results whose statement or proof uses this declaration.
- KaehlerDifferentialproof · cited by 204
- Derivation.liftKaehlerDifferentialproof · cited by 12
- KaehlerDifferential.one_smul_sub_smul_one_mem_idealstatement · cited by 7
- KaehlerDifferential.span_range_derivationproof · cited by 7
- KaehlerDifferential.tensorProductTo_surjectiveproof · cited by 3
- KaehlerDifferential.fromIdealstatement and proof · cited by 2
- KaehlerDifferential.ideal_fgstatement and proof · cited by 2
- Derivation.liftKaehlerDifferential_applystatement and proof · cited by 2
- Algebra.FormallyUnramified.iff_exists_tensorProductproof · cited by 2
- KaehlerDifferential.submodule_span_range_eq_idealstatement and proof · cited by 2
- KaehlerDifferential.DLinearMapproof · cited by 1
- KaehlerDifferential.DLinearMap_applystatement · cited by 1