Merge branch 'leanprover-community:master' into HasMulAntidiagonal

Author: IlPreteRosso

.github/workflows/labels_from_comment.yml

@@ -9,6 +9,10 @@ name: Label PR based on Comment
 on:
   issue_comment:
     types: [created]
+  pull_request_review:
+    types: [submitted]
+  pull_request_review_comment:
+    types: [created]
 
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:

Mathlib/Geometry/Euclidean/Angle/Sphere.lean

@@ -106,6 +106,26 @@ theorem angle_eq_pi_div_two_iff_mem_sphere_ofDiameter {p₁ p₂ p₃ : P} :
 
 alias thales_theorem := angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter
 
+/-- Converse of Thales' theorem in 2D: if three distinct points on a circle
+    form a right angle, then the chord is a diameter. -/
+theorem isDiameter_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} {s : Sphere P}
+    [Fact (finrank ℝ V = 2)]
+    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
+    (hne₁₂ : p₁ ≠ p₂) (hne₂₃ : p₂ ≠ p₃)
+    (hangle : ∠ p₁ p₂ p₃ = π / 2) :
+    s.IsDiameter p₁ p₃ := by
+  haveI : FiniteDimensional ℝ V := .of_finrank_eq_succ (Fact.out : finrank ℝ V = 2)
+  have hne₁₃ : p₁ ≠ p₃ := fun h ↦ by
+    rw [h, angle_self_of_ne hne₂₃.symm] at hangle; linarith [Real.pi_pos]
+  have hd := Sphere.isDiameter_ofDiameter p₁ p₃
+  have h_eq : s = Sphere.ofDiameter p₁ p₃ := by
+    by_contra hne
+    have := eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
+      (Fact.out : finrank ℝ V = 2) hne hne₁₃ hp₁ hp₃ hp₂
+      hd.left_mem hd.right_mem (angle_eq_pi_div_two_iff_mem_sphere_ofDiameter.mp hangle)
+    exact this.elim hne₁₂.symm hne₂₃
+  exact h_eq ▸ hd
+
 /-- For a tangent line to a sphere, the angle between the line and the radius at the tangent point
 equals `π / 2`. -/
 theorem IsTangentAt.angle_eq_pi_div_two {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P}

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -324,7 +324,8 @@ lemma ιMulti_range (n : ℕ) :
   exact ⟨fun i => ⟨ι R (v i), LinearMap.mem_range_self _ _⟩, rfl⟩
 
 /-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power, as a submodule
-of the exterior algebra. -/
+of the exterior algebra. See `exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top` for a version
+where we restrict to elements of the form `x₁ ∧ ⋯ ∧ xₙ` where the `xᵢ` belong to a spanning set. -/
 lemma ιMulti_span_fixedDegree (n : ℕ) :
     Submodule.span R (Set.range (ιMulti R n)) = ⋀[R]^n M := by
   refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

@@ -66,6 +66,10 @@ noncomputable def ιMulti_family {I : Type*} [LinearOrder I] (v : I → M)
     (s : {s : Finset I // Finset.card s = n}) : ⋀[R]^n M :=
   ιMulti R n fun i ↦ v <| Finset.orderIsoOfFin s.val s.property i
 
+lemma ιMulti_family_eq_coe_comp {I : Type*} [LinearOrder I] (v : I → M) :
+    ExteriorAlgebra.ιMulti_family R n v = (↑) ∘ ιMulti_family R n v :=
+  rfl
+
 @[simp] lemma ιMulti_family_apply_coe {I : Type*} [LinearOrder I] (v : I → M)
     (s : {s : Finset I // Finset.card s = n}) :
     ιMulti_family R n v s = ExteriorAlgebra.ιMulti_family R n v s := rfl
@@ -77,6 +81,29 @@ lemma ιMulti_span_fixedDegree :
     Submodule.span R (Set.range (ExteriorAlgebra.ιMulti R n)) = ⋀[R]^n M :=
   ExteriorAlgebra.ιMulti_span_fixedDegree R n
 
+open Set Submodule in
+/-- If a set `s` spans the module `M`, then the set of all elements of the form `x₁ ∧ ⋯ ∧ xₙ`
+where `xᵢ ∈ s` spans `⋀ⁿ M`. -/
+lemma ιMulti_span_fixedDegree_of_span_eq_top {s : Set M} (hs : span R s = ⊤) :
+    span R (ExteriorAlgebra.ιMulti R n '' {a | range a ⊆ s}) = ⋀[R]^n M := by
+  apply le_antisymm
+  · rw [span_le]
+    rintro - ⟨y, ⟨y_mem, rfl⟩⟩
+    apply ExteriorAlgebra.ιMulti_range R n
+    simp
+  · rw [ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map, ← hs, map_span, span_pow, span_le]
+    rintro x hx
+    obtain ⟨f, rfl⟩ := Set.mem_pow.mp hx
+    refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩
+    · rw [Set.mem_setOf_eq, Set.range_comp, Set.image_subset_iff]
+      apply Subset.trans ?_ (s.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse)
+      grind
+    · rw [ExteriorAlgebra.ιMulti_apply]
+      apply congrArg (List.prod ∘ List.ofFn)
+      ext i
+      obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2
+      rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]
+
 /-- The image of `exteriorPower.ιMulti` spans `⋀[R]^n M`. -/
 lemma ιMulti_span :
     Submodule.span R (Set.range (ιMulti R n)) = (⊤ : Submodule R (⋀[R]^n M)) := by
@@ -86,6 +113,13 @@ lemma ιMulti_span :
     Submodule.range_subtype]
   exact ExteriorAlgebra.ιMulti_span_fixedDegree R n
 
+open Set Submodule in
+/-- A version of `ιMulti_span_fixedDegree_of_span` that works in the exterior power. -/
+lemma ιMulti_span_of_span {s : Set M} (hs : span R s = ⊤) :
+    span R (ιMulti R n '' {a | range a ⊆ s}) = ⊤ := by
+  apply LinearMap.map_injective (ker_subtype (⋀[R]^n M))
+  simpa [LinearMap.map_span, Set.image_image] using ιMulti_span_fixedDegree_of_span_eq_top R n M hs
+
 namespace presentation
 
 /-- The index type for the relations in the standard presentation of `⋀[R]^n M`,
@@ -288,6 +322,87 @@ lemma map_surjective {f : M →ₗ[R] N} (hf : Surjective f) :
   rw [Set.range_eq_univ]
   exact Surjective.comp_left hf
 
+section ιMulti_family
+
+variable (R)
+
+open Submodule Set in
+/-- Given an ordered family of vectors `i ↦ v i` ranging over `i ∈ I`, and indexes
+`α₁, α₂, …, αₙ ∈ I` (not necessarily in order) the wedge product `v (α 1) ∧ ⋯ ∧ v (α n)` belongs to
+the span of `n`-fold _ordered_ wedge products of elements of the `v i`. -/
+private lemma ιMulti_family_span_fixedDegree_aux
+    {I : Type*} [LinearOrder I] (v : I → M) (α : Fin n → I) :
+    ExteriorAlgebra.ιMulti R n (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v)) := by
+  by_cases α_inj : Injective α; swap
+  · suffices ExteriorAlgebra.ιMulti R n (v ∘ α) = 0 by simp [this]
+    exact AlternatingMap.map_eq_zero_of_not_injective _ _ <| fun h ↦ α_inj (Injective.of_comp h)
+  suffices ∃ σ : Equiv.Perm (Fin n), (ExteriorAlgebra.ιMulti R n ((v ∘ α) ∘ σ)) ∈
+      Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) by
+    obtain ⟨σ, hσ⟩ := this
+    rw [AlternatingMap.map_perm] at hσ
+    refine (Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ
+    rw [isUnit_iff_exists_inv]
+    use (σ.sign : R)
+    norm_cast
+    simp only [Int.units_mul_self, Units.val_one, Int.cast_one]
+  have α_card : (Finset.image α Finset.univ).card = n :=
+    (Finset.card_image_of_injective Finset.univ α_inj).trans (Finset.card_fin n)
+  use (Finset.orderIsoOfFin (Finset.image α Finset.univ) α_card).toEquiv.trans
+    ((Equiv.setCongr Fintype.coe_image_univ).trans (Equiv.ofInjective α α_inj).symm)
+  apply Submodule.mem_span_of_mem
+  use ⟨(Finset.image α Finset.univ), α_card⟩
+  rw [ExteriorAlgebra.ιMulti_family, Function.comp_assoc]
+  congr
+  ext i
+  simp [Equiv.apply_ofInjective_symm]
+  rfl
+
+open Finset in
+/-- If a family of vectors spans `M`, then the family of its `n`-fold exterior products spans
+`⋀[R]^n M`. Here we work in the exterior algebra. -/
+lemma ιMulti_family_span_fixedDegree_of_span {I : Type*} [LinearOrder I] {v : I → M}
+    (hv : Submodule.span R (Set.range v) = ⊤) :
+    Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) = ⋀[R]^n M := by
+  apply le_antisymm
+  · rw [Submodule.span_le, Set.range_subset_iff]
+    intro
+    rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]
+    exact Submodule.coe_mem _
+  · rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]
+    rintro - ⟨f, ⟨f_range, rfl⟩⟩
+    rw [Set.mem_setOf] at f_range
+    obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range
+    exact ιMulti_family_span_fixedDegree_aux R v α
+
+/-- If a family of vectors spans `M`, then the family of its `n`-fold exterior products spans
+`⋀[R]^n M`. This is a variant of `ιMulti_family_span_fixedDegree_of_span` where we
+work in the exterior power and not the exterior algebra. -/
+lemma ιMulti_family_span_of_span {I : Type*} [LinearOrder I]
+    {v : I → M} (hv : Submodule.span R (Set.range v) = ⊤) :
+    Submodule.span R (Set.range (ιMulti_family R n v)) = ⊤ := by
+  apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))
+  rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]
+  simpa using ιMulti_family_span_fixedDegree_of_span R hv
+
+open Set Submodule in
+/-- If `v` is a family of vectors of `M` indexed by a linearly ordered type, then the span of the
+range of `exteriorPower.ιMulti_family R n v`, i.e., of the family of `n`-fold exterior products
+of elements of `v`, is the image of the map of exterior powers induced by the inclusion of
+the span of `v` into `M`. -/
+lemma ιMulti_family_span {I : Type*} [LinearOrder I] (v : I → M) :
+    (map n (span R (range v)).subtype).range = span R (range (ιMulti_family R n v)) := by
+  have ⟨f, hf⟩ : ∃ f : I → Submodule.span R (Set.range v), Submodule.subtype _ ∘ f = v :=
+    ⟨fun i ↦ ⟨v i, Submodule.subset_span (Set.mem_range_self i)⟩, rfl⟩
+  have htop : Submodule.span R (Set.range f) = ⊤ := by
+    apply SetLike.coe_injective
+    apply Set.image_injective.mpr (Submodule.span R (Set.range v)).injective_subtype
+    rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
+      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
+  rw [LinearMap.range_eq_map (M := ⋀[R]^n _), ← ιMulti_family_span_of_span _ htop,
+    Submodule.map_span, ← Set.range_comp, map_comp_ιMulti_family, hf]
+
+end ιMulti_family
+
 /-! Linear equivalences in degrees 0 and 1. -/
 
 variable (R M) in

docs/100.yaml

@@ -32,9 +32,9 @@
   title  : Gödel’s Incompleteness Theorem
   authors: Shogo Saito
   links  :
-    First incompleteness theorem: https://github.com/FormalizedFormalLogic/Incompleteness/blob/master/Incompleteness/Arith/First.lean
-    Second incompleteness theorem: https://github.com/FormalizedFormalLogic/Incompleteness/blob/master/Incompleteness/Arith/Second.lean
-    website: https://formalizedformallogic.github.io/Book/
+    First incompleteness theorem: https://github.com/FormalizedFormalLogic/Foundation/blob/7c74089c2442ee211abfa1e2dd5a75091800f57b/Foundation/FirstOrder/Incompleteness/First.lean#L24-L53
+    Second incompleteness theorem: https://github.com/FormalizedFormalLogic/Foundation/blob/7c74089c2442ee211abfa1e2dd5a75091800f57b/Foundation/FirstOrder/Incompleteness/Second.lean#L15-L18
+    website: https://formalizedformallogic.github.io/Catalogue/
 7:
   title  : Law of Quadratic Reciprocity
   decls  :

docs/1000.yaml

@@ -188,11 +188,7 @@ Q195133:
 Q200787:
   title: Gödel's incompleteness theorem
   authors: Shogo Saito
-  # TODO: how to display this data nicely? want two URLs, right?
-  # results:
-  #   - First: https://github.com/FormalizedFormalLogic/Incompleteness/blob/master/Incompleteness/Arith/First.lean
-  #   - Second: https://github.com/FormalizedFormalLogic/Incompleteness/blob/master/Incompleteness/Arith/Second.lean
-  url: https://formalizedformallogic.github.io/Book/
+  url: https://formalizedformallogic.github.io/Catalogue/
 
 Q203565:
   title: Solutions of a general cubic equation

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9957d56fa7dcf3fbc4066e3268eaaa739420ae5c",
+   "rev": "ab9f3956f91980e61bea324c0cf1e9e7d9c8518b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

scripts/bench/lint/README.md

@@ -1,4 +1,4 @@
-## The `lint` benchmark
+# The `lint` benchmark
 
 This benchmark runs `lake exe runLinter Mathlib`.
 It measures the following metrics:

scripts/bench/open-mathlib/README.md

@@ -1,4 +1,4 @@
-## The `open-mathlib` benchmark
+# The `open-mathlib` benchmark
 
 This benchmark approximates `import Mathlib` in the editor by running `lake lean Mathlib.lean`.
 It measures the following metrics:

scripts/bench/size/README.md

@@ -1,4 +1,4 @@
-## The `size` benchmark
+# The `size` benchmark
 
 This benchmark measures a few deterministic values.