Clearing a finite family of denominators in a localization #
Mathlib's IsLocalization.finsetIntegerMultiple simultaneously clears the denominators of a
finite family in a localization. This file records how those cleared elements map back into the
localization and the resulting identity between the ideals generated before and after clearing.
Main results #
TauCeti.IsLocalization.algebraMap_integerMultiple: the cleared representative maps to the original element multiplied by the common denominator.TauCeti.IsLocalization.finsetIntegerMultiple_image_algebraMap: the image of the finite family of cleared representatives is the original family multiplied by the common denominator.TauCeti.IsLocalization.map_span_finsetIntegerMultiple: the ideal generated by the cleared representatives maps to the ideal generated by the original family.
theorem
TauCeti.IsLocalization.algebraMap_integerMultiple
{A : Type u_1}
{S : Type u_2}
[CommSemiring A]
[CommSemiring S]
[Algebra A S]
(M : Submonoid A)
[IsLocalization M S]
(T : Finset S)
(x : ↥T)
:
(algebraMap A S) (IsLocalization.integerMultiple M T id x) = ↑x * (algebraMap A S) ↑(IsLocalization.commonDenomOfFinset M T)
The image of an integer multiple used to clear a finite family of denominators is the original element multiplied by the image of the common denominator.
theorem
TauCeti.IsLocalization.finsetIntegerMultiple_image_algebraMap
{A : Type u_1}
{S : Type u_2}
[CommSemiring A]
[CommSemiring S]
[Algebra A S]
(M : Submonoid A)
[IsLocalization M S]
[DecidableEq A]
[DecidableEq S]
(T : Finset S)
:
Finset.image (⇑(algebraMap A S)) (IsLocalization.finsetIntegerMultiple M T) = Finset.image (fun (x : S) => x * (algebraMap A S) ↑(IsLocalization.commonDenomOfFinset M T)) T
The image of the finite family obtained by clearing denominators is the original family multiplied by the image of its common denominator.
theorem
TauCeti.IsLocalization.map_span_finsetIntegerMultiple
{A : Type u_1}
{S : Type u_2}
[CommSemiring A]
[CommSemiring S]
[Algebra A S]
(M : Submonoid A)
[IsLocalization M S]
[DecidableEq A]
(T : Finset S)
:
Clearing the denominators of a finite family does not change the ideal it generates after mapping to the localization.