quotientToQuotientRangePowQuotSucc_injective

English

If a map between quotient modules is both injective and surjective, it is an isomorphism; this is used to compare quotient modules via ramification indices.

Русский

Если отображение между квотиентами инъективно и сюръективно, то оно изоморфизм; используется для сравнения квотиентов через ramificationIdx.

LaTeX

$$$(quotientToQuotientRangePowQuotSucc p P a\_mem) \\text{ is bijective }$$$

Lean4

theorem quotientToQuotientRangePowQuotSucc_injective [IsDedekindDomain S] [P.IsPrime] {i : ℕ} (hi : i < e) {a : S}
    (a_mem : a ∈ P ^ i) (a_notMem : a ∉ P ^ (i + 1)) :
    Function.Injective (quotientToQuotientRangePowQuotSucc p P a_mem) := fun x =>
  Quotient.inductionOn' x fun x y =>
    Quotient.inductionOn' y fun y h =>
      by
      have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1) := Ideal.pow_le_pow_right hi
      simp only [Submodule.Quotient.mk''_eq_mk, quotientToQuotientRangePowQuotSucc_mk, Submodule.Quotient.eq,
        LinearMap.mem_range, Subtype.ext_iff, Submodule.coe_sub] at h ⊢
      rcases h with ⟨⟨⟨z⟩, hz⟩, h⟩
      rw [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.mem_quotient_iff_mem_sup,
        sup_eq_left.mpr Pe_le_Pi1] at hz
      rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, ←
        map_sub, Ideal.Quotient.eq, ← mul_sub] at h
      exact (Ideal.IsPrime.mem_pow_mul _ ((Submodule.sub_mem_iff_right _ hz).mp (Pe_le_Pi1 h))).resolve_left a_notMem

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