comap_map_eq_map_adjoin_of_coprime_conductor

English

If hx and h_alg hold (coprimality and injectivity), then (I.map algebraMap R S).comap (algebraMap R<x> S) = I.map (algebraMap R R<x>).

Русский

При условиях hx и h_alg выполняется равенство: сонтрог помножение I.map(algebraMap R S) обратно через algebraMap R<x> S равно I.map (algebraMap R R<x>).

LaTeX

$$$(I.map(\\mathrm{algebraMap} \\ R S)).comap(\\mathrm{algebraMap} \\ R\\langle x\\rangle S) = I.map(\\mathrm{algebraMap} \\ R\\langle x\\rangle) $$$

Lean4

/-- A technical result telling us that `(I * S) ∩ R<x> = I * R<x>` for any ideal `I` of `R`. -/
theorem comap_map_eq_map_adjoin_of_coprime_conductor (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤)
    (h_alg : Function.Injective (algebraMap R<x> S)) :
    (I.map (algebraMap R S)).comap (algebraMap R<x> S) = I.map (algebraMap R R<x>) :=
  by
  apply le_antisymm
  · -- This is adapted from [Neukirch1992]. Let `C = (conductor R x)`. The idea of the proof
        -- is that since `I` and `C ∩ R` are coprime, we have
        -- `(I * S) ∩ R<x> ⊆ (I + C) * ((I * S) ∩ R<x>) ⊆ I * R<x> + I * C * S ⊆ I * R<x>`.

    intro y hy
    obtain ⟨z, hz⟩ := y
    obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp ((Ideal.eq_top_iff_one _).mp hx)
    have temp : algebraMap R S p * z + algebraMap R S q * z = z := by
      simp only [← add_mul, ← RingHom.map_add (algebraMap R S), hpq, map_one, one_mul]
    suffices z ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>) ↔ (⟨z, hz⟩ : R<x>) ∈ I.map (algebraMap R R<x>)
      by
      rw [← this, ← temp]
      obtain ⟨a, ha⟩ :=
        (Set.mem_image _ _ _).mp
          (prod_mem_ideal_map_of_mem_conductor hp (show z ∈ I.map (algebraMap R S) by rwa [Ideal.mem_comap] at hy))
      use a + algebraMap R R<x> q * ⟨z, hz⟩
      refine
        ⟨Ideal.add_mem (I.map (algebraMap R R<x>)) ha.left ?_, by simp only [ha.right, map_add, map_mul, add_right_inj];
          rfl⟩
      rw [mul_comm]
      exact Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ hq)
    refine ⟨fun h => ?_, fun h => (Set.mem_image _ _ _).mpr (Exists.intro ⟨z, hz⟩ ⟨by simp [h], rfl⟩)⟩
    obtain ⟨x₁, hx₁, hx₂⟩ := (Set.mem_image _ _ _).mp h
    have : x₁ = ⟨z, hz⟩ := by
      apply h_alg
      simp only [hx₂, algebraMap_eq_smul_one]
      rw [Submonoid.mk_smul, smul_eq_mul, mul_one]
    rwa [← this]
  · -- The converse inclusion is trivial

    have : algebraMap R S = (algebraMap _ S).comp (algebraMap R R<x>) := by ext; rfl
    rw [this, ← Ideal.map_map]
    apply Ideal.le_comap_map

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