English
Let A,B be rings and e: A ≃+* B a ring equivalence compatible with a common ambient algebra C. Then for any x ∈ C, e(norm_A(x)) = norm_B(x).
Русский
Пусть A,B — кольца, e: A ≃+* B — кольцевой эквив, совместимый с общей алгеброй C. Тогда для любого x ∈ C выполняется e(norm_A(x)) = norm_B(x).
LaTeX
$$$ e(\\operatorname{norm}_A(x)) = \\operatorname{norm}_B(x) $$$
Lean4
theorem norm_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [Ring C] [Algebra A C] [Algebra B C]
(e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C) (x : C) : e (Algebra.norm A x) = Algebra.norm B x :=
by
classical
by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
· obtain ⟨s, ⟨b⟩⟩ := h
letI : Algebra A B := RingHom.toAlgebra e
letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
rw [Algebra.norm_eq_matrix_det b,
Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he])), e.map_det]
congr
ext i j
simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
rw [norm_eq_one_of_not_exists_basis _ h, norm_eq_one_of_not_exists_basis, map_one]
intro ⟨s, ⟨b⟩⟩
exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩
