R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
⊢ comap f (map f p) ≤ p ⊔ LinearMap.ker f
R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
⊢ comap f (map f p) = p ⊔ LinearMap.ker f
refine' le_antisymm _ (sup_le (le_comap_map _ _) (comap_mono bot_le))
case intro.intro
R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
x y : M
hy : y ∈ ↑p
e : ↑f y = ↑f x
⊢ x ∈ p ⊔ LinearMap.ker f
R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
⊢ comap f (map f p) ≤ p ⊔ LinearMap.ker f
rintro x ⟨y, hy, e⟩
no goals
case intro.intro
R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
x y : M
hy : y ∈ ↑p
e : ↑f y = ↑f x
⊢ x ∈ p ⊔ LinearMap.ker f
exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩
no goals
R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
x y : M
hy : y ∈ ↑p
e : ↑f y = ↑f x
⊢ x - y ∈ LinearMap.ker f
simpa using sub_eq_zero.2 e.symm
no goals
R : Type u_1
R₂ : Type u_3
K : Type ?u.292037
M : Type u_2
M₂ : Type u_4
V : Type ?u.292046
S : Type ?u.292049
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
x y : M
hy : y ∈ ↑p
e : ↑f y = ↑f x
⊢ y + (x - y) = x
simp