coeSubmodule_differentIdeal — Mathlib

English

The dual operation on fractional ideals is an involution: applying it twice returns the original.

Русский

Операция двойственности над дробными идеалами является инволюторной: дважды применение возвращает исходный идеал.

LaTeX

$$Function.Involutive(dual) (A,K) on FractionalIdeal B^0 L$$

Lean4

theorem coeSubmodule_differentIdeal : coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 1 :=
  by
  have :
    (FractionRing.algEquiv B L).toLinearEquiv.comp (Algebra.linearMap B (FractionRing B)) = Algebra.linearMap B L := by
    ext; simp
  rw [coeSubmodule, ← this]
  have H :
    RingHom.comp (algebraMap (FractionRing A) (FractionRing B)) ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
      RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L) :=
    by
    apply IsLocalization.ringHom_ext A⁰
    ext
    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe, AlgEquiv.coe_ringEquiv,
      Function.comp_apply, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
    rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
  have : Algebra.IsSeparable (FractionRing A) (FractionRing B) := Algebra.IsSeparable.of_equiv_equiv _ _ H
  have : FiniteDimensional (FractionRing A) (FractionRing B) := Module.Finite.of_equiv_equiv _ _ H
  have : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra _ L
  simp only [AlgEquiv.toLinearEquiv_toLinearMap, Submodule.map_comp]
  rw [← coeSubmodule, coeSubmodule_differentIdeal_fractionRing _ _, Submodule.map_div, ← AlgEquiv.toAlgHom_toLinearMap,
    Submodule.map_one]
  congr 1
  refine (map_equiv_traceDual A K _).trans ?_
  congr 1
  ext
  simp

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