int_two_exacttheoremProved here from basic factspropext, Classical.choice, Quot.sound
int_two_exactLean 4Proved here from basic factsFormally verified
/-- **The short exact sequence `0 → ℤ --2·--> ℤ → ℤ/2 → 0` is exact in the middle**: the imageof multiplication by `2` is exactly the kernel of reduction mod `2`. (Exactness at the ends saysthat `2·` is injective and reduction is surjective; both are immediate.) The proof is thearithmetic fact that an integer reduces to `0` in `ℤ/2` exactly when it is even. -/theorem int_two_exact : Function.Exact (fun n : ℤ => 2 * n) (fun n : ℤ => (n : ZMod 2)) := by intro n constructor · intro h have h2 : (2 : ℤ) ∣ n := (ZMod.intCast_zmod_eq_zero_iff_dvd n 2).mp h obtain ⟨m, hm⟩ := h2 exact ⟨m, hm.symm⟩ · rintro ⟨m, rfl⟩ push_cast have : (2 : ZMod 2) = 0 := rfl rw [this, zero_mul]
zmod_two_not_freetheoremProved here from basic factspropext, Classical.choice, Quot.sound
zmod_two_not_freeLean 4Proved here from basic factsFormally verified
/-- **`ℤ/2` is a `ℤ`-module with no basis.** Human proof: suppose `b` were a basis. Since`ℤ/2 ≠ 0` the basis is non-empty; pick a basis vector `b i`. Then `2 • b i = 0` in `ℤ/2`, anon-trivial linear relation (the coefficient `2 ≠ 0` in `ℤ`), contradicting linear independence.So modules, unlike vector spaces, can fail to be free: torsion is the obstruction. -/theorem zmod_two_not_free : ¬ Module.Free ℤ (ZMod 2) := by intro hfree let b := Module.Free.chooseBasis ℤ (ZMod 2) have hne : Nonempty (Module.Free.ChooseBasisIndex ℤ (ZMod 2)) := by by_contra hempty rw [not_nonempty_iff] at hempty have h1 : (1 : ZMod 2) = 0 := by rw [← b.sum_repr (1 : ZMod 2)] simp exact one_ne_zero h1 obtain ⟨i⟩ := hne have h2 : (2 : ℤ) • b i = 0 := by have : ∀ x : ZMod 2, (2 : ℤ) • x = 0 := by decide exact this _ -- a basis vector is never killed by a non-zero scalar have key : (2 : ℤ) = 0 := by have hli := b.linearIndependent rw [LinearIndependent] at hli have := hli (a₁ := Finsupp.single i 2) (a₂ := 0) simp only [Finsupp.linearCombination_single, map_zero] at this have h := this h2 simpa using congrArg (fun f => f i) h exact two_ne_zero key
free_liftingtheoremProved here from basic factspropext, Classical.choice, Quot.sound
free_liftingLean 4Proved here from basic factsFormally verified
/-- **Maps out of a free module lift along surjections.** Let `g : M → N` be surjective and`f : R^(ι) → N` a homomorphism from the free module on `ι`. For each basis vector `eᵢ`, choose`mᵢ ∈ M` with `g mᵢ = f eᵢ` (surjectivity); the universal property of the free module gives aunique `h` with `h eᵢ = mᵢ`, and `g ∘ h = f` because both agree on the basis. This is exactly whyfree modules are projective. -/theorem free_lifting {R : Type*} [Ring R] {ι M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (g : M →ₗ[R] N) (hg : Function.Surjective g) (f : (ι →₀ R) →ₗ[R] N) : ∃ h : (ι →₀ R) →ₗ[R] M, g ∘ₗ h = f := by choose m hm using fun i : ι => hg (f (Finsupp.single i 1)) refine ⟨Finsupp.linearCombination R m, ?_⟩ ext i simp [hm]
projective_of_freetheoremApplies a library theorempropext, Classical.choice, Quot.sound
projective_of_freeLean 4Applies a library theoremFormally verified
/-- **Free modules are projective.** This is Mathlib's instance `Module.Projective.of_free`,whose proof is the lifting argument of `free_lifting`. -/theorem projective_of_free {R P : Type*} [Ring R] [AddCommGroup P] [Module R P] [Module.Free R P] : Module.Projective R P := Module.Projective.of_free
projective_liftingtheoremApplies a library theorempropext, Classical.choice, Quot.sound
projective_liftingLean 4Applies a library theoremFormally verified
/-- **The lifting property of projective modules**: every map from a projective module to thetarget of a surjection lifts through it — equivalently, `Hom(P, −)` carries surjections tosurjections. Mathlib: `Module.projective_lifting_property`. -/theorem projective_lifting {R P M N : Type*} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Projective R P] (g : M →ₗ[R] N) (f : P →ₗ[R] N) (hg : Function.Surjective g) : ∃ h : P →ₗ[R] M, g ∘ₗ h = f := Module.projective_lifting_property g f hg
submodule_free_pidtheoremApplies a library theorempropext, Classical.choice, Quot.sound
submodule_free_pidLean 4Applies a library theoremFormally verified
/-- **Over a PID, submodules of finite free modules are free** (of rank at most the rank of theambient module). Mathlib: `Submodule.basisOfPid`, which produces a basis of the submodule indexedby `Fin n`; the proof is the induction on the rank given in the lesson. -/theorem submodule_free_pid {R M : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] {ι : Type*} [Finite ι] (b : Module.Basis ι R M) (N : Submodule R M) : ∃ n : ℕ, Nonempty (Module.Basis (Fin n) R N) := ⟨(Submodule.basisOfPid b N).1, ⟨(Submodule.basisOfPid b N).2⟩⟩
structure_theoremtheoremApplies a library theorempropext, Classical.choice, Quot.sound
structure_theoremLean 4Applies a library theoremFormally verified
/-- **Structure theorem for finitely generated modules over a PID** (elementary divisor form):`M ≅ Rⁿ ⊕ ⨁ᵢ R/(pᵢ^eᵢ)` with each `pᵢ` irreducible (prime). Mathlib:`Module.equiv_free_prod_directSum`. Grouping the prime powers gives the invariant factor form`R/(d₁) ⊕ ⋯ ⊕ R/(dₖ)` with `d₁ ∣ ⋯ ∣ dₖ` used in the lesson. -/theorem structure_theorem {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (ι : Type u) (_ : Fintype ι) (p : ι → R) (_ : ∀ i, Irreducible (p i)) (e : ι → ℕ), Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι (fun i => R ⧸ R ∙ p i ^ e i)) := Module.equiv_free_prod_directSum R M
tensor_homdefApplies a library theorempropext, Quot.sound
tensor_homLean 4Applies a library theoremFormally verified
/-- **The tensor–hom adjunction** (one variable at a time): bilinear maps `M × N → P`, that islinear maps `M → Hom(N, P)`, are the same as linear maps `M ⊗ N → P`, naturally. Mathlib:`TensorProduct.lift.equiv`. -/noncomputable def tensor_hom (R M N P : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] (M ⊗[R] N →ₗ[R] P) := TensorProduct.lift.equiv (RingHom.id R) M N P
tensor_right_exacttheoremApplies a library theorempropext, Classical.choice, Quot.sound
tensor_right_exactLean 4Applies a library theoremFormally verified
/-- **Tensoring is right exact**: if `M → N → P → 0` is exact then so is`M ⊗ Q → N ⊗ Q → P ⊗ Q → 0`. Mathlib: `rTensor_exact` (exactness in the middle) and`LinearMap.rTensor_surjective` (at the right). The lesson derives it from the tensor–homadjunction. -/theorem tensor_right_exact {R M N P : Type*} (Q : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact f g) (hg : Function.Surjective g) : Function.Exact (f.rTensor Q) (g.rTensor Q) ∧ Function.Surjective (g.rTensor Q) := ⟨rTensor_exact Q hfg hg, LinearMap.rTensor_surjective Q hg⟩
tensor_not_left_exacttheoremProved here from basic factspropext, Classical.choice, Quot.sound
tensor_not_left_exactLean 4Proved here from basic factsFormally verified
/-- **…but not exact.** Multiplication by `2` on `ℤ` is injective, yet after tensoring with`ℤ/2` it becomes the zero map on `ℤ ⊗ ℤ/2 ≅ ℤ/2 ≠ 0`, so it is no longer injective.Human proof: on a pure tensor, `(2a) ⊗ b = a ⊗ 2b = a ⊗ 0 = 0`; and `1 ⊗ 1 ≠ 0` because`n ⊗ b ↦ n • b` is a well-defined map `ℤ ⊗ ℤ/2 → ℤ/2` sending it to `1`. -/theorem tensor_not_left_exact : Function.Injective (2 • LinearMap.id : ℤ →ₗ[ℤ] ℤ) ∧ ¬ Function.Injective ((2 • LinearMap.id : ℤ →ₗ[ℤ] ℤ).rTensor (ZMod 2)) := by constructor · intro a b h have h' : 2 * a = 2 * b := by simpa [two_smul, two_mul] using h omega · intro hinj -- the element `1 ⊗ 1` is sent to `2 ⊗ 1 = 1 ⊗ 2 = 0` have himg : ((2 • LinearMap.id : ℤ →ₗ[ℤ] ℤ).rTensor (ZMod 2)) ((1 : ℤ) ⊗ₜ (1 : ZMod 2)) = 0 := by rw [LinearMap.rTensor_tmul] simp only [LinearMap.smul_apply, LinearMap.id_apply] rw [TensorProduct.smul_tmul] have : (2 : ℕ) • (1 : ZMod 2) = 0 := by decide rw [this, TensorProduct.tmul_zero] have hzero : (1 : ℤ) ⊗ₜ[ℤ] (1 : ZMod 2) = 0 := hinj (himg.trans (map_zero _).symm) -- but `1 ⊗ 1` maps to `1 ≠ 0` under `ℤ ⊗ ℤ/2 ≅ ℤ/2` have := congrArg (TensorProduct.lid ℤ (ZMod 2)) hzero rw [TensorProduct.lid_tmul, map_zero, one_smul] at this exact one_ne_zero this
/-- Maps out of a free module lift along surjections.Hint: `choose m hm using fun i : ι => hg (f (Finsupp.single i 1))` picks preimages of the imagesof the basis vectors; then use `Finsupp.linearCombination R m`, and check equality on basisvectors with `ext i` followed by `simp [hm]`. -/theorem free_lifting {R : Type*} [Ring R] {ι M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (g : M →ₗ[R] N) (hg : Function.Surjective g) (f : (ι →₀ R) →ₗ[R] N) : ∃ h : (ι →₀ R) →ₗ[R] M, g ∘ₗ h = f := by sorry
Show the compiled solution
free_liftingLean 4Proved here from basic factsFormally verified
/-- **Maps out of a free module lift along surjections.** Let `g : M → N` be surjective and`f : R^(ι) → N` a homomorphism from the free module on `ι`. For each basis vector `eᵢ`, choose`mᵢ ∈ M` with `g mᵢ = f eᵢ` (surjectivity); the universal property of the free module gives aunique `h` with `h eᵢ = mᵢ`, and `g ∘ h = f` because both agree on the basis. This is exactly whyfree modules are projective. -/theorem free_lifting {R : Type*} [Ring R] {ι M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (g : M →ₗ[R] N) (hg : Function.Surjective g) (f : (ι →₀ R) →ₗ[R] N) : ∃ h : (ι →₀ R) →ₗ[R] M, g ∘ₗ h = f := by choose m hm using fun i : ι => hg (f (Finsupp.single i 1)) refine ⟨Finsupp.linearCombination R m, ?_⟩ ext i simp [hm]
/-- The sequence `ℤ --2·--> ℤ → ℤ/2` is exact in the middle.Hint: `ZMod.intCast_zmod_eq_zero_iff_dvd` turns `(n : ZMod 2) = 0` into `2 ∣ n`. -/theorem int_two_exact : Function.Exact (fun n : ℤ => 2 * n) (fun n : ℤ => (n : ZMod 2)) := by sorry
Show the compiled solution
int_two_exactLean 4Proved here from basic factsFormally verified
/-- **The short exact sequence `0 → ℤ --2·--> ℤ → ℤ/2 → 0` is exact in the middle**: the imageof multiplication by `2` is exactly the kernel of reduction mod `2`. (Exactness at the ends saysthat `2·` is injective and reduction is surjective; both are immediate.) The proof is thearithmetic fact that an integer reduces to `0` in `ℤ/2` exactly when it is even. -/theorem int_two_exact : Function.Exact (fun n : ℤ => 2 * n) (fun n : ℤ => (n : ZMod 2)) := by intro n constructor · intro h have h2 : (2 : ℤ) ∣ n := (ZMod.intCast_zmod_eq_zero_iff_dvd n 2).mp h obtain ⟨m, hm⟩ := h2 exact ⟨m, hm.symm⟩ · rintro ⟨m, rfl⟩ push_cast have : (2 : ZMod 2) = 0 := rfl rw [this, zero_mul]