@@ -206,33 +206,31 @@ theorem comp_codLift :
206206end
207207
208208/-- Restrict domain and codomain of a linear map. -/
209- def restrict (f : M →ₗ[R ] M₁ ) {p : Submodule R M} {q : Submodule R M₁ } (hf : ∀ x ∈ p, f x ∈ q) :
210- p →ₗ[R ] q :=
209+ def restrict (f : M →ₛₗ[σ₁₂ ] M₂ ) {p : Submodule R M} {q : Submodule R₂ M₂ } (hf : ∀ x ∈ p, f x ∈ q) :
210+ p →ₛₗ[σ₁₂ ] q :=
211211 (f.domRestrict p).codRestrict q <| SetLike.forall.2 hf
212212
213213@[simp]
214- theorem restrict_coe_apply (f : M →ₗ[R ] M₁ ) {p : Submodule R M} {q : Submodule R M₁ }
214+ theorem restrict_coe_apply (f : M →ₛₗ[σ₁₂ ] M₂ ) {p : Submodule R M} {q : Submodule R₂ M₂ }
215215 (hf : ∀ x ∈ p, f x ∈ q) (x : p) : ↑(f.restrict hf x) = f x :=
216216 rfl
217217
218- theorem restrict_apply {f : M →ₗ[R ] M₁ } {p : Submodule R M} {q : Submodule R M₁ }
218+ theorem restrict_apply {f : M →ₛₗ[σ₁₂ ] M₂ } {p : Submodule R M} {q : Submodule R₂ M₂ }
219219 (hf : ∀ x ∈ p, f x ∈ q) (x : p) : f.restrict hf x = ⟨f x, hf x.1 x.2 ⟩ :=
220220 rfl
221221
222- lemma restrict_sub {R M M₁ : Type *}
223- [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁ ]
224- {p : Submodule R M} {q : Submodule R M₁ } {f g : M →ₗ[R ] M₁ }
222+ lemma restrict_sub {R R₂ M M₂ : Type *}
223+ [Ring R] [Ring R₂] {σ₁₂ : R →+* R₂} [AddCommGroup M] [AddCommGroup M₂ ]
224+ [Module R M] [Module R₂ M₂] {p : Submodule R M} {q : Submodule R₂ M₂ } {f g : M →ₛₗ[σ₁₂ ] M₂ }
225225 (hf : MapsTo f p q) (hg : MapsTo g p q)
226226 (hfg : MapsTo (f - g) p q := fun _ hx ↦ q.sub_mem (hf hx) (hg hx)) :
227227 f.restrict hf - g.restrict hg = (f - g).restrict hfg := by
228228 ext; simp
229229
230- lemma restrict_comp
231- {M₂ M₃ : Type *} [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃]
232- {p : Submodule R M} {p₂ : Submodule R M₂} {p₃ : Submodule R M₃}
233- {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃}
234- (hf : MapsTo f p p₂) (hg : MapsTo g p₂ p₃) (hfg : MapsTo (g ∘ₗ f) p p₃ := hg.comp hf) :
235- (g ∘ₗ f).restrict hfg = (g.restrict hg) ∘ₗ (f.restrict hf) :=
230+ lemma restrict_comp {p : Submodule R M} {p₂ : Submodule R₂ M₂} {p₃ : Submodule R₃ M₃}
231+ {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₃] M₃}
232+ (hf : MapsTo f p p₂) (hg : MapsTo g p₂ p₃) (hfg : MapsTo (g ∘ₛₗ f) p p₃ := hg.comp hf) :
233+ (g ∘ₛₗ f).restrict hfg = (g.restrict hg) ∘ₛₗ (f.restrict hf) :=
236234 rfl
237235
238236-- TODO Consider defining `Algebra R (p.compatibleMaps p)`, `AlgHom` version of `LinearMap.restrict`
@@ -248,17 +246,17 @@ lemma restrict_commute {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R
248246 change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)
249247 congr 1
250248
251- theorem subtype_comp_restrict {f : M →ₗ[R ] M₁ } {p : Submodule R M} {q : Submodule R M₁ }
249+ theorem subtype_comp_restrict {f : M →ₛₗ[σ₁₂ ] M₂ } {p : Submodule R M} {q : Submodule R₂ M₂ }
252250 (hf : ∀ x ∈ p, f x ∈ q) : q.subtype.comp (f.restrict hf) = f.domRestrict p :=
253251 rfl
254252
255- theorem restrict_eq_codRestrict_domRestrict {f : M →ₗ[R ] M₁ } {p : Submodule R M}
256- {q : Submodule R M₁ } (hf : ∀ x ∈ p, f x ∈ q) :
253+ theorem restrict_eq_codRestrict_domRestrict {f : M →ₛₗ[σ₁₂ ] M₂ } {p : Submodule R M}
254+ {q : Submodule R₂ M₂ } (hf : ∀ x ∈ p, f x ∈ q) :
257255 f.restrict hf = (f.domRestrict p).codRestrict q fun x => hf x.1 x.2 :=
258256 rfl
259257
260- theorem restrict_eq_domRestrict_codRestrict {f : M →ₗ[R ] M₁ } {p : Submodule R M}
261- {q : Submodule R M₁ } (hf : ∀ x, f x ∈ q) :
258+ theorem restrict_eq_domRestrict_codRestrict {f : M →ₛₗ[σ₁₂ ] M₂ } {p : Submodule R M}
259+ {q : Submodule R₂ M₂ } (hf : ∀ x, f x ∈ q) :
262260 (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p :=
263261 rfl
264262
0 commit comments