Mathlib.Topology.Algebra.Module.Determinant

ContinuousLinearMap.det abbrev

{R : Type*} [CommRing R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M] (A : M →L[R] M) : R

Full source

/-- The determinant of a continuous linear map, mainly as a convenience device to be able to
write `A.det` instead of `(A : M →ₗ[R] M).det`. -/
noncomputable abbrev det {R : Type*} [CommRing R] {M : Type*} [TopologicalSpace M] [AddCommGroup M]
    [Module R M] (A : M →L[R] M) : R :=
  LinearMap.det (A : M →ₗ[R] M)

Determinant of a Continuous Linear Map

Informal description

For a commutative ring $R$ and a topological space $M$ that is also an $R$-module with an additive commutative group structure, the determinant of a continuous $R$-linear map $A \colon M \to M$ is an element of $R$, denoted $\det(A)$.

ContinuousLinearMap.det_pi theorem

 {ι R M : Type*} [Fintype ι] [CommRing R] [AddCommGroup M] [TopologicalSpace M] [Module R M] [Module.Free R M]
  [Module.Finite R M] (f : ι → M →L[R] M) : (pi (fun i ↦ (f i).comp (proj i))).det = ∏ i, (f i).det

Full source

theorem det_pi {ι R M : Type*} [Fintype ι] [CommRing R] [AddCommGroup M]
    [TopologicalSpace M] [Module R M] [Module.Free R M] [Module.Finite R M]
    (f : ι → M →L[R] M) :
    (pi (fun i ↦ (f i).comp (proj i))).det = ∏ i, (f i).det :=
  LinearMap.det_pi _

Determinant of Product of Continuous Linear Maps Equals Product of Determinants

Informal description

Let $\iota$ be a finite type, $R$ a commutative ring, and $M$ a topological space equipped with an additive commutative group structure and an $R$-module structure that is both free and finitely generated. Given a family of continuous $R$-linear maps $f_i \colon M \to M$ indexed by $\iota$, the determinant of the product map $\prod_{i \in \iota} (f_i \circ \pi_i)$ (where $\pi_i$ is the projection onto the $i$-th component) is equal to the product of the determinants of the individual maps $f_i$, i.e., \[ \det\left(\prod_{i \in \iota} (f_i \circ \pi_i)\right) = \prod_{i \in \iota} \det(f_i). \]

ContinuousLinearMap.det_one_smulRight theorem

 {𝕜 : Type*} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (v : 𝕜) : ((1 : 𝕜 →L[𝕜] 𝕜).smulRight v).det = v

Full source

theorem det_one_smulRight {𝕜 : Type*} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (v : 𝕜) :
    ((1 : 𝕜 →L[𝕜] 𝕜).smulRight v).det = v := by
  nontriviality 𝕜
  have : (1 : 𝕜 →L[𝕜] 𝕜).smulRight v = v • (1 : 𝕜 →L[𝕜] 𝕜) := by
    ext1
    simp only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
      Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.coe_smul', Pi.smul_apply, mul_one]
  rw [this, ContinuousLinearMap.det, ContinuousLinearMap.coe_smul,
    ContinuousLinearMap.one_def, ContinuousLinearMap.coe_id, LinearMap.det_smul,
    Module.finrank_self, LinearMap.det_id, pow_one, mul_one]

Determinant of Scalar Multiplication by Identity: $\det(1 \cdot v) = v$

Informal description

Let $\mathbb{K}$ be a commutative ring equipped with a topology such that multiplication is continuous. For any element $v \in \mathbb{K}$, the determinant of the continuous linear map $1 \cdot v \colon \mathbb{K} \to \mathbb{K}$ (where $1$ is the identity map and $v$ acts by right scalar multiplication) is equal to $v$, i.e., \[ \det(1 \cdot v) = v. \]

ContinuousLinearEquiv.det_coe_symm theorem

 {R : Type*} [Field R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M] (A : M ≃L[R] M) :
  (A.symm : M →L[R] M).det = (A : M →L[R] M).det⁻¹

Full source

@[simp]
theorem det_coe_symm {R : Type*} [Field R] {M : Type*} [TopologicalSpace M] [AddCommGroup M]
    [Module R M] (A : M ≃L[R] M) : (A.symm : M →L[R] M).det = (A : M →L[R] M).det⁻¹ :=
  LinearEquiv.det_coe_symm A.toLinearEquiv

Determinant of Inverse of Continuous Linear Equivalence

Informal description

Let $R$ be a field and $M$ be a topological space equipped with an additive commutative group structure and an $R$-module structure. For any continuous linear equivalence $A \colon M \to M$, the determinant of its inverse $A^{-1}$ is equal to the multiplicative inverse of the determinant of $A$, i.e., $\det(A^{-1}) = \det(A)^{-1}$.