English
If e1: A1 ≃+* A2 and e2: B1 ≃+* B2 satisfy a compatibility condition with embeddings into a common C, then for x ∈ B1 we have norm_A1(x) = e1^{-1}(norm_A2(e2 x)).
Русский
Если e1: A1 ≃+* A2 и e2: B1 ≃+* B2 удовлетворяют совместимости с вложениями в общий C, то для x ∈ B1 выполняется norm_A1(x) = e1^{-1}(norm_A2(e2 x)).
LaTeX
$$$ \\operatorname{norm}_{A_1}(x) = e_1^{-1}( \\operatorname{norm}_{A_2}( e_2 x ) ) $$$
Lean4
theorem norm_eq_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [Ring B₁] [CommRing A₂] [Ring B₂] [Algebra A₁ B₁]
[Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
(he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) (x) :
Algebra.norm A₁ x = e₁.symm (Algebra.norm A₂ (e₂ x)) :=
by
letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra' ?_
· let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }
rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e']
simp [e']
intro c x
apply e₂.symm.injective
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_mul, RingEquiv.symm_apply_apply, commutes]
