def Equiv.piCongrSigmaFiber {α : Type u_1} {β : Type u_2} {f : α → β} {γ₁ : α → Sort u_3} {γ₂ : α → Sort u_4} (e : (a : α) → γ₁ a ≃ γ₂ a) : ((σ : (y : β) × { x : α // f x = y }) → γ₁ ↑σ.snd) ≃ ((a : α) → γ₂ a)

A family of equivalences ∀ a, γ₁ a ≃ γ₂ a generates an equivalence between the product over the fibers of a function f : α → β on index types.

Equations

• Equiv.piCongrSigmaFiber e = (Equiv.piCongrLeft γ₁ (Equiv.sigmaFiberEquiv f)).trans (Equiv.piCongrRight e)

@[simp]

theorem Equiv.piCongrSigmaFiber_apply {α : Type u_1} {β : Type u_2} {f : α → β} {γ₁ : α → Sort u_3} {γ₂ : α → Sort u_4} (e : (a : α) → γ₁ a ≃ γ₂ a) (g : (σ : (y : β) × { x : α // f x = y }) → γ₁ ↑σ.snd) (a : α) : (piCongrSigmaFiber e) g a = (e a) (g ⟨f a, ⟨a, ⋯⟩⟩)

@[simp]

theorem Equiv.piCongrSigmaFiber_symm_apply {α : Type u_1} {β : Type u_2} {f : α → β} {γ₁ : α → Sort u_3} {γ₂ : α → Sort u_4} (e : (a : α) → γ₁ a ≃ γ₂ a) (g : (a : α) → γ₂ a) (σ : (y : β) × { x : α // f x = y }) : (piCongrSigmaFiber e).symm g σ = (e ↑σ.snd).symm (g ↑σ.snd)

def Equiv.piCongrFiberwise {α : Type u_1} {β : Type u_2} {γ₁ : α → Type u_3} {γ₂ : β → Type u_4} {f : α → β} (e : (b : β) → ((σ : { a : α // f a = b }) → γ₁ ↑σ) ≃ γ₂ b) : ((a : α) → γ₁ a) ≃ ((b : β) → γ₂ b)

Let f : α → β be a function on index types. A family of equivalences, indexed by b : β, between the product over the fiber of b under f given as ∀ (σ : { a : α // f a = b }) → γ₁ σ.1) ≃ γ₂ b lifts to an equivalence over the products ∀ a, γ₁ a ≃ ∀ b, γ₂ b.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Equiv.piCongrFiberwise_apply {α : Type u_1} {β : Type u_2} {γ₁ : α → Type u_3} {γ₂ : β → Type u_4} {f : α → β} (e : (b : β) → ((σ : { a : α // f a = b }) → γ₁ ↑σ) ≃ γ₂ b) (g : (a : α) → γ₁ a) (b : β) : (piCongrFiberwise e) g b = (e b) fun (σ : { a : α // f a = b }) => g ↑σ

@[simp]

theorem Equiv.piCongrFiberwise_symm_apply {α : Type u_1} {β : Type u_2} {γ₁ : α → Type u_3} {γ₂ : β → Type u_4} {f : α → β} (e : (b : β) → ((σ : { a : α // f a = b }) → γ₁ ↑σ) ≃ γ₂ b) (g : (b : β) → γ₂ b) (a : α) : (piCongrFiberwise e).symm g a = (e (f a)).symm (g (f a)) ⟨a, ⋯⟩