Theorems · Theorem · commutative algebra

Ideal.primaryComponent.map_surjective

∀ {A : Type u_1} [inst : CommRing A] [IsDedekindDomain A] {M₁ : Type u_5} {M₂ : Type u_6} [inst_2 : AddCommGroup M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₁] [inst_5 : Module A M₂],
  Module.IsTorsion A M₁ →
    ∀ (P : IsDedekindDomain.HeightOneSpectrum A) (φ : M₁ →ₗ[A] M₂),
      Function.Surjective ⇑φ → Function.Surjective ⇑(Ideal.primaryComponent.map P.asIdeal φ)

Defined in

Mathlib.Algebra.Module.Torsion.PrimaryComponent

Cited by

0 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainAddCommGroupAddCommGroupModuleModule