English
A second variant reinforcing that the intNorm respects localization in the AKLB environment.
Русский
Второй вариант подчёркивает, что intNorm сохраняет локализацию в рамках AKLB.
LaTeX
$$$[IsLocalization M A_m] \\Rightarrow intNorm A B = intNorm A_m B_m\\ (after localization)$$$
Lean4
theorem dvd_algebraMap_intNorm_self [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (x : B) :
x ∣ algebraMap A B (intNorm A B x) := by
classical
by_cases hx : x = 0
· exact ⟨1, by simp [hx]⟩
let K := FractionRing A
let L := FractionRing B
let E := AlgebraicClosure L
suffices IsIntegral A ((algebraMap B L x)⁻¹ * (algebraMap A L (intNorm A B x)))
by
obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <| _root_.IsIntegral.tower_top (A := B) this
refine ⟨y, ?_⟩
apply FaithfulSMul.algebraMap_injective B L
rw [← IsScalarTower.algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
rw [← isIntegral_algHom_iff (IsScalarTower.toAlgHom A L E) (FaithfulSMul.algebraMap_injective L E),
IsScalarTower.coe_toAlgHom', map_mul, map_inv₀, IsScalarTower.algebraMap_apply A K L, algebraMap_intNorm (L := L), ←
IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply, norm_eq_prod_embeddings, ←
Finset.univ.mul_prod_erase _ (Finset.mem_univ (IsScalarTower.toAlgHom K L E)), IsScalarTower.coe_toAlgHom', ←
IsScalarTower.algebraMap_apply, inv_mul_cancel_left₀]
· refine _root_.IsIntegral.prod _ fun σ _ ↦ ?_
change IsIntegral A ((σ.restrictScalars A) (IsScalarTower.toAlgHom A B L x))
rw [isIntegral_algHom_iff _ (RingHom.injective _), isIntegral_algHom_iff _ (FaithfulSMul.algebraMap_injective B L)]
exact IsIntegral.isIntegral x
· have := NoZeroSMulDivisors.trans_faithfulSMul B L E
exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
