Theorems · Theorem · ring theory
Algebra.algebraMapSubmonoid_le_comap
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submonoid R)
{B : Type w} [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
Algebra.algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Algebra.algebraMapSubmonoid B M)- Defined in
- Mathlib.Algebra.Algebra.Hom
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement · cited by 10,189
- AlgHomstatement and proof · cited by 3,236
- Submonoidstatement and proof · cited by 3,086
- AlgHom.toRingHomstatement and proof · cited by 490
- Submonoid.comapstatement and proof · cited by 179
- Algebra.algebraMapSubmonoidstatement and proof · cited by 137
- Submonoid.le_comap_mapproof · cited by 24
- Algebra.algebraMapSubmonoid_map_eqproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- injective_of_isLocalization_of_span_eq_topproof · cited by 1
- IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐproof · cited by 1
- surjective_of_isLocalization_of_span_eq_topproof · cited by 1
- IsLocalization.mapₐ_coestatement · cited by 0
- AlgHom.toKerIsLocalization_applystatement · cited by 0