The fibre product of two coproducts of open embeddings #
Step (ii) of the proof of [Kol07, Proposition 37] sets X'' := ∐_{i≤j} Uᵢ ∩ Uⱼ with the natural
maps τ₁, τ₂ : X'' → X' (Uᵢ ∩ Uⱼ → Uᵢ and Uᵢ ∩ Uⱼ → Uⱼ); the proof of [Kol07, Theorem 105]
uses X'' := X' ×_X X'. For two coproducts of open embeddings g₁ : N₁ → M (pieces Uᵢ) and
g₂ : N₂ → M (pieces Vⱼ, on which g₂ is injective), the fibre product is the disjoint union
over the pairs (i, j) of the open subsets Uᵢ ∩ g₁⁻¹(g₂ Vⱼ) of N₁: the first projection is
the inclusion, the second is (g₂|_{Vⱼ})⁻¹ ∘ g₁; the pair is a bijection onto
{(x, y) | g₁ x = g₂ y} because the pieces of each coproduct partition its source. A coproduct's
pieces are first normalised to a countable family of nonempty pieces (second countability), so
that the disjoint union is one of the manifolds of the library (sigmaManifold).
theorem
Manifold.IsCoprodOfOpenEmbeddings.exists_countable
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N : AnalyticManifold 𝕜 E}
{g : AnalyticMap N M}
(hg : IsCoprodOfOpenEmbeddings g)
:
The pieces of a coproduct of open embeddings can be taken countable and nonempty (second countability: a pairwise disjoint family of nonempty open sets is countable).
def
Manifold.fibrePieceSet
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(ij : σ₁ × σ₂)
:
Kollár's Uᵢ ∩ Uⱼ: the open piece Uᵢ ∩ g₁⁻¹(g₂ Vⱼ) of N₁.
Equations
Instances For
noncomputable def
Manifold.fibrePiece
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(ij : σ₁ × σ₂)
:
AnalyticManifold 𝕜 E
The piece as a manifold.
Equations
- Manifold.fibrePiece hg₂ hUo hVo ij = N₁.restrict (Manifold.fibrePieceSet hg₂ hUo hVo ij)
Instances For
noncomputable def
Manifold.fibreManifold
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
[Countable σ₁]
[Countable σ₂]
:
AnalyticManifold 𝕜 E
Kollár's X'' := ∐ Uᵢ ∩ Uⱼ: the disjoint union of the pieces.
Equations
- Manifold.fibreManifold hg₂ hUo hVo = Manifold.sigmaManifold (Manifold.fibrePiece hg₂ hUo hVo)
Instances For
def
Manifold.fibreFst
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
[Countable σ₁]
[Countable σ₂]
:
AnalyticMap (fibreManifold hg₂ hUo hVo) N₁
Kollár's τ₁: the first projection, the inclusion on each piece.
Equations
- Manifold.fibreFst hg₂ hUo hVo = ⟨fun (w : (Manifold.fibreManifold hg₂ hUo hVo).carrier) => (N₁.inclusion (Manifold.fibrePieceSet hg₂ hUo hVo w.fst)) w.snd, ⋯⟩
Instances For
theorem
Manifold.fibreFst_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
[Countable σ₁]
[Countable σ₂]
(w : (fibreManifold hg₂ hUo hVo).carrier)
:
noncomputable def
Manifold.pieceInv
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₂ : AnalyticManifold 𝕜 E}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₂ : Type u}
{V : σ₂ → Set N₂.carrier}
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(j : σ₂)
:
PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N₂.carrier M.carrier ⊤
The local inverse of g₂ on the piece Vⱼ.
Equations
- Manifold.pieceInv hg₂ hVo hVi hVne j = hg₂.restrictInjOn ⋯ ⋯
Instances For
theorem
Manifold.pieceInv_source
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₂ : AnalyticManifold 𝕜 E}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₂ : Type u}
{V : σ₂ → Set N₂.carrier}
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(j : σ₂)
:
theorem
Manifold.pieceInv_target
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₂ : AnalyticManifold 𝕜 E}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₂ : Type u}
{V : σ₂ → Set N₂.carrier}
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(j : σ₂)
:
theorem
Manifold.pieceInv_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₂ : AnalyticManifold 𝕜 E}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₂ : Type u}
{V : σ₂ → Set N₂.carrier}
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(j : σ₂)
(y : N₂.carrier)
:
noncomputable def
Manifold.fibreSndFun
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(ij : σ₁ × σ₂)
(x : (fibrePiece hg₂ hUo hVo ij).carrier)
:
N₂.carrier
Kollár's τ₂ on the piece Uᵢ ∩ g₁⁻¹(g₂ Vⱼ): (g₂|_{Vⱼ})⁻¹ ∘ g₁.
Equations
- Manifold.fibreSndFun hg₂ hUo hVo hVi hVne ij x = ↑(Manifold.pieceInv hg₂ hVo hVi hVne ij.2).symm.toPartialEquiv (g₁ ↑x)
Instances For
theorem
Manifold.contMDiff_fibreSndFun
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(ij : σ₁ × σ₂)
:
ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (fibreSndFun hg₂ hUo hVo hVi hVne ij)
theorem
Manifold.isLocalDiffeomorph_fibreSndFun
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
(hg₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₁)
(ij : σ₁ × σ₂)
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (fibreSndFun hg₂ hUo hVo hVi hVne ij)
noncomputable def
Manifold.fibreSnd
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
[Countable σ₁]
[Countable σ₂]
:
AnalyticMap (fibreManifold hg₂ hUo hVo) N₂
Kollár's τ₂: the second projection.
Equations
- Manifold.fibreSnd hg₂ hUo hVo hVi hVne = ⟨fun (w : (Manifold.fibreManifold hg₂ hUo hVo).carrier) => Manifold.fibreSndFun hg₂ hUo hVo hVi hVne w.fst w.snd, ⋯⟩
Instances For
theorem
Manifold.fibreSnd_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
[Countable σ₁]
[Countable σ₂]
(w : (fibreManifold hg₂ hUo hVo).carrier)
:
theorem
Manifold.isFibreProduct_fibre
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
{g₁ : AnalyticMap N₁ M}
{g₂ : AnalyticMap N₂ M}
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
{σ₁ σ₂ : Type u}
{U : σ₁ → Set N₁.carrier}
{V : σ₂ → Set N₂.carrier}
(hUo : ∀ (i : σ₁), IsOpen (U i))
(hVo : ∀ (j : σ₂), IsOpen (V j))
(hVi : ∀ (j : σ₂), Set.InjOn (⇑g₂) (V j))
(hVne : ∀ (j : σ₂), (V j).Nonempty)
[Countable σ₁]
[Countable σ₂]
(hg₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₁)
(hUd : Pairwise (Function.onFun Disjoint U))
(hUcov : ⋃ (i : σ₁), U i = Set.univ)
(hVd : Pairwise (Function.onFun Disjoint V))
(hVcov : ⋃ (j : σ₂), V j = Set.univ)
:
IsFibreProduct g₁ g₂ (fibreFst hg₂ hUo hVo) (fibreSnd hg₂ hUo hVo hVi hVne)
[Kol07, Proposition 37] (ii) / Theorem 105: (∐ Uᵢ ∩ g₁⁻¹(g₂ Vⱼ), τ₁, τ₂) is a
fibre product of g₁ and g₂.
theorem
Manifold.exists_isFibreProduct
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
(g₁ : AnalyticMap N₁ M)
(g₂ : AnalyticMap N₂ M)
(h₁ : IsCoprodOfOpenEmbeddings g₁)
(h₂ : IsCoprodOfOpenEmbeddings g₂)
:
∃ (P : AnalyticManifold 𝕜 E) (p₁ : AnalyticMap P N₁) (p₂ : AnalyticMap P N₂), IsFibreProduct g₁ g₂ p₁ p₂
Two coproducts of open embeddings into M have a fibre product.
theorem
Manifold.exists_isFibreProduct_of_isLocalDiffeomorph
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N₁ N₂ : AnalyticManifold 𝕜 E}
(g₁ : AnalyticMap N₁ M)
(g₂ : AnalyticMap N₂ M)
(hg₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₁)
(h₂ : IsCoprodOfOpenEmbeddings g₂)
:
∃ (P : AnalyticManifold 𝕜 E) (p₁ : AnalyticMap P N₁) (p₂ : AnalyticMap P N₂), IsFibreProduct g₁ g₂ p₁ p₂
The fibre product exists as soon as one factor is a coproduct of open embeddings (the other any
local analytic isomorphism): the instance of isFibreProduct_fibre with the one piece N₁.