English
A canonical data describing how to present a restricted scalars module, built from a presentation of M over B and a presentation of A over B.
Русский
Канонические данные, описывающие ограничение скаляров модуля, построенные из презентации M над B и презентации A над B.
LaTeX
$$$(presM.RestrictScalarsData presB) := (presM.finsupp presB.G).CokernelData(\\cdot)$$$
Lean4
/-- A presentation of the restriction of scalars from `B` to `A` of a `B`-module `M`,
given a presentation of `M` as a `B`-module, a presentation of `B` as an `A`-module,
and an additional data. -/
noncomputable def restrictScalars : Presentation A M :=
ofExact (g := LinearMap.restrictScalars A presM.π) (presB.finsupp presM.G) data presM.exact presM.surjective_π
(by
ext v
dsimp
simp only [Submodule.mem_top, iff_true]
apply Finsupp.induction
· simp
· intro r b w _ _ hw
refine Submodule.add_mem _ ?_ hw
obtain ⟨β, rfl⟩ := presB.surjective_π b
apply Finsupp.induction (motive := fun β ↦ Finsupp.single r (presB.π β) ∈ _)
· simp
· intro g a f _ _ hf
rw [map_add, Finsupp.single_add]
refine Submodule.add_mem _ ?_ hf
rw [← Finsupp.smul_single_one, ← Finsupp.smul_single_one, map_smul, Relations.Solution.π_single, smul_assoc]
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨⟨g, r⟩, rfl⟩))