English
The intersection of two lattices is again a lattice over K.
Русский
Пересечение двух решёток над K снова является решёткой над K.
LaTeX
$$$IsLattice_K(M \cap N)$$$
Lean4
/-- The intersection of two lattices is a lattice. -/
instance inf [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V) [IsLattice K M] [IsLattice K N] :
IsLattice K (M ⊓ N)
where
fg := by
have : IsNoetherian R ↥(M ⊓ N) := isNoetherian_of_le inf_le_left
rw [← Module.Finite.iff_fg]
infer_instance
span_eq_top := by
rw [← range_subtype (M ⊓ N)]
apply Submodule.span_range_eq_top_of_injective_of_rank_le (M ⊓ N).injective_subtype
have h := Submodule.rank_sup_add_rank_inf_eq M N
rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h
rw [Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)]
