10. 선형대수학

10.1. 벡터 공간과 선형 사상

10.1.1. 벡터 공간

임의의 체 위의 벡터 공간에서 이루어지는 추상 선형대수를 바로 시작하겠습니다. 하지만 이 추상 이론에 논리적으로 의존하지 않는 행렬에 관한 정보는 Section 10.4.1에서 찾을 수 있습니다. Mathlib은 실제로 module이라는 단어를 사용하는 더 일반화된 형태의 선형대수를 다루지만, 지금은 이를 그저 특이한 표기 습관인 척하겠습니다.

“\(K\)를 체라 하고, \(V\)를 \(K\) 위의 벡터 공간이라 하자”라고 말하는 방법(그리고 이를 이후 결과들의 암묵적 인자로 만드는 방법)은 다음과 같습니다:

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

왜 우리가 [AddCommGroup V] [Module K V]라는 두 개의 별도 타입 클래스가 필요한지는 Chapter 8에서 설명했습니다. 간단히 말하면 다음과 같습니다. 수학적으로 우리는 \(K\)-벡터 공간 구조를 가진다는 것이 덧셈적 가환군 구조를 가진다는 것을 함의한다고 말하고자 합니다. 이를 Lean에게 알려줄 수도 있습니다. 하지만 그러면 Lean이 타입 \(V\)에서 그런 군 구조를 찾아야 할 때마다, \(V\)로부터 추론할 수 없는 완전히 특정되지 않은 체 \(K\)를 사용하는 벡터 공간 구조를 찾아 헤매게 될 것입니다. 이는 타입 클래스 합성 시스템에 매우 나쁜 영향을 미칠 것입니다.

벡터 v와 스칼라 a의 곱셈은 a • v로 표기됩니다. 다음 예시에서 이 연산과 덧셈의 상호작용에 관한 몇 가지 대수적 규칙을 나열합니다. 물론 simp나 apply?가 이러한 증명을 찾아낼 것입니다. ring 택틱이 가환환에서 사용되거나 group 택틱이 군에서 사용되는 것과 같은 방식으로, 벡터 공간과 체의 공리로부터 따라오는 목표를 해결하는 module 택틱도 있습니다. 하지만 보조정리 이름에서 스칼라 곱셈이 smul로 축약된다는 것을 기억해 두는 것이 여전히 유용합니다.

example (a : K) (u v : V) : a • (u + v) = a • u + a • v :=
  smul_add a u v

example (a b : K) (u : V) : (a + b) • u = a • u + b • u :=
  add_smul a b u

example (a b : K) (u : V) : a • b • u = b • a • u :=
  smul_comm a b u

좀 더 숙련된 독자를 위한 간단한 참고 사항으로, 용어에서 암시하듯이 Mathlib의 선형대수학은 (반드시 가환적이지는 않은) 환 위의 가군도 다룬다는 점을 짚어 봅시다. 사실 반환 위의 반가군까지도 다룹니다. 이 정도의 일반성이 필요 없다고 생각한다면, 부분가군에 작용하는 아이디얼에 관한 많은 대수적 규칙을 잘 담아내는 다음 예시를 곰곰이 생각해 볼 수 있습니다:

example {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Module (Ideal R) (Submodule R M) :=
  inferInstance

M이 환 R 위의 가군이라고 말하려면 다음과 같이 씁니다:

section
variable {R : Type*} [Ring R] {M : Type*} [AddCommGroup M] [Module R M]
end

이를 벡터 공간을 선언하는 것과 비교해 보면, 두 가지 차이점을 볼 수 있습니다. 변수 이름을 바꾸는 것을 제외하면, 유일한 변화는 Field K 가정을 Ring R 가정으로 바꾸는 것입니다.

M이 반환 R 위의 반가군이라고 말하려면, Ring R 가정을 Semiring R 가정으로 바꾸고, 반가군에는 음수가 없다는 사실을 반영하여 AddCommGroup M도 AddCommMonoid M으로 바꿉니다:

section
variable {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] [Module R M]
end

R이 부정을 가지고 있다고 해서 Lean이 M도 부정을 가진다고 자동으로 추론할 수는 없습니다. 임의의 M이 주어졌을 때 선험적으로 올바른 R을 추측할 수 없기 때문입니다. 따라서 R을 환으로, M을 R위의 가군으로 선언하면, M을 AddCommGroup으로 선언하거나 해당 인스턴스를 지역 문맥에 수동으로 추가해야 합니다:

example {R : Type*} [Ring R] {M : Type*} [AddCommMonoid M] [Module R M] : M → M :=
  -- Make sure to use `letI` (instead of `haveI` or `let`) to make it easier to
  -- identify the existing additive structure from the `AddCommMonoid M` hypothesis
  -- with the new one introduced in the line below.
  letI : AddCommGroup M := Module.addCommMonoidToAddCommGroup R
  fun x => - x

10.1.2. 선형 사상

다음으로 선형 사상이 필요합니다. 군 준동형사상과 마찬가지로, Mathlib에서 선형 사상은 번들 사상, 즉 사상과 그 선형성 성질의 증명으로 이루어진 패키지입니다. 이러한 번들 사상은 적용될 때 일반 함수로 변환됩니다. 이 설계에 대한 자세한 내용은 Chapter 8을 참조하십시오.

두 K-벡터 공간 V와 W 사이의 선형 사상의 타입은 V →ₗ[K] W로 표기됩니다. 아래첨자 l은 선형(linear)을 나타냅니다. 처음에는 이 표기법에서 K를 명시하는 것이 이상하게 느껴질 수 있습니다. 하지만 여러 체가 관련될 때는 이것이 결정적입니다. 예를 들어 \(ℂ\)에서 \(ℂ\)로 가는 실선형 사상은 \(z ↦ az + b\bar{z}\) 형태의 모든 사상이지만, 복소선형 사상은 \(z ↦ az\) 형태의 사상뿐이며, 이 차이는 복소해석학에서 결정적입니다.

variable {W : Type*} [AddCommGroup W] [Module K W]

variable (φ : V →ₗ[K] W)

example (a : K) (v : V) : φ (a • v) = a • φ v :=
  map_smul φ a v

example (v w : V) : φ (v + w) = φ v + φ w :=
  map_add φ v w

V →ₗ[K] W는 그 자체로 흥미로운 대수적 구조를 지니고 있음에 유의하십시오(이는 이러한 사상들을 묶는 동기의 일부입니다). 이는 K-벡터 공간이므로 선형 사상을 더하고 스칼라를 곱할 수 있습니다.

variable (ψ : V →ₗ[K] W)

#check (2 • φ + ψ : V →ₗ[K] W)

묶음 사상을 사용할 때의 한 가지 단점은 일반적인 함수 합성을 사용할 수 없다는 것입니다. LinearMap.comp를 사용하거나 ∘ₗ 표기법을 사용해야 합니다.

variable (θ : W →ₗ[K] V)

#check (φ.comp θ : W →ₗ[K] W)
#check (φ ∘ₗ θ : W →ₗ[K] W)

선형 사상을 구성하는 주요 방법은 두 가지가 있습니다. 첫째, 함수와 선형성 증명을 제공하여 구조체를 만들 수 있습니다. 평소와 같이 이는 구조체 코드 액션으로 쉽게 할 수 있습니다: example : V →ₗ[K] V := _를 입력한 다음, 밑줄에 첨부된 “뼈대 생성”(Generate a skeleton) 코드 액션을 사용하면 됩니다.

example : V →ₗ[K] V where
  toFun v := 3 • v
  map_add' _ _ := smul_add ..
  map_smul' _ _ := smul_comm ..

LinearMap의 증명 필드 이름이 프라임(prime)으로 끝나는 이유가 궁금할 수 있습니다. 이는 함수로의 강제 변환이 정의되기 전에 이 필드들이 정의되기 때문이며, 따라서 LinearMap.toFun을 사용해 표현됩니다. 그런 다음 함수로의 강제 변환을 사용해 LinearMap.map_add와 LinearMap.map_smul로 다시 서술됩니다. 이것이 이야기의 끝은 아닙니다. 덧셈군 준동형사상, 선형 사상, 연속 선형 사상, K-대수 사상 등 덧셈을 보존하는 모든 (번들된) 사상에 적용되는 map_add의 버전도 필요합니다. 이것이 바로 (루트 네임스페이스에 있는) map_add입니다. 중간 버전인 LinearMap.map_add는 다소 중복되지만 점(dot) 표기법을 사용할 수 있게 해주며, 이는 때때로 유용할 수 있습니다. map_smul에 대해서도 비슷한 이야기가 있으며, 일반적인 프레임워크는 8장에서 설명합니다.

#check (φ.map_add' : ∀ x y : V, φ.toFun (x + y) = φ.toFun x + φ.toFun y)
#check (φ.map_add : ∀ x y : V, φ (x + y) = φ x + φ y)
#check (map_add φ : ∀ x y : V, φ (x + y) = φ x + φ y)

다양한 조합자(combinator)를 사용해 Mathlib에 이미 정의되어 있는 선형 사상들로부터 새로운 선형 사상을 만들 수도 있습니다. 예를 들어 위의 예제는 이미 LinearMap.lsmul K V 3으로 알려져 있습니다. 여기서 K와 V가 명시적 인자인 데에는 여러 이유가 있습니다. 가장 시급한 이유는 단순한 LinearMap.lsmul 3만으로는 Lean이 V는 물론 K조차도 추론할 방법이 없기 때문입니다. 하지만 LinearMap.lsmul K V자체도 흥미로운 대상입니다. 이는 K →ₗ[K] V →ₗ[K] V타입을 가지는데, 이는 K가 스스로에 대한 벡터 공간으로 간주될 때, V에서 V로 가는 K-선형 사상들의 공간으로 가는 K-선형 사상이라는 의미입니다.

#check (LinearMap.lsmul K V 3 : V →ₗ[K] V)
#check (LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V)

V ≃ₗ[K] W로 표시되는 선형 동형사상의 타입 LinearEquiv도 있습니다. f : V ≃ₗ[K] W의 역은 f.symm : W ≃ₗ[K] V이고, f와 g의 합성은 f.trans g이며 이는 f ≪≫ₗ g로도 표시되고, V의 항등 동형사상은 LinearEquiv.refl K V입니다. 이 타입의 원소는 필요할 때 자동으로 사상과 함수로 강제 변환됩니다.

example (f : V ≃ₗ[K] W) : f ≪≫ₗ f.symm = LinearEquiv.refl K V :=
  f.self_trans_symm

LinearEquiv.ofBijective를 사용하면 전단사 사상으로부터 동형사상을 만들 수 있습니다. 그렇게 하면 역함수는 계산 불가능해집니다.

noncomputable example (f : V →ₗ[K] W) (h : Function.Bijective f) : V ≃ₗ[K] W :=
  .ofBijective f h

위 예제에서 Lean은 선언된 타입을 사용하여 .ofBijective가 LinearEquiv.ofBijective를 가리킨다는 것을 이해한다는 점에 유의하십시오(어떤 네임스페이스도 열 필요 없이).

10.1.3. 벡터 공간의 합과 곱

직합과 직적을 사용하여 기존 벡터 공간으로부터 새로운 벡터 공간을 만들 수 있습니다. 두 벡터 공간으로 시작해봅시다. 이 경우 합과 곱 사이에 차이가 없으므로, 단순히 곱 타입을 사용할 수 있습니다. 다음 코드 스니펫에서는 모든 구조 사상(포함 사상과 사영 사상)을 선형 사상으로 얻는 방법과, 곱으로 들어가거나 합에서 나오는 선형 사상을 구성하는 보편 성질을 단순히 보여줍니다(합과 곱 사이의 범주론적 구분에 익숙하지 않다면, 보편 성질 관련 용어는 무시하고 다음 예제들의 타입에만 집중해도 됩니다).

section binary_product

variable {W : Type*} [AddCommGroup W] [Module K W]
variable {U : Type*} [AddCommGroup U] [Module K U]
variable {T : Type*} [AddCommGroup T] [Module K T]

-- First projection map
example : V × W →ₗ[K] V := LinearMap.fst K V W

-- Second projection map
example : V × W →ₗ[K] W := LinearMap.snd K V W

-- Universal property of the product
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : U →ₗ[K]  V × W := LinearMap.prod φ ψ

-- The product map does the expected thing, first component
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.fst K V W ∘ₗ LinearMap.prod φ ψ = φ := rfl

-- The product map does the expected thing, second component
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.snd K V W ∘ₗ LinearMap.prod φ ψ = ψ := rfl

-- We can also combine maps in parallel
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) : (V × W) →ₗ[K] (U × T) := φ.prodMap ψ

-- This is simply done by combining the projections with the universal property
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) :
  φ.prodMap ψ = (φ ∘ₗ .fst K V W).prod (ψ ∘ₗ .snd K V W) := rfl

-- First inclusion map
example : V →ₗ[K] V × W := LinearMap.inl K V W

-- Second inclusion map
example : W →ₗ[K] V × W := LinearMap.inr K V W

-- Universal property of the sum (aka coproduct)
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : V × W →ₗ[K] U := φ.coprod ψ

-- The coproduct map does the expected thing, first component
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inl K V W = φ :=
  LinearMap.coprod_inl φ ψ

-- The coproduct map does the expected thing, second component
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inr K V W = ψ :=
  LinearMap.coprod_inr φ ψ

-- The coproduct map is defined in the expected way
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) (v : V) (w : W) :
    φ.coprod ψ (v, w) = φ v + ψ w :=
  rfl

end binary_product

이제 임의의 벡터 공간 족의 합과 곱으로 넘어가 봅시다. 여기서는 벡터 공간의 족을 정의하는 방법과 합과 곱의 보편 성질에 접근하는 방법을 간단히 살펴볼 것입니다. 직접합 표기법이 DirectSum 네임스페이스에 범위가 지정되어 있다는 점, 그리고 직접합의 보편 성질이 인덱싱 타입에 대한 결정 가능한 동등성을 요구한다는 점(이는 어떤 면에서 구현상의 우연입니다)에 유의하십시오.

section families
open DirectSum

variable {ι : Type*} [DecidableEq ι]
         (V : ι → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]

-- The universal property of the direct sum assembles maps from the summands to build
-- a map from the direct sum
example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
  DirectSum.toModule K ι W φ

-- The universal property of the direct product assembles maps into the factors
-- to build a map into the direct product
example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
  LinearMap.pi φ

-- The projection maps from the product
example (i : ι) : (Π j, V j) →ₗ[K] V i := LinearMap.proj i

-- The inclusion maps into the sum
example (i : ι) : V i →ₗ[K] (⨁ i, V i) := DirectSum.lof K ι V i

-- The inclusion maps into the product
example (i : ι) : V i →ₗ[K] (Π i, V i) := LinearMap.single K V i

-- In case `ι` is a finite type, there is an isomorphism between the sum and product.
example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
  linearEquivFunOnFintype K ι V

end families

10.2. 부분공간과 몫공간

10.2.1. 부분공간

선형 사상이 번들되는 것과 마찬가지로, V의 선형 부분공간 또한 부분공간의 담체(carrier)라 불리는 V의 집합과 관련된 닫힘 성질들로 구성된 번들 구조입니다. Mathlib이 실제로 선형대수학에 사용하는 더 일반적인 맥락 때문에 여기서도 벡터 공간 대신 모듈(module)이라는 단어가 등장합니다.

section
variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (U : Submodule K V) {x y : V} (hx : x ∈ U) (hy : y ∈ U) :
    x + y ∈ U :=
  U.add_mem hx hy

example (U : Submodule K V) {x : V} (hx : x ∈ U) (a : K) :
    a • x ∈ U :=
  U.smul_mem a hx
end

위 예시에서, Submodule K V는 U가 Set V의 원소인 술어 IsSubmodule U가 아니라, V의 K-선형 부분공간들의 타입이라는 점을 이해하는 것이 중요합니다. Submodule K V에는 Set V로의 강제 변환과 V에 대한 소속 술어가 부여되어 있습니다. 이것이 어떻게, 왜 이루어지는지에 대한 설명은 제 8.3 절를 참고하십시오.

물론 두 부분공간은 같은 원소를 가질 때에만 서로 같습니다. 이 사실은 ext 택틱과 함께 사용할 수 있도록 등록되어 있으며, 이 택틱은 두 집합이 같음을 증명할 때와 같은 방식으로 두 부분공간이 같음을 증명하는 데 사용할 수 있습니다.

예를 들어 ℝ가 ℂ의 ℝ-선형 부분공간이라는 것을 서술하고 증명하려면, 실제로 우리가 원하는 것은 Set ℂ로의 사영이 ℝ, 더 정확히는 ℂ 안의 ℝ의 상(image)이 되는 Submodule ℝ ℂ 타입의 항을 구성하는 것입니다.

noncomputable example : Submodule ℝ ℂ where
  carrier := Set.range ((↑) : ℝ → ℂ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  smul_mem' := by
    rintro c - ⟨a, rfl⟩
    use c*a
    simp

Submodule의 증명 필드 끝에 붙은 프라임은 LinearMap의 것과 유사합니다. 이 필드들은 MemberShip 인스턴스보다 먼저 정의되기 때문에 carrier 필드를 사용해 서술됩니다. 이후 이 필드들은 앞서 살펴본 Submodule.add_mem, Submodule.zero_mem, Submodule.smul_mem으로 대체됩니다.

부분공간과 선형 사상을 다루는 연습으로서, 여러분은 선형 사상에 의한 부분공간의 원상을 정의하게 됩니다(물론 아래에서 Mathlib가 이미 이를 알고 있음을 보게 될 것입니다). Set.mem_preimage가 소속과 원상을 포함하는 명제를 다시 쓰는 데 사용될 수 있음을 기억하십시오. 이것이 위에서 논의된 LinearMap과 Submodule에 관한 보조정리들 외에 여러분에게 필요한 유일한 보조정리입니다.

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

def preimage {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) :
    Submodule K V where
  carrier := φ ⁻¹' H
  zero_mem' := by
    sorry
  add_mem' := by
    sorry
  smul_mem' := by
    sorry

타입 클래스를 사용하여, Mathlib는 벡터 공간의 부분공간이 벡터 공간 구조를 물려받는다는 것을 알고 있습니다.

example (U : Submodule K V) : Module K U := inferInstance

이 예제는 미묘합니다. 객체 U는 타입이 아니지만, Lean은 이를 V의 부분타입으로 해석하여 자동으로 타입으로 강제 변환합니다. 따라서 위 예제는 다음과 같이 더 명시적으로 다시 서술될 수 있습니다.

example (U : Submodule K V) : Module K {x : V // x ∈ U} := inferInstance

10.2.2. 완비 격자 구조와 내부 직합

술어 IsSubmodule : Set V → Prop 대신 타입 Submodule K V를 갖는 것의 중요한 이점은 Submodule K V에 추가 구조를 쉽게 부여할 수 있다는 것입니다. 중요한 점은, 이것이 포함 관계에 대해 완비 격자 구조를 가진다는 것입니다. 예를 들어, V의 두 부분공간의 교집합이 다시 부분공간이라는 것을 진술하는 보조정리를 갖는 대신, 우리는 격자 연산 ⊓를 사용하여 교집합을 구성합니다. 그런 다음 우리는 그 구성에 격자에 관한 임의의 보조정리를 적용할 수 있습니다.

두 부분공간의 하한(infimum)의 기저 집합이 정의상 실제로 그 교집합임을 확인해 봅시다.

example (H H' : Submodule K V) :
    ((H ⊓ H' : Submodule K V) : Set V) = (H : Set V) ∩ (H' : Set V) := rfl

기저 집합의 교집합에 해당하는 것에 대해 다른 표기법을 사용하는 것이 이상해 보일 수 있지만, 이 대응 관계는 상한(supremum) 연산과 집합의 합집합에는 적용되지 않습니다. 왜냐하면 부분공간들의 합집합은 일반적으로 부분공간이 아니기 때문입니다. 대신 합집합에 의해 생성된 부분공간을 사용해야 하며, 이는 Submodule.span을 사용하여 수행됩니다.

example (H H' : Submodule K V) :
    ((H ⊔ H' : Submodule K V) : Set V) = Submodule.span K ((H : Set V) ∪ (H' : Set V)) := by
  simp [Submodule.span_union]

또 다른 미묘한 점은 V 자체는 Submodule K V 타입을 가지지 않으므로, V를 V의 부분공간으로 다루는 방법이 필요하다는 것입니다. 이것 또한 격자(lattice) 구조에 의해 제공됩니다: 전체 부분공간이 이 격자의 최상 원소입니다.

example (x : V) : x ∈ (⊤ : Submodule K V) := trivial

마찬가지로 이 격자의 최하 원소는 원소가 영원소(zero element) 하나뿐인 부분공간입니다.

example (x : V) : x ∈ (⊥ : Submodule K V) ↔ x = 0 := Submodule.mem_bot K

특히 (내부) 직합(direct sum)을 이루는 부분공간들의 경우를 다룰 수 있습니다. 두 부분공간의 경우, 유계인 임의의 부분 순서 타입에 대해 의미를 가지는 범용 술어 IsCompl을 사용합니다. 일반적인 부분공간 족의 경우에는 DirectSum.IsInternal을 사용합니다.

-- If two subspaces are in direct sum then they span the whole space.
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊔ V = ⊤ := h.sup_eq_top

-- If two subspaces are in direct sum then they intersect only at zero.
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊓ V = ⊥ := h.inf_eq_bot

section
open DirectSum
variable {ι : Type*} [DecidableEq ι]

-- If subspaces are in direct sum then they span the whole space.
example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
  ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top

-- If subspaces are in direct sum then they pairwise intersect only at zero.
example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
  (h.submodule_iSupIndep.pairwiseDisjoint hij).eq_bot

-- Those conditions characterize direct sums.
#check DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top

-- The relation with external direct sums: if a family of subspaces is
-- in internal direct sum then the map from their external direct sum into `V`
-- is a linear isomorphism.
noncomputable example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V)
    (h : DirectSum.IsInternal U) : (⨁ i, U i) ≃ₗ[K] V :=
  LinearEquiv.ofBijective (coeLinearMap U) h
end

10.2.3. 집합에 의해 생성된 부분공간

기존 부분공간들로부터 부분공간을 만드는 것 외에도, s를 포함하는 가장 작은 부분공간을 만드는 Submodule.span K s를 사용하여 임의의 집합 s로부터도 부분공간을 만들 수 있습니다. 종이 위에서는 이 공간이 s의 원소들의 모든 선형 결합으로 이루어져 있다는 사실을 사용하는 것이 일반적입니다. 하지만 Submodule.span_le로 표현되는 그 보편 성질과 Galois 연결에 관한 전체 이론을 사용하는 것이 종종 더 효율적입니다.

example {s : Set V} (E : Submodule K V) : Submodule.span K s ≤ E ↔ s ⊆ E :=
  Submodule.span_le

example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :=
  Submodule.gi K V

이것들만으로 충분하지 않은 경우에는, zero와 s의 원소들에 대해 성립하고 합과 스칼라 곱셈에 대해 안정적이기만 하면 s의 span에 속한 모든 원소에 대해 어떤 성질이 성립함을 보장하는 관련 귀납법 원리 Submodule.span_induction을 사용할 수 있습니다.

연습 삼아, Submodule.mem_sup의 한쪽 함의를 다시 증명해 봅시다. V 위의 다양한 대수 연산들을 연관짓는 공리들로부터 따라오는 목표를 닫는 데 module 택틱을 사용할 수 있다는 것을 기억하십시오.

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  induction h using Submodule.span_induction with
  | mem y h =>
      sorry
  | zero =>
      sorry
  | add x y hx hy hx' hy' =>
      sorry
  | smul a x hx hx' =>
      sorry

10.2.4. 부분공간 밀어내기와 당겨오기

앞서 약속했듯이, 이제 선형 사상으로 부분공간을 밀어내고 당겨오는 방법을 설명합니다. Mathlib에서 늘 그렇듯이, 첫 번째 연산은 map이라고 하고 두 번째 연산은 comap이라고 합니다.

section

variable {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W)

variable (E : Submodule K V) in
#check (Submodule.map φ E : Submodule K W)

variable (F : Submodule K W) in
#check (Submodule.comap φ F : Submodule K V)

이들은 Submodule 이름공간에 속해 있으므로 점 표기법을 사용하여 Submodule.map φ E 대신 E.map φ를 쓸 수 있다는 점에 유의하십시오. 다만 이렇게 쓰면 읽기가 상당히 어색합니다(일부 Mathlib 기여자들은 이런 표기를 사용하기도 합니다만).

특히 선형 사상의 치역과 핵은 부분공간입니다. 이 특수한 경우들은 별도의 선언을 가질 만큼 중요합니다.

example : LinearMap.range φ = .map φ ⊤ := LinearMap.range_eq_map φ

example : LinearMap.ker φ = .comap φ ⊥ := Submodule.comap_bot φ -- or `rfl`

LinearMap.ker는 구조를 더 많이 보존하는 함수들의 클래스에도 적용되며, 따라서 타입이 LinearMap으로 시작하는 인자를 기대하지 않으므로, 여기서는 점 표기법이 작동하지 않기 때문에, LinearMap.ker φ 대신 φ.ker를 쓸 수 없다는 점에 유의하십시오. 그러나 우변에서는 다른 방식의 점 표기법을 사용할 수 있었습니다. Lean은 좌변을 정교화(elaborate)한 후 타입이 Submodule K V인 항을 기대하기 때문에, .comap을 Submodule.comap으로 해석합니다.

다음 보조정리들은 이러한 부분공간과 φ의 성질 사이의 핵심적인 관계를 보여줍니다.

open Function LinearMap

example : Injective φ ↔ ker φ = ⊥ := ker_eq_bot.symm

example : Surjective φ ↔ range φ = ⊤ := range_eq_top.symm

연습 삼아, map과 comap에 대한 갈루아 연결(Galois connection) 성질을 증명해 봅시다. 다음 보조정리들을 사용할 수 있지만, 이는 정의에 의해 참이므로 필수는 아닙니다.

#check Submodule.mem_map_of_mem
#check Submodule.mem_map
#check Submodule.mem_comap

example (E : Submodule K V) (F : Submodule K W) :
    Submodule.map φ E ≤ F ↔ E ≤ Submodule.comap φ F := by
  sorry

10.2.5. 몫공간

몫벡터공간은 일반적인 몫 표기법(일반적인 /가 아니라 \quot으로 입력)을 사용합니다. 몫공간으로의 사영은 Submodule.mkQ이고, 보편 성질은 Submodule.liftQ입니다.

variable (E : Submodule K V)

example : Module K (V ⧸ E) := inferInstance

example : V →ₗ[K] V ⧸ E := E.mkQ

example : ker E.mkQ = E := E.ker_mkQ

example : range E.mkQ = ⊤ := E.range_mkQ

example (hφ : E ≤ ker φ) : V ⧸ E →ₗ[K] W := E.liftQ φ hφ

example (F : Submodule K W) (hφ : E ≤ .comap φ F) : V ⧸ E →ₗ[K] W ⧸ F := E.mapQ F φ hφ

noncomputable example : (V ⧸ LinearMap.ker φ) ≃ₗ[K] range φ := φ.quotKerEquivRange

연습 삼아, 몫공간의 부분공간에 대한 대응 정리를 증명해 봅시다. Mathlib은 이보다 좀 더 정밀한 버전을 Submodule.comapMkQRelIso로 알고 있습니다.

open Submodule

#check Submodule.map_comap_eq
#check Submodule.comap_map_eq

example : Submodule K (V ⧸ E) ≃ { F : Submodule K V // E ≤ F } where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

10.3. 자기사상

선형 사상의 중요한 특수 사례는 자기사상, 즉 벡터 공간에서 자기 자신으로 가는 선형 사상입니다. 이들이 흥미로운 이유는 K-대수를 이루기 때문입니다. 특히 K에 계수를 갖는 다항식을 이들에 대입하여 계산할 수 있으며, 이들은 고유값과 고유벡터를 가질 수 있습니다.

Mathlib은 Module.End K V := V →ₗ[K] V라는 축약형을 사용하는데, 이는 이러한 것들을 많이 사용할 때(특히 Module 네임스페이스를 연 후에) 편리합니다.

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

variable {W : Type*} [AddCommGroup W] [Module K W]


open Polynomial Module LinearMap End

example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ :=
  End.mul_eq_comp φ ψ -- `rfl` would also work

-- evaluating `P` on `φ`
example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
  aeval φ P

-- evaluating `X` on `φ` gives back `φ`
example (φ : End K V) : aeval φ (X : K[X]) = φ :=
  aeval_X φ

자기사상, 부분공간, 다항식을 다루는 연습으로서, (이항) 핵 보조정리를 증명해 봅시다: 임의의 자기사상 \(φ\)와 서로소인 두 다항식 \(P\), \(Q\)에 대해 \(\ker P(φ) ⊕ \ker Q(φ) = \ker \big(PQ(φ)\big)\)가 성립합니다.

IsCoprime x y는 ∃ a b, a * x + b * y = 1로 정의됨에 유의하십시오.

#check Submodule.eq_bot_iff
#check Submodule.mem_inf
#check LinearMap.mem_ker

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) : ker (aeval φ P) ⊓ ker (aeval φ Q) = ⊥ := by
  sorry

#check Submodule.add_mem_sup
#check map_mul
#check End.mul_apply
#check LinearMap.ker_le_ker_comp

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P*Q)) := by
  sorry

이제 고유공간과 고유값에 대한 논의로 넘어갑니다. 자기사상 \(φ\)와 스칼라 \(a\)에 대응하는 고유공간은 \(φ - aId\)의 핵입니다. 고유공간은 a의 모든 값에 대해 정의되지만, 이들이 흥미로운 경우는 0이 아닐 때뿐입니다. 그러나 고유벡터는 정의상 고유공간의 0이 아닌 원소입니다. 이에 대응하는 술어는 End.HasEigenvector입니다.

example (φ : End K V) (a : K) : φ.eigenspace a = LinearMap.ker (φ - a • 1) :=
  End.eigenspace_def

그리고 술어 End.HasEigenvalue와 이에 대응하는 부분 타입 End.Eigenvalues가 있습니다.

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ φ.eigenspace a ≠ ⊥ :=
  Iff.rfl

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ ∃ v, φ.HasEigenvector a v  :=
  ⟨End.HasEigenvalue.exists_hasEigenvector, fun ⟨_, hv⟩ ↦ φ.hasEigenvalue_of_hasEigenvector hv⟩

example (φ : End K V) : φ.Eigenvalues = {a // φ.HasEigenvalue a} :=
  rfl

-- Eigenvalue are roots of the minimal polynomial
example (φ : End K V) (a : K) : φ.HasEigenvalue a → (minpoly K φ).IsRoot a :=
  φ.isRoot_of_hasEigenvalue

-- In finite dimension, the converse is also true (we will discuss dimension below)
example [FiniteDimensional K V] (φ : End K V) (a : K) :
    φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
  φ.hasEigenvalue_iff_isRoot

-- Cayley-Hamilton
example [FiniteDimensional K V] (φ : End K V) : aeval φ φ.charpoly = 0 :=
  φ.aeval_self_charpoly

10.4. 행렬, 기저와 차원

10.4.1. 행렬

추상 벡터 공간에 대한 기저를 소개하기 전에, 어떤 체 \(K\)에 대한 \(K^n\)에서의 훨씬 더 기초적인 선형대수 설정으로 돌아가 보겠습니다. 여기서 주요 대상은 벡터와 행렬입니다. 구체적인 벡터의 경우, ![…] 표기법을 사용할 수 있으며, 성분들은 쉼표로 구분됩니다. 구체적인 행렬의 경우, !![…] 표기법을 사용할 수 있으며, 행은 세미콜론으로 구분되고 각 행의 원소는 쉼표로 구분됩니다. 원소가 ℕ 또는 ℚ와 같은 계산 가능한 타입을 가질 때, eval 명령을 사용해 기본 연산을 시험해볼 수 있습니다.

section matrices

-- Adding vectors
#eval ![1, 2] + ![3, 4]  -- ![4, 6]

-- Adding matrices
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

-- Multiplying matrices
#eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![13, 16; 29, 36]

#eval의 이러한 사용은 오직 탐구를 위해서만 흥미로운 것이며, Sage와 같은 컴퓨터 대수 시스템을 대체하려는 것이 아니라는 점을 이해하는 것이 중요합니다. 여기서 행렬에 사용된 데이터 표현 방식은 어떤 식으로도 계산적으로 효율적이지 않습니다. 배열 대신 함수를 사용하며, 계산이 아니라 증명을 위해 최적화되어 있습니다. #eval이 사용하는 가상 머신 또한 이러한 용도에 최적화되어 있지 않습니다.

행렬 표기법은 행을 나열하지만 벡터 표기법은 행 벡터도 열 벡터도 아니라는 점에 주의하십시오. 행렬과 벡터의 곱셈에서 벡터가 왼쪽(각각 오른쪽)에 있으면 해당 벡터를 행(각각 열) 벡터로 해석합니다. 이는 표기법이 ᵥ*인 Matrix.vecMul과, 표기법이 ` *ᵥ`인 Matrix.mulVec 연산에 해당합니다. 이 표기법들은 Matrix 네임스페이스에 범위가 지정되어 있으므로 이를 열어야 합니다.

open Matrix

-- matrices acting on vectors on the left
#eval !![1, 2; 3, 4] *ᵥ ![1, 1] -- ![3, 7]

-- matrices acting on vectors on the left, resulting in a size one matrix
#eval !![1, 2] *ᵥ ![1, 1]  -- ![3]

-- matrices acting on vectors on the right
#eval  ![1, 1, 1] ᵥ* !![1, 2; 3, 4; 5, 6] -- ![9, 12]

벡터로 지정된 동일한 행이나 열을 갖는 행렬을 생성하기 위해, 행이나 열을 인덱싱하는 타입과 벡터를 인자로 받는 Matrix.replicateRow와 Matrix.replicateCol을 사용합니다. 예를 들어 단일 행 또는 단일 열 행렬을 얻을 수 있습니다(더 정확히는 행이나 열이 Fin 1로 인덱싱되는 행렬입니다).

#eval replicateRow (Fin 1) ![1, 2] -- !![1, 2]

#eval replicateCol (Fin 1) ![1, 2] -- !![1; 2]

다른 익숙한 연산으로는 벡터의 내적, 행렬의 전치, 그리고 정방행렬의 경우 행렬식과 대각합이 있습니다.

-- vector dot product
#eval ![1, 2] ⬝ᵥ ![3, 4] -- `11`

-- matrix transpose
#eval !![1, 2; 3, 4]ᵀ -- `!![1, 3; 2, 4]`

-- determinant
#eval !![(1 : ℤ), 2; 3, 4].det -- `-2`

-- trace
#eval !![(1 : ℤ), 2; 3, 4].trace -- `5`

항목들이 계산 가능한 타입을 가지지 않는 경우, 예를 들어 실수인 경우에는 #eval이 도움이 될 것이라고 기대할 수 없습니다. 또한 이런 종류의 평가는 신뢰된 코드베이스(즉, 증명을 검사할 때 신뢰해야 하는 Lean의 부분)를 상당히 확장하지 않고는 증명에서 사용할 수 없습니다.

따라서 증명에서 simp와 norm_num 택틱을 사용하거나, 빠른 탐색을 위해 이에 대응하는 명령어를 사용하는 것도 좋습니다.

#simp !![(1 : ℝ), 2; 3, 4].det -- `4 - 2*3`

#norm_num !![(1 : ℝ), 2; 3, 4].det -- `-2`

#norm_num !![(1 : ℝ), 2; 3, 4].trace -- `5`

variable (a b c d : ℝ) in
#simp !![a, b; c, d].det -- `a * d – b * c`

정방행렬에 대한 다음으로 중요한 연산은 역행렬입니다. 수의 나눗셈이 항상 정의되어 있고 0으로 나누는 경우에는 인위적인 값인 0을 반환하는 것과 마찬가지로, 역행렬을 구하는 연산은 모든 행렬에 대해 정의되어 있고 가역적이지 않은 행렬에 대해서는 영행렬을 반환합니다.

더 정확히 말하면, 임의의 환에서 이를 수행하는 일반 함수 Ring.inverse가 있으며, 임의의 행렬 A에 대해 A⁻¹는 Ring.inverse A.det • A.adjugate로 정의됩니다. 크라메르 공식에 따르면, 이는 A의 행렬식이 0이 아닐 때 실제로 A의 역행렬입니다.

#norm_num [Matrix.inv_def] !![(1 : ℝ), 2; 3, 4]⁻¹ -- !![-2, 1; 3 / 2, -(1 / 2)]

물론 이 정의는 가역 행렬에 대해서만 실제로 유용합니다. 이를 기록하는 데 도움이 되는 일반 타입 클래스 Invertible이 있습니다. 예를 들어, 다음 예제의 simp 호출은 Invertible 타입 클래스 가정을 갖는 inv_mul_of_invertible 보조정리를 사용하므로, 이것이 타입 클래스 합성 시스템에 의해 발견될 수 있는 경우에만 실행됩니다. 여기서는 have 문을 사용하여 이 사실을 사용 가능하게 만듭니다.

example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  have : Invertible !![(1 : ℝ), 2; 3, 4] := by
    apply Matrix.invertibleOfIsUnitDet
    norm_num
  simp

이 완전히 구체적인 경우에는 norm_num 메커니즘과 apply?를 사용하여 마지막 줄을 찾을 수도 있습니다.

example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  norm_num [Matrix.inv_def]
  exact one_fin_two.symm

위에 나온 모든 구체적인 행렬은 행과 열이 어떤 n에 대해 Fin n으로 색인됩니다(행과 열에 반드시 같은 값일 필요는 없습니다). 하지만 때로는 임의의 유한 타입을 사용하여 행렬을 색인하는 것이 더 편리합니다. 예를 들어 유한 그래프의 인접 행렬은 그래프의 정점에 의해 자연스럽게 색인되는 행과 열을 가집니다.

사실 행렬에 아무 연산도 정의하지 않고 단순히 행렬만 정의하고자 한다면, 인덱싱 타입의 유한성조차 필요하지 않으며, 계수는 어떤 대수적 구조도 없이 임의의 타입을 가질 수 있습니다. 따라서 Mathlib은 임의의 타입 m, n, α에 대해 Matrix m n α를 그저 m → n → α로 정의하며, 지금까지 사용한 행렬들은 Matrix (Fin 2) (Fin 2) ℝ와 같은 타입을 가졌습니다. 물론 대수적 연산은 m, n, α에 대해 더 많은 가정을 필요로 합니다.

m → n → α를 직접 사용하지 않는 주된 이유는 타입 클래스 시스템이 우리가 원하는 바를 이해할 수 있도록 하기 위함임에 유의하십시오. 예를 들어 환 R에 대해 타입 n → R은 점별 곱셈 연산을 갖추고 있으며, 마찬가지로 m → n → R도 이 연산을 가지는데, 이는 행렬에 대해 우리가 원하는 곱셈이 아닙니다.

아래 첫 번째 예제에서는 Lean이 Matrix의 정의를 꿰뚫어 보고 해당 명제를 의미 있는 것으로 받아들이도록 강제한 다음, 모든 항목을 확인하여 증명합니다.

그러나 이어지는 두 예제는 Lean이 Fin 2 → Fin 2 → ℤ에서는 점별 곱셈을 사용하지만 Matrix (Fin 2) (Fin 2) ℤ에서는 행렬 곱셈을 사용함을 보여줍니다.

section

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) * (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : !![1, 1; 1, 1] * !![1, 1; 1, 1] = !![2, 2; 2, 2] := by
  norm_num

Matrix의 타입 클래스 합성 이점을 잃지 않으면서 행렬을 함수로 정의하기 위해, 함수와 행렬 사이의 동치 Matrix.of를 사용할 수 있습니다. 이 동치는 내부적으로 Equiv.refl을 사용하여 정의됩니다.

예를 들어 벡터 v에 대응하는 반데르몬드 행렬을 정의할 수 있습니다.

example {n : ℕ} (v : Fin n → ℝ) :
    Matrix.vandermonde v = Matrix.of (fun i j : Fin n ↦ v i ^ (j : ℕ)) :=
  rfl
end
end matrices

10.4.2. 기저

이제 벡터 공간의 기저에 대해 논의하고자 합니다. 비형식적으로 말하면 이 개념을 정의하는 방법에는 여러 가지가 있습니다. 보편 성질을 사용할 수 있습니다. 기저는 선형독립이면서 생성하는 벡터족이라고 말할 수 있습니다. 또는 이러한 성질들을 결합하여, 기저는 모든 벡터가 기저 벡터들의 선형결합으로 유일하게 표현될 수 있는 벡터족이라고 직접 말할 수도 있습니다. 이를 말하는 또 다른 방법은, 기저가 K-벡터 공간으로 간주되는 기저체 K의 거듭제곱과의 선형 동형사상을 제공한다는 것입니다.

이 동형사상 버전이 실제로 Mathlib이 내부적으로 정의로 사용하는 것이며, 다른 특성화들은 이로부터 증명됩니다. 무한 기저의 경우 “K의 거듭제곱”이라는 개념에 대해 약간의 주의가 필요합니다. 실제로 이 대수적 맥락에서는 유한 선형결합만이 의미를 가집니다. 따라서 참조 벡터 공간으로 필요한 것은 K의 사본들의 직접곱이 아니라 직합입니다. 기저를 색인화하는 어떤 타입 ι에 대해 ⨁ i : ι, K를 사용할 수도 있지만, 대신 더 특수화된 표기법인 ι →₀ K를 사용하는데, 이는 “ι에서 K로 가는 유한 지지를 갖는 함수”, 즉 ι안의 유한 집합 밖에서는 0이 되는 함수를 의미합니다(이 유한 집합은 고정되어 있지 않으며, 함수에 따라 달라집니다). 기저 B로부터 나온 이러한 함수를 벡터 v와 i : ι에서 계산하면 i번째 기저 벡터에 대한 v의 성분(또는 좌표)이 반환됩니다.

K 벡터 공간으로서의 V의 ι 타입으로 인덱싱된 기저의 타입은 Basis ι K V입니다. 동형사상은 Basis.repr이라 불립니다.

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

section

open Module

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)

-- The basis vector with index ``i``
#check (B i : V)

-- the linear isomorphism with the model space given by ``B``
#check (B.repr : V ≃ₗ[K] ι →₀ K)

-- the component function of ``v``
#check (B.repr v : ι →₀ K)

-- the component of ``v`` with index ``i``
#check (B.repr v i : K)

그런 동형사상에서 시작하는 대신, 선형독립이고 생성하는 벡터족 b에서 시작할 수도 있는데, 이것이 Basis.mk입니다.

그 벡터족이 생성한다는 가정은 ⊤ ≤ Submodule.span K (Set.range b)로 표현됩니다. 여기서 ⊤는 V의 최상위 부분공간, 즉 V를 그 자신의 부분공간으로 본 것입니다. 이 표현은 다소 복잡해 보이지만, 아래에서 더 읽기 쉬운 ∀ v, v ∈ Submodule.span K (Set.range b)와 정의상 거의 동치임을 보게 될 것입니다(아래 코드 조각의 밑줄은 v ∈ ⊤라는 불필요한 정보를 가리킵니다).

noncomputable example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) : Basis ι K V :=
  Basis.mk b_indep (fun v _ ↦ b_spans v)

-- The family of vectors underlying the above basis is indeed ``b``.
example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) (i : ι) :
    Basis.mk b_indep (fun v _ ↦ b_spans v) i = b i :=
  Basis.mk_apply b_indep (fun v _ ↦ b_spans v) i

특히 모델 벡터 공간 ι →₀ K는 이른바 표준 기저를 가지며, 이 기저의 repr 함수는 임의의 벡터에 대해 항등 동형사상으로 평가됩니다. 이는 Finsupp.basisSingleOne이라 불리는데, 여기서 Finsupp는 유한 지지 함수를 뜻하고 basisSingleOne은 기저 벡터가 하나의 입력값을 제외하고는 사라지는 함수라는 사실을 가리킵니다. 더 정확히 말하면 i : ι로 색인된 기저 벡터는 Finsupp.single i 1인데, 이는 i에서는 값 1을, 그 외의 모든 곳에서는 0을 취하는 유한 지지 함수입니다.

variable [DecidableEq ι]

example : Finsupp.basisSingleOne.repr = LinearEquiv.refl K (ι →₀ K) :=
  rfl

example (i : ι) : Finsupp.basisSingleOne i = Finsupp.single i 1 :=
  rfl

색인 타입이 유한할 때는 유한 지지 함수 이야기가 필요 없습니다. 이 경우에는 더 단순한 Pi.basisFun을 사용할 수 있는데, 이는 전체 ι → K의 기저를 제공합니다.

example [Finite ι] (x : ι → K) (i : ι) : (Pi.basisFun K ι).repr x i = x i := by
  simp

추상 벡터 공간의 기저에 대한 일반적인 경우로 돌아가서, 임의의 벡터를 기저 벡터들의 선형 결합으로 표현할 수 있습니다. 먼저 유한 기저의 쉬운 경우를 살펴봅시다.

example [Fintype ι] : ∑ i : ι, B.repr v i • (B i) = v :=
  B.sum_repr v

ι가 유한하지 않으면 위 명제는 애초에 의미가 없습니다: ι에 대해 합을 취할 수 없습니다. 하지만 합산되는 함수의 지지집합은 유한합니다(이는 B.repr v의 지지집합입니다). 하지만 이를 고려하는 구성을 적용해야 합니다. 여기서 Mathlib은 익숙해지는 데 시간이 좀 걸리는 특수 목적 함수인 Finsupp.linearCombination을 사용합니다(이는 더 일반적인 Finsupp.sum 위에 구축되어 있습니다). 타입 ι에서 기저체 K로 가는 유한 지지 함수 c와 ι에서 V로 가는 임의의 함수 f가 주어졌을 때, Finsupp.linearCombination K f c는 c의 지지집합에 대한 스칼라 곱 c • f의 합입니다. 특히, 이를 c의 지지집합을 포함하는 임의의 유한 집합에 대한 합으로 대체할 수 있습니다.

example (c : ι →₀ K) (f : ι → V) (s : Finset ι) (h : c.support ⊆ s) :
    Finsupp.linearCombination K f c = ∑ i ∈ s, c i • f i :=
  Finsupp.linearCombination_apply_of_mem_supported K h

f가 유한하게 지지된다고 가정해도 여전히 잘 정의된 합을 얻을 수 있습니다. 하지만 Finsupp.linearCombination이 채택한 선택은 Basis.sum_repr의 일반화를 서술할 수 있게 해주므로 우리의 기저 논의와 관련된 것입니다.

example : Finsupp.linearCombination K B (B.repr v) = v :=
  B.linearCombination_repr v

K가 c의 타입으로부터 추론될 수 있음에도 불구하고, 왜 여기서 명시적 인자로 쓰이는지 궁금할 수 있습니다. 핵심은 부분 적용된 Finsupp.linearCombination K f가 그 자체로 흥미롭다는 점입니다. 이것은 ι →₀ K에서 V로 가는 단순한 함수가 아니라 K-선형 사상입니다.

variable (f : ι → V) in
#check (Finsupp.linearCombination K f : (ι →₀ K) →ₗ[K] V)

수학적 논의로 돌아가서, 기저에서의 벡터의 표현이 여러분이 생각하는 것보다 형식화된 수학에서 덜 유용하다는 점을 이해하는 것이 중요합니다. 실제로 기저의 더 추상적인 성질을 직접 사용하는 것이 훨씬 더 효율적인 경우가 매우 흔합니다. 특히 기저를 대수학의 다른 자유 대상과 연결하는 보편적 성질을 이용하면 기저 벡터의 상을 지정함으로써 선형 사상을 구성할 수 있습니다. 이것이 바로 Basis.constr입니다. 임의의 K-벡터 공간 W에 대해, 우리의 기저 B는 ι → W에서 V →ₗ[K] W로 가는 선형 동형사상 Basis.constr B K를 제공합니다. 이 동형사상은 모든 i : ι에 대해 임의의 함수 u : ι → W를 기저 벡터 B i를 u i로 보내는 선형 사상으로 보낸다는 사실로 특징지어집니다.

section

variable {W : Type*} [AddCommGroup W] [Module K W]
         (φ : V →ₗ[K] W) (u : ι → W)

#check (B.constr K : (ι → W) ≃ₗ[K] (V →ₗ[K] W))

#check (B.constr K u : V →ₗ[K] W)

example (i : ι) : B.constr K u (B i) = u i :=
  B.constr_basis K u i

이 성질은 선형 사상이 기저에서의 값에 의해 결정되기 때문에 실제로 특징적입니다:

example (φ ψ : V →ₗ[K] W) (h : ∀ i, φ (B i) = ψ (B i)) : φ = ψ :=
  B.ext h

만약 목표 공간에도 기저 B'가 있다면, 우리는 선형 사상을 행렬과 동일시할 수 있습니다. 이 식별은 K-선형 동형사상입니다.

variable {ι' : Type*} (B' : Basis ι' K W) [Fintype ι] [Fintype ι'] [DecidableEq ι']

open LinearMap

#check (toMatrix B B' : (V →ₗ[K] W) ≃ₗ[K] Matrix ι' ι K)

open Matrix -- get access to the ``*ᵥ`` notation for multiplication between matrices and vectors.

example (φ : V →ₗ[K] W) (v : V) : (toMatrix B B' φ) *ᵥ (B.repr v) = B'.repr (φ v) :=
  toMatrix_mulVec_repr B B' φ v


variable {ι'' : Type*} (B'' : Basis ι'' K W) [Fintype ι''] [DecidableEq ι'']

example (φ : V →ₗ[K] W) : (toMatrix B B'' φ) = (toMatrix B' B'' .id) * (toMatrix B B' φ) := by
  simp

end

이 주제에 대한 연습으로, 자기준동형사상이 잘 정의된 행렬식을 가짐을 보장하는 정리의 일부를 증명하겠습니다. 구체적으로, 두 기저가 같은 타입으로 인덱싱될 때 그 기저들이 임의의 자기준동형사상에 부여하는 행렬이 같은 행렬식을 가짐을 증명하고자 합니다. 그런 다음 완전한 결과를 얻기 위해서는 모든 기저가 동형인 인덱싱 타입을 가진다는 사실을 이용해 이를 보완해야 할 것입니다.

물론 Mathlib은 이미 이를 알고 있으며, simp가 목표를 즉시 닫을 수 있으므로 너무 일찍 사용해서는 안 되며, 대신 제공된 보조정리를 사용해야 합니다.

open Module LinearMap Matrix

-- Some lemmas coming from the fact that `LinearMap.toMatrix` is an algebra morphism.
#check toMatrix_comp
#check id_comp
#check comp_id
#check toMatrix_id

-- Some lemmas coming from the fact that ``Matrix.det`` is a multiplicative monoid morphism.
#check Matrix.det_mul
#check Matrix.det_one

example [Fintype ι] (B' : Basis ι K V) (φ : End K V) :
    (toMatrix B B φ).det = (toMatrix B' B' φ).det := by
  set M := toMatrix B B φ
  set M' := toMatrix B' B' φ
  set P := (toMatrix B B') LinearMap.id
  set P' := (toMatrix B' B) LinearMap.id
  sorry
end

10.4.3. 차원

단일 벡터 공간의 경우로 돌아가서, 기저는 차원의 개념을 정의하는 데에도 유용합니다. 여기서도 마찬가지로, 유한 차원 벡터공간이라는 기본적인 경우가 있습니다. 이러한 공간에 대해서는 자연수인 차원을 기대합니다. 이것이 바로 Module.finrank입니다. 주어진 아벨 군이 서로 다른 체 위에서 벡터 공간이 될 수 있으므로, 이는 명시적 인자로 기본 체를 받습니다.

section

#check (Module.finrank K V : ℕ)

-- `Fin n → K` is the archetypical space with dimension `n` over `K`.
example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
  Module.finrank_fin_fun K

-- Seen as a vector space over itself, `ℂ` has dimension one.
example : Module.finrank ℂ ℂ = 1 :=
  Module.finrank_self ℂ

-- But as a real vector space it has dimension two.
example : Module.finrank ℝ ℂ = 2 :=
  Complex.finrank_real_complex

Module.finrank는 임의의 벡터 공간에 대해 정의된다는 점에 유의하십시오. 이는 0으로 나눗셈이 0을 반환하는 것처럼, 무한 차원 벡터공간에 대해서는 0을 반환합니다.

물론 많은 보조정리는 유한 차원 가정을 필요로 합니다. 이것이 FiniteDimensional 타입 클래스의 역할입니다. 예를 들어 다음 예제가 이 가정 없이는 어떻게 실패하는지 생각해 보십시오.

example [FiniteDimensional K V] : 0 < Module.finrank K V ↔ Nontrivial V  :=
  Module.finrank_pos_iff

위 명제에서 Nontrivial V는 V가 서로 다른 원소를 최소 두 개 가짐을 의미합니다. Module.finrank_pos_iff는 명시적 인자가 없다는 점에 유의하십시오. 이는 왼쪽에서 오른쪽으로 사용할 때는 문제없지만, 오른쪽에서 왼쪽으로 사용할 때는 그렇지 않은데, Lean이 Nontrivial V라는 명제로부터 K를 추측할 방법이 없기 때문입니다. 이 경우 보조정리가 R이라는 이름의 환에 대해 서술되어 있는지 확인한 후, 이름 인자 구문을 사용하는 것이 유용합니다. 따라서 다음과 같이 작성할 수 있습니다:

example [FiniteDimensional K V] (h : 0 < Module.finrank K V) : Nontrivial V := by
  apply (Module.finrank_pos_iff (R := K)).1
  exact h

위와 같은 표기는 이상해 보이는데, 이미 h를 가정으로 가지고 있으므로 전체 증명 Module.finrank_pos_iff.1 h를 그냥 써도 되기 때문이지만, 더 복잡한 경우를 위해 알아두면 좋습니다.

정의에 따라 FiniteDimensional K V는 임의의 기저로부터 읽어낼 수 있습니다.

variable {ι : Type*} (B : Module.Basis ι K V)

example [Finite ι] : FiniteDimensional K V := Module.Basis.finiteDimensional_of_finite B

example [FiniteDimensional K V] : Finite ι :=
  (FiniteDimensional.fintypeBasisIndex B).finite
end

선형 부분공간에 대응하는 부분 타입이 벡터 공간 구조를 가진다는 사실을 이용하면, 부분공간의 차원에 대해 이야기할 수 있습니다.

section
variable (E F : Submodule K V) [FiniteDimensional K V]

open Module

example : finrank K (E ⊔ F : Submodule K V) + finrank K (E ⊓ F : Submodule K V) =
    finrank K E + finrank K F :=
  Submodule.finrank_sup_add_finrank_inf_eq E F

example : finrank K E ≤ finrank K V := Submodule.finrank_le E

위의 첫 번째 명제에서 타입 명시의 목적은 Type*로의 강제 변환이 너무 일찍 일어나지 않도록 하기 위함입니다.

이제 finrank와 부분공간에 관한 연습문제를 풀 준비가 되었습니다.

example (h : finrank K V < finrank K E + finrank K F) :
    Nontrivial (E ⊓ F : Submodule K V) := by
  sorry
end

이제 차원 이론의 일반적인 경우로 넘어가 봅시다. 이 경우 finrank는 쓸모가 없지만, 같은 벡터 공간의 임의의 두 기저에 대해 그 기저들을 인덱싱하는 타입들 사이에 전단사 함수가 존재한다는 사실은 여전히 성립합니다. 따라서 우리는 여전히 랭크를 기수, 즉 “전단사 함수의 존재라는 동치 관계 아래 타입들의 모임의 몫”의 원소로 정의할 수 있기를 바랄 수 있습니다.

기수를 논할 때는, 이 책의 다른 부분에서처럼 러셀의 역설을 둘러싼 기초적인 문제들을 무시하기가 더 어려워집니다. 모든 타입의 타입은 존재하지 않는데, 그것이 논리적 모순으로 이어지기 때문입니다. 이 문제는 우리가 평소에 무시하려고 하는 유니버스의 계층 구조에 의해 해결됩니다.

각 타입은 유니버스 레벨을 가지며, 이 레벨들은 자연수와 비슷하게 동작합니다. 특히 0번째 레벨이 존재하며, 그에 해당하는 유니버스 Type 0은 단순히 Type으로 표기됩니다. 이 유니버스는 고전 수학의 거의 전부를 담기에 충분합니다. 예를 들어 ℕ과 ℝ은 타입 Type을 가집니다. 각 레벨 u는 u + 1로 표기되는 후속자를 가지며, Type u는 타입 Type (u+1)을 가집니다.

하지만 우주 수준은 자연수가 아니며, 이는 매우 다른 성질을 가지고 있고 타입을 가지지 않습니다. 특히 Lean에서는 u ≠ u + 1과 같은 것을 서술할 수 없습니다. 이러한 일이 일어날 수 있는 타입은 애초에 존재하지 않습니다. Type u ≠ Type (u+1)을 서술하는 것조차 말이 되지 않는데, Type u와 Type (u+1)은 서로 다른 타입을 가지기 때문입니다.

Type*를 쓸 때마다, Lean은 u_n이라는 이름의 우주 수준 변수를 삽입하며, 여기서 n은 숫자입니다. 이는 정의와 명제가 모든 우주에 걸쳐 존재할 수 있게 해줍니다.

우주 수준 u가 주어지면, Type u 위에서 두 타입 α와 β 사이에 전단사 함수가 있으면 서로 동치라고 말하는 동치 관계를 정의할 수 있습니다. 몫 타입 Cardinal.{u}는 Type (u+1)에 존재합니다. 중괄호는 우주 변수를 나타냅니다. 이 몫에서 α : Type u의 상은 Cardinal.mk α : Cardinal.{u}입니다.

하지만 서로 다른 유니버스에 속한 기수는 직접 비교할 수 없습니다. 따라서 엄밀히 말하면 벡터 공간 V의 랭크를 V의 기저를 인덱싱하는 모든 타입의 기수로 정의할 수 없습니다. 그래서 대신 V 안의 모든 선형독립 집합의 기수의 상한인 Module.rank K V로 정의됩니다. V가 유니버스 레벨 u를 가진다면, 그 랭크는 타입 Cardinal.{u}를 가집니다.

#check V -- Type u_2
#check Module.rank K V -- Cardinal.{u_2}

그럼에도 이 정의를 기저와 연관 지을 수 있습니다. 실제로 유니버스 레벨에는 교환법칙이 성립하는 max 연산도 있으며, 두 유니버스 레벨 u와 v가 주어지면 기수들을 공통 유니버스에 놓아 차원 정리를 서술할 수 있게 해주는 연산 Cardinal.lift.{u, v} : Cardinal.{v} → Cardinal.{max v u}가 있습니다.

universe u v -- `u` and `v` will denote universe levels

variable {ι : Type u} (B : Module.Basis ι K V)
         {ι' : Type v} (B' : Module.Basis ι' K V)

example : Cardinal.lift.{v, u} (.mk ι) = Cardinal.lift.{u, v} (.mk ι') :=
  mk_eq_mk_of_basis B B'

자연수에서 유한 기수로의 강제 변환(더 정확히는 V의 유니버스 레벨인 v에서 Cardinal.{v} 안에 존재하는 유한 기수로의 강제 변환)을 사용하여 유한 차원인 경우를 이 논의와 연관 지을 수 있습니다.

example [FiniteDimensional K V] :
    (Module.finrank K V : Cardinal) = Module.rank K V :=
  Module.finrank_eq_rank K V