English
If I,J are fractional ideals with compatibility conditions, then the dual respects linear combinations and restrictions along trace.
Русский
При совместимости а(р) дуальность сохраняется при линейных combinations и ограничениях по trace.
LaTeX
$$$I,J : \text{FractionalIdeal} \; (nonZeroDivisors B) L \quad \Rightarrow\quad \text{dual}$ preserves restrictions and linear combinations via trace.$$
Lean4
/-- If `b` is an `A`-integral basis of `L` with discriminant `b`, then `d • a * x` is integral over
`A` for all `a ∈ I` and `x ∈ Iᵛ`. -/
theorem isIntegral_discr_mul_of_mem_traceDual (I : Submodule B L) {ι} [DecidableEq ι] [Fintype ι] {b : Basis ι K L}
(hb : ∀ i, IsIntegral A (b i)) {a x : L} (ha : a ∈ I) (hx : x ∈ Iᵛ) : IsIntegral A ((discr K b) • a * x) :=
by
have hinv : IsUnit (traceMatrix K b).det := by simpa [← discr_def] using discr_isUnit_of_basis _ b
have H := mulVec_cramer (traceMatrix K b) fun i => trace K L (x * a * b i)
have : Function.Injective (traceMatrix K b).mulVec := by rwa [mulVec_injective_iff_isUnit, isUnit_iff_isUnit_det]
rw [← traceMatrix_of_basis_mulVec, ← mulVec_smul, this.eq_iff, traceMatrix_of_basis_mulVec] at H
rw [← b.equivFun.symm_apply_apply (_ * _), b.equivFun_symm_apply]
apply IsIntegral.sum
intro i _
rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def]
refine RingHom.IsIntegralElem.mul _ ?_ (hb _)
apply IsIntegral.algebraMap
rw [cramer_apply]
apply IsIntegral.det
intro j k
rw [updateCol_apply]
split
· rw [mul_assoc]
rw [mem_traceDual_iff_isIntegral] at hx
apply hx
have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp (hb j)
rw [mul_comm, ← hy, ← Algebra.smul_def]
exact I.smul_mem _ (ha)
· exact isIntegral_trace (RingHom.IsIntegralElem.mul _ (hb j) (hb k))
