English
If two powMul algebra norms are equivalent on every subring R[y], they are equal.
Русский
Если две powMul алгебрnorm эквивалентны на каждом подкольце R[y], то они равны.
LaTeX
$$f = g$$
Lean4
/-- Given two power-multiplicative ring seminorms `f, g` on `α`, if `f` is bounded by a positive
multiple of `g` and vice versa, then `f = g`. -/
theorem eq_seminorms {F : Type*} {α : outParam (Type*)} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {f g : F}
(hfpm : IsPowMul f) (hgpm : IsPowMul g) (hfg : ∃ (r : ℝ) (_ : 0 < r), ∀ a : α, f a ≤ r * g a)
(hgf : ∃ (r : ℝ) (_ : 0 < r), ∀ a : α, g a ≤ r * f a) : f = g :=
by
obtain ⟨r, hr0, hr⟩ := hfg
obtain ⟨s, hs0, hs⟩ := hgf
have hle : RingHom.IsBoundedWrt f g (RingHom.id _) := ⟨s, hs0, hs⟩
have hge : RingHom.IsBoundedWrt g f (RingHom.id _) := ⟨r, hr0, hr⟩
rw [← Function.Injective.eq_iff DFunLike.coe_injective']
ext x
exact
le_antisymm (contraction_of_isPowMul_of_boundedWrt g hfpm hge x)
(contraction_of_isPowMul_of_boundedWrt f hgpm hle x)
