case h'
R : Type u_1
M : Type u_2
M₂ : Type ?u.57346
M₃ : Type ?u.57349
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ker (subToSupQuotient p p') ≤ comap (Submodule.subtype p) (p ⊓ p')
R : Type u_1
M : Type u_2
M₂ : Type ?u.57346
M₃ : Type ?u.57349
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ Function.Injective ↑(quotientInfToSupQuotient p p')
rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]
case h'
R : Type u_1
M : Type u_2
M₂ : Type ?u.57346
M₃ : Type ?u.57349
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (ofLe (_ : p ≤ p ⊔ p')) (comap (Submodule.subtype (p ⊔ p')) p') ≤ comap (Submodule.subtype p) (p ⊓ p')
case h'
R : Type u_1
M : Type u_2
M₂ : Type ?u.57346
M₃ : Type ?u.57349
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ker (subToSupQuotient p p') ≤ comap (Submodule.subtype p) (p ⊓ p')
rw [ker_comp, ker_mkQ]
no goals
case h'
R : Type u_1
M : Type u_2
M₂ : Type ?u.57346
M₃ : Type ?u.57349
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (ofLe (_ : p ≤ p ⊔ p')) (comap (Submodule.subtype (p ⊔ p')) p') ≤ comap (Submodule.subtype p) (p ⊓ p')
exact fun ⟨x, hx1⟩ hx2 => ⟨hx1, hx2⟩