/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro

! This file was ported from Lean 3 source module group_theory.perm.via_embedding
! leanprover-community/mathlib commit 9116dd6709f303dcf781632e15fdef382b0fc579
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Perm.Basic
import Mathlib.Logic.Equiv.Set

/-!
# `Equiv.Perm.viaEmbedding`, a noncomputable analogue of `Equiv.Perm.viaFintypeEmbedding`.
-/


variable {
α: Type ?u.631
α 
β: Type ?u.24
β : 
Type _: Type (?u.5+1)
Type _}

namespace Equiv

namespace Perm

variable (
e: Perm α
e : 
Perm: Sort ?u.996 → Sort (max1?u.996)
Perm 
α: Type ?u.8
α) (
ι: α ↪ β
ι : 
α: Type ?u.2280
α ↪ 
β: Type ?u.634
β)

open Classical

/-- Noncomputable version of `Equiv.Perm.viaFintypeEmbedding` that does not assume `Fintype` -/
noncomputable def 
viaEmbedding: {α : Type u_1} → {β : Type u_2} → Perm α → (α ↪ β) → Perm β
viaEmbedding : 
Perm: Sort ?u.34 → Sort (max1?u.34)
Perm 
β: Type ?u.24
β :=
  
extendDomain: {α' : Type ?u.37} → {β' : Type ?u.36} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
e: Perm α
e (
ofInjective: {α : Sort ?u.46} → {β : Type ?u.45} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)
ofInjective 
ι: α ↪ β
ι.
1: {α : Sort ?u.50} → {β : Sort ?u.49} → (α ↪ β) → α → β
1 
ι: α ↪ β
ι.
2: ∀ {α : Sort ?u.66} {β : Sort ?u.65} (self : α ↪ β), Function.Injective self.toFun
2)
#align equiv.perm.via_embedding 
Equiv.Perm.viaEmbedding: {α : Type u_1} → {β : Type u_2} → Perm α → (α ↪ β) → Perm β
Equiv.Perm.viaEmbedding

theorem 
viaEmbedding_apply: ∀ {α : Type u_2} {β : Type u_1} (e : Perm α) (ι : α ↪ β) (x : α), ↑(viaEmbedding e ι) (↑ι x) = ↑ι (↑e x)
viaEmbedding_apply (
x: α
x : 
α: Type ?u.105
α) : 
e: Perm α
e.
viaEmbedding: {α : Type ?u.122} → {β : Type ?u.121} → Perm α → (α ↪ β) → Perm β
viaEmbedding 
ι: α ↪ β
ι (
ι: α ↪ β
ι 
x: α
x) = 
ι: α ↪ β
ι (
e: Perm α
e 
x: α
x) :=
  
extendDomain_apply_image: ∀ {α' : Type ?u.562} {β' : Type ?u.561} (e : Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  (a : α'), ↑(extendDomain e f) ↑(↑f a) = ↑(↑f (↑e a))
extendDomain_apply_image 
e: Perm α
e (
ofInjective: {α : Sort ?u.570} → {β : Type ?u.569} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)
ofInjective 
ι: α ↪ β
ι.
1: {α : Sort ?u.574} → {β : Sort ?u.573} → (α ↪ β) → α → β
1 
ι: α ↪ β
ι.
2: ∀ {α : Sort ?u.590} {β : Sort ?u.589} (self : α ↪ β), Function.Injective self.toFun
2) 
x: α
x
#align equiv.perm.via_embedding_apply 
Equiv.Perm.viaEmbedding_apply: ∀ {α : Type u_2} {β : Type u_1} (e : Perm α) (ι : α ↪ β) (x : α), ↑(viaEmbedding e ι) (↑ι x) = ↑ι (↑e x)
Equiv.Perm.viaEmbedding_apply

theorem 
viaEmbedding_apply_of_not_mem: ∀ (x : β), ¬x ∈ Set.range ↑ι → ↑(viaEmbedding e ι) x = x
viaEmbedding_apply_of_not_mem (
x: β
x : 
β: Type ?u.634
β) (
hx: ¬x ∈ Set.range ↑ι
hx : 
x: β
x ∉ 
Set.range: {α : Type ?u.652} → {ι : Sort ?u.651} → (ι → α) → Set α
Set.range 
ι: α ↪ β
ι) : 
e: Perm α
e.
viaEmbedding: {α : Type ?u.809} → {β : Type ?u.808} → Perm α → (α ↪ β) → Perm β
viaEmbedding 
ι: α ↪ β
ι 
x: β
x = 
x: β
x :=
  
extendDomain_apply_not_subtype: ∀ {α' : Type ?u.907} {β' : Type ?u.906} (e : Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  {b : β'}, ¬p b → ↑(extendDomain e f) b = b
extendDomain_apply_not_subtype 
e: Perm α
e (
ofInjective: {α : Sort ?u.915} → {β : Type ?u.914} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)
ofInjective 
ι: α ↪ β
ι.
1: {α : Sort ?u.919} → {β : Sort ?u.918} → (α ↪ β) → α → β
1 
ι: α ↪ β
ι.
2: ∀ {α : Sort ?u.935} {β : Sort ?u.934} (self : α ↪ β), Function.Injective self.toFun
2) 
hx: ¬x ∈ Set.range ↑ι
hx
#align equiv.perm.via_embedding_apply_of_not_mem 
Equiv.Perm.viaEmbedding_apply_of_not_mem: ∀ {α : Type u_2} {β : Type u_1} (e : Perm α) (ι : α ↪ β) (x : β), ¬x ∈ Set.range ↑ι → ↑(viaEmbedding e ι) x = x
Equiv.Perm.viaEmbedding_apply_of_not_mem

/-- `viaEmbedding` as a group homomorphism -/
noncomputable def 
viaEmbeddingHom: Perm α →* Perm β
viaEmbeddingHom : 
Perm: Sort ?u.1005 → Sort (max1?u.1005)
Perm 
α: Type ?u.990
α →* 
Perm: Sort ?u.1006 → Sort (max1?u.1006)
Perm 
β: Type ?u.993
β :=
  
extendDomainHom: {α : Type ?u.1507} → {β : Type ?u.1506} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
extendDomainHom (
ofInjective: {α : Sort ?u.1639} → {β : Type ?u.1638} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)
ofInjective 
ι: α ↪ β
ι.
1: {α : Sort ?u.1643} → {β : Sort ?u.1642} → (α ↪ β) → α → β
1 
ι: α ↪ β
ι.
2: ∀ {α : Sort ?u.1659} {β : Sort ?u.1658} (self : α ↪ β), Function.Injective self.toFun
2)
#align equiv.perm.via_embedding_hom 
Equiv.Perm.viaEmbeddingHom: {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Perm α →* Perm β
Equiv.Perm.viaEmbeddingHom

theorem 
viaEmbeddingHom_apply: ∀ {α : Type u_2} {β : Type u_1} (e : Perm α) (ι : α ↪ β), ↑(viaEmbeddingHom ι) e = viaEmbedding e ι
viaEmbeddingHom_apply : 
viaEmbeddingHom: {α : Type ?u.1710} → {β : Type ?u.1709} → (α ↪ β) → Perm α →* Perm β
viaEmbeddingHom 
ι: α ↪ β
ι 
e: Perm α
e = 
viaEmbedding: {α : Type ?u.2239} → {β : Type ?u.2238} → Perm α → (α ↪ β) → Perm β
viaEmbedding 
e: Perm α
e 
ι: α ↪ β
ι :=
  
rfl: ∀ {α : Sort ?u.2249} {a : α}, a = a
rfl
#align equiv.perm.via_embedding_hom_apply 
Equiv.Perm.viaEmbeddingHom_apply: ∀ {α : Type u_2} {β : Type u_1} (e : Perm α) (ι : α ↪ β), ↑(viaEmbeddingHom ι) e = viaEmbedding e ι
Equiv.Perm.viaEmbeddingHom_apply

theorem 
viaEmbeddingHom_injective: ∀ {α : Type u_1} {β : Type u_2} (ι : α ↪ β), Function.Injective ↑(viaEmbeddingHom ι)
viaEmbeddingHom_injective : 
Function.Injective: {α : Sort ?u.2294} → {β : Sort ?u.2293} → (α → β) → Prop
Function.Injective (
viaEmbeddingHom: {α : Type ?u.2298} → {β : Type ?u.2297} → (α ↪ β) → Perm α →* Perm β
viaEmbeddingHom 
ι: α ↪ β
ι) :=
  
extendDomainHom_injective: ∀ {α : Type ?u.2830} {β : Type ?u.2829} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  Function.Injective ↑(extendDomainHom f)
extendDomainHom_injective (
ofInjective: {α : Sort ?u.2836} → {β : Type ?u.2835} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)
ofInjective 
ι: α ↪ β
ι.
1: {α : Sort ?u.2840} → {β : Sort ?u.2839} → (α ↪ β) → α → β
1 
ι: α ↪ β
ι.
2: ∀ {α : Sort ?u.2856} {β : Sort ?u.2855} (self : α ↪ β), Function.Injective self.toFun
2)
#align equiv.perm.via_embedding_hom_injective 
Equiv.Perm.viaEmbeddingHom_injective: ∀ {α : Type u_1} {β : Type u_2} (ι : α ↪ β), Function.Injective ↑(viaEmbeddingHom ι)
Equiv.Perm.viaEmbeddingHom_injective

end Perm

end Equiv