English
For ideals I,J of S, spanNorm R I multiplied by spanNorm R J is above or equal to spanNorm R (I J).
Русский
Для идеалов I, J из S произведение spanNorm R I и spanNorm R J доминирует над spanNorm R (I J).
LaTeX
$$$$\operatorname{spanNorm}(R,I) \cdot \operatorname{spanNorm}(R,J) \le \operatorname{spanNorm}(R, IJ). $$$$
Lean4
theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰) {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ]
[Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ]
[IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[IsIntegrallyClosed Rₘ] [IsDomain Rₘ] [IsDomain Sₘ] [NoZeroSMulDivisors Rₘ Sₘ] [Module.Finite Rₘ Sₘ]
[IsIntegrallyClosed Sₘ] : spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ) :=
by
let K := FractionRing R
let f : Rₘ →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
let L := FractionRing S
let g : Sₘ →+* L :=
IsLocalization.map _ (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) (RingHom.id S)
(Submonoid.map_le_of_le_comap _ <|
hM.trans (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _)))
algebraize [f, g, (algebraMap K L).comp f]
have : IsScalarTower R Rₘ K :=
IsScalarTower.of_algebraMap_eq'
(by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
have : IsScalarTower S Sₘ L :=
IsScalarTower.of_algebraMap_eq'
(by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
have : IsScalarTower Rₘ Sₘ L := by
apply IsScalarTower.of_algebraMap_eq'
apply IsLocalization.ringHom_ext M
rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc, RingHom.comp_assoc, ←
IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ, IsLocalization.map_comp, RingHom.comp_id, ←
RingHom.comp_assoc, IsLocalization.map_comp, RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ←
IsScalarTower.algebraMap_eq]
let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
rw [map_spanIntNorm]
refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
· intro a' ha'
simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩, ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩
simp only [map_pow] at has ⊢
apply_fun algebraMap _ L at has
apply_fun Algebra.norm K at has
simp only [map_mul] at has
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
IsScalarTower.algebraMap_apply R K L, Algebra.norm_algebraMap] at has
apply IsFractionRing.injective Rₘ K
simp only [map_mul, map_pow]
rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
Algebra.algebraMap_intNorm (L := L)]
· intro a ha
rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization M (Bₘ := Sₘ)]
exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))
