Merge remote-tracking branch 'mathnetwork/develop'

Author: Xinze-Li-Moqian

OpenGALib/Algebraic/Auxiliary/Fin.lean

@@ -33,22 +33,9 @@ theorem finAddFlip_finSumFinEquiv {m n : ℕ} (a : Fin m ⊕ Fin n) :
 /-- `Fin (m + n) ≃ Fin (n + m)`. -/
 def finAddCongr : Fin (m + n) ≃ Fin (n + m) := finCongr (add_comm m n)
 
-@[simp]
-lemma finAddCongr_finAddCongr (i : Fin (m + n)) :
-    finAddCongr (finAddCongr i) = i :=
-  rfl
-
-@[simp]
-lemma finAddCongr_symm_finAddCongr_symm (i : Fin (m + n)) :
-    finAddCongr.symm (finAddCongr.symm i) = i :=
-  rfl
-
-/-- `Fin m ⊕ Fin n ≃ Fin n ⊕ Fin m` via `Sum.swap`. -/
-def finSumCongr : Fin m ⊕ Fin n ≃ Fin n ⊕ Fin m where
-  toFun x := x.swap
-  invFun x := x.swap
-  left_inv := Sum.swap_swap
-  right_inv := Sum.swap_swap
+/-- `Fin m ⊕ Fin n ≃ Fin n ⊕ Fin m` via `Sum.swap`.
+Thin wrapper over Mathlib `Equiv.sumComm`. -/
+def finSumCongr : Fin m ⊕ Fin n ≃ Fin n ⊕ Fin m := Equiv.sumComm (Fin m) (Fin n)
 
 @[simp]
 lemma finSumCongr_symm_inl_inr (x : Fin m) :

OpenGALib/Algebraic/Auxiliary/Perm.lean

@@ -15,24 +15,6 @@ open Fin
 
 variable {m n p k : ℕ}
 
-@[simps!]
-def addAssocPerm :
-    Equiv.Perm ((Fin m ⊕ Fin n) ⊕ Fin p) ≃ Equiv.Perm (Fin m ⊕ Fin n ⊕ Fin p) :=
-  Equiv.permCongr (Equiv.sumAssoc (Fin m) (Fin n) (Fin p))
-
-@[simp]
-lemma addAssocPerm_symm_addAssocPerm (σ₁ : Equiv.Perm ((Fin m ⊕ Fin n) ⊕ Fin p)) :
-    addAssocPerm.symm (addAssocPerm σ₁) = σ₁ :=
-  Equiv.symm_apply_apply addAssocPerm σ₁
-
-@[simp]
-lemma sign_addAssocPerm (σ₁ : Equiv.Perm ((Fin m ⊕ Fin n) ⊕ Fin p)) :
-    Equiv.Perm.sign (addAssocPerm σ₁) = Equiv.Perm.sign σ₁ := by
-  simp only [addAssocPerm, Equiv.Perm.sign_permCongr]
-
-def addCongrPerm : Equiv.Perm (Fin (m + n)) ≃ Equiv.Perm (Fin (n + m)) :=
-  Equiv.permCongr finAddCongr
-
 def sumCongrPerm : Equiv.Perm (Fin m ⊕ Fin n) ≃ Equiv.Perm (Fin n ⊕ Fin m) :=
   Equiv.permCongr finSumCongr
 

OpenGALib/Algebraic/Auxiliary/ShuffleSplit.lean

@@ -144,25 +144,13 @@ theorem removeNone_sign {α : Type*} [DecidableEq α] [Fintype α]
   conv_rhs => rw [← optionCongr_removeNone_of_fix_none σ h]
   exact (Equiv.optionCongr_sign _).symm
 
-/-- `Equiv.permCongr` preserves sign. -/
-theorem permCongr_sign {α β : Type*} [DecidableEq α] [DecidableEq β]
-    [Fintype α] [Fintype β]
-    (e : α ≃ β) (σ : Equiv.Perm α) :
-    Equiv.Perm.sign (Equiv.permCongr e σ) = Equiv.Perm.sign σ :=
-  Equiv.Perm.sign_permCongr _ _
-
-/-- `Equiv.permCongr` commutes with `Equiv.Perm` inverse-multiply. -/
+/-- `Equiv.permCongr` commutes with `Equiv.Perm` inverse-multiply.
+Thin wrapper over the `MulEquiv` `Equiv.permCongrHom`. -/
 theorem permCongr_inv_mul {α β : Type*}
     (e : α ≃ β) (σ₁ σ₂ : Equiv.Perm α) :
     Equiv.permCongr e (σ₁⁻¹ * σ₂) =
       (Equiv.permCongr e σ₁)⁻¹ * Equiv.permCongr e σ₂ := by
-  have h_inv : (Equiv.permCongr e σ₁ : Equiv.Perm _)⁻¹ =
-      Equiv.permCongr e σ₁⁻¹ := by
-    ext y
-    show (Equiv.permCongr e σ₁).symm y = e (σ₁⁻¹ (e.symm y))
-    simp [Equiv.permCongr_def, Equiv.Perm.inv_def]
-  ext x
-  simp only [Equiv.Perm.coe_mul, Function.comp_apply, Equiv.permCongr_apply,
-    h_inv, Equiv.symm_apply_apply]
+  have := map_mul e.permCongrHom σ₁⁻¹ σ₂
+  simpa only [Equiv.permCongrHom_coe, map_inv] using this
 
 end ShuffleSplit

OpenGALib/Algebraic/BilinearForm/Basic.lean

@@ -1,4 +1,5 @@
 import Mathlib.LinearAlgebra.BilinearForm.Basic
+import Mathlib.LinearAlgebra.BilinearForm.Properties
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Algebra.Order.Ring.Defs
 
@@ -18,20 +19,21 @@ positive-definite forms in optimisation, matrix calculus.
 
 namespace BilinearForm
 
-/-- A bilinear form on `V` over field `𝕜`: a linear map
-`V →ₗ[𝕜] V →ₗ[𝕜] 𝕜`. -/
-abbrev Form (𝕜 : Type*) [Field 𝕜]
-    (V : Type*) [AddCommGroup V] [Module 𝕜 V] :=
-  V →ₗ[𝕜] V →ₗ[𝕜] 𝕜
+/-- A bilinear form on `V` over `𝕜`: a linear map
+`V →ₗ[𝕜] V →ₗ[𝕜] 𝕜`. Definitionally Mathlib's `LinearMap.BilinForm`. -/
+abbrev Form (𝕜 : Type*) [CommSemiring 𝕜]
+    (V : Type*) [AddCommMonoid V] [Module 𝕜 V] :=
+  LinearMap.BilinForm 𝕜 V
 
 section Algebra
 
 variable {𝕜 : Type*} [Field 𝕜]
   {V : Type*} [AddCommGroup V] [Module 𝕜 V]
 
-/-- The bilinear form is symmetric. -/
-def IsSymm (B : Form 𝕜 V) : Prop :=
-  ∀ v w, B v w = B w v
+/-- The bilinear form is symmetric. Alias of Mathlib's
+`LinearMap.BilinForm.IsSymm`. -/
+abbrev IsSymm (B : Form 𝕜 V) : Prop :=
+  LinearMap.BilinForm.IsSymm B
 
 /-- The **inner product** $\langle v, w \rangle_B$ via a bilinear form. -/
 def inner (B : Form 𝕜 V) (v w : V) : 𝕜 :=
@@ -50,7 +52,7 @@ generic version of the framework's `metricInner_*` lemmas. -/
 /-- **Symmetry** (when the form is symmetric). -/
 theorem inner_comm {B : Form 𝕜 V} (hB : IsSymm B) (v w : V) :
     inner B v w = inner B w v :=
-  hB v w
+  hB.eq v w
 
 /-- **Additivity in left argument**. -/
 theorem inner_add_left (B : Form 𝕜 V) (v₁ v₂ w : V) :
@@ -100,13 +102,13 @@ theorem inner_neg_right (B : Form 𝕜 V) (v w : V) :
 @[simp]
 theorem inner_sub_left (B : Form 𝕜 V) (v₁ v₂ w : V) :
     inner B (v₁ - v₂) w = inner B v₁ w - inner B v₂ w := by
-  rw [sub_eq_add_neg, inner_add_left, inner_neg_left, sub_eq_add_neg]
+  simp [inner_def, map_sub, LinearMap.sub_apply]
 
 /-- **Subtraction in right argument**. -/
 @[simp]
 theorem inner_sub_right (B : Form 𝕜 V) (v w₁ w₂ : V) :
     inner B v (w₁ - w₂) = inner B v w₁ - inner B v w₂ := by
-  rw [sub_eq_add_neg, inner_add_right, inner_neg_right, sub_eq_add_neg]
+  simp [inner_def, map_sub]
 
 end Algebra
 

OpenGALib/Algebraic/BilinearForm/Riesz.lean

@@ -1,6 +1,5 @@
 import OpenGALib.Algebraic.BilinearForm.Basic
-import Mathlib.LinearAlgebra.Dual.Lemmas
-import Mathlib.LinearAlgebra.FiniteDimensional.Defs
+import Mathlib.LinearAlgebra.BilinearForm.Properties
 
 /-!
 # Riesz extraction — algebraic core
@@ -45,6 +44,19 @@ omit [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] in
 theorem toDual_apply (B : Form 𝕜 V) (v w : V) :
     toDual B v w = inner B v w := rfl
 
+omit [IsStrictOrderedRing 𝕜] in
+/-- **Positive-definite ⇒ nondegenerate** (`LinearMap.BilinForm.Nondegenerate`):
+a positive-definite bilinear form is nondegenerate, the hypothesis Mathlib's
+`LinearMap.BilinForm.toDual` requires. Both separating directions follow from
+`B v v > 0` for `v ≠ 0` (no symmetry needed). -/
+theorem IsPosDef.nondegenerate {B : Form 𝕜 V} (hB : IsPosDef B) :
+    (B : LinearMap.BilinForm 𝕜 V).Nondegenerate := by
+  refine ⟨fun x hx => ?_, fun y hy => ?_⟩
+  · by_contra hne
+    exact ne_of_gt (inner_self_pos hB x hne) (hx x)
+  · by_contra hne
+    exact ne_of_gt (inner_self_pos hB y hne) (hy y)
+
 /-- **Injectivity of forward Riesz**: from positive-definiteness. -/
 theorem toDual_injective {B : Form 𝕜 V} (hB : IsPosDef B) :
     Function.Injective (toDual B) := by
@@ -70,33 +82,23 @@ theorem inner_eq_iff_eq {B : Form 𝕜 V} (hB : IsPosDef B) (v w : V) :
 
 variable [FiniteDimensional 𝕜 V]
 
-/-- **Bijectivity of forward Riesz**: injective + same finrank ⇒ bijective. -/
-theorem toDual_bijective {B : Form 𝕜 V} (hB : IsPosDef B) :
-    Function.Bijective (toDual B) := by
-  refine ⟨toDual_injective hB, ?_⟩
-  have h_finrank : Module.finrank 𝕜 (V →ₗ[𝕜] 𝕜) = Module.finrank 𝕜 V :=
-    Subspace.dual_finrank_eq
-  exact (LinearMap.injective_iff_surjective_of_finrank_eq_finrank
-    (f := toDual B) h_finrank.symm).mp (toDual_injective hB)
-
-/-- The Riesz isomorphism as a `LinearEquiv`. -/
+/-- The Riesz isomorphism as a `LinearEquiv`, delegating to Mathlib's
+`LinearMap.BilinForm.toDual` for the nondegenerate form `B`. -/
 noncomputable def toDualEquiv {B : Form 𝕜 V} (hB : IsPosDef B) :
     V ≃ₗ[𝕜] (V →ₗ[𝕜] 𝕜) :=
-  LinearEquiv.ofBijective (toDual B) (toDual_bijective hB)
+  LinearMap.BilinForm.toDual B hB.nondegenerate
 
 /-- **Inverse Riesz**: linear functional → vector via bilinear form. -/
 noncomputable def riesz {B : Form 𝕜 V} (hB : IsPosDef B)
     (φ : V →ₗ[𝕜] 𝕜) : V :=
   (toDualEquiv hB).symm φ
 
+omit [IsStrictOrderedRing 𝕜] in
 /-- **Riesz defining property**: `inner B (riesz hB φ) v = φ v`. -/
 theorem riesz_inner {B : Form 𝕜 V} (hB : IsPosDef B)
     (φ : V →ₗ[𝕜] 𝕜) (v : V) :
-    inner B (riesz hB φ) v = φ v := by
-  show toDual B (riesz hB φ) v = φ v
-  have heq : toDual B ((toDualEquiv hB).symm φ) = φ :=
-    (toDualEquiv hB).apply_symm_apply φ
-  exact congrArg (fun (f : V →ₗ[𝕜] 𝕜) => f v) heq
+    inner B (riesz hB φ) v = φ v :=
+  LinearMap.BilinForm.apply_toDual_symm_apply (hB := hB.nondegenerate) φ v
 
 /-- **Riesz uniqueness**: if `v` represents `φ`, then `v = riesz hB φ`. -/
 theorem riesz_unique {B : Form 𝕜 V} (hB : IsPosDef B) (v : V)
@@ -105,10 +107,7 @@ theorem riesz_unique {B : Form 𝕜 V} (hB : IsPosDef B) (v : V)
   apply toDual_injective hB
   ext w
   rw [toDual_apply, h w]
-  show φ w = toDual B (riesz hB φ) w
-  have heq : toDual B ((toDualEquiv hB).symm φ) = φ :=
-    (toDualEquiv hB).apply_symm_apply φ
-  exact congrArg (fun (f : V →ₗ[𝕜] 𝕜) => f w) heq.symm
+  exact (riesz_inner hB φ w).symm
 
 end Riesz
 

OpenGALib/Algebraic/Instances/RatVector.lean

@@ -1,15 +1,19 @@
 import OpenGALib.Algebraic.BilinearForm.Basic
+import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.Rat.Defs
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.LinearAlgebra.Matrix.DotProduct
+import Mathlib.Algebra.Order.Ring.Rat
+import Mathlib.Tactic.NormNum.Ineq
 
 /-!
 # Concrete instance: rational vectors
 
 A fully `#eval`-able `BilinearForm` on `Fin n → ℚ`. `#eval inner`
-produces a `Rat`; `native_decide` closes concrete equalities like
-`inner ![1,2,3] ![4,5,6] = 32`. The same operations on the abstract
+produces a `Rat`; concrete equalities like
+`inner ![1,2,3] ![4,5,6] = 32` are closed by kernel-checked
+`simp`/`norm_num` proofs. The same operations on the abstract
 `Form ℚ V` API give the same numerical results, demonstrating
 algebraic-core ↔ concrete-instance consistency.
 
@@ -78,24 +82,32 @@ open BilinearForm RatVector
 
 #eval inner (stdForm 3) ![1, 0, 0] ![1, 0, 0]    -- 1
 
-/-! ## `native_decide`-closed equalities — proof by execution
+/-! ## Kernel-checked equalities — proof by computation
 
-The same equations that `#eval` produces are closed as theorems via
-`native_decide`, which compiles the term to native code and uses the
-result as a proof. -/
+The same equations that `#eval` produces are closed as theorems by
+unfolding `inner` to the concrete sum (`stdForm_apply`,
+`Fin.sum_univ_two`/`Fin.sum_univ_three`) and discharging the rational
+arithmetic with `norm_num`. Each proof is checked by the kernel — no
+native code or compiler trust. -/
 
-example : inner (stdForm 3) ![1, 2, 3] ![4, 5, 6] = 32 := by native_decide
+example : inner (stdForm 3) ![1, 2, 3] ![4, 5, 6] = 32 := by
+  simp [stdForm_apply, Fin.sum_univ_three]; norm_num
 
-example : inner (stdForm 2) ![3, 4] ![3, 4] = 25 := by native_decide
+example : inner (stdForm 2) ![3, 4] ![3, 4] = 25 := by
+  simp [stdForm_apply, Fin.sum_univ_two]; norm_num
 
-example : inner (stdForm 3) ![1, 0, 0] ![0, 1, 0] = 0 := by native_decide
+example : inner (stdForm 3) ![1, 0, 0] ![0, 1, 0] = 0 := by
+  simp [stdForm_apply, Fin.sum_univ_three]
 
-example : inner (stdForm 3) ![1, 0, 0] ![1, 0, 0] = 1 := by native_decide
+example : inner (stdForm 3) ![1, 0, 0] ![1, 0, 0] = 1 := by
+  simp [stdForm_apply, Fin.sum_univ_three]
 
-/-- Cauchy–Schwarz on a concrete pair, verified by execution. -/
+/-- Cauchy–Schwarz on a concrete pair, kernel-checked. -/
 example :
     let v : Fin 3 → ℚ := ![1, 2, 3]
     let w : Fin 3 → ℚ := ![4, 5, 6]
     (inner (stdForm 3) v w) ^ 2
       ≤ inner (stdForm 3) v v * inner (stdForm 3) w w := by
-  native_decide
+  norm_num [inner_def, stdForm_apply, Fin.sum_univ_three,
+    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
+    Matrix.cons_val_two, Matrix.tail_cons]

OpenGALib/Manifold.lean

@@ -1,11 +1,32 @@
+import OpenGALib.Manifold.Charts.ChartedSpaceCore
 import OpenGALib.Manifold.Charts.CoordinateBall
 import OpenGALib.Manifold.Charts.PrecompactBasis
+import OpenGALib.Manifold.Covering.LiftedStructure
+import OpenGALib.Manifold.Covering.LocalSection
+import OpenGALib.Manifold.Covering.ProperLocalDiffeomorph
+import OpenGALib.Manifold.Covering.SmoothCoveringMap
+import OpenGALib.Manifold.Instances.Pi
+import OpenGALib.Manifold.Instances.RealProjectiveSpace
+import OpenGALib.Manifold.Map.LocalDiffeomorph
+import OpenGALib.Manifold.Map.TopologicalImmersionSubmersion
+import OpenGALib.Manifold.Submanifold.Embedded
+import OpenGALib.Manifold.Submanifold.SliceCharts
+import OpenGALib.Manifold.Submanifold.TangentSpace
+import OpenGALib.Manifold.Cutoff.Exhaustion
+import OpenGALib.Manifold.Tangent.CoordinateComponents
+import OpenGALib.Manifold.Tangent.CurveVelocity
+import OpenGALib.Manifold.Tangent.MFDeriv
 
 /-!
 # Manifold
 
 Manifold-foundations domain: chart-level and atlas-level structure on
 topological and smooth manifolds, stated directly on Mathlib's
 `ChartedSpace` / `IsManifold` API. Sits below `Riemannian` in the library
-layering. Currently provides coordinate-ball predicates for charts.
+layering. Provides coordinate-ball predicates for charts, the inverse
+function theorem with local-diffeomorphism characterizations for maps, the
+point-set immersion/submersion conditions underlying them, the smooth
+refinement of topological covering maps, immersed/embedded submanifold
+structures with their tangent spaces, and the canonical manifold instance on
+finite products.
 -/