1. Physlib
  2. Mathematics
  3. LinearPMap
Imports
/- Copyright (c) 2026 Gregory J. Loges. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gregory J. Loges -/ module public import Mathlib.Analysis.InnerProductSpace.LinearPMap

LinearPMap

i. Overview

In this module we collect some basic results about LinearPMaps.

Most important is the definition of restricted composition. The composition of two partial linear maps g : F →ₗ.[R] G and f : E →ₗ.[R] F is defined only if the range of f is contained in the domain of g (c.f. LinearPMap.comp). g.compRestricted f (g ∘ᵣ f) is defined to be the composition of g with the restriction of f to exactly those x : f.domain for which f x ∈ g.domain. This allows one to work with the composition of partial linear maps while having the domain implicitly accounted for.

ii. Key results

    LinearPMap.sum : The finite sum of partial linear maps.

    LinearPMap.compRestricted (∘ᵣ) : For two partial linear maps g : F →ₗ[R] G and f : E →ₗ[R] F, the composition of g with f with natural domain {x : f.domain | f x ∈ g.domain}.

    LinearPMap.instMonoid : Partial linear maps E →ₗ.[R] E with compRestricted for multiplication and the identity map for 1 comprise a monoid.

iii. Table of contents

    A. Inequalities

    B. Zero smul

    C. Finite sums

    D. Restricted composition

    E. Monoid

    F. Inverses

iv. References

@[expose] public section

A. Inequalities

lemma sub_le_zero : f - f ≤ 0 := ⟨le_top, R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] F⊢ ∀ ⦃x : ↥(f - f).domain⦄ ⦃y : ↥(domain 0)⦄, ↑x = ↑y → ↑(f - f) x = ↑0 y All goals completed! 🐙⟩lemma neg_add_le_zero : -f + f ≤ 0 := ⟨le_top, R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] F⊢ ∀ ⦃x : ↥(-f + f).domain⦄ ⦃y : ↥(domain 0)⦄, ↑x = ↑y → ↑(-f + f) x = ↑0 y All goals completed! 🐙⟩lemma le_iff_neg_le_neg : g₁ ≤ g₂ ↔ -g₁ ≤ -g₂ := ⟨fun ⟨h, h'⟩ ↦ ⟨h, fun _ _ h'' ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fx✝²:g₁ ≤ g₂h:g₁.domain ≤ g₂.domainh':∀ ⦃x : ↥g₁.domain⦄ ⦃y : ↥g₂.domain⦄, ↑x = ↑y → ↑g₁ x = ↑g₂ yx✝¹:↥(-g₁).domainx✝:↥(-g₂).domainh'':↑x✝¹ = ↑x✝⊢ ↑(-g₁) x✝¹ = ↑(-g₂) x✝ All goals completed! 🐙⟩, fun ⟨h, _⟩ ↦ ⟨h, fun _ _ _ ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fx✝³:-g₁ ≤ -g₂h:(-g₁).domain ≤ (-g₂).domainright✝:∀ ⦃x : ↥(-g₁).domain⦄ ⦃y : ↥(-g₂).domain⦄, ↑x = ↑y → ↑(-g₁) x = ↑(-g₂) yx✝²:↥g₁.domainx✝¹:↥g₂.domainx✝:↑x✝² = ↑x✝¹⊢ ↑g₁ x✝² = ↑g₂ x✝¹ All goals completed! 🐙⟩⟩All goals completed! 🐙lemma add_sub_le_cancel : f₁ + (f₂ - f₁) ≤ f₂ := ⟨R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ (f₁ + (f₂ - f₁)).domain ≤ f₂.domain All goals completed! 🐙, fun _ _ h ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx✝¹:↥(f₁ + (f₂ - f₁)).domainx✝:↥f₂.domainh:↑x✝¹ = ↑x✝⊢ ↑(f₁ + (f₂ - f₁)) x✝¹ = ↑f₂ x✝ All goals completed! 🐙⟩lemma add_sub_le_cancel_left : f₁ + f₂ - f₁ ≤ f₂ := add_sub_assoc f₁ f₂ f₁ ▸ add_sub_le_cancel f₁ f₂lemma add_sub_le_cancel_right : f₁ + f₂ - f₂ ≤ f₁ := add_comm f₁ f₂ ▸ add_sub_le_cancel_left f₂ f₁lemma add_add_sub_le_cancel : f₁ + f₂ + (f₃ - f₂) ≤ f₁ + f₃ := ⟨fun _ _ ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Ff₃:E →ₗ.[R] Fx✝¹:Ex✝:x✝¹ ∈ (f₁ + f₂ + (f₃ - f₂)).domain⊢ x✝¹ ∈ (f₁ + f₃).domain All goals completed! 🐙, fun _ _ h ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Ff₃:E →ₗ.[R] Fx✝¹:↥(f₁ + f₂ + (f₃ - f₂)).domainx✝:↥(f₁ + f₃).domainh:↑x✝¹ = ↑x✝⊢ ↑(f₁ + f₂ + (f₃ - f₂)) x✝¹ = ↑(f₁ + f₃) x✝ All goals completed! 🐙⟩lemma add_sub_sub_le_cancel : f₁ + f₂ - (f₁ - f₃) ≤ f₂ + f₃ := ⟨fun _ _ ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Ff₃:E →ₗ.[R] Fx✝¹:Ex✝:x✝¹ ∈ (f₁ + f₂ - (f₁ - f₃)).domain⊢ x✝¹ ∈ (f₂ + f₃).domain All goals completed! 🐙, fun _ _ h ↦ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Ff₃:E →ₗ.[R] Fx✝¹:↥(f₁ + f₂ - (f₁ - f₃)).domainx✝:↥(f₂ + f₃).domainh:↑x✝¹ = ↑x✝⊢ ↑(f₁ + f₂ - (f₁ - f₃)) x✝¹ = ↑(f₂ + f₃) x✝ All goals completed! 🐙⟩lemma sub_sub_sub_le_cancel_right : f₁ - f₂ - (f₃ - f₂) ≤ f₁ - f₃ := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Ff₃:E →ₗ.[R] F⊢ f₁ - f₂ - (f₃ - f₂) ≤ f₁ - f₃ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Ff₃:E →ₗ.[R] F⊢ f₁ + -f₂ + (-f₃ + - -f₂) ≤ f₁ + -f₃ All goals completed! 🐙lemma sub_sub_sub_le_cancel_left : f₁ - f₂ - (f₁ - f₃) ≤ f₃ - f₂ := sub_eq_add_neg f₁ f₂ ▸ neg_add_eq_sub f₂ f₃ ▸ add_sub_sub_le_cancel f₁ (-f₂) f₃lemma sub_le_of_le_add (h : g ≤ g₁ + g₂) : g - g₂ ≤ g₁ := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g ≤ g₁ + g₂⊢ g - g₂ ≤ g₁ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g ≤ g₁ + g₂⊢ (g - g₂).domain ≤ g₁.domainR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g ≤ g₁ + g₂⊢ ∀ ⦃x : ↥(g - g₂).domain⦄ ⦃y : ↥g₁.domain⦄, ↑x = ↑y → ↑(g - g₂) x = ↑g₁ y R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g ≤ g₁ + g₂⊢ (g - g₂).domain ≤ g₁.domain All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g ≤ g₁ + g₂⊢ ∀ ⦃x : ↥(g - g₂).domain⦄ ⦃y : ↥g₁.domain⦄, ↑x = ↑y → ↑(g - g₂) x = ↑g₁ y R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Fg:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g ≤ g₁ + g₂x:Ehx:x ∈ (g - g₂).domainhy:↑⟨x, hx⟩ ∈ g₁.domain⊢ ↑(g - g₂) ⟨x, hx⟩ = ↑g₁ ⟨↑⟨x, hx⟩, hy⟩ All goals completed! 🐙lemma sub_add_le_cancel : f₁ - f₂ + f₂ ≤ f₁ := sub_eq_add_neg f₁ f₂ ▸ sub_neg_eq_add _ f₂ ▸ add_sub_le_cancel_right f₁ (-f₂)lemma add_le_of_le_sub (h : g ≤ g₁ - g₂) : g + g₂ ≤ g₁ := sub_neg_eq_add g g₂ ▸ sub_le_of_le_add (sub_eq_add_neg g₁ g₂ ▸ h)lemma add_left_le_of_le (h : g₁ ≤ g₂) : f + g₁ ≤ f + g₂ := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂⊢ f + g₁ ≤ f + g₂ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂⊢ (f + g₁).domain ≤ (f + g₂).domainR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂⊢ ∀ ⦃x : ↥(f + g₁).domain⦄ ⦃y : ↥(f + g₂).domain⦄, ↑x = ↑y → ↑(f + g₁) x = ↑(f + g₂) y R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂⊢ (f + g₁).domain ≤ (f + g₂).domain R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂⊢ f.domain ⊓ g₁.domain ≤ g₂.domain All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂⊢ ∀ ⦃x : ↥(f + g₁).domain⦄ ⦃y : ↥(f + g₂).domain⦄, ↑x = ↑y → ↑(f + g₁) x = ↑(f + g₂) y R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂x:↥(f + g₁).domainy:↥(f + g₂).domainhxy:↑x = ↑y⊢ ↑(f + g₁) x = ↑(f + g₂) y simp_rw R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂x:↥(f + g₁).domainy:↥(f + g₂).domainhxy:↑x = ↑y⊢ ↑(f + g₁) x = ↑(f + g₂) yR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂x:↥(f + g₁).domainy:↥(f + g₂).domainhxy:↑x = ↑y⊢ ↑f ⟨↑x, ⋯⟩ + ↑g₁ ⟨↑x, ⋯⟩ = ↑f ⟨↑y, ⋯⟩ + ↑g₂ ⟨↑y, ⋯⟩ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fg₁:E →ₗ.[R] Fg₂:E →ₗ.[R] Fh:g₁ ≤ g₂x:↥(f + g₁).domainy:↥(f + g₂).domainhxy:↑x = ↑y⊢ ↑f ⟨↑x, ⋯⟩ + ↑g₂ ⟨↑y, ⋯⟩ = ↑f ⟨↑y, ⋯⟩ + ↑g₂ ⟨↑y, ⋯⟩ All goals completed! 🐙]lemma add_right_le_of_le (h : g₁ ≤ g₂) : g₁ + f ≤ g₂ + f := add_comm f g₁ ▸ add_comm f g₂ ▸ add_left_le_of_le f hlemma sub_right_le_of_le (h : g₁ ≤ g₂) : g₁ - f ≤ g₂ - f := sub_eq_add_neg g₁ f ▸ sub_eq_add_neg g₂ f ▸ add_right_le_of_le (-f) hlemma sub_left_le_of_le (h : g₁ ≤ g₂) : f - g₁ ≤ f - g₂ := neg_sub g₁ f ▸ neg_sub g₂ f ▸ le_iff_neg_le_neg.mp (sub_right_le_of_le f h)

B. Zero smul

lemma zero_smul_le (f : E →ₗ.[𝕜] F) : (0 : 𝕜) • f ≤ 0 := ⟨le_top, E:Type u_2inst✝⁴:AddCommGroup EF:Type u_3inst✝³:AddCommGroup F𝕜:Type u_4inst✝²:Field 𝕜inst✝¹:Module 𝕜 Einst✝:Module 𝕜 Ff:E →ₗ.[𝕜] F⊢ ∀ ⦃x : ↥(0 • f).domain⦄ ⦃y : ↥(domain 0)⦄, ↑x = ↑y → ↑(0 • f) x = ↑0 y All goals completed! 🐙⟩@[simp] lemma zero_smul_eq {f : E →ₗ.[𝕜] F} (h : f.domain = ⊤) : (0 : 𝕜) • f = 0 := eq_of_le_of_domain_eq f.zero_smul_le h

C. Finite sums

A finite sum of partial linear maps.

sum f and ∑ a, f a are equal, but not by definition. With sum f both domain and toFun are made explicit.

def sum : E →ₗ.[R] F where domain := ⨅ a, (f a).domain toFun := ∑ a, (f a).toFun ∘ₗ inclusion (fun _ _ ↦ R:Type u_1inst✝⁵:Ring RE:Type u_2inst✝⁴:AddCommGroup Einst✝³:Module R EF:Type u_3inst✝²:AddCommGroup Finst✝¹:Module R Fα:Type u_4inst✝:Fintype αf:α → E →ₗ.[R] Fa:αx✝¹:Ex✝:x✝¹ ∈ ⨅ a, (f a).domain⊢ x✝¹ ∈ (f a).domain All goals completed! 🐙)
lemma sum_domain : (sum f).domain = ⨅ a, (f a).domain := rfllemma sum_domain_le (a : α) : (sum f).domain ≤ (f a).domain := fun _ _ ↦ R:Type u_1inst✝⁵:Ring RE:Type u_2inst✝⁴:AddCommGroup Einst✝³:Module R EF:Type u_3inst✝²:AddCommGroup Finst✝¹:Module R Fα:Type u_4inst✝:Fintype αf:α → E →ₗ.[R] Fa:αx✝¹:Ex✝:x✝¹ ∈ (sum f).domain⊢ x✝¹ ∈ (f a).domain All goals completed! 🐙@[simp] lemma sum_apply (ψ : (sum f).domain) : sum f ψ = ∑ a, f a ⟨ψ, sum_domain_le f a ψ.2⟩ := R:Type u_1inst✝⁵:Ring RE:Type u_2inst✝⁴:AddCommGroup Einst✝³:Module R EF:Type u_3inst✝²:AddCommGroup Finst✝¹:Module R Fα:Type u_4inst✝:Fintype αf:α → E →ₗ.[R] Fψ:↥(sum f).domain⊢ ↑(sum f) ψ = ∑ a, ↑(f a) ⟨↑ψ, ⋯⟩ All goals completed! 🐙

D. Restricted composition

g ∘ᵣ f is the composition of g with f restricted to a domain consisting of exactly those x : f.domain for which f x ∈ g.domain.

R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] Ff₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fv:F →ₗ.[R] Gu:E →ₗ.[R] Fx:Eh:x ∈ ↑(map f.domain.subtype (comap f.toFun g.domain))right✝:x ∈ ↑f.domainy:↥f.domainhy:↑f y ∈ g.domainhy':↑y = x⊢ ↑f y ∈ g.domain All goals completed! 🐙)
@[inherit_doc compRestricted] infixr:80 " ∘ᵣ " => compRestrictedlemma compRestricted_domain_le : (g ∘ᵣ f).domain ≤ f.domain := fun _ h ↦ h.2R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] F⊢ map f.domain.subtype (comap f.toFun g.domain) ⊓ f.domain = map f.domain.subtype (comap f.toFun g.domain) R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] F⊢ map f.domain.subtype (comap f.toFun g.domain) ≤ f.domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Eh:x ∈ map f.domain.subtype (comap f.toFun g.domain)⊢ x ∈ f.domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Eh:∃ (x_1 : x ∈ f.domain), ↑f ⟨x, ⋯⟩ ∈ g.domain⊢ x ∈ f.domain All goals completed! 🐙lemma mem_compRestricted_domain_iff {x : E} : x ∈ (v ∘ᵣ u).domain ↔ ∃ h : x ∈ u.domain, u ⟨x, h⟩ ∈ v.domain := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fx:E⊢ x ∈ (v ∘ᵣ u).domain ↔ ∃ (h : x ∈ u.domain), ↑u ⟨x, h⟩ ∈ v.domain All goals completed! 🐙lemma mem_compRestricted_domain_iff' {x : E} : x ∈ (v ∘ᵣ u).domain ↔ ∃ y : u.domain, x = y ∧ ∃ y' : v.domain, u y = y' := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fx:E⊢ x ∈ (v ∘ᵣ u).domain ↔ ∃ y, x = ↑y ∧ ∃ y', ↑u y = ↑y' All goals completed! 🐙lemma mem_domain_of_mem_compRestricted_domain (x : (v ∘ᵣ u).domain) : u ⟨x, x.2.2⟩ ∈ v.domain := (mem_compRestricted_domain_iff.mp x.2).choose_spec@[simp] lemma compRestricted_apply (x : (v ∘ᵣ u).domain) : (v ∘ᵣ u) x = v ⟨u ⟨x, x.2.2⟩, mem_domain_of_mem_compRestricted_domain x⟩ := rfl

The zero map is right-absorbing.

@[simp] lemma compRestricted_zero : g ∘ᵣ (0 : E →ₗ.[R] F) = 0 := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] G⊢ g ∘ᵣ 0 = 0 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gx✝:E⊢ x✝ ∈ (g ∘ᵣ 0).domain ↔ x✝ ∈ domain 0R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gx✝:Ehf✝:x✝ ∈ (g ∘ᵣ 0).domainhg✝:x✝ ∈ domain 0⊢ ↑(g ∘ᵣ 0) ⟨x✝, hf✝⟩ = ↑0 ⟨x✝, hg✝⟩ R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gx✝:E⊢ x✝ ∈ (g ∘ᵣ 0).domain ↔ x✝ ∈ domain 0 All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gx✝:Ehf✝:x✝ ∈ (g ∘ᵣ 0).domainhg✝:x✝ ∈ domain 0⊢ ↑(g ∘ᵣ 0) ⟨x✝, hf✝⟩ = ↑0 ⟨x✝, hg✝⟩ All goals completed! 🐙
lemma compRestricted_assoc {H : Type*} [AddCommGroup H] [Module R H] (f₁ : G →ₗ.[R] H) (f₂ : F →ₗ.[R] G) (f₃ : E →ₗ.[R] F) : (f₁ ∘ᵣ f₂) ∘ᵣ f₃ = f₁ ∘ᵣ f₂ ∘ᵣ f₃ := R:Type u_1inst✝⁸:Ring RE:Type u_2inst✝⁷:AddCommGroup Einst✝⁶:Module R EF:Type u_3inst✝⁵:AddCommGroup Finst✝⁴:Module R FG:Type u_4inst✝³:AddCommGroup Ginst✝²:Module R GH:Type u_5inst✝¹:AddCommGroup Hinst✝:Module R Hf₁:G →ₗ.[R] Hf₂:F →ₗ.[R] Gf₃:E →ₗ.[R] F⊢ (f₁ ∘ᵣ f₂) ∘ᵣ f₃ = f₁ ∘ᵣ f₂ ∘ᵣ f₃ R:Type u_1inst✝⁸:Ring RE:Type u_2inst✝⁷:AddCommGroup Einst✝⁶:Module R EF:Type u_3inst✝⁵:AddCommGroup Finst✝⁴:Module R FG:Type u_4inst✝³:AddCommGroup Ginst✝²:Module R GH:Type u_5inst✝¹:AddCommGroup Hinst✝:Module R Hf₁:G →ₗ.[R] Hf₂:F →ₗ.[R] Gf₃:E →ₗ.[R] Fx✝:E⊢ x✝ ∈ ((f₁ ∘ᵣ f₂) ∘ᵣ f₃).domain ↔ x✝ ∈ (f₁ ∘ᵣ f₂ ∘ᵣ f₃).domainR:Type u_1inst✝⁸:Ring RE:Type u_2inst✝⁷:AddCommGroup Einst✝⁶:Module R EF:Type u_3inst✝⁵:AddCommGroup Finst✝⁴:Module R FG:Type u_4inst✝³:AddCommGroup Ginst✝²:Module R GH:Type u_5inst✝¹:AddCommGroup Hinst✝:Module R Hf₁:G →ₗ.[R] Hf₂:F →ₗ.[R] Gf₃:E →ₗ.[R] Fx✝:Ehf✝:x✝ ∈ ((f₁ ∘ᵣ f₂) ∘ᵣ f₃).domainhg✝:x✝ ∈ (f₁ ∘ᵣ f₂ ∘ᵣ f₃).domain⊢ ↑((f₁ ∘ᵣ f₂) ∘ᵣ f₃) ⟨x✝, hf✝⟩ = ↑(f₁ ∘ᵣ f₂ ∘ᵣ f₃) ⟨x✝, hg✝⟩ R:Type u_1inst✝⁸:Ring RE:Type u_2inst✝⁷:AddCommGroup Einst✝⁶:Module R EF:Type u_3inst✝⁵:AddCommGroup Finst✝⁴:Module R FG:Type u_4inst✝³:AddCommGroup Ginst✝²:Module R GH:Type u_5inst✝¹:AddCommGroup Hinst✝:Module R Hf₁:G →ₗ.[R] Hf₂:F →ₗ.[R] Gf₃:E →ₗ.[R] Fx✝:E⊢ x✝ ∈ ((f₁ ∘ᵣ f₂) ∘ᵣ f₃).domain ↔ x✝ ∈ (f₁ ∘ᵣ f₂ ∘ᵣ f₃).domain R:Type u_1inst✝⁸:Ring RE:Type u_2inst✝⁷:AddCommGroup Einst✝⁶:Module R EF:Type u_3inst✝⁵:AddCommGroup Finst✝⁴:Module R FG:Type u_4inst✝³:AddCommGroup Ginst✝²:Module R GH:Type u_5inst✝¹:AddCommGroup Hinst✝:Module R Hf₁:G →ₗ.[R] Hf₂:F →ₗ.[R] Gf₃:E →ₗ.[R] Fx✝:E⊢ (∃ (h : x✝ ∈ f₃.domain) (h_1 : ↑f₃ ⟨x✝, ⋯⟩ ∈ f₂.domain), ↑f₂ ⟨↑f₃ ⟨x✝, ⋯⟩, h_1⟩ ∈ f₁.domain) ↔ ∃ (h : ∃ (h : x✝ ∈ f₃.domain), ↑f₃ ⟨x✝, h⟩ ∈ f₂.domain), ↑(f₂ ∘ᵣ f₃) ⟨x✝, ⋯⟩ ∈ f₁.domain All goals completed! 🐙 R:Type u_1inst✝⁸:Ring RE:Type u_2inst✝⁷:AddCommGroup Einst✝⁶:Module R EF:Type u_3inst✝⁵:AddCommGroup Finst✝⁴:Module R FG:Type u_4inst✝³:AddCommGroup Ginst✝²:Module R GH:Type u_5inst✝¹:AddCommGroup Hinst✝:Module R Hf₁:G →ₗ.[R] Hf₂:F →ₗ.[R] Gf₃:E →ₗ.[R] Fx✝:Ehf✝:x✝ ∈ ((f₁ ∘ᵣ f₂) ∘ᵣ f₃).domainhg✝:x✝ ∈ (f₁ ∘ᵣ f₂ ∘ᵣ f₃).domain⊢ ↑((f₁ ∘ᵣ f₂) ∘ᵣ f₃) ⟨x✝, hf✝⟩ = ↑(f₁ ∘ᵣ f₂ ∘ᵣ f₃) ⟨x✝, hg✝⟩ All goals completed! 🐙

compRestricted is the same as comp when the range of u is contained in v.domain.

lemma compRestricted_eq_comp (h : ∀ x : u.domain, u x ∈ v.domain) : v ∘ᵣ u = v.comp u h := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fh:∀ (x : ↥u.domain), ↑u x ∈ v.domain⊢ v ∘ᵣ u = v.comp u h R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fh:∀ (x : ↥u.domain), ↑u x ∈ v.domainx:E⊢ x ∈ (v ∘ᵣ u).domain ↔ x ∈ (v.comp u h).domainR:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fh:∀ (x : ↥u.domain), ↑u x ∈ v.domainx:Ehf✝:x ∈ (v ∘ᵣ u).domainhg✝:x ∈ (v.comp u h).domain⊢ ↑(v ∘ᵣ u) ⟨x, hf✝⟩ = ↑(v.comp u h) ⟨x, hg✝⟩ R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fh:∀ (x : ↥u.domain), ↑u x ∈ v.domainx:E⊢ x ∈ (v ∘ᵣ u).domain ↔ x ∈ (v.comp u h).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fh:∀ (x : ↥u.domain), ↑u x ∈ v.domainx:E⊢ x ∈ (v ∘ᵣ u).domain ↔ x ∈ u.domain All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] Fh:∀ (x : ↥u.domain), ↑u x ∈ v.domainx:Ehf✝:x ∈ (v ∘ᵣ u).domainhg✝:x ∈ (v.comp u h).domain⊢ ↑(v ∘ᵣ u) ⟨x, hf✝⟩ = ↑(v.comp u h) ⟨x, hg✝⟩ All goals completed! 🐙

compRestricted is maximal amongst compositions of v with domain restrictions of u.

lemma comp_le_compRestricted {S : Submodule R E} (h : ∀ x : (u.domRestrict S).domain, u ⟨x, x.2.2⟩ ∈ v.domain) : v.comp (u.domRestrict S) h ≤ v ∘ᵣ u := ⟨fun x hx ↦ mem_compRestricted_domain_iff.mpr ⟨hx.2, h ⟨x, hx⟩⟩, R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gv:F →ₗ.[R] Gu:E →ₗ.[R] FS:Submodule R Eh:∀ (x : ↥(u.domRestrict S).domain), ↑u ⟨↑x, ⋯⟩ ∈ v.domain⊢ ∀ ⦃x : ↥(v.comp (u.domRestrict S) h).domain⦄ ⦃y : ↥(v ∘ᵣ u).domain⦄, ↑x = ↑y → ↑(v.comp (u.domRestrict S) h) x = ↑(v ∘ᵣ u) y All goals completed! 🐙⟩
lemma compRestricted_mono_left {g g' : F →ₗ.[R] G} (h : g ≤ g') (f : E →ₗ.[R] F) : g ∘ᵣ f ≤ g' ∘ᵣ f := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] F⊢ g ∘ᵣ f ≤ g' ∘ᵣ f R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] F⊢ (g ∘ᵣ f).domain ≤ (g' ∘ᵣ f).domainR:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] F⊢ ∀ ⦃x : ↥(g ∘ᵣ f).domain⦄ ⦃y : ↥(g' ∘ᵣ f).domain⦄, ↑x = ↑y → ↑(g ∘ᵣ f) x = ↑(g' ∘ᵣ f) y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] F⊢ (g ∘ᵣ f).domain ≤ (g' ∘ᵣ f).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ f).domain⊢ x ∈ (g' ∘ᵣ f).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ f).domainhx':x ∈ f.domainhfx:↑f ⟨x, hx'⟩ ∈ g.domain⊢ x ∈ (g' ∘ᵣ f).domain All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] F⊢ ∀ ⦃x : ↥(g ∘ᵣ f).domain⦄ ⦃y : ↥(g' ∘ᵣ f).domain⦄, ↑x = ↑y → ↑(g ∘ᵣ f) x = ↑(g' ∘ᵣ f) y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] Fx:↥(g ∘ᵣ f).domainy:↥(g' ∘ᵣ f).domainhxy:↑x = ↑y⊢ ↑(g ∘ᵣ f) x = ↑(g' ∘ᵣ f) y exact @h.2 ⟨f ⟨x, x.2.2⟩, mem_domain_of_mem_compRestricted_domain x⟩ ⟨f ⟨y, y.2.2⟩, mem_domain_of_mem_compRestricted_domain y⟩ (R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gg':F →ₗ.[R] Gh:g ≤ g'f:E →ₗ.[R] Fx:↥(g ∘ᵣ f).domainy:↥(g' ∘ᵣ f).domainhxy:↑x = ↑y⊢ ↑⟨↑f ⟨↑x, ⋯⟩, ⋯⟩ = ↑⟨↑f ⟨↑y, ⋯⟩, ⋯⟩ All goals completed! 🐙)lemma compRestricted_mono_right (g : F →ₗ.[R] G) {f f' : E →ₗ.[R] F} (h : f ≤ f') : g ∘ᵣ f ≤ g ∘ᵣ f' := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'⊢ g ∘ᵣ f ≤ g ∘ᵣ f' R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'⊢ (g ∘ᵣ f).domain ≤ (g ∘ᵣ f').domainR:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'⊢ ∀ ⦃x : ↥(g ∘ᵣ f).domain⦄ ⦃y : ↥(g ∘ᵣ f').domain⦄, ↑x = ↑y → ↑(g ∘ᵣ f) x = ↑(g ∘ᵣ f') y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'⊢ (g ∘ᵣ f).domain ≤ (g ∘ᵣ f').domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'x:Ehx:x ∈ (g ∘ᵣ f).domain⊢ x ∈ (g ∘ᵣ f').domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'x:Ehx:x ∈ (g ∘ᵣ f).domainhx':x ∈ f.domainhfx:↑f ⟨x, hx'⟩ ∈ g.domain⊢ x ∈ (g ∘ᵣ f').domain All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'⊢ ∀ ⦃x : ↥(g ∘ᵣ f).domain⦄ ⦃y : ↥(g ∘ᵣ f').domain⦄, ↑x = ↑y → ↑(g ∘ᵣ f) x = ↑(g ∘ᵣ f') y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Ff':E →ₗ.[R] Fh:f ≤ f'x:↥(g ∘ᵣ f).domainy:↥(g ∘ᵣ f').domainhxy:↑x = ↑y⊢ ↑(g ∘ᵣ f) x = ↑(g ∘ᵣ f') y All goals completed! 🐙@[simp] lemma neg_compRestricted : (-g) ∘ᵣ f = -g ∘ᵣ f := rfl@[simp] lemma compRestricted_neg : g ∘ᵣ (-f) = -g ∘ᵣ f := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] F⊢ g ∘ᵣ (-f) = -g ∘ᵣ f R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:E⊢ x ∈ (g ∘ᵣ (-f)).domain ↔ x ∈ (-g ∘ᵣ f).domainR:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ (-f)).domainhx':x ∈ (-g ∘ᵣ f).domain⊢ ↑(g ∘ᵣ (-f)) ⟨x, hx⟩ = ↑(-g ∘ᵣ f) ⟨x, hx'⟩ R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:E⊢ x ∈ (g ∘ᵣ (-f)).domain ↔ x ∈ (-g ∘ᵣ f).domain All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ (-f)).domainhx':x ∈ (-g ∘ᵣ f).domain⊢ ↑(g ∘ᵣ (-f)) ⟨x, hx⟩ = ↑(-g ∘ᵣ f) ⟨x, hx'⟩ R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ (-f)).domainhx':x ∈ (-g ∘ᵣ f).domainh:x ∈ f.domainh':↑f ⟨x, h⟩ ∈ g.domain⊢ ↑(g ∘ᵣ (-f)) ⟨x, hx⟩ = ↑(-g ∘ᵣ f) ⟨x, hx'⟩ All goals completed! 🐙lemma add_compRestricted : (g₁ + g₂) ∘ᵣ f = g₁ ∘ᵣ f + g₂ ∘ᵣ f := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] F⊢ (g₁ + g₂) ∘ᵣ f = g₁ ∘ᵣ f + g₂ ∘ᵣ f R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] Fx:E⊢ x ∈ ((g₁ + g₂) ∘ᵣ f).domain ↔ x ∈ (g₁ ∘ᵣ f + g₂ ∘ᵣ f).domainR:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Ehx:x ∈ ((g₁ + g₂) ∘ᵣ f).domainhx':x ∈ (g₁ ∘ᵣ f + g₂ ∘ᵣ f).domain⊢ ↑((g₁ + g₂) ∘ᵣ f) ⟨x, hx⟩ = ↑(g₁ ∘ᵣ f + g₂ ∘ᵣ f) ⟨x, hx'⟩ R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] Fx:E⊢ x ∈ ((g₁ + g₂) ∘ᵣ f).domain ↔ x ∈ (g₁ ∘ᵣ f + g₂ ∘ᵣ f).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] Fx:E⊢ (∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ ∈ g₁.domain ∧ ↑f ⟨x, ⋯⟩ ∈ g₂.domain) ↔ (∃ (h : x ∈ f.domain), ↑f ⟨x, h⟩ ∈ g₁.domain) ∧ ∃ (h : x ∈ f.domain), ↑f ⟨x, h⟩ ∈ g₂.domain All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] Fx:Ehx:x ∈ ((g₁ + g₂) ∘ᵣ f).domainhx':x ∈ (g₁ ∘ᵣ f + g₂ ∘ᵣ f).domain⊢ ↑((g₁ + g₂) ∘ᵣ f) ⟨x, hx⟩ = ↑(g₁ ∘ᵣ f + g₂ ∘ᵣ f) ⟨x, hx'⟩ All goals completed! 🐙lemma sub_compRestricted : (g₁ - g₂) ∘ᵣ f = g₁ ∘ᵣ f - g₂ ∘ᵣ f := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg₁:F →ₗ.[R] Gg₂:F →ₗ.[R] Gf:E →ₗ.[R] F⊢ (g₁ - g₂) ∘ᵣ f = g₁ ∘ᵣ f - g₂ ∘ᵣ f All goals completed! 🐙lemma compRestricted_add_ge : g ∘ᵣ f₁ + g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ + f₂) := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ g ∘ᵣ f₁ + g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ + f₂) R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ (g ∘ᵣ f₁ + g ∘ᵣ f₂).domain ≤ (g ∘ᵣ (f₁ + f₂)).domainR:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ ∀ ⦃x : ↥(g ∘ᵣ f₁ + g ∘ᵣ f₂).domain⦄ ⦃y : ↥(g ∘ᵣ (f₁ + f₂)).domain⦄, ↑x = ↑y → ↑(g ∘ᵣ f₁ + g ∘ᵣ f₂) x = ↑(g ∘ᵣ (f₁ + f₂)) y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ (g ∘ᵣ f₁ + g ∘ᵣ f₂).domain ≤ (g ∘ᵣ (f₁ + f₂)).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ f₁ + g ∘ᵣ f₂).domain⊢ x ∈ (g ∘ᵣ (f₁ + f₂)).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ f₁ + g ∘ᵣ f₂).domainh₁:x ∈ f₁.domainh₁':↑f₁ ⟨x, h₁⟩ ∈ g.domain⊢ x ∈ (g ∘ᵣ (f₁ + f₂)).domain R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx:Ehx:x ∈ (g ∘ᵣ f₁ + g ∘ᵣ f₂).domainh₁:x ∈ f₁.domainh₁':↑f₁ ⟨x, h₁⟩ ∈ g.domainh₂:x ∈ f₂.domainh₂':↑f₂ ⟨x, h₂⟩ ∈ g.domain⊢ x ∈ (g ∘ᵣ (f₁ + f₂)).domain All goals completed! 🐙 R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ ∀ ⦃x : ↥(g ∘ᵣ f₁ + g ∘ᵣ f₂).domain⦄ ⦃y : ↥(g ∘ᵣ (f₁ + f₂)).domain⦄, ↑x = ↑y → ↑(g ∘ᵣ f₁ + g ∘ᵣ f₂) x = ↑(g ∘ᵣ (f₁ + f₂)) y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx:↥(g ∘ᵣ f₁ + g ∘ᵣ f₂).domainy:↥(g ∘ᵣ (f₁ + f₂)).domainhxy:↑x = ↑y⊢ ↑(g ∘ᵣ f₁ + g ∘ᵣ f₂) x = ↑(g ∘ᵣ (f₁ + f₂)) y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx:↥(g ∘ᵣ f₁ + g ∘ᵣ f₂).domainy:↥(g ∘ᵣ (f₁ + f₂)).domainhxy:↑x = ↑yh₁:↑x ∈ f₁.domainh₁':↑f₁ ⟨↑x, h₁⟩ ∈ g.domain⊢ ↑(g ∘ᵣ f₁ + g ∘ᵣ f₂) x = ↑(g ∘ᵣ (f₁ + f₂)) y R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] Fx:↥(g ∘ᵣ f₁ + g ∘ᵣ f₂).domainy:↥(g ∘ᵣ (f₁ + f₂)).domainhxy:↑x = ↑yh₁:↑x ∈ f₁.domainh₁':↑f₁ ⟨↑x, h₁⟩ ∈ g.domainh₂:↑x ∈ f₂.domainh₂':↑f₂ ⟨↑x, h₂⟩ ∈ g.domain⊢ ↑(g ∘ᵣ f₁ + g ∘ᵣ f₂) x = ↑(g ∘ᵣ (f₁ + f₂)) y All goals completed! 🐙lemma compRestricted_sub_ge : g ∘ᵣ f₁ - g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ - f₂) := R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ g ∘ᵣ f₁ - g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ - f₂) R:Type u_1inst✝⁶:Ring RE:Type u_2inst✝⁵:AddCommGroup Einst✝⁴:Module R EF:Type u_3inst✝³:AddCommGroup Finst✝²:Module R FG:Type u_4inst✝¹:AddCommGroup Ginst✝:Module R Gg:F →ₗ.[R] Gf₁:E →ₗ.[R] Ff₂:E →ₗ.[R] F⊢ g ∘ᵣ f₁ + g ∘ᵣ (-f₂) ≤ g ∘ᵣ (f₁ + -f₂) All goals completed! 🐙lemma compRestricted_smul {S : Type*} [DivisionRing S] [Module S E] [Module S F] [Module S G] [SMulCommClass S S F] [SMulCommClass S S G] {c : S} (hc : c ≠ 0) (g : F →ₗ.[S] G) (f : E →ₗ.[S] F) : g ∘ᵣ (c • f) = c • (g ∘ᵣ f) := E:Type u_2inst✝⁸:AddCommGroup EF:Type u_3inst✝⁷:AddCommGroup FG:Type u_4inst✝⁶:AddCommGroup GS:Type u_5inst✝⁵:DivisionRing Sinst✝⁴:Module S Einst✝³:Module S Finst✝²:Module S Ginst✝¹:SMulCommClass S S Finst✝:SMulCommClass S S Gc:Shc:c ≠ 0g:F →ₗ.[S] Gf:E →ₗ.[S] F⊢ g ∘ᵣ (c • f) = c • g ∘ᵣ f E:Type u_2inst✝⁸:AddCommGroup EF:Type u_3inst✝⁷:AddCommGroup FG:Type u_4inst✝⁶:AddCommGroup GS:Type u_5inst✝⁵:DivisionRing Sinst✝⁴:Module S Einst✝³:Module S Finst✝²:Module S Ginst✝¹:SMulCommClass S S Finst✝:SMulCommClass S S Gc:Shc:c ≠ 0g:F →ₗ.[S] Gf:E →ₗ.[S] Fx:E⊢ x ∈ (g ∘ᵣ (c • f)).domain ↔ x ∈ (c • g ∘ᵣ f).domainE:Type u_2inst✝⁸:AddCommGroup EF:Type u_3inst✝⁷:AddCommGroup FG:Type u_4inst✝⁶:AddCommGroup GS:Type u_5inst✝⁵:DivisionRing Sinst✝⁴:Module S Einst✝³:Module S Finst✝²:Module S Ginst✝¹:SMulCommClass S S Finst✝:SMulCommClass S S Gc:Shc:c ≠ 0g:F →ₗ.[S] Gf:E →ₗ.[S] Fx:Ehx:x ∈ (g ∘ᵣ (c • f)).domainhx':x ∈ (c • g ∘ᵣ f).domain⊢ ↑(g ∘ᵣ (c • f)) ⟨x, hx⟩ = ↑(c • g ∘ᵣ f) ⟨x, hx'⟩ E:Type u_2inst✝⁸:AddCommGroup EF:Type u_3inst✝⁷:AddCommGroup FG:Type u_4inst✝⁶:AddCommGroup GS:Type u_5inst✝⁵:DivisionRing Sinst✝⁴:Module S Einst✝³:Module S Finst✝²:Module S Ginst✝¹:SMulCommClass S S Finst✝:SMulCommClass S S Gc:Shc:c ≠ 0g:F →ₗ.[S] Gf:E →ₗ.[S] Fx:E⊢ x ∈ (g ∘ᵣ (c • f)).domain ↔ x ∈ (c • g ∘ᵣ f).domain All goals completed! 🐙 E:Type u_2inst✝⁸:AddCommGroup EF:Type u_3inst✝⁷:AddCommGroup FG:Type u_4inst✝⁶:AddCommGroup GS:Type u_5inst✝⁵:DivisionRing Sinst✝⁴:Module S Einst✝³:Module S Finst✝²:Module S Ginst✝¹:SMulCommClass S S Finst✝:SMulCommClass S S Gc:Shc:c ≠ 0g:F →ₗ.[S] Gf:E →ₗ.[S] Fx:Ehx:x ∈ (g ∘ᵣ (c • f)).domainhx':x ∈ (c • g ∘ᵣ f).domain⊢ ↑(g ∘ᵣ (c • f)) ⟨x, hx⟩ = ↑(c • g ∘ᵣ f) ⟨x, hx'⟩ E:Type u_2inst✝⁸:AddCommGroup EF:Type u_3inst✝⁷:AddCommGroup FG:Type u_4inst✝⁶:AddCommGroup GS:Type u_5inst✝⁵:DivisionRing Sinst✝⁴:Module S Einst✝³:Module S Finst✝²:Module S Ginst✝¹:SMulCommClass S S Finst✝:SMulCommClass S S Gc:Shc:c ≠ 0g:F →ₗ.[S] Gf:E →ₗ.[S] Fx:Ehx:x ∈ (g ∘ᵣ (c • f)).domainhx':x ∈ (c • g ∘ᵣ f).domainh:x ∈ f.domainh':↑f ⟨x, h⟩ ∈ g.domain⊢ ↑(g ∘ᵣ (c • f)) ⟨x, hx⟩ = ↑(c • g ∘ᵣ f) ⟨x, hx'⟩ All goals completed! 🐙@[simp] lemma smul_compRestricted {M : Type*} [Monoid M] [DistribMulAction M G] [SMulCommClass R M G] (c : M) (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : (c • g) ∘ᵣ f = c • (g ∘ᵣ f) := R:Type u_1inst✝⁹:Ring RE:Type u_2inst✝⁸:AddCommGroup Einst✝⁷:Module R EF:Type u_3inst✝⁶:AddCommGroup Finst✝⁵:Module R FG:Type u_4inst✝⁴:AddCommGroup Ginst✝³:Module R GM:Type u_5inst✝²:Monoid Minst✝¹:DistribMulAction M Ginst✝:SMulCommClass R M Gc:Mg:F →ₗ.[R] Gf:E →ₗ.[R] F⊢ (c • g) ∘ᵣ f = c • g ∘ᵣ f R:Type u_1inst✝⁹:Ring RE:Type u_2inst✝⁸:AddCommGroup Einst✝⁷:Module R EF:Type u_3inst✝⁶:AddCommGroup Finst✝⁵:Module R FG:Type u_4inst✝⁴:AddCommGroup Ginst✝³:Module R GM:Type u_5inst✝²:Monoid Minst✝¹:DistribMulAction M Ginst✝:SMulCommClass R M Gc:Mg:F →ₗ.[R] Gf:E →ₗ.[R] Fx✝:E⊢ x✝ ∈ ((c • g) ∘ᵣ f).domain ↔ x✝ ∈ (c • g ∘ᵣ f).domainR:Type u_1inst✝⁹:Ring RE:Type u_2inst✝⁸:AddCommGroup Einst✝⁷:Module R EF:Type u_3inst✝⁶:AddCommGroup Finst✝⁵:Module R FG:Type u_4inst✝⁴:AddCommGroup Ginst✝³:Module R GM:Type u_5inst✝²:Monoid Minst✝¹:DistribMulAction M Ginst✝:SMulCommClass R M Gc:Mg:F →ₗ.[R] Gf:E →ₗ.[R] Fx✝:Ehf✝:x✝ ∈ ((c • g) ∘ᵣ f).domainhg✝:x✝ ∈ (c • g ∘ᵣ f).domain⊢ ↑((c • g) ∘ᵣ f) ⟨x✝, hf✝⟩ = ↑(c • g ∘ᵣ f) ⟨x✝, hg✝⟩ R:Type u_1inst✝⁹:Ring RE:Type u_2inst✝⁸:AddCommGroup Einst✝⁷:Module R EF:Type u_3inst✝⁶:AddCommGroup Finst✝⁵:Module R FG:Type u_4inst✝⁴:AddCommGroup Ginst✝³:Module R GM:Type u_5inst✝²:Monoid Minst✝¹:DistribMulAction M Ginst✝:SMulCommClass R M Gc:Mg:F →ₗ.[R] Gf:E →ₗ.[R] Fx✝:E⊢ x✝ ∈ ((c • g) ∘ᵣ f).domain ↔ x✝ ∈ (c • g ∘ᵣ f).domain All goals completed! 🐙 R:Type u_1inst✝⁹:Ring RE:Type u_2inst✝⁸:AddCommGroup Einst✝⁷:Module R EF:Type u_3inst✝⁶:AddCommGroup Finst✝⁵:Module R FG:Type u_4inst✝⁴:AddCommGroup Ginst✝³:Module R GM:Type u_5inst✝²:Monoid Minst✝¹:DistribMulAction M Ginst✝:SMulCommClass R M Gc:Mg:F →ₗ.[R] Gf:E →ₗ.[R] Fx✝:Ehf✝:x✝ ∈ ((c • g) ∘ᵣ f).domainhg✝:x✝ ∈ (c • g ∘ᵣ f).domain⊢ ↑((c • g) ∘ᵣ f) ⟨x✝, hf✝⟩ = ↑(c • g ∘ᵣ f) ⟨x✝, hg✝⟩ All goals completed! 🐙

E. Monoid

Partial linear maps E →ₗ.[R] E with compRestricted for multiplication and the identity map (domain ⊤) for 1 comprise a monoid.

instance instMonoid : Monoid (E →ₗ.[R] E) where mul := compRestricted mul_assoc := compRestricted_assoc one := ⟨⊤, topEquiv.toLinearMap⟩ one_mul f := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] E⊢ 1 * f = f R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] E⊢ { domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f = f R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:E⊢ x✝ ∈ ({ domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f).domain ↔ x✝ ∈ f.domainR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:Ehf✝:x✝ ∈ ({ domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f).domainhg✝:x✝ ∈ f.domain⊢ ↑({ domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f) ⟨x✝, hf✝⟩ = ↑f ⟨x✝, hg✝⟩ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:E⊢ x✝ ∈ ({ domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f).domain ↔ x✝ ∈ f.domain All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:Ehf✝:x✝ ∈ ({ domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f).domainhg✝:x✝ ∈ f.domain⊢ ↑({ domain := ⊤, toFun := ↑topEquiv } ∘ᵣ f) ⟨x✝, hf✝⟩ = ↑f ⟨x✝, hg✝⟩ All goals completed! 🐙 mul_one f := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] E⊢ f * 1 = f R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] E⊢ f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv } = f R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:E⊢ x✝ ∈ (f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv }).domain ↔ x✝ ∈ f.domainR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:Ehf✝:x✝ ∈ (f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv }).domainhg✝:x✝ ∈ f.domain⊢ ↑(f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv }) ⟨x✝, hf✝⟩ = ↑f ⟨x✝, hg✝⟩ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:E⊢ x✝ ∈ (f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv }).domain ↔ x✝ ∈ f.domain All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Ex✝:Ehf✝:x✝ ∈ (f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv }).domainhg✝:x✝ ∈ f.domain⊢ ↑(f ∘ᵣ { domain := ⊤, toFun := ↑topEquiv }) ⟨x✝, hf✝⟩ = ↑f ⟨x✝, hg✝⟩ All goals completed! 🐙lemma mul_def (f₁ f₂ : E →ₗ.[R] E) : f₁ * f₂ = f₁ ∘ᵣ f₂ := rfl@[simp] lemma one_domain : (1 : E →ₗ.[R] E).domain = ⊤ := rfl@[simp] lemma one_toFun : (1 : E →ₗ.[R] E).toFun = topEquiv.toLinearMap := rfl@[simp] lemma one_coe : (1 : E →ₗ.[R] E).toFun' = ⇑topEquiv.toLinearMap := rfl

F. Inverses

include h_kerlemma inverse_ker : f.inverse.toFun.ker = ⊥ := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥⊢ f.inverse.toFun.ker = ⊥ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x✝:↥f.inverse.domainy:Fhy:y ∈ f.inverse.domainhy':f.inverse.toFun ⟨y, hy⟩ = 0⊢ ⟨y, hy⟩ = 0 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x✝:↥f.inverse.domainy:Fhy:y ∈ f.inverse.domainhy':f.inverse.toFun ⟨y, hy⟩ = 0x:↥f.domainhx:f.toFun x = y⊢ ⟨y, hy⟩ = 0 All goals completed! 🐙All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ f.inverse.inverse.domainhx':x ∈ f.domain⊢ ↑f.inverse.inverse ⟨x, hx⟩ = ↑f ⟨x, hx'⟩ refine inverse_apply_eq (y := ⟨x, hx⟩) (x := ⟨f ⟨x, hx'⟩, R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ f.inverse.inverse.domainhx':x ∈ f.domain⊢ ↑f ⟨x, hx'⟩ ∈ f.inverse.domain All goals completed! 🐙⟩) ?_ ?_ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ f.inverse.inverse.domainhx':x ∈ f.domain⊢ f.inverse.toFun.ker = ⊥ All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ f.inverse.inverse.domainhx':x ∈ f.domain⊢ ↑f.inverse ⟨↑f ⟨x, hx'⟩, ⋯⟩ = ↑⟨x, hx⟩ exact inverse_apply_eq (y := ⟨f ⟨x, hx'⟩, R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ f.inverse.inverse.domainhx':x ∈ f.domain⊢ ↑f ⟨x, hx'⟩ ∈ f.inverse.domain All goals completed! 🐙⟩) (x := ⟨x, hx'⟩) h_ker rfllemma inverse_compRestricted_eq : f.inverse ∘ᵣ f = domRestrict 1 f.domain := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥⊢ f.inverse ∘ᵣ f = domRestrict 1 f.domain R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:E⊢ x ∈ (f.inverse ∘ᵣ f).domain ↔ x ∈ (domRestrict 1 f.domain).domainR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ (f.inverse ∘ᵣ f).domainhx':x ∈ (domRestrict 1 f.domain).domain⊢ ↑(f.inverse ∘ᵣ f) ⟨x, hx⟩ = ↑(domRestrict 1 f.domain) ⟨x, hx'⟩ R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:E⊢ x ∈ (f.inverse ∘ᵣ f).domain ↔ x ∈ (domRestrict 1 f.domain).domain All goals completed! 🐙 R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥x:Ehx:x ∈ (f.inverse ∘ᵣ f).domainhx':x ∈ (domRestrict 1 f.domain).domain⊢ ↑(f.inverse ∘ᵣ f) ⟨x, hx⟩ = ↑(domRestrict 1 f.domain) ⟨x, hx'⟩ All goals completed! 🐙lemma compRestricted_inverse_eq : f ∘ᵣ f.inverse = domRestrict 1 f.inverse.domain := R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥⊢ f ∘ᵣ f.inverse = domRestrict 1 f.inverse.domain nth_rw 1 [R:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥⊢ f.inverse.inverse ∘ᵣ f.inverse = domRestrict 1 f.inverse.domainR:Type u_1inst✝⁴:Ring RE:Type u_2inst✝³:AddCommGroup Einst✝²:Module R EF:Type u_3inst✝¹:AddCommGroup Finst✝:Module R Ff:E →ₗ.[R] Fh_ker:f.toFun.ker = ⊥⊢ f.inverse.inverse ∘ᵣ f.inverse = domRestrict 1 f.inverse.domain All goals completed! 🐙