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으로 바꿉니다. 이는 반가군에 부호 반전(negation)이 없다는 사실을 반영합니다:

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

Lean은 R이 부정(negation)을 가진다고 해서 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의 증명 필드 이름이 왜 프라임 기호로 끝나는지 궁금할 수 있습니다. 이는 이 필드들이 함수로의 강제 변환보다 먼저 정의되기 때문이며, 따라서 LinearMap.toFun을 사용하여 서술됩니다. 그런 다음 이들은 함수로의 강제 변환을 사용하여 LinearMap.map_add와 LinearMap.map_smul로 다시 서술됩니다. 이야기는 아직 끝나지 않았습니다. 또한 덧셈군 준동형사상, 선형 사상, 연속 선형 사상, K-대수 사상 등과 같이 덧셈을 보존하는 모든 (묶인) 사상에 적용되는 map_add의 버전도 필요합니다. 이것이 (루트 네임스페이스에 있는) map_add입니다. 중간 버전인 LinearMap.map_add는 다소 중복되지만 점 표기법을 사용할 수 있게 해 주며, 이는 때때로 편리합니다. 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)해집니다.

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 네임스페이스 안에서만 사용할 수 있으며, 직합의 보편 성질은 인덱스 타입에 결정 가능한 동등성(decidable equality)을 요구한다는 점에 유의하십시오(이는 어느 정도 구현상의 우연입니다).

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의 선형 부분공간도 묶인 구조입니다. 이 구조는 부분공간의 바탕 집합이라고 부르는 V 안의 집합과 관련된 닫힘 성질들로 이루어져 있습니다. 여기서도 벡터 공간 대신 가군이라는 단어가 쓰입니다. Mathlib이 실제로 선형대수에 사용하는 문맥이 더 일반적이기 때문입니다.

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는 Set V의 원소 U에 대한 술어 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의 부분공간으로 간주하여 다룰 방법이 필요하다는 것입니다. 이것도 격자 구조가 제공합니다. 전체 부분공간이 이 격자의 최대 원소입니다.

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

마찬가지로 이 격자의 최소 원소는 영원소만을 원소로 갖는 부분공간입니다.

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. 집합이 생성하는 부분공간

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

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

이것으로 충분하지 않을 때는 관련된 귀납법 원리인 Submodule.span_induction을 사용할 수 있습니다. 이 원리는 어떤 성질이 zero와 s의 원소에서 성립하고 합과 스칼라 곱셈에 대해 닫혀 있기만 하면, 그 성질이 s의 생성 공간의 모든 원소에서 성립함을 보장합니다.

연습 삼아 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 φ 대신 φ.ker라고 쓸 수 없다는 점에 유의하십시오. LinearMap.ker는 더 많은 구조를 보존하는 사상들의 클래스에도 적용되므로 타입이 LinearMap으로 시작하는 인자를 기대하지 않으며, 따라서 여기서는 점 표기법이 작동하지 않습니다. 하지만 우변에서는 다른 종류의 점 표기법을 사용할 수 있었습니다. Lean은 좌변을 엘라보레이션한 후 타입이 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에 대한 갈루아 연결 성질을 증명해 봅시다. 다음 보조정리들을 사용할 수 있지만, 정의에 의해 참이므로 꼭 사용할 필요는 없습니다.

#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]

그 밖에 익숙한 연산으로는 벡터의 내적(dot product)에 해당하는 곱, 행렬의 전치, 그리고 정사각 행렬에 대한 행렬식과 대각합이 있습니다.

-- 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으로 인덱싱됩니다(행과 열의 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은 기저 벡터들이 단 하나의 입력값을 제외한 모든 곳에서 0이 되는 함수라는 사실을 가리킵니다. 더 정확히 말하면, 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

인덱스 타입이 유한하면 유한 지지 함수 이야기는 필요하지 않습니다. 이 경우에는 ι → K 전체의 기저를 제공하는 더 간단한 Pi.basisFun을 사용할 수 있습니다.

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를 줍니다. 이 동형사상은 임의의 함수 u : ι → W를 모든 i : ι에 대해 기저 벡터 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'

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

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