Mathlib.Algebra.Module.Submodule.EqLocus

LinearMap.eqLocus definition

(f g : F) : Submodule R M

Full source

/-- A linear map version of `AddMonoidHom.eqLocusM` -/
def eqLocus (f g : F) : Submodule R M :=
  { (f : M →+ M₂).eqLocusM g with
    carrier := { x | f x = g x }
    smul_mem' := fun {r} {x} (hx : _ = _) => show _ = _ by
      -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` into `map_smulₛₗ _`
      simpa only [map_smulₛₗ _] using congr_arg (τ₁₂ r • ·) hx }

Equalizer submodule of linear maps

Informal description

Given two linear maps $ f, g : M \to M_2 $ between modules over a semiring $ R $, the submodule $\text{eqLocus}(f, g)$ consists of all elements $ x \in M $ such that $ f(x) = g(x) $. This submodule is closed under addition and scalar multiplication.

LinearMap.mem_eqLocus theorem

{x : M} {f g : F} : x ∈ eqLocus f g ↔ f x = g x

Full source

@[simp]
theorem mem_eqLocus {x : M} {f g : F} : x ∈ eqLocus f gx ∈ eqLocus f g ↔ f x = g x :=
  Iff.rfl

Characterization of Equalizer Submodule Membership: $x \in \text{eqLocus}(f, g) \leftrightarrow f(x) = g(x)$

Informal description

For any element $x$ in a module $M$ over a semiring $R$, and for any two linear maps $f, g : M \to M_2$, the element $x$ belongs to the equalizer submodule $\text{eqLocus}(f, g)$ if and only if $f(x) = g(x)$.

LinearMap.eqLocus_toAddSubmonoid theorem

(f g : F) : (eqLocus f g).toAddSubmonoid = (f : M →+ M₂).eqLocusM g

Full source

theorem eqLocus_toAddSubmonoid (f g : F) :
    (eqLocus f g).toAddSubmonoid = (f : M →+ M₂).eqLocusM g :=
  rfl

Equalizer Submodule's Additive Submonoid is Equalizer of Underlying Additive Homomorphisms

Informal description

For any two linear maps $f, g : M \to M_2$ between modules over a semiring $R$, the underlying additive submonoid of the equalizer submodule $\text{eqLocus}(f, g)$ (consisting of all $x \in M$ such that $f(x) = g(x)$) is equal to the equalizer submonoid of the underlying additive monoid homomorphisms of $f$ and $g$.

LinearMap.eqLocus_eq_top theorem

{f g : F} : eqLocus f g = ⊤ ↔ f = g

Full source

@[simp]
theorem eqLocus_eq_top {f g : F} : eqLocuseqLocus f g = ⊤ ↔ f = g := by
  simp [SetLike.ext_iff, DFunLike.ext_iff]

Equalizer Submodule is Entire Module if and only if Linear Maps are Equal

Informal description

For two linear maps $f, g : M \to M_2$ between modules over a semiring $R$, the equalizer submodule $\text{eqLocus}(f, g)$ (consisting of all $x \in M$ such that $f(x) = g(x)$) is equal to the entire module $M$ if and only if $f = g$.

LinearMap.eqLocus_same theorem

(f : F) : eqLocus f f = ⊤

Full source

@[simp]
theorem eqLocus_same (f : F) : eqLocus f f = ⊤ := eqLocus_eq_top.2 rfl

Equalizer submodule of a linear map with itself is the entire module

Informal description

For any linear map $f \colon M \to M_2$ between modules over a semiring $R$, the equalizer submodule $\text{eqLocus}(f, f)$ (consisting of all $x \in M$ such that $f(x) = f(x)$) is equal to the entire module $M$.

LinearMap.le_eqLocus theorem

{f g : F} {S : Submodule R M} : S ≤ eqLocus f g ↔ Set.EqOn f g S

Full source

theorem le_eqLocus {f g : F} {S : Submodule R M} : S ≤ eqLocus f g ↔ Set.EqOn f g S := Iff.rfl

Submodule Containment in Equalizer Submodule is Equivalent to Function Equality on Submodule

Informal description

For two linear maps $f, g \colon M \to M_2$ between modules over a semiring $R$ and a submodule $S \subseteq M$, the following are equivalent: 1. $S$ is contained in the equalizer submodule $\text{eqLocus}(f, g)$ (i.e., for all $x \in S$, $f(x) = g(x)$). 2. The functions $f$ and $g$ are equal on the subset $S$. In other words, $S \leq \text{eqLocus}(f, g)$ if and only if $f$ and $g$ agree on all elements of $S$.

LinearMap.eqOn_sup theorem

{f g : F} {S T : Submodule R M} (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) : Set.EqOn f g ↑(S ⊔ T)

Full source

theorem eqOn_sup {f g : F} {S T : Submodule R M} (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) :
    Set.EqOn f g ↑(S ⊔ T) := by
  rw [← le_eqLocus] at hS hT ⊢
  exact sup_le hS hT

Agreement of Linear Maps on Join of Submodules

Informal description

Let $f, g \colon M \to M_2$ be linear maps between modules over a semiring $R$, and let $S, T$ be submodules of $M$. If $f$ and $g$ agree on $S$ (i.e., $f(x) = g(x)$ for all $x \in S$) and they also agree on $T$, then $f$ and $g$ agree on the join of $S$ and $T$ (i.e., $f(x) = g(x)$ for all $x \in S \sqcup T$).

LinearMap.ext_on_codisjoint theorem

{f g : F} {S T : Submodule R M} (hST : Codisjoint S T) (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) : f = g

Full source

theorem ext_on_codisjoint {f g : F} {S T : Submodule R M} (hST : Codisjoint S T)
    (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) : f = g :=
  DFunLike.ext _ _ fun _ ↦ eqOn_sup hS hT <| hST.eq_top.symm ▸ trivial

Linear Map Equality via Codisjoint Submodules

Informal description

Let $M$ and $M_2$ be modules over a semiring $R$, and let $f, g \colon M \to M_2$ be linear maps. Suppose there exist submodules $S, T \subseteq M$ such that: 1. $S$ and $T$ are codisjoint (i.e., $S \sqcup T = M$) 2. $f$ and $g$ agree on $S$ (i.e., $f(x) = g(x)$ for all $x \in S$) 3. $f$ and $g$ agree on $T$ (i.e., $f(x) = g(x)$ for all $x \in T$) Then $f = g$.

LinearMap.eqLocus_eq_ker_sub theorem

(f g : M →ₛₗ[τ₁₂] M₂) : eqLocus f g = ker (f - g)

Full source

theorem eqLocus_eq_ker_sub (f g : M →ₛₗ[τ₁₂] M₂) : eqLocus f g = ker (f - g) :=
  SetLike.ext fun _ => sub_eq_zero.symm

Equalizer Submodule as Kernel of Difference Map

Informal description

For any two linear maps $f, g : M \to M_2$ between modules over a semiring $R$, the equalizer submodule $\mathrm{eqLocus}(f, g)$ (consisting of all $x \in M$ such that $f(x) = g(x)$) is equal to the kernel of the difference map $(f - g)$. In other words: \[ \mathrm{eqLocus}(f, g) = \ker(f - g) \]

Mathlib.Algebra.Module.Submodule.EqLocus

Main declarations

Tags