Field/algebra norm and localization #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains results on the combination of algebra.norm and is_localization.

Main results #

algebra.norm_localization: let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the norm of a : Sₘ over Rₘ is the norm of a : S over R if S is free as R-module

Tags #

field norm, algebra norm, localization

theorem algebra.norm_localization (R : Type u_1) {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [comm_ring Rₘ] [algebra R Rₘ] [comm_ring Sₘ] [algebra S Sₘ] (M : submonoid R) [is_localization M Rₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ] [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] [module.free R S] [module.finite R S] (a : S) :

⇑(algebra.norm Rₘ) (⇑(algebra_map S Sₘ) a) = ⇑(algebra_map R Rₘ) (⇑(algebra.norm R) a)

Let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the norm of a : Sₘ over Rₘ is the norm of a : S over R if S is free as R-module.