Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright Β© 2021 NicolΓ² Cavalleri. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: NicolΓ² Cavalleri

! This file was ported from Lean 3 source module data.bundle
! leanprover-community/mathlib commit 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Module.Basic

/-!
# Bundle
Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file
should contain all possible results that do not involve any topology.

We represent a bundle `E` over a base space `B` as a dependent type `E : B β†’ Type _`.

We provide a type synonym of `Ξ£ x, E x` as `Bundle.TotalSpace E`, to be able to endow it with
a topology which is not the disjoint union topology `Sigma.TopologicalSpace`. In general, the
constructions of fiber bundles we will make will be of this form.

## Main Definitions

* `Bundle.TotalSpace` the total space of a bundle.
* `Bundle.TotalSpace.proj` the projection from the total space to the base space.
* `Bundle.totalSpaceMk` the constructor for the total space.

## References
- https://en.wikipedia.org/wiki/Bundle_(mathematics)
-/


namespace Bundle

variable {
B: Type ?u.6034
B : 
Type _: Type (?u.10+1)
Type _} (
E: B β†’ Type ?u.6039
E : 
B: Type ?u.14817
B β†’ 
Type _: Type (?u.6039+1)
Type _)

/-- `Bundle.TotalSpace E` is the total space of the bundle `Ξ£ x, E x`.
This type synonym is used to avoid conflicts with general sigma types.
-/
def 
TotalSpace: ?m.18
TotalSpace :=
  Ξ£
x: ?m.24
x, 
E: B β†’ Type ?u.15
E 
x: ?m.24
x
#align bundle.total_space 
Bundle.TotalSpace: {B : Type u_1} β†’ (B β†’ Type u_2) β†’ Type (maxu_1u_2)
Bundle.TotalSpace


instance: {B : Type u_1} β†’ (E : B β†’ Type u_2) β†’ [inst : Inhabited B] β†’ [inst : Inhabited (E default)] β†’ Inhabited (TotalSpace E)
instance [
Inhabited: Sort ?u.45 β†’ Sort (max1?u.45)
Inhabited 
B: Type ?u.37
B] [
Inhabited: Sort ?u.48 β†’ Sort (max1?u.48)
Inhabited (
E: B β†’ Type ?u.42
E 
default: {Ξ± : Sort ?u.49} β†’ [self : Inhabited Ξ±] β†’ Ξ±
default)] : 
Inhabited: Sort ?u.204 β†’ Sort (max1?u.204)
Inhabited (
TotalSpace: {B : Type ?u.206} β†’ (B β†’ Type ?u.205) β†’ Type (max?u.206?u.205)
TotalSpace 
E: B β†’ Type ?u.42
E) :=
  ⟨⟨
default: {Ξ± : Sort ?u.232} β†’ [self : Inhabited Ξ±] β†’ Ξ±
default, 
default: {Ξ± : Sort ?u.383} β†’ [self : Inhabited Ξ±] β†’ Ξ±
default⟩⟩

variable {
E: ?m.622
E}

/-- `bundle.TotalSpace.proj` is the canonical projection `Bundle.TotalSpace E β†’ B` from the
total space to the base space. -/
@[simp, reducible]
def 
TotalSpace.proj: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ TotalSpace E β†’ B
TotalSpace.proj : 
TotalSpace: {B : Type ?u.635} β†’ (B β†’ Type ?u.634) β†’ Type (max?u.635?u.634)
TotalSpace 
E: B β†’ Type ?u.630
E β†’ 
B: Type ?u.625
B :=
  
Sigma.fst: {Ξ± : Type ?u.643} β†’ {Ξ² : Ξ± β†’ Type ?u.642} β†’ Sigma Ξ² β†’ Ξ±
Sigma.fst
#align bundle.total_space.proj 
Bundle.TotalSpace.proj: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ TotalSpace E β†’ B
Bundle.TotalSpace.proj

-- this notation won't be used in the pretty-printer
set_option quotPrecheck false in
/-- The canonical projection defining a bundle. -/
scoped notation "Ο€" 
E: ?m.846
E => @Bundle.TotalSpace.proj _ 
E: ?m.846
E

/-- Constructor for the total space of a bundle. -/
@[simp, reducible]
def 
totalSpaceMk: (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk (
b: B
b : 
B: Type ?u.3016
B) (
a: E b
a : 
E: B β†’ Type ?u.3021
E 
b: B
b) : 
Bundle.TotalSpace: {B : Type ?u.3029} β†’ (B β†’ Type ?u.3028) β†’ Type (max?u.3029?u.3028)
Bundle.TotalSpace 
E: B β†’ Type ?u.3021
E :=
  ⟨
b: B
b, 
a: E b
a⟩
#align bundle.total_space_mk 
Bundle.totalSpaceMk: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ (b : B) β†’ E b β†’ TotalSpace E
Bundle.totalSpaceMk

theorem 
TotalSpace.proj_mk: βˆ€ {x : B} {y : E x}, proj (totalSpaceMk x y) = x
TotalSpace.proj_mk {
x: B
x : 
B: Type ?u.3120
B} {
y: E x
y : 
E: B β†’ Type ?u.3125
E 
x: B
x} : (
totalSpaceMk: {B : Type ?u.3134} β†’ {E : B β†’ Type ?u.3133} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
x: B
x 
y: E x
y).
proj: {B : Type ?u.3139} β†’ {E : B β†’ Type ?u.3138} β†’ TotalSpace E β†’ B
proj = 
x: B
x :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3153} {a : Ξ±}, a = a
rfl
#align bundle.total_space.proj_mk 
Bundle.TotalSpace.proj_mk: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} {x : B} {y : E x}, TotalSpace.proj (totalSpaceMk x y) = x
Bundle.TotalSpace.proj_mk

theorem 
sigma_mk_eq_totalSpaceMk: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} {x : B} {y : E x}, { fst := x, snd := y } = totalSpaceMk x y
sigma_mk_eq_totalSpaceMk {
x: B
x : 
B: Type ?u.3165
B} {
y: E x
y : 
E: B β†’ Type ?u.3170
E 
x: B
x} : 
Sigma.mk: {Ξ± : Type ?u.3179} β†’ {Ξ² : Ξ± β†’ Type ?u.3178} β†’ (fst : Ξ±) β†’ Ξ² fst β†’ Sigma Ξ²
Sigma.mk 
x: B
x 
y: E x
y = 
totalSpaceMk: {B : Type ?u.3184} β†’ {E : B β†’ Type ?u.3183} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
x: B
x 
y: E x
y :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3195} {a : Ξ±}, a = a
rfl
#align bundle.sigma_mk_eq_total_space_mk 
Bundle.sigma_mk_eq_totalSpaceMk: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} {x : B} {y : E x}, { fst := x, snd := y } = totalSpaceMk x y
Bundle.sigma_mk_eq_totalSpaceMk

theorem 
TotalSpace.mk_cast: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} {x x' : B} (h : x = x') (b : E x),
  totalSpaceMk x' (cast (_ : E x = E x') b) = totalSpaceMk x b
TotalSpace.mk_cast {
x: B
x 
x': B
x' : 
B: Type ?u.3212
B} (
h: x = x'
h : 
x: B
x = 
x': B
x') (
b: E x
b : 
E: B β†’ Type ?u.3217
E 
x: B
x) :
    
totalSpaceMk: {B : Type ?u.3232} β†’ {E : B β†’ Type ?u.3231} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
x': B
x' (
cast: {Ξ± Ξ² : Sort ?u.3235} β†’ Ξ± = Ξ² β†’ Ξ± β†’ Ξ²
cast (
congr_arg: βˆ€ {Ξ± : Sort ?u.3239} {Ξ² : Sort ?u.3238} {a₁ aβ‚‚ : Ξ±} (f : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ f a₁ = f aβ‚‚
congr_arg 
E: B β†’ Type ?u.3217
E 
h: x = x'
h) 
b: E x
b) = 
totalSpaceMk: {B : Type ?u.3258} β†’ {E : B β†’ Type ?u.3257} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
x: B
x 
b: E x
b := 
Goals accomplished! πŸ™
B: Type u_1

E: B β†’ Type u_2

x, x': B

h: x = x'

b: E x

totalSpaceMk x' (cast (_ : E x = E x') b) = totalSpaceMk x b
B: Type u_1

E: B β†’ Type u_2

x: B

b: E x

totalSpaceMk x (cast (_ : E x = E x) b) = totalSpaceMk x b
B: Type u_1

E: B β†’ Type u_2

x, x': B

h: x = x'

b: E x

totalSpaceMk x' (cast (_ : E x = E x') b) = totalSpaceMk x b
Goals accomplished! πŸ™

#align bundle.total_space.mk_cast 
Bundle.TotalSpace.mk_cast: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} {x x' : B} (h : x = x') (b : E x),
  totalSpaceMk x' (cast (_ : E x = E x') b) = totalSpaceMk x b
Bundle.TotalSpace.mk_cast

theorem 
TotalSpace.eta: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} (z : TotalSpace E), totalSpaceMk (proj z) z.snd = z
TotalSpace.eta (
z: TotalSpace E
z : 
TotalSpace: {B : Type ?u.3311} β†’ (B β†’ Type ?u.3310) β†’ Type (max?u.3311?u.3310)
TotalSpace 
E: B β†’ Type ?u.3307
E) : 
totalSpaceMk: {B : Type ?u.3320} β†’ {E : B β†’ Type ?u.3319} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
z: TotalSpace E
z.
proj: {B : Type ?u.3324} β†’ {E : B β†’ Type ?u.3323} β†’ TotalSpace E β†’ B
proj 
z: TotalSpace E
z.
2: {Ξ± : Type ?u.3335} β†’ {Ξ² : Ξ± β†’ Type ?u.3334} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
2 = 
z: TotalSpace E
z :=
  
Sigma.eta: βˆ€ {Ξ± : Type ?u.3348} {Ξ² : Ξ± β†’ Type ?u.3349} (x : (a : Ξ±) Γ— Ξ² a), { fst := x.fst, snd := x.snd } = x
Sigma.eta 
z: TotalSpace E
z
#align bundle.total_space.eta 
Bundle.TotalSpace.eta: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} (z : TotalSpace E), totalSpaceMk (TotalSpace.proj z) z.snd = z
Bundle.TotalSpace.eta


instance: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ {x : B} β†’ CoeTC (E x) (TotalSpace E)
instance {
x: B
x : 
B: Type ?u.3372
B} : 
CoeTC: Sort ?u.3383 β†’ Sort ?u.3382 β†’ Sort (max(max1?u.3383)?u.3382)
CoeTC (
E: B β†’ Type ?u.3377
E 
x: B
x) (
TotalSpace: {B : Type ?u.3385} β†’ (B β†’ Type ?u.3384) β†’ Type (max?u.3385?u.3384)
TotalSpace 
E: B β†’ Type ?u.3377
E) :=
  ⟨
totalSpaceMk: {B : Type ?u.3402} β†’ {E : B β†’ Type ?u.3401} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
x: B
x⟩

-- porting note: removed simp attribute, variable as head symbol
theorem 
coe_fst: βˆ€ (x : B) (v : E x), (totalSpaceMk x v).fst = x
coe_fst (
x: B
x : 
B: Type ?u.3501
B) (
v: E x
v : 
E: B β†’ Type ?u.3506
E 
x: B
x) : (
v: E x
v : 
TotalSpace: {B : Type ?u.3516} β†’ (B β†’ Type ?u.3515) β†’ Type (max?u.3516?u.3515)
TotalSpace 
E: B β†’ Type ?u.3506
E).
fst: {Ξ± : Type ?u.3609} β†’ {Ξ² : Ξ± β†’ Type ?u.3608} β†’ Sigma Ξ² β†’ Ξ±
fst = 
x: B
x :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3621} {a : Ξ±}, a = a
rfl
#align bundle.coe_fst 
Bundle.coe_fst: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} (x : B) (v : E x), (totalSpaceMk x v).fst = x
Bundle.coe_fst

-- porting note: removed simp attribute, variable as head symbol
theorem 
coe_snd: βˆ€ {x : B} {y : E x}, (totalSpaceMk x y).snd = y
coe_snd {
x: B
x : 
B: Type ?u.3634
B} {
y: E x
y : 
E: B β†’ Type ?u.3639
E 
x: B
x} : (
y: E x
y : 
TotalSpace: {B : Type ?u.3649} β†’ (B β†’ Type ?u.3648) β†’ Type (max?u.3649?u.3648)
TotalSpace 
E: B β†’ Type ?u.3639
E).
snd: {Ξ± : Type ?u.3742} β†’ {Ξ² : Ξ± β†’ Type ?u.3741} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
snd = 
y: E x
y :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3755} {a : Ξ±}, a = a
rfl
#align bundle.coe_snd 
Bundle.coe_snd: βˆ€ {B : Type u_2} {E : B β†’ Type u_1} {x : B} {y : E x}, (totalSpaceMk x y).snd = y
Bundle.coe_snd

-- porting note: removed `to_total_space_coe`, syntactic tautology
#noalign bundle.to_total_space_coe

-- mathport name: Β«expr ×ᡇ Β»
/-- The direct sum of two bundles. -/
notation:100 -- notation for the direct sum of two bundles over the same base

E₁: ?m.3894
E₁ " ×ᡇ " 
Eβ‚‚: ?m.3885
Eβ‚‚ => fun x => 
E₁: ?m.3894
E₁ x Γ— 
Eβ‚‚: ?m.3885
Eβ‚‚ x

/-- `Bundle.Trivial B F` is the trivial bundle over `B` of fiber `F`. -/
def 
Trivial: (B : Type ?u.6007) β†’ Type ?u.6010 β†’ B β†’ Type ?u.6015
Trivial (
B: Type ?u.6007
B : 
Type _: Type (?u.6007+1)
Type _) (
F: Type ?u.6010
F : 
Type _: Type (?u.6010+1)
Type _) : 
B: Type ?u.6007
B β†’ 
Type _: Type (?u.6015+1)
Type _ :=
  
Function.const: {Ξ± : Sort ?u.6020} β†’ (Ξ² : Sort ?u.6019) β†’ Ξ± β†’ Ξ² β†’ Ξ±
Function.const 
B: Type ?u.6007
B 
F: Type ?u.6010
F
#align bundle.trivial 
Bundle.Trivial: (B : Type u_1) β†’ Type u_2 β†’ B β†’ Type u_2
Bundle.Trivial


instance: {B : Type u_1} β†’ {F : Type u_2} β†’ [inst : Inhabited F] β†’ {b : B} β†’ Inhabited (Trivial B F b)
instance {
F: Type ?u.6042
F : 
Type _: Type (?u.6042+1)
Type _} [
Inhabited: Sort ?u.6045 β†’ Sort (max1?u.6045)
Inhabited 
F: Type ?u.6042
F] {
b: B
b : 
B: Type ?u.6034
B} : 
Inhabited: Sort ?u.6050 β†’ Sort (max1?u.6050)
Inhabited (
Bundle.Trivial: (B : Type ?u.6052) β†’ Type ?u.6051 β†’ B β†’ Type ?u.6051
Bundle.Trivial 
B: Type ?u.6034
B 
F: Type ?u.6042
F 
b: B
b) :=
  ⟨(
default: {Ξ± : Sort ?u.6063} β†’ [self : Inhabited Ξ±] β†’ Ξ±
default : 
F: Type ?u.6042
F)⟩

/-- The trivial bundle, unlike other bundles, has a canonical projection on the fiber. -/
def 
Trivial.projSnd: (B : Type u_1) β†’ (F : Type u_2) β†’ TotalSpace (Trivial B F) β†’ F
Trivial.projSnd (
B: Type ?u.6278
B : 
Type _: Type (?u.6278+1)
Type _) (
F: Type ?u.6281
F : 
Type _: Type (?u.6281+1)
Type _) : 
TotalSpace: {B : Type ?u.6286} β†’ (B β†’ Type ?u.6285) β†’ Type (max?u.6286?u.6285)
TotalSpace (
Bundle.Trivial: (B : Type ?u.6289) β†’ Type ?u.6288 β†’ B β†’ Type ?u.6288
Bundle.Trivial 
B: Type ?u.6278
B 
F: Type ?u.6281
F) β†’ 
F: Type ?u.6281
F :=
  
Sigma.snd: {Ξ± : Type ?u.6300} β†’ {Ξ² : Ξ± β†’ Type ?u.6299} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
Sigma.snd
#align bundle.trivial.proj_snd 
Bundle.Trivial.projSnd: (B : Type u_1) β†’ (F : Type u_2) β†’ TotalSpace (Trivial B F) β†’ F
Bundle.Trivial.projSnd

section Pullback

variable {
B': Type ?u.6457
B' : 
Type _: Type (?u.6510+1)
Type _}

/-- The pullback of a bundle `E` over a base `B` under a map `f : B' β†’ B`, denoted by `Pullback f E`
or `f *α΅– E`,  is the bundle over `B'` whose fiber over `b'` is `E (f b')`. -/
-- porting note: `has_nonempty_instance` linter not found
--  @[nolint has_nonempty_instance]
def 
Pullback: (f : B' β†’ B) β†’ (E : B β†’ Type ?u.6401) β†’ ?m.6405 f E
Pullback (
f: B' β†’ B
f : 
B': Type ?u.6392
B' β†’ 
B: Type ?u.6384
B) (
E: B β†’ Type ?u.6401
E : 
B: Type ?u.6384
B β†’ 
Type _: Type (?u.6401+1)
Type _) := fun 
x: ?m.6410
x => 
E: B β†’ Type ?u.6401
E (
f: B' β†’ B
f 
x: ?m.6410
x)
#align bundle.pullback 
Bundle.Pullback: {B : Type u_1} β†’ {B' : Type u_2} β†’ (B' β†’ B) β†’ (B β†’ Type u_3) β†’ B' β†’ Type u_3
Bundle.Pullback

-- mathport name: Β«expr *α΅– Β»
@[inherit_doc]
notation 
f: ?m.8526
f " *α΅– " 
E: ?m.8517
E => 
Pullback: {B : Type u_1} β†’ {B' : Type u_2} β†’ (B' β†’ B) β†’ (B β†’ Type u_3) β†’ B' β†’ Type u_3
Pullback 
f: ?m.8526
f 
E: ?m.8517
E

/-- Natural embedding of the total space of `f *α΅– E` into `B' Γ— TotalSpace E`. -/
@[simp]
def 
pullbackTotalSpaceEmbedding: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ {B' : Type u_3} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ B' Γ— TotalSpace E
pullbackTotalSpaceEmbedding (
f: B' β†’ B
f : 
B': Type ?u.14282
B' β†’ 
B: Type ?u.14274
B) : 
TotalSpace: {B : Type ?u.14291} β†’ (B β†’ Type ?u.14290) β†’ Type (max?u.14291?u.14290)
TotalSpace (
f: B' β†’ B
f *α΅– 
E: B β†’ Type ?u.14279
E) β†’ 
B': Type ?u.14282
B' Γ— 
TotalSpace: {B : Type ?u.14313} β†’ (B β†’ Type ?u.14312) β†’ Type (max?u.14313?u.14312)
TotalSpace 
E: B β†’ Type ?u.14279
E := fun 
z: ?m.14321
z =>
  (
z: ?m.14321
z.
proj: {B : Type ?u.14330} β†’ {E : B β†’ Type ?u.14329} β†’ TotalSpace E β†’ B
proj, 
totalSpaceMk: {B : Type ?u.14341} β†’ {E : B β†’ Type ?u.14340} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk (
f: B' β†’ B
f 
z: ?m.14321
z.
proj: {B : Type ?u.14349} β†’ {E : B β†’ Type ?u.14348} β†’ TotalSpace E β†’ B
proj) 
z: ?m.14321
z.
2: {Ξ± : Type ?u.14357} β†’ {Ξ² : Ξ± β†’ Type ?u.14356} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
2)
#align bundle.pullback_total_space_embedding 
Bundle.pullbackTotalSpaceEmbedding: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ {B' : Type u_3} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ B' Γ— TotalSpace E
Bundle.pullbackTotalSpaceEmbedding

/-- The base map `f : B' β†’ B` lifts to a canonical map on the total spaces. -/
def 
Pullback.lift: (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ TotalSpace E
Pullback.lift (
f: B' β†’ B
f : 
B': Type ?u.14518
B' β†’ 
B: Type ?u.14510
B) : 
TotalSpace: {B : Type ?u.14527} β†’ (B β†’ Type ?u.14526) β†’ Type (max?u.14527?u.14526)
TotalSpace (
f: B' β†’ B
f *α΅– 
E: B β†’ Type ?u.14515
E) β†’ 
TotalSpace: {B : Type ?u.14547} β†’ (B β†’ Type ?u.14546) β†’ Type (max?u.14547?u.14546)
TotalSpace 
E: B β†’ Type ?u.14515
E := fun 
z: ?m.14557
z =>
  
totalSpaceMk: {B : Type ?u.14560} β†’ {E : B β†’ Type ?u.14559} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk (
f: B' β†’ B
f 
z: ?m.14557
z.
proj: {B : Type ?u.14568} β†’ {E : B β†’ Type ?u.14567} β†’ TotalSpace E β†’ B
proj) 
z: ?m.14557
z.
2: {Ξ± : Type ?u.14579} β†’ {Ξ² : Ξ± β†’ Type ?u.14578} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
2
#align bundle.pullback.lift 
Bundle.Pullback.lift: {B : Type u_1} β†’ {E : B β†’ Type u_2} β†’ {B' : Type u_3} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ TotalSpace E
Bundle.Pullback.lift

@[simp]
theorem 
Pullback.proj_lift: βˆ€ (f : B' β†’ B) (x : TotalSpace (f *α΅– E)), TotalSpace.proj (lift f x) = f x.fst
Pullback.proj_lift (
f: B' β†’ B
f : 
B': Type ?u.14710
B' β†’ 
B: Type ?u.14702
B) (
x: TotalSpace (f *α΅– E)
x : 
TotalSpace: {B : Type ?u.14718} β†’ (B β†’ Type ?u.14717) β†’ Type (max?u.14718?u.14717)
TotalSpace (
f: B' β†’ B
f *α΅– 
E: B β†’ Type ?u.14707
E)) :
    (
Pullback.lift: {B : Type ?u.14741} β†’ {E : B β†’ Type ?u.14740} β†’ {B' : Type ?u.14739} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ TotalSpace E
Pullback.lift 
f: B' β†’ B
f 
x: TotalSpace (f *α΅– E)
x).
proj: {B : Type ?u.14762} β†’ {E : B β†’ Type ?u.14761} β†’ TotalSpace E β†’ B
proj = 
f: B' β†’ B
f 
x: TotalSpace (f *α΅– E)
x.
1: {Ξ± : Type ?u.14773} β†’ {Ξ² : Ξ± β†’ Type ?u.14772} β†’ Sigma Ξ² β†’ Ξ±
1 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.14785} {a : Ξ±}, a = a
rfl
#align bundle.pullback.proj_lift 
Bundle.Pullback.proj_lift: βˆ€ {B : Type u_3} {E : B β†’ Type u_2} {B' : Type u_1} (f : B' β†’ B) (x : TotalSpace (f *α΅– E)),
  TotalSpace.proj (Pullback.lift f x) = f x.fst
Bundle.Pullback.proj_lift

@[simp]
theorem 
Pullback.lift_mk: βˆ€ (f : B' β†’ B) (x : B') (y : E (f x)), lift f (totalSpaceMk x y) = totalSpaceMk (f x) y
Pullback.lift_mk (
f: B' β†’ B
f : 
B': Type ?u.14825
B' β†’ 
B: Type ?u.14817
B) (
x: B'
x : 
B': Type ?u.14825
B') (
y: E (f x)
y : 
E: B β†’ Type ?u.14822
E (
f: B' β†’ B
f 
x: B'
x)) :
    
Pullback.lift: {B : Type ?u.14839} β†’ {E : B β†’ Type ?u.14838} β†’ {B' : Type ?u.14837} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ TotalSpace E
Pullback.lift 
f: B' β†’ B
f (
totalSpaceMk: {B : Type ?u.14847} β†’ {E : B β†’ Type ?u.14846} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk 
x: B'
x 
y: E (f x)
y) = 
totalSpaceMk: {B : Type ?u.14859} β†’ {E : B β†’ Type ?u.14858} β†’ (b : B) β†’ E b β†’ TotalSpace E
totalSpaceMk (
f: B' β†’ B
f 
x: B'
x) 
y: E (f x)
y :=
  
rfl: βˆ€ {Ξ± : Sort ?u.14871} {a : Ξ±}, a = a
rfl
#align bundle.pullback.lift_mk 
Bundle.Pullback.lift_mk: βˆ€ {B : Type u_1} {E : B β†’ Type u_2} {B' : Type u_3} (f : B' β†’ B) (x : B') (y : E (f x)),
  Pullback.lift f (totalSpaceMk x y) = totalSpaceMk (f x) y
Bundle.Pullback.lift_mk

theorem 
pullbackTotalSpaceEmbedding_snd: βˆ€ (f : B' β†’ B) (x : TotalSpace (f *α΅– E)), (pullbackTotalSpaceEmbedding f x).snd = Pullback.lift f x
pullbackTotalSpaceEmbedding_snd (
f: B' β†’ B
f : 
B': Type ?u.14924
B' β†’ 
B: Type ?u.14916
B) (
x: TotalSpace (f *α΅– E)
x : 
TotalSpace: {B : Type ?u.14932} β†’ (B β†’ Type ?u.14931) β†’ Type (max?u.14932?u.14931)
TotalSpace (
f: B' β†’ B
f *α΅– 
E: B β†’ Type ?u.14921
E)) :
    (
pullbackTotalSpaceEmbedding: {B : Type ?u.14955} β†’
  {E : B β†’ Type ?u.14954} β†’ {B' : Type ?u.14953} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ B' Γ— TotalSpace E
pullbackTotalSpaceEmbedding 
f: B' β†’ B
f 
x: TotalSpace (f *α΅– E)
x).
2: {Ξ± : Type ?u.14976} β†’ {Ξ² : Type ?u.14975} β†’ Ξ± Γ— Ξ² β†’ Ξ²
2 = 
Pullback.lift: {B : Type ?u.14983} β†’ {E : B β†’ Type ?u.14982} β†’ {B' : Type ?u.14981} β†’ (f : B' β†’ B) β†’ TotalSpace (f *α΅– E) β†’ TotalSpace E
Pullback.lift 
f: B' β†’ B
f 
x: TotalSpace (f *α΅– E)
x :=
  
rfl: βˆ€ {Ξ± : Sort ?u.15007} {a : Ξ±}, a = a
rfl
#align bundle.pullback_total_space_embedding_snd 
Bundle.pullbackTotalSpaceEmbedding_snd: βˆ€ {B : Type u_3} {E : B β†’ Type u_2} {B' : Type u_1} (f : B' β†’ B) (x : TotalSpace (f *α΅– E)),
  (pullbackTotalSpaceEmbedding f x).snd = Pullback.lift f x
Bundle.pullbackTotalSpaceEmbedding_snd

end Pullback

section FiberStructures

variable [βˆ€ 
x: ?m.15033
x, 
AddCommMonoid: Type ?u.16918 β†’ Type ?u.16918
AddCommMonoid (
E: B β†’ Type ?u.15029
E 
x: ?m.15033
x)]

@[simp]
theorem 
coe_snd_map_apply: βˆ€ {B : Type u_2} {E : B β†’ Type u_1} [inst : (x : B) β†’ AddCommMonoid (E x)] (x : B) (v w : E x),
  (totalSpaceMk x (v + w)).snd = (totalSpaceMk x v).snd + (totalSpaceMk x w).snd
coe_snd_map_apply (
x: B
x : 
B: Type ?u.15040
B) (
v: E x
v 
w: E x
w : 
E: B β†’ Type ?u.15045
E 
x: B
x) :
    (↑(
v: E x
v + 
w: E x
w) : 
TotalSpace: {B : Type ?u.15065} β†’ (B β†’ Type ?u.15064) β†’ Type (max?u.15065?u.15064)
TotalSpace 
E: B β†’ Type ?u.15045
E).
snd: {Ξ± : Type ?u.15984} β†’ {Ξ² : Ξ± β†’ Type ?u.15983} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
snd = (
v: E x
v : 
TotalSpace: {B : Type ?u.15997} β†’ (B β†’ Type ?u.15996) β†’ Type (max?u.15997?u.15996)
TotalSpace 
E: B β†’ Type ?u.15045
E).
snd: {Ξ± : Type ?u.16063} β†’ {Ξ² : Ξ± β†’ Type ?u.16062} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
snd + (
w: E x
w : 
TotalSpace: {B : Type ?u.16070} β†’ (B β†’ Type ?u.16069) β†’ Type (max?u.16070?u.16069)
TotalSpace 
E: B β†’ Type ?u.15045
E).
snd: {Ξ± : Type ?u.16136} β†’ {Ξ² : Ξ± β†’ Type ?u.16135} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
snd :=
  
rfl: βˆ€ {Ξ± : Sort ?u.16862} {a : Ξ±}, a = a
rfl
#align bundle.coe_snd_map_apply 
Bundle.coe_snd_map_apply: βˆ€ {B : Type u_2} {E : B β†’ Type u_1} [inst : (x : B) β†’ AddCommMonoid (E x)] (x : B) (v w : E x),
  (totalSpaceMk x (v + w)).snd = (totalSpaceMk x v).snd + (totalSpaceMk x w).snd
Bundle.coe_snd_map_apply

variable (
R: Type ?u.16922
R : 
Type _: Type (?u.16922+1)
Type _) [
Semiring: Type ?u.16981 β†’ Type ?u.16981
Semiring 
R: Type ?u.16922
R] [βˆ€ 
x: ?m.16929
x, 
Module: (R : Type ?u.16933) β†’
  (M : Type ?u.16932) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.16933?u.16932)
Module 
R: Type ?u.16922
R (
E: B β†’ Type ?u.16911
E 
x: ?m.16929
x)]

@[simp]
theorem 
coe_snd_map_smul: βˆ€ {B : Type u_2} {E : B β†’ Type u_1} [inst : (x : B) β†’ AddCommMonoid (E x)] (R : Type u_3) [inst_1 : Semiring R]
  [inst_2 : (x : B) β†’ Module R (E x)] (x : B) (r : R) (v : E x),
  (totalSpaceMk x (r β€’ v)).snd = r β€’ (totalSpaceMk x v).snd
coe_snd_map_smul (
x: B
x : 
B: Type ?u.16962
B) (
r: R
r : 
R: Type ?u.16978
R) (
v: E x
v : 
E: B β†’ Type ?u.16967
E 
x: B
x) :
    (↑(
r: R
r β€’ 
v: E x
v) : 
TotalSpace: {B : Type ?u.17027} β†’ (B β†’ Type ?u.17026) β†’ Type (max?u.17027?u.17026)
TotalSpace 
E: B β†’ Type ?u.16967
E).
snd: {Ξ± : Type ?u.17982} β†’ {Ξ² : Ξ± β†’ Type ?u.17981} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
snd = 
r: R
r β€’ (
v: E x
v : 
TotalSpace: {B : Type ?u.18000} β†’ (B β†’ Type ?u.17999) β†’ Type (max?u.18000?u.17999)
TotalSpace 
E: B β†’ Type ?u.16967
E).
snd: {Ξ± : Type ?u.18066} β†’ {Ξ² : Ξ± β†’ Type ?u.18065} β†’ (self : Sigma Ξ²) β†’ Ξ² self.fst
snd :=
  
rfl: βˆ€ {Ξ± : Sort ?u.18717} {a : Ξ±}, a = a
rfl
#align bundle.coe_snd_map_smul 
Bundle.coe_snd_map_smul: βˆ€ {B : Type u_2} {E : B β†’ Type u_1} [inst : (x : B) β†’ AddCommMonoid (E x)] (R : Type u_3) [inst_1 : Semiring R]
  [inst_2 : (x : B) β†’ Module R (E x)] (x : B) (r : R) (v : E x),
  (totalSpaceMk x (r β€’ v)).snd = r β€’ (totalSpaceMk x v).snd
Bundle.coe_snd_map_smul

end FiberStructures

section TrivialInstances

variable {
F: Type ?u.18779
F : 
Type _: Type (?u.18886+1)
Type _} {
R: Type ?u.18977
R : 
Type _: Type (?u.18977+1)
Type _} [
Semiring: Type ?u.18892 β†’ Type ?u.18892
Semiring 
R: Type ?u.18782
R] (
b: B
b : 
B: Type ?u.18771
B)


instance: {B : Type u_1} β†’ {F : Type u_2} β†’ (b : B) β†’ [inst : AddCommMonoid F] β†’ AddCommMonoid (Trivial B F b)
instance [
AddCommMonoid: Type ?u.18809 β†’ Type ?u.18809
AddCommMonoid 
F: Type ?u.18798
F] : 
AddCommMonoid: Type ?u.18812 β†’ Type ?u.18812
AddCommMonoid (
Bundle.Trivial: (B : Type ?u.18814) β†’ Type ?u.18813 β†’ B β†’ Type ?u.18813
Bundle.Trivial 
B: Type ?u.18790
B 
F: Type ?u.18798
F 
b: B
b) :=
  β€ΉAddCommMonoid Fβ€Ί


instance: {B : Type u_1} β†’ {F : Type u_2} β†’ (b : B) β†’ [inst : AddCommGroup F] β†’ AddCommGroup (Trivial B F b)
instance [
AddCommGroup: Type ?u.18897 β†’ Type ?u.18897
AddCommGroup 
F: Type ?u.18886
F] : 
AddCommGroup: Type ?u.18900 β†’ Type ?u.18900
AddCommGroup (
Bundle.Trivial: (B : Type ?u.18902) β†’ Type ?u.18901 β†’ B β†’ Type ?u.18901
Bundle.Trivial 
B: Type ?u.18878
B 
F: Type ?u.18886
F 
b: B
b) :=
  β€ΉAddCommGroup Fβ€Ί


instance: {B : Type u_1} β†’
  {F : Type u_2} β†’
    {R : Type u_3} β†’
      [inst : Semiring R] β†’ (b : B) β†’ [inst_1 : AddCommMonoid F] β†’ [inst_2 : Module R F] β†’ Module R (Trivial B F b)
instance [
AddCommMonoid: Type ?u.18985 β†’ Type ?u.18985
AddCommMonoid 
F: Type ?u.18974
F] [
Module: (R : Type ?u.18989) β†’
  (M : Type ?u.18988) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.18989?u.18988)
Module 
R: Type ?u.18977
R 
F: Type ?u.18974
F] : 
Module: (R : Type ?u.19015) β†’
  (M : Type ?u.19014) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.19015?u.19014)
Module 
R: Type ?u.18977
R (
Bundle.Trivial: (B : Type ?u.19017) β†’ Type ?u.19016 β†’ B β†’ Type ?u.19016
Bundle.Trivial 
B: Type ?u.18966
B 
F: Type ?u.18974
F 
b: B
b) :=
  β€ΉModule R Fβ€Ί