Clearing denominators in the image of a linear map #
Pulling Mathlib's multiple_mem_span_of_mem_localization_span back along an injective linear map
clears denominators in a localized span. This applies to arbitrary spanning sets in modules,
including lifts of a basis along an injective algebra map.
Main results #
LinearMap.exists_smul_mem_span_of_apply_mem_span_image: if an injective linear map sends an element into the localized span of the image of a set, a multiple of that element by a denominator lies in the original span.
theorem
LinearMap.exists_smul_mem_span_of_apply_mem_span_image
{A : Type u_1}
{K : Type u_2}
{B : Type u_3}
{L : Type u_4}
[CommSemiring A]
[CommSemiring K]
[Algebra A K]
[AddCommMonoid B]
[AddCommMonoid L]
[Module A B]
[Module A L]
[Module K L]
[IsScalarTower A K L]
(f : B →ₗ[A] L)
(hf : Function.Injective ⇑f)
(M : Submonoid A)
[IsLocalization M K]
(s : Set B)
(x : B)
(hx : f x ∈ Submodule.span K (⇑f '' s))
:
∃ a ∈ M, a • x ∈ Submodule.span A s
If an injective linear map sends x into the span over a localization of the image of s,
then a multiple of x by an element of the localizing submonoid lies in the original span
of s.