equivNum — Mathlib

English

There is a linear equivalence between the fractional ideal I and its Num ideal, given by the map x ↦ I.den • x.

Русский

Существует линейное эквивалентное отображение между дробнымideal и его числителем, задаваемое отображением x ↦ I.den • x.

LaTeX

$$$I \\cong_{R} I.num \\quad\\text{via}\\quad x \\mapsto I.den \\cdot x$$$

Lean4

/-- The linear equivalence between the fractional ideal `I` and the integral ideal `I.num`
defined by mapping `x` to `den I • x`. -/
noncomputable def equivNum [Nontrivial P] [NoZeroSMulDivisors R P] {I : FractionalIdeal S P} (h_nz : (I.den : R) ≠ 0) :
    I ≃ₗ[R] I.num :=
  by
  refine
    LinearEquiv.trans
      (LinearEquiv.ofBijective ((DistribMulAction.toLinearMap R P I.den).restrict fun _ hx ↦ ?_)
        ⟨fun _ _ hxy ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩)
      (Submodule.equivMapOfInjective (Algebra.linearMap R P) (FaithfulSMul.algebraMap_injective R P) (num I)).symm
  · rw [← den_mul_self_eq_num]
    exact Submodule.smul_mem_pointwise_smul _ _ _ hx
  · simp_rw [LinearMap.restrict_apply, DistribMulAction.toLinearMap_apply, Subtype.mk.injEq] at hxy
    rwa [Submonoid.smul_def, Submonoid.smul_def, smul_right_inj h_nz, SetCoe.ext_iff] at hxy
  · rw [← den_mul_self_eq_num] at hy
    obtain ⟨x, hx, hxy⟩ := hy
    exact ⟨⟨x, hx⟩, by simp_rw [LinearMap.restrict_apply, Subtype.ext_iff, ← hxy]; rfl⟩

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