English
Build a ModuleFilterBasis on a module M from a RingFilterBasis BR on R and an AddGroupFilterBasis BM on M, together with smul compatibility data smul, smul_left, smul_right which satisfy the expected subset relations.
Русский
Построить ModuleFilterBasis на модуле M из BR на R и BM на M с данными совместимости умножения smul, smul_left, smul_right, удовлетворяющими необходимым отношениям подмножеств.
LaTeX
$$$\text{ModuleFilterBasis.ofBases }(BR,BM,smul,smul\_left,smul\_right) : \text{ModuleFilterBasis } R M$.$$
Lean4
/-- Build a module filter basis from compatible ring and additive group filter bases. -/
def ofBases {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (BR : RingFilterBasis R)
(BM : AddGroupFilterBasis M) (smul : ∀ {U}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U)
(smul_left : ∀ (x₀ : R) {U}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U)
(smul_right : ∀ (m₀ : M) {U}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U) :
@ModuleFilterBasis R M _ BR.topology _ _ :=
let _ := BR.topology
{
BM with
smul' := by
intro U U_in
rcases smul U_in with ⟨V, V_in, W, W_in, H⟩
exact ⟨V, BR.toAddGroupFilterBasis.mem_nhds_zero V_in, W, W_in, H⟩
smul_left' := smul_left
smul_right' := by
intro m₀ U U_in
rcases smul_right m₀ U_in with ⟨V, V_in, H⟩
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H }
