R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ span R (↑f ⁻¹' s) = comap f (span R₂ s)
suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : ker f ≤ span R (↑f ⁻¹' s)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
have hk : ker f ≤ span R (f ⁻¹' s) := by
  let y := Classical.choose h₀
  have hy : y ∈ s := Classical.choose_spec h₀
  rw [ker_le_iff]
  use y, h₁ hy
  rw [← Set.singleton_subset_iff] at hy
  exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : ker f ≤ span R (↑f ⁻¹' s)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
rw [← left_eq_sup] at hk
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
rw [range_coe f] at h₁
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ range f ⊓ span R₂ s ≤ span R₂ s
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]
no goals
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ range f ⊓ span R₂ s ≤ span R₂ s
exact inf_le_right
no goals
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
this : comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
⊢ span R (↑f ⁻¹' s) = comap f (span R₂ s)
exact le_antisymm (span_preimage_le f s) this
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
⊢ ker f ≤ span R (↑f ⁻¹' s)
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ ker f ≤ span R (↑f ⁻¹' s)
let y := Classical.choose h₀
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ker f ≤ span R (↑f ⁻¹' s)
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
⊢ ker f ≤ span R (↑f ⁻¹' s)
have hy : y ∈ s := Classical.choose_spec h₀
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ker f ≤ span R (↑f ⁻¹' s)
rw [ker_le_iff]
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
use y, h₁ hy
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
rw [← Set.singleton_subset_iff] at hy
no goals
R : Type u_1
M : Type u_3
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))