not_dvd_differentIdeal_of_intTrace_not_mem

English

If P and Q are coprime and P Q maps to p, then P does not divide the different ideal under separability assumptions.

Русский

Если P и Q взаимно простые и PQ образуют p, тогда P не делит различный идеал при сепарабельности.

LaTeX

$$¬(P ∣ differentIdeal(A,B))$$

Lean4

theorem not_dvd_differentIdeal_of_intTrace_not_mem [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A}
    (P Q : Ideal B) (hP : P * Q = Ideal.map (algebraMap A B) p) (x : B) (hxQ : x ∈ Q)
    (hx : Algebra.intTrace A B x ∉ p) : ¬P ∣ differentIdeal A B :=
  by
  by_cases hp : p = ⊥
  · subst hp
    simp only [Ideal.map_bot, Ideal.mul_eq_bot] at hP
    obtain (rfl | rfl) := hP
    · rw [← Ideal.zero_eq_bot, zero_dvd_iff]
      exact differentIdeal_ne_bot
    · obtain rfl := hxQ
      simp at hx
  letI : Algebra (A ⧸ p) (B ⧸ Q) :=
    Ideal.Quotient.algebraQuotientOfLEComap
      (by
        rw [← Ideal.map_le_iff_le_comap, ← hP]
        exact Ideal.mul_le_left)
  let K := FractionRing A
  let L := FractionRing B
  have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L := IsIntegralClosure.isLocalization _ K _ _
  have : FiniteDimensional K L := .of_isLocalization A B A⁰
  rw [Ideal.dvd_iff_le]
  intro H
  replace H := (mul_le_mul_right' H Q).trans_eq hP
  replace H := (FractionalIdeal.coeIdeal_le_coeIdeal' _ (P := L) le_rfl).mpr H
  rw [FractionalIdeal.coeIdeal_mul, coeIdeal_differentIdeal A K] at H
  replace H := mul_le_mul_left' H (FractionalIdeal.dual A K 1)
  simp only [ne_eq, FractionalIdeal.dual_eq_zero_iff, one_ne_zero, not_false_eq_true, mul_inv_cancel_left₀] at H
  apply hx
  suffices Algebra.trace K L (algebraMap B L x) ∈ (p : FractionalIdeal A⁰ K)
    by
    obtain ⟨y, hy, e⟩ := this
    rw [← Algebra.algebraMap_intTrace (A := A), Algebra.linearMap_apply,
      (IsLocalization.injective _ le_rfl).eq_iff] at e
    exact e ▸ hy
  refine FractionalIdeal.mul_induction_on (H ⟨_, hxQ, rfl⟩) ?_ ?_
  · rintro x hx _ ⟨y, hy, rfl⟩
    induction hy using Submodule.span_induction generalizing x with
    | mem y h =>
      obtain ⟨y, hy, rfl⟩ := h
      obtain ⟨z, hz⟩ := (FractionalIdeal.mem_dual (by simp)).mp hx 1 ⟨1, trivial, (algebraMap B L).map_one⟩
      simp only [Algebra.traceForm_apply, mul_one] at hz
      refine ⟨z * y, Ideal.mul_mem_left _ _ hy, ?_⟩
      rw [Algebra.linearMap_apply, Algebra.linearMap_apply, mul_comm x, ← IsScalarTower.algebraMap_apply, ←
        Algebra.smul_def, LinearMap.map_smul_of_tower, ← hz, Algebra.smul_def, map_mul, mul_comm]
    | zero => simp
    | add y z _ _ hy hz =>
      simp only [map_add, mul_add]
      exact Submodule.add_mem _ (hy x hx) (hz x hx)
    | smul y z hz IH =>
      simpa [Algebra.smul_def, mul_assoc, -FractionalIdeal.mem_coeIdeal, mul_left_comm x] using
        IH _ (Submodule.smul_mem _ y hx)
  · simp only [map_add]
    exact fun _ _ h₁ h₂ ↦ Submodule.add_mem _ h₁ h₂

Похожие утверждения