bump to nightly-2023-04-26-02

mathlib commit leanprover-community/mathlib@d2d964c

Mathbin/ModelTheory/Types.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 
 ! This file was ported from Lean 3 source module model_theory.types
-! leanprover-community/mathlib commit a50170a88a47570ed186b809ca754110590f9476
+! leanprover-community/mathlib commit 98bd247d933fb581ff37244a5998bd33d81dd46d
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,10 +18,15 @@ This file defines the space of complete types over a first-order theory.
 ## Main Definitions
 * `first_order.language.Theory.complete_type`:
   `T.complete_type α` consists of complete types over the theory `T` with variables `α`.
+* `first_order.language.Theory.type_of` is the type of a given tuple.
+* `first_order.language.Theory.realized_types`: `T.realized_types M α` is the set of
+  types in `T.complete_type α` that are realized in `M` - that is, the type of some tuple in `M`.
 
 ## Main Results
 * `first_order.language.Theory.complete_type.nonempty_iff`:
   The space `T.complete_type α` is nonempty exactly when `T` is satisfiable.
+* `first_order.language.Theory.complete_type.exists_Model_is_realized_in`: Every type is realized in
+some model.
 
 ## Implementation Notes
 * Complete types are implemented as maximal consistent theories in an expanded language.
@@ -170,6 +175,57 @@ theorem toList_foldr_inf_mem {p : T.CompleteType α} {t : Finset L[[α]].Sentenc
 
 end CompleteType
 
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+variable {M : Type w'} [L.Structure M] [Nonempty M] [M ⊨ T] (T)
+
+/-- The set of all formulas true at a tuple in a structure forms a complete type. -/
+def typeOf (v : α → M) : T.CompleteType α :=
+  haveI : (constants_on α).Structure M := constants_on.Structure v
+  { toTheory := L[[α]].completeTheory M
+    subset' := model_iff_subset_complete_theory.1 ((Lhom.on_Theory_model _ T).2 inferInstance)
+    is_maximal' := complete_theory.is_maximal _ _ }
+#align first_order.language.Theory.type_of FirstOrder.Language.Theory.typeOf
+
+namespace CompleteType
+
+variable {T} {v : α → M}
+
+@[simp]
+theorem mem_typeOf {φ : L[[α]].Sentence} :
+    φ ∈ T.typeOf v ↔ (Formula.equivSentence.symm φ).realize v :=
+  letI : (constants_on α).Structure M := constants_on.Structure v
+  mem_complete_theory.trans (formula.realize_equiv_sentence_symm _ _ _).symm
+#align first_order.language.Theory.complete_type.mem_type_of FirstOrder.Language.Theory.CompleteType.mem_typeOf
+
+theorem formula_mem_typeOf {φ : L.Formula α} : Formula.equivSentence φ ∈ T.typeOf v ↔ φ.realize v :=
+  by simp
+#align first_order.language.Theory.complete_type.formula_mem_type_of FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf
+
+end CompleteType
+
+variable (M)
+
+/-- A complete type `p` is realized in a particular structure when there is some
+  tuple `v` whose type is `p`. -/
+@[simp]
+def realizedTypes (α : Type w) : Set (T.CompleteType α) :=
+  Set.range (T.typeOf : (α → M) → T.CompleteType α)
+#align first_order.language.Theory.realized_types FirstOrder.Language.Theory.realizedTypes
+
+theorem exists_modelCat_is_realized_in (p : T.CompleteType α) :
+    ∃ M : Theory.ModelCat.{u, v, max u v w} T, p ∈ T.realizedTypes M α :=
+  by
+  obtain ⟨M⟩ := p.is_maximal.1
+  refine' ⟨(M.subtheory_Model p.subset).reduct (L.Lhom_with_constants α), fun a => (L.con a : M), _⟩
+  refine' SetLike.ext fun φ => _
+  simp only [complete_type.mem_type_of]
+  refine'
+    (formula.realize_equiv_sentence_symm_con _ _).trans
+      (trans (trans _ (p.is_maximal.is_complete.realize_sentence_iff φ M))
+        (p.is_maximal.mem_iff_models φ).symm)
+  rfl
+#align first_order.language.Theory.exists_Model_is_realized_in FirstOrder.Language.Theory.exists_modelCat_is_realized_in
+
 end Theory
 
 end Language

Mathbin/Topology/VectorBundle/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri, Sebastien Gouezel, Heather Macbeth, Patrick Massot, Floris van Doorn
 
 ! This file was ported from Lean 3 source module topology.vector_bundle.basic
-! leanprover-community/mathlib commit 7dfe85833014fb54258a228081ebb76b7e96ec98
+! leanprover-community/mathlib commit d2d964c64f8ddcccd6704a731c41f95d13e72f5c
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -33,6 +33,21 @@ If these conditions are satisfied, we register the typeclass `vector_bundle R F
 
 We define constructions on vector bundles like pullbacks and direct sums in other files.
 
+## Main Definitions
+
+* `trivialization.is_linear`: a class stating that a trivialization is fiberwise linear on its base
+  set.
+* `trivialization.linear_equiv_at` and `trivialization.continuous_linear_map_at` are the
+  (continuous) linear fiberwise equivalences a trivialization induces.
+* They have forward maps `trivialization.linear_map_at` / `trivialization.continuous_linear_map_at`
+  and inverses `trivialization.symmₗ` / `trivialization.symmL`. Note that these are all defined
+  everywhere, since they are extended using the zero function.
+* `trivialization.coord_changeL` is the coordinate change induced by two trivializations. It only
+  makes sense on the intersection of their base sets, but is extended outside it using the identity.
+* Given a continuous (semi)linear map between `E x` and `E' y` where `E` and `E'` are bundles over
+  possibly different base sets, `continuous_linear_map.in_coordinates` turns this into a continuous
+  (semi)linear map between the chosen fibers of those bundles.
+
 ## Implementation notes
 
 The implementation choices in the vector bundle definition are discussed in the "Implementation
@@ -1036,5 +1051,74 @@ theorem to_vectorBundle :
 
 end VectorPrebundle
 
+namespace ContinuousLinearMap
+
+variable {𝕜₁ 𝕜₂ : Type _} [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂]
+
+variable {σ : 𝕜₁ →+* 𝕜₂}
+
+variable {B' : Type _} [TopologicalSpace B']
+
+variable [NormedSpace 𝕜₁ F] [∀ x, Module 𝕜₁ (E x)] [TopologicalSpace (TotalSpace E)]
+
+variable {F' : Type _} [NormedAddCommGroup F'] [NormedSpace 𝕜₂ F'] {E' : B' → Type _}
+  [∀ x, AddCommMonoid (E' x)] [∀ x, Module 𝕜₂ (E' x)] [TopologicalSpace (TotalSpace E')]
+
+variable [∀ x, TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜₁ F E]
+
+variable [∀ x, TopologicalSpace (E' x)] [FiberBundle F' E'] [VectorBundle 𝕜₂ F' E']
+
+variable (F E F' E')
+
+/-- When `ϕ` is a continuous (semi)linear map between the fibers `E x` and `E' y` of two vector
+bundles `E` and `E'`, `continuous_linear_map.in_coordinates F E F' E' x₀ x y₀ y ϕ` is a coordinate
+change of this continuous linear map w.r.t. the chart around `x₀` and the chart around `y₀`.
+
+It is defined by composing `ϕ` with appropriate coordinate changes given by the vector bundles
+`E` and `E'`.
+We use the operations `trivialization.continuous_linear_map_at` and `trivialization.symmL` in the
+definition, instead of `trivialization.continuous_linear_equiv_at`, so that
+`continuous_linear_map.in_coordinates` is defined everywhere (but see
+`continuous_linear_map.in_coordinates_eq`).
+
+This is the (second component of the) underlying function of a trivialization of the hom-bundle
+(see `hom_trivialization_at_apply`). However, note that `continuous_linear_map.in_coordinates` is
+defined even when `x` and `y` live in different base sets.
+Therefore, it is is also convenient when working with the hom-bundle between pulled back bundles.
+-/
+def inCoordinates (x₀ x : B) (y₀ y : B') (ϕ : E x →SL[σ] E' y) : F →SL[σ] F' :=
+  ((trivializationAt F' E' y₀).continuousLinearMapAt 𝕜₂ y).comp <|
+    ϕ.comp <| (trivializationAt F E x₀).symmL 𝕜₁ x
+#align continuous_linear_map.in_coordinates ContinuousLinearMap.inCoordinates
+
+variable {F F'}
+
+/-- rewrite `in_coordinates` using continuous linear equivalences. -/
+theorem inCoordinates_eq (x₀ x : B) (y₀ y : B') (ϕ : E x →SL[σ] E' y)
+    (hx : x ∈ (trivializationAt F E x₀).baseSet) (hy : y ∈ (trivializationAt F' E' y₀).baseSet) :
+    inCoordinates F E F' E' x₀ x y₀ y ϕ =
+      ((trivializationAt F' E' y₀).continuousLinearEquivAt 𝕜₂ y hy : E' y →L[𝕜₂] F').comp
+        (ϕ.comp <|
+          (((trivializationAt F E x₀).continuousLinearEquivAt 𝕜₁ x hx).symm : F →L[𝕜₁] E x)) :=
+  by
+  ext
+  simp_rw [in_coordinates, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
+    Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]
+#align continuous_linear_map.in_coordinates_eq ContinuousLinearMap.inCoordinates_eq
+
+/-- rewrite `in_coordinates` in a `vector_bundle_core`. -/
+protected theorem VectorBundleCore.inCoordinates_eq {ι ι'} (Z : VectorBundleCore 𝕜₁ B F ι)
+    (Z' : VectorBundleCore 𝕜₂ B' F' ι') {x₀ x : B} {y₀ y : B'} (ϕ : F →SL[σ] F')
+    (hx : x ∈ Z.baseSet (Z.indexAt x₀)) (hy : y ∈ Z'.baseSet (Z'.indexAt y₀)) :
+    inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
+      (Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp
+        (ϕ.comp <| Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x) :=
+  by
+  simp_rw [in_coordinates, Z'.trivialization_at_continuous_linear_map_at hy,
+    Z.trivialization_at_symmL hx]
+#align continuous_linear_map.vector_bundle_core.in_coordinates_eq ContinuousLinearMap.VectorBundleCore.inCoordinates_eq
+
+end ContinuousLinearMap
+
 end
 

Mathbin/Topology/VectorBundle/Hom.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, Floris van Doorn
 
 ! This file was ported from Lean 3 source module topology.vector_bundle.hom
-! leanprover-community/mathlib commit be2c24f56783935652cefffb4bfca7e4b25d167e
+! leanprover-community/mathlib commit d2d964c64f8ddcccd6704a731c41f95d13e72f5c
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -56,11 +56,11 @@ variable {B : Type _}
 
 variable (F₁ : Type _) (E₁ : B → Type _) [∀ x, AddCommMonoid (E₁ x)] [∀ x, Module 𝕜₁ (E₁ x)]
 
-variable [∀ x : B, TopologicalSpace (E₁ x)]
+variable [∀ x, TopologicalSpace (E₁ x)]
 
 variable (F₂ : Type _) (E₂ : B → Type _) [∀ x, AddCommMonoid (E₂ x)] [∀ x, Module 𝕜₂ (E₂ x)]
 
-variable [∀ x : B, TopologicalSpace (E₂ x)]
+variable [∀ x, TopologicalSpace (E₂ x)]
 
 include F₁ F₂
 
@@ -74,7 +74,7 @@ include F₁ F₂
 We intentionally add `F₁` and `F₂` as arguments to this type, so that instances on this type
 (that depend on `F₁` and `F₂`) actually refer to `F₁` and `F₂`. -/
 @[nolint unused_arguments]
-def Bundle.ContinuousLinearMap (x : B) : Type _ :=
+protected def Bundle.ContinuousLinearMap (x : B) : Type _ :=
   E₁ x →SL[σ] E₂ x deriving Inhabited
 #align bundle.continuous_linear_map Bundle.ContinuousLinearMap
 
@@ -125,9 +125,9 @@ def continuousLinearMapCoordChange [e₁.isLinear 𝕜₁] [e₁'.isLinear 𝕜
 
 variable {σ e₁ e₁' e₂ e₂'}
 
-variable [∀ x : B, TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁]
+variable [∀ x, TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁]
 
-variable [∀ x : B, TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂]
+variable [∀ x, TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂]
 
 theorem continuousOn_continuousLinearMapCoordChange [VectorBundle 𝕜₁ F₁ E₁] [VectorBundle 𝕜₂ F₂ E₂]
     [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂]
@@ -341,3 +341,28 @@ theorem Trivialization.continuousLinearMap_apply
   rfl
 #align trivialization.continuous_linear_map_apply Trivialization.continuousLinearMap_apply
 
+omit he₁ he₂
+
+theorem hom_trivializationAt_apply (x₀ : B)
+    (x : TotalSpace (Bundle.ContinuousLinearMap σ F₁ E₁ F₂ E₂)) :
+    trivializationAt (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ F₁ E₁ F₂ E₂) x₀ x =
+      ⟨x.1, inCoordinates F₁ E₁ F₂ E₂ x₀ x.1 x₀ x.1 x.2⟩ :=
+  rfl
+#align hom_trivialization_at_apply hom_trivializationAt_apply
+
+@[simp, mfld_simps]
+theorem hom_trivializationAt_source (x₀ : B) :
+    (trivializationAt (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ F₁ E₁ F₂ E₂) x₀).source =
+      π (Bundle.ContinuousLinearMap σ F₁ E₁ F₂ E₂) ⁻¹'
+        ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) :=
+  rfl
+#align hom_trivialization_at_source hom_trivializationAt_source
+
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+@[simp, mfld_simps]
+theorem hom_trivializationAt_target (x₀ : B) :
+    (trivializationAt (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ F₁ E₁ F₂ E₂) x₀).target =
+      ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) ×ˢ Set.univ :=
+  rfl
+#align hom_trivialization_at_target hom_trivializationAt_target
+

README.md

@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`2651125b48fc5c170ab1111afd0817c903b1fc6c`](https://github.com/leanprover-community/mathlib/commit/2651125b48fc5c170ab1111afd0817c903b1fc6c)
+Tracking mathlib commit: [`d2d964c64f8ddcccd6704a731c41f95d13e72f5c`](https://github.com/leanprover-community/mathlib/commit/d2d964c64f8ddcccd6704a731c41f95d13e72f5c)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

lake-manifest.json

@@ -4,9 +4,9 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "ad8d99d587d061f638285c1f088d90c5885afe3d",
+    "rev": "5e06e5a188b78a2e8777a5f6414a94cf7c9b4506",
     "name": "lean3port",
-    "inputRev?": "ad8d99d587d061f638285c1f088d90c5885afe3d"}},
+    "inputRev?": "5e06e5a188b78a2e8777a5f6414a94cf7c9b4506"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-04-26-00"
+def tag : String := "nightly-2023-04-26-02"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ad8d99d587d061f638285c1f088d90c5885afe3d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5e06e5a188b78a2e8777a5f6414a94cf7c9b4506"
 
 @[default_target]
 lean_lib Mathbin where

upstream-rev

@@ -1 +1 @@
-2651125b48fc5c170ab1111afd0817c903b1fc6c
+d2d964c64f8ddcccd6704a731c41f95d13e72f5c