text:
/-
Copyright (c) 2021 Andrew Yang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Andrew Yang, Yury G. Kudryashov
-/
import topology.continuous_on
import data.setoid.basic
import tactic.tfae

/-!
# Inseparable points in a topological space

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

In this file we define

* `specializes` (notation: `x ⤳ y`) : a relation saying that `𝓝 x ≤ 𝓝 y`;

* `inseparable`: a relation saying that two points in a topological space have the same
  neighbourhoods; equivalently, they can't be separated by an open set;

* `inseparable_setoid X`: same relation, as a `setoid`;

* `separation_quotient X`: the quotient of `X` by its `inseparable_setoid`.

We also prove various basic properties of the relation `inseparable`.

## Notations

- `x ⤳ y`: notation for `specializes x y`;
- `x ~ y` is used as a local notation for `inseparable x y`;
- `𝓝 x` is the neighbourhoods filter `nhds x` of a point `x`, defined elsewhere.

## Tags

topological space, separation setoid
-/

open set filter function
open_locale topology filter

variables {X Y Z α ι : Type*} {π : ι → Type*} [topological_space X] [topological_space Y]
  [topological_space Z] [∀ i, topological_space (π i)] {x y z : X} {s : set X} {f : X → Y}

/-!
### `specializes` relation
-/

/-- `x` specializes to `y` (notation: `x ⤳ y`) if either of the following equivalent properties
hold:

* `𝓝 x ≤ 𝓝 y`; this property is used as the definition;
* `pure x ≤ 𝓝 y`; in other words, any neighbourhood of `y` contains `x`;
* `y ∈ closure {x}`;
* `closure {y} ⊆ closure {x}`;
* for any closed set `s` we have `x ∈ s → y ∈ s`;
* for any open set `s` we have `y ∈ s → x ∈ s`;
* `y` is a cluster point of the filter `pure x = 𝓟 {x}`.

This relation defines a `preorder` on `X`. If `X` is a T₀ space, then this preorder is a partial
order. If `X` is a T₁ space, then this partial order is trivial : `x ⤳ y ↔ x = y`. -/
def specializes (x y : X) : Prop := 𝓝 x ≤ 𝓝 y

infix ` ⤳ `:300 := specializes

/-- A collection of equivalent definitions of `x ⤳ y`. The public API is given by `iff` lemmas
below. -/
lemma specializes_tfae (x y : X) :
  tfae [x ⤳ y,
    pure x ≤ 𝓝 y,
    ∀ s : set X, is_open s → y ∈ s → x ∈ s,
    ∀ s : set X, is_closed s → x ∈ s → y ∈ s,
    y ∈ closure ({x} : set X),
    closure ({y} : set X) ⊆ closure {x},
    cluster_pt y (pure x)] :=
begin
  tfae_have : 1 → 2, from (pure_le_nhds _).trans,
  tfae_have : 2 → 3, from λ h s hso hy, h (hso.mem_nhds hy),
  tfae_have : 3 → 4, from λ h s hsc hx, of_not_not $ λ hy, h sᶜ hsc.is_open_compl hy hx,
  tfae_have : 4 → 5, from λ h, h _ is_closed_closure (subset_closure $ mem_singleton _),
  tfae_have : 6 ↔ 5, from is_closed_closure.closure_subset_iff.trans singleton_subset_iff,
  tfae_have : 5 ↔ 7, by rw [mem_closure_iff_cluster_pt, principal_singleton],
  tfae_have : 5 → 1,
  { refine λ h, (nhds_basis_opens _).ge_iff.2 _,
    rintro s ⟨hy, ho⟩,
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, (rfl : z = x)⟩,
    exact ho.mem_nhds hxs },
  tfae_finish
end

lemma specializes_iff_nhds : x ⤳ y ↔ 𝓝 x ≤ 𝓝 y := iff.rfl
lemma specializes_iff_pure : x ⤳ y ↔ pure x ≤ 𝓝 y := (specializes_tfae x y).out 0 1

alias specializes_iff_nhds ↔ specializes.nhds_le_nhds _
alias specializes_iff_pure ↔ specializes.pure_le_nhds _

lemma specializes_iff_forall_open : x ⤳ y ↔ ∀ s : set X, is_open s → y ∈ s → x ∈ s :=
(specializes_tfae x y).out 0 2

lemma specializes.mem_open (h : x ⤳ y) (hs : is_open s) (hy : y ∈ s) : x ∈ s :=
specializes_iff_forall_open.1 h s hs hy

lemma is_open.not_specializes (hs : is_open s) (hx : x ∉ s) (hy : y ∈ s) : ¬ x ⤳ y :=
λ h, hx $ h.mem_open hs hy

lemma specializes_iff_forall_closed : x ⤳ y ↔ ∀ s : set X, is_closed s → x ∈ s → y ∈ s :=
(specializes_tfae x y).out 0 3

lemma specializes.mem_closed (h : x ⤳ y) (hs : is_closed s) (hx : x ∈ s) : y ∈ s :=
specializes_iff_forall_closed.1 h s hs hx

lemma is_closed.not_specializes (hs : is_closed s) (hx : x ∈ s) (hy : y ∉ s) : ¬ x ⤳ y :=
λ h, hy $ h.mem_closed hs hx

lemma specializes_iff_mem_closure : x ⤳ y ↔ y ∈ closure ({x} : set X) :=
(specializes_tfae x y).out 0 4

alias specializes_iff_mem_closure ↔ specializes.mem_closure _

lemma specializes_iff_closure_subset :
  x ⤳ y ↔ closure ({y} : set X) ⊆ closure {x} :=
(specializes_tfae x y).out 0 5

alias specializes_iff_closure_subset ↔ specializes.closure_subset _

lemma filter.has_basis.specializes_iff {ι} {p : ι → Prop} {s : ι → set X}
  (h : (𝓝 y).has_basis p s) :
  x ⤳ y ↔ ∀ i, p i → x ∈ s i :=
specializes_iff_pure.trans h.ge_iff

lemma specializes_rfl : x ⤳ x := le_rfl

@[refl] lemma specializes_refl (x : X) : x ⤳ x := specializes_rfl

@[trans] lemma specializes.trans : x ⤳ y → y ⤳ z → x ⤳ z := le_trans

lemma specializes_of_eq (e : x = y) : x ⤳ y := e ▸ specializes_refl x

lemma specializes_of_nhds_within (h₁ : 𝓝[s] x ≤ 𝓝[s] y) (h₂ : x ∈ s) : x ⤳ y :=
specializes_iff_pure.2 $
calc pure x ≤ 𝓝[s] x : le_inf (pure_le_nhds _) (le_principal_iff.2 h₂)
        ... ≤ 𝓝[s] y : h₁
        ... ≤ 𝓝 y    : inf_le_left

lemma specializes.map_of_continuous_at (h : x ⤳ y) (hy : continuous_at f y) : f x ⤳ f y :=
specializes_iff_pure.2 $ λ s hs, mem_pure.2 $ mem_preimage.1 $ mem_of_mem_nhds $ hy.mono_left h hs

lemma specializes.map (h : x ⤳ y) (hf : continuous f) : f x ⤳ f y :=
h.map_of_continuous_at hf.continuous_at

lemma inducing.specializes_iff (hf : inducing f) : f x ⤳ f y ↔ x ⤳ y :=
by simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton,
  mem_preimage]

lemma subtype_specializes_iff {p : X → Prop} (x y : subtype p) : x ⤳ y ↔ (x : X) ⤳ y :=
inducing_coe.specializes_iff.symm

@[simp] lemma specializes_prod {x₁ x₂ : X} {y₁ y₂ : Y} :
  (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂ :=
by simp only [specializes, nhds_prod_eq, prod_le_prod]

lemma specializes.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) :
  (x₁, y₁) ⤳ (x₂, y₂) :=
specializes_prod.2 ⟨hx, hy⟩

@[simp] lemma specializes_pi {f g : Π i, π i} : f ⤳ g ↔ ∀ i, f i ⤳ g i :=
by simp only [specializes, nhds_pi, pi_le_pi]

lemma not_specializes_iff_exists_open : ¬ x ⤳ y ↔ ∃ (S : set X), is_open S ∧ y ∈ S ∧ x ∉ S :=
by { rw [specializes_iff_forall_open], push_neg, refl }

lemma not_specializes_iff_exists_closed : ¬ x ⤳ y ↔ ∃ (S : set X), is_closed S ∧ x ∈ S ∧ y ∉ S :=
by { rw [specializes_iff_forall_closed], push_neg, refl }

variable (X)

/-- Specialization forms a preorder on the topological space. -/
def specialization_preorder : preorder X :=
{ le := λ x y, y ⤳ x,
  lt := λ x y, y ⤳ x ∧ ¬(x ⤳ y),
  .. preorder.lift (order_dual.to_dual ∘ 𝓝) }

variable {X}

/-- A continuous function is monotone with respect to the specialization preorders on the domain and
the codomain. -/
lemma continuous.specialization_monotone (hf : continuous f) :
  @monotone _ _ (specialization_preorder X) (specialization_preorder Y) f :=
λ x y h, h.map hf

/-!
### `inseparable` relation
-/

/-- Two points `x` and `y` in a topological space are `inseparable` if any of the following
equivalent properties hold:

- `𝓝 x = 𝓝 y`; we use this property as the definition;
- for any open set `s`, `x ∈ s ↔ y ∈ s`, see `inseparable_iff_open`;
- for any closed set `s`, `x ∈ s ↔ y ∈ s`, see `inseparable_iff_closed`;
- `x ∈ closure {y}` and `y ∈ closure {x}`, see `inseparable_iff_mem_closure`;
- `closure {x} = closure {y}`, see `inseparable_iff_closure_eq`.
-/
def inseparable (x y : X) : Prop := 𝓝 x = 𝓝 y

local infix ` ~ ` := inseparable

lemma inseparable_def : x ~ y ↔ 𝓝 x = 𝓝 y := iff.rfl

lemma inseparable_iff_specializes_and : x ~ y ↔ x ⤳ y ∧ y ⤳ x := le_antisymm_iff

lemma inseparable.specializes (h : x ~ y) : x ⤳ y := h.le

lemma inseparable.specializes' (h : x ~ y) : y ⤳ x := h.ge

lemma specializes.antisymm (h₁ : x ⤳ y) (h₂ : y ⤳ x) : x ~ y := le_antisymm h₁ h₂

lemma inseparable_iff_forall_open : x ~ y ↔ ∀ s : set X, is_open s → (x ∈ s ↔ y ∈ s) :=
by simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and_distrib,
  ← iff_def, iff.comm]

lemma not_inseparable_iff_exists_open : ¬(x ~ y) ↔ ∃ s : set X, is_open s ∧ xor (x ∈ s) (y ∈ s) :=
by simp [inseparable_iff_forall_open, ← xor_iff_not_iff]

lemma inseparable_iff_forall_closed : x ~ y ↔ ∀ s : set X, is_closed s → (x ∈ s ↔ y ∈ s) :=
by simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and_distrib,
  ← iff_def]

lemma inseparable_iff_mem_closure :
  x ~ y ↔ x ∈ closure ({y} : set X) ∧ y ∈ closure ({x} : set X) :=
inseparable_iff_specializes_and.trans $ by simp only [specializes_iff_mem_closure, and_comm]

lemma inseparable_iff_closure_eq : x ~ y ↔ closure ({x} : set X) = closure {y} :=
by simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset,
  ← subset_antisymm_iff, eq_comm]

lemma inseparable_of_nhds_within_eq (hx : x ∈ s) (hy : y ∈ s) (h : 𝓝[s] x = 𝓝[s] y) : x ~ y :=
(specializes_of_nhds_within h.le hx).antisymm (specializes_of_nhds_within h.ge hy)

lemma inducing.inseparable_iff (hf : inducing f) : f x ~ f y ↔ x ~ y :=
by simp only [inseparable_iff_specializes_and, hf.specializes_iff]

lemma subtype_inseparable_iff {p : X → Prop} (x y : subtype p) : x ~ y ↔ (x : X) ~ y :=
inducing_coe.inseparable_iff.symm

@[simp] lemma inseparable_prod {x₁ x₂ : X} {y₁ y₂ : Y} :
  (x₁, y₁) ~ (x₂, y₂) ↔ x₁ ~ x₂ ∧ y₁ ~ y₂ :=
by simp only [inseparable, nhds_prod_eq, prod_inj]

lemma inseparable.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ~ x₂) (hy : y₁ ~ y₂) :
  (x₁, y₁) ~ (x₂, y₂) :=
inseparable_prod.2 ⟨hx, hy⟩

@[simp] lemma inseparable_pi {f g : Π i, π i} : f ~ g ↔ ∀ i, f i ~ g i :=
by simp only [inseparable, nhds_pi, funext_iff, pi_inj]

namespace inseparable

@[refl] lemma refl (x : X) : x ~ x := eq.refl (𝓝 x)

lemma rfl : x ~ x := refl x

lemma of_eq (e : x = y) : inseparable x y := e ▸ refl x

@[symm] lemma symm (h : x ~ y) : y ~ x := h.symm

@[trans] lemma trans (h₁ : x ~ y) (h₂ : y ~ z) : x ~ z := h₁.trans h₂

lemma nhds_eq (h : x ~ y) : 𝓝 x = 𝓝 y := h

lemma mem_open_iff (h : x ~ y) (hs : is_open s) : x ∈ s ↔ y ∈ s :=
inseparable_iff_forall_open.1 h s hs

lemma mem_closed_iff (h : x ~ y) (hs : is_closed s) : x ∈ s ↔ y ∈ s :=
inseparable_iff_forall_closed.1 h s hs

lemma map_of_continuous_at (h : x ~ y) (hx : continuous_at f x) (hy : continuous_at f y) :
  f x ~ f y :=
(h.specializes.map_of_continuous_at hy).antisymm (h.specializes'.map_of_continuous_at hx)

lemma map (h : x ~ y) (hf : continuous f) : f x ~ f y :=
h.map_of_continuous_at hf.continuous_at hf.continuous_at

end inseparable

lemma is_closed.not_inseparable (hs : is_closed s) (hx : x ∈ s) (hy : y ∉ s) : ¬x ~ y :=
λ h, hy $ (h.mem_closed_iff hs).1 hx

lemma is_open.not_inseparable (hs : is_open s) (hx : x ∈ s) (hy : y ∉ s) : ¬x ~ y :=
λ h, hy $ (h.mem_open_iff hs).1 hx

/-!
### Separation quotient

In this section we define the quotient of a topological space by the `inseparable` relation.
-/

variable (X)

/-- A `setoid` version of `inseparable`, used to define the `separation_quotient`. -/
def inseparable_setoid : setoid X :=
{ r := (~),
  .. setoid.comap 𝓝 ⊥ }

/-- The quotient of a topological space by its `inseparable_setoid`. This quotient is guaranteed to
be a T₀ space. -/
@[derive topological_space]
def separation_quotient := quotient (inseparable_setoid X)

variables {X} {t : set (separation_quotient X)}

namespace separation_quotient

/-- The natural map from a topological space to its separation quotient. -/
def mk : X → separation_quotient X := quotient.mk'

lemma quotient_map_mk : quotient_map (mk : X → separation_quotient X) :=
quotient_map_quot_mk

lemma continuous_mk : continuous (mk : X → separation_quotient X) :=
continuous_quot_mk

@[simp] lemma mk_eq_mk : mk x = mk y ↔ x ~ y := quotient.eq'

lemma surjective_mk : surjective (mk : X → separation_quotient X) :=
surjective_quot_mk _

@[simp] lemma range_mk : range (mk : X → separation_quotient X) = univ :=
surjective_mk.range_eq

instance [nonempty X] : nonempty (separation_quotient X) := nonempty.map mk ‹_›
instance [inhabited X] : inhabited (separation_quotient X) := ⟨mk default⟩
instance [subsingleton X] : subsingleton (separation_quotient X) := surjective_mk.subsingleton

lemma preimage_image_mk_open (hs : is_open s) : mk ⁻¹' (mk '' s) = s :=
begin
  refine subset.antisymm _ (subset_preimage_image _ _),
  rintro x ⟨y, hys, hxy⟩,
  exact ((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys
end

lemma is_open_map_mk : is_open_map (mk : X → separation_quotient X) :=
λ s hs, quotient_map_mk.is_open_preimage.1 $ by rwa preimage_image_mk_open hs

lemma preimage_image_mk_closed (hs : is_closed s) : mk ⁻¹' (mk '' s) = s :=
begin
  refine subset.antisymm _ (subset_preimage_image _ _),
  rintro x ⟨y, hys, hxy⟩,
  exact ((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys
end

lemma inducing_mk : inducing (mk : X → separation_quotient X) :=
⟨le_antisymm (continuous_iff_le_induced.1 continuous_mk)
  (λ s hs, ⟨mk '' s, is_open_map_mk s hs, preimage_image_mk_open hs⟩)⟩

lemma is_closed_map_mk : is_closed_map (mk : X → separation_quotient X) :=
inducing_mk.is_closed_map $ by { rw [range_mk], exact is_closed_univ }

@[simp] lemma comap_mk_nhds_mk : comap mk (𝓝 (mk x)) = 𝓝 x :=
(inducing_mk.nhds_eq_comap _).symm

@[simp] lemma comap_mk_nhds_set_image : comap mk (𝓝ˢ (mk '' s)) = 𝓝ˢ s :=
(inducing_mk.nhds_set_eq_comap _).symm

lemma map_mk_nhds : map mk (𝓝 x) = 𝓝 (mk x) :=
by rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]

lemma map_mk_nhds_set : map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s) :=
by rw [← comap_mk_nhds_set_image, map_comap_of_surjective surjective_mk]

lemma comap_mk_nhds_set : comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t) :=
by conv_lhs { rw [← image_preimage_eq t surjective_mk, comap_mk_nhds_set_image] }

lemma preimage_mk_interior : mk ⁻¹' (interior t) = interior (mk ⁻¹' t) :=
is_open_map_mk.preimage_interior_eq_interior_preimage continuous_mk t

lemma preimage_mk_frontier : mk ⁻¹' (frontier t) = frontier (mk ⁻¹' t) :=
is_open_map_mk.preimage_frontier_eq_frontier_preimage continuous_mk t

lemma image_mk_closure : mk '' closure s = closure (mk '' s) :=
(image_closure_subset_closure_image continuous_mk).antisymm $
  is_closed_map_mk.closure_image_subset _

lemma map_prod_map_mk_nhds (x : X) (y : Y) : map (prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y) :=
by rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]

lemma map_mk_nhds_within_preimage (s : set (separation_quotient X)) (x : X) :
  map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] (mk x) :=
by rw [nhds_within, ← comap_principal, filter.push_pull, nhds_within, map_mk_nhds]

/-- Lift a map `f : X → α` such that `inseparable x y → f x = f y` to a map
`separation_quotient X → α`. -/
def lift (f : X → α) (hf : ∀ x y, x ~ y → f x = f y) : separation_quotient X → α :=
λ x, quotient.lift_on' x f hf

@[simp] lemma lift_mk {f : X → α} (hf : ∀ x y, x ~ y → f x = f y) (x : X) :
  lift f hf (mk x) = f x := rfl

@[simp] lemma lift_comp_mk {f : X → α} (hf : ∀ x y, x ~ y → f x = f y) : lift f hf ∘ mk = f := rfl

@[simp] lemma tendsto_lift_nhds_mk {f : X → α} {hf : ∀ x y, x ~ y → f x = f y} {x : X}
  {l : filter α} : tendsto (lift f hf) (𝓝 $ mk x) l ↔ tendsto f (𝓝 x) l :=
by simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]

@[simp] lemma tendsto_lift_nhds_within_mk {f : X → α} {hf : ∀ x y, x ~ y → f x = f y} {x : X}
  {s : set (separation_quotient X)} {l : filter α} :
  tendsto (lift f hf) (𝓝[s] (mk x)) l ↔ tendsto f (𝓝[mk ⁻¹' s] x) l :=
by simp only [← map_mk_nhds_within_preimage, tendsto_map'_iff, lift_comp_mk]

@[simp] lemma continuous_at_lift {f : X → Y} {hf : ∀ x y, x ~ y → f x = f y} {x : X} :
  continuous_at (lift f hf) (mk x) ↔ continuous_at f x :=
tendsto_lift_nhds_mk

@[simp] lemma continuous_within_at_lift {f : X → Y} {hf : ∀ x y, x ~ y → f x = f y}
  {s : set (separation_quotient X)} {x : X} :
  continuous_within_at (lift f hf) s (mk x) ↔ continuous_within_at f (mk ⁻¹' s) x :=
tendsto_lift_nhds_within_mk

@[simp] lemma continuous_on_lift {f : X → Y} {hf : ∀ x y, x ~ y → f x = f y}
  {s : set (separation_quotient X)} :
  continuous_on (lift f hf) s ↔ continuous_on f (mk ⁻¹' s) :=
by simp only [continuous_on, surjective_mk.forall, continuous_within_at_lift, mem_preimage]

@[simp] lemma continuous_lift {f : X → Y} {hf : ∀ x y, x ~ y → f x = f y} :
  continuous (lift f hf) ↔ continuous f :=
by simp only [continuous_iff_continuous_on_univ, continuous_on_lift, preimage_univ]

/-- Lift a map `f : X → Y → α` such that `inseparable a b → inseparable c d → f a c = f b d` to a
map `separation_quotient X → separation_quotient Y → α`. -/
def lift₂ (f : X → Y → α) (hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d) :
  separation_quotient X → separation_quotient Y → α :=
λ x y, quotient.lift_on₂' x y f hf

@[simp] lemma lift₂_mk {f : X → Y → α} (hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d) (x : X)
  (y : Y) : lift₂ f hf (mk x) (mk y) = f x y :=
rfl

@[simp] lemma tendsto_lift₂_nhds {f : X → Y → α} {hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d}
  {x : X} {y : Y} {l : filter α} :
  tendsto (uncurry $ lift₂ f hf) (𝓝 (mk x, mk y)) l ↔ tendsto (uncurry f) (𝓝 (x, y)) l :=
by { rw [← map_prod_map_mk_nhds, tendsto_map'_iff], refl }

@[simp] lemma tendsto_lift₂_nhds_within {f : X → Y → α}
  {hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d} {x : X} {y : Y}
  {s : set (separation_quotient X × separation_quotient Y)} {l : filter α} :
  tendsto (uncurry $ lift₂ f hf) (𝓝[s] (mk x, mk y)) l ↔
    tendsto (uncurry f) (𝓝[prod.map mk mk ⁻¹' s] (x, y)) l :=
by { rw [nhds_within, ← map_prod_map_mk_nhds, ← filter.push_pull, comap_principal], refl }

@[simp] lemma continuous_at_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d}
  {x : X} {y : Y} :
  continuous_at (uncurry $ lift₂ f hf) (mk x, mk y) ↔ continuous_at (uncurry f) (x, y) :=
tendsto_lift₂_nhds

@[simp] lemma continuous_within_at_lift₂ {f : X → Y → Z}
  {hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d}
  {s : set (separation_quotient X × separation_quotient Y)} {x : X} {y : Y} :
  continuous_within_at (uncurry $ lift₂ f hf) s (mk x, mk y) ↔
    continuous_within_at (uncurry f) (prod.map mk mk ⁻¹' s) (x, y) :=
tendsto_lift₂_nhds_within

@[simp] lemma continuous_on_lift₂ {f : X → Y → Z}
  {hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d}
  {s : set (separation_quotient X × separation_quotient Y)} :
  continuous_on (uncurry $ lift₂ f hf) s ↔ continuous_on (uncurry f) (prod.map mk mk ⁻¹' s) :=
begin
  simp_rw [continuous_on, (surjective_mk.prod_map surjective_mk).forall, prod.forall, prod.map,
    continuous_within_at_lift₂],
  refl
end

@[simp] lemma continuous_lift₂ {f : X → Y → Z}
  {hf : ∀ a b c d, a ~ c → b ~ d → f a b = f c d} :
  continuous (uncurry $ lift₂ f hf) ↔ continuous (uncurry f) :=
by simp only [continuous_iff_continuous_on_univ, continuous_on_lift₂, preimage_univ]

end separation_quotient

author: leanprover-community

repo: mathlib


text:
-- Implementation of HPP Lattice Gas CA.

-- Cell states 'cellT' are represented as constructors named as possible combinations of
-- of the four directly-connected cardinal directions. 'X' is an empty cell.
-- The definition 'mk_hpp' builds an instance of HPP
-- from an initial configuration of cell states.

import cell_automaton utils data.list.perm

open utils

namespace hpp

section hpp

-- 'X' is empty
-- 'N' 'W' 'E' 'S' and their combinations represent presence (or absence) of
-- a gas molecule heading in the respective direction.
@[derive decidable_eq]
inductive cellT | X | N | W | E | S
                | NW | NE | NS | WS | WE | ES
                | NWE | NWS | NES | WES | NWSE

-- Cardinal directions of HPP cells.
inductive cardinal | CN | CW | CE | CS

open cellT cardinal

def cellT_str : cellT → string
	| N    := "↑"
	| W    := "←"
	| E    := "→"
	| S    := "↓"
  | NW   := "↖"
  | NE   := "↗"
  | NS   := "↕"
  | WS   := "↙"
  | WE   := "↔"
  | ES   := "↙"
  | NWE  := "⊥"
  | NWS  := "⊣"
  | NES  := "⊢"
  | WES  := "⊤"
  | NWSE := "+"
  | X    := " "

instance cellT_to_str : has_to_string cellT := ⟨cellT_str⟩

instance cellT_repr : has_repr cellT := ⟨cellT_str⟩

attribute [reducible]
def hpp := cell_automaton cellT

def has_cardinal : cellT → cardinal → bool
  | N CN := tt
  | N _  := ff
  | W CW := tt
  | W _  := ff
  | E CE := tt
  | E _  := ff
  | S CS := tt
  | S _  := ff
  | NW CN := tt
  | NW CW := tt
  | NW _  := ff
  | NE CN := tt
  | NE CE := tt
  | NE _  := ff
  | NS CW := tt
  | NS CE := tt
  | NS _  := ff
  | WS CW := tt
  | WS CS := tt
  | WS _  := ff
  | WE CS := tt
  | WE CN := tt
  | WE _  := ff
  | ES CE := tt
  | ES CS := tt
  | ES _  := ff
  | NWE CN := tt
  | NWE CW := tt
  | NWE CE := tt
  | NWE _  := ff
  | NWS CN := tt
  | NWS CW := tt
  | NWS CS := tt
  | NWS _  := ff
  | NES CN := tt
  | NES CE := tt
  | NES CS := tt
  | NES _  := ff
  | WES CW := tt
  | WES CE := tt
  | WES CS := tt
  | WES _  := ff
  | NWSE _ := tt
  | X _ := ff

def collision : cellT → cellT
  | NS := WE
  | WE := NS
  | x  := x

def translation' : bool → bool → bool → bool → cellT
  | tt tt tt tt := NWSE
  | tt tt tt ff := WES
  | tt tt ff tt := NES
  | tt tt ff ff := ES
  | tt ff tt tt := NWS
  | tt ff tt ff := WS
  | tt ff ff tt := NS
  | tt ff ff ff := S
  | ff tt tt tt := NWE
  | ff tt tt ff := WE
  | ff tt ff tt := NE
  | ff tt ff ff := E
  | ff ff tt tt := NW
  | ff ff tt ff := W
  | ff ff ff tt := N
  | ff ff ff ff := X

def translation (neigh : list cellT) : cellT :=
  let north := list.nth neigh 0 in
  let west  := list.nth neigh 1 in
  let east  := list.nth neigh 2 in
  let south := list.nth neigh 3 in
  match north with
    | none     := X
    | (some n) :=
  match west with
    | none     := X
    | (some w) :=
  match east with
    | none     := X
    | (some e) :=
  match south with
    | none     := X
    | (some s) :=
      translation' (has_cardinal n CS)
                   (has_cardinal w CE)
                   (has_cardinal e CW)
                   (has_cardinal s CN)
  end end end end

lemma translation_eq_translation' {neigh : list cellT}
  (h : list.length neigh = 4) :
  translation neigh =
    let n := list.nth_le neigh 0 $ by simp [h]; exact dec_trivial in
    let w := list.nth_le neigh 1 $ by simp [h]; exact dec_trivial in
    let e := list.nth_le neigh 2 $ by simp [h]; exact dec_trivial in
    let s := list.nth_le neigh 3 $ by simp [h]; exact dec_trivial in
      translation' (has_cardinal n CS)
                   (has_cardinal w CE)
                   (has_cardinal e CW)
                   (has_cardinal s CN) :=
begin
  cases neigh with x₁ xs₁, cases h,
  cases xs₁ with x₂ xs₂, cases h,
  cases xs₂ with x₃ xs₃, cases h,
  cases xs₃ with x₄ xs₄, cases h,
  cases xs₄ with x₅ xs₅, swap 2, cases h,
  unfold translation, simp,
  delta translation, simp
end

def mk_hpp (g : vec_grid₀ cellT) : hpp :=
  ⟨g, X, cell_automatons.neumann, (λ_ neigh, translation neigh), cell_automatons.ext_one⟩

def hpp_g :=
  vec_grid₀.mk
    ⟨11, 11, dec_trivial,
    ⟨[X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, WE, X, X, X, S, X,
      E, X, X, X, E, X, W, X, X, N, N,
      X, X, X, X, X, N, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X,
      X, X, X, X, X, X, X, X, X, X, X], rfl⟩⟩
    ⟨0, 0⟩

def simple := mk_hpp hpp_g

end hpp

end hpp

author: FerdoSil

repo: LatticesAndCellularAutomata


text:
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Mario Carneiro
-/

import linear_algebra.basic

/-!
# Basics on bilinear maps

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file provides basics on bilinear maps. The most general form considered are maps that are
semilinear in both arguments. They are of type `M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P`, where `M` and `N`
are modules over `R` and `S` respectively, `P` is a module over both `R₂` and `S₂` with
commuting actions, and `ρ₁₂ : R →+* R₂` and `σ₁₂ : S →+* S₂`.

## Main declarations

* `linear_map.mk₂`: a constructor for bilinear maps,
  taking an unbundled function together with proof witnesses of bilinearity
* `linear_map.flip`: turns a bilinear map `M × N → P` into `N × M → P`
* `linear_map.lcomp` and `linear_map.llcomp`: composition of linear maps as a bilinear map
* `linear_map.compl₂`: composition of a bilinear map `M × N → P` with a linear map `Q → M`
* `linear_map.compr₂`: composition of a bilinear map `M × N → P` with a linear map `Q → N`
* `linear_map.lsmul`: scalar multiplication as a bilinear map `R × M → M`

## Tags

bilinear
-/

namespace linear_map

section semiring

-- the `ₗ` subscript variables are for special cases about linear (as opposed to semilinear) maps
variables {R : Type*} [semiring R] {S : Type*} [semiring S]
variables {R₂ : Type*} [semiring R₂] {S₂ : Type*} [semiring S₂]
variables {M : Type*} {N : Type*} {P : Type*}
variables {M₂ : Type*} {N₂ : Type*} {P₂ : Type*}
variables {Nₗ : Type*} {Pₗ : Type*}
variables {M' : Type*} {N' : Type*} {P' : Type*}

variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
variables [add_comm_monoid M₂] [add_comm_monoid N₂] [add_comm_monoid P₂]
variables [add_comm_monoid Nₗ] [add_comm_monoid Pₗ]
variables [add_comm_group M'] [add_comm_group N'] [add_comm_group P']
variables [module R M] [module S N] [module R₂ P] [module S₂ P]
variables [module R M₂] [module S N₂] [module R P₂] [module S₂ P₂]
variables [module R Pₗ] [module S Pₗ]
variables [module R M'] [module S N'] [module R₂ P'] [module S₂ P']
variables [smul_comm_class S₂ R₂ P] [smul_comm_class S R Pₗ] [smul_comm_class S₂ R₂ P']
variables [smul_comm_class S₂ R P₂]
variables {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}

variables (ρ₁₂ σ₁₂)
/-- Create a bilinear map from a function that is semilinear in each component.
See `mk₂'` and `mk₂` for the linear case. -/
def mk₂'ₛₗ (f : M → N → P)
  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c:R) m n, f (c • m) n = (ρ₁₂ c) • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c:S) m n, f m (c • n) = (σ₁₂ c) • f m n) : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P :=
{ to_fun := λ m, { to_fun := f m, map_add' := H3 m, map_smul' := λ c, H4 c m},
  map_add' := λ m₁ m₂, linear_map.ext $ H1 m₁ m₂,
  map_smul' := λ c m, linear_map.ext $ H2 c m }
variables {ρ₁₂ σ₁₂}

@[simp] theorem mk₂'ₛₗ_apply
  (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
  (mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) m n = f m n := rfl

variables (R S)
/-- Create a bilinear map from a function that is linear in each component.
See `mk₂` for the special case where both arguments come from modules over the same ring. -/
def mk₂' (f : M → N → Pₗ)
  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c:S) m n, f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[S] Pₗ :=
mk₂'ₛₗ (ring_hom.id R) (ring_hom.id S) f H1 H2 H3 H4
variables {R S}

@[simp] theorem mk₂'_apply
  (f : M → N → Pₗ) {H1 H2 H3 H4} (m : M) (n : N) :
  (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] Pₗ) m n = f m n := rfl

theorem ext₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
  (H : ∀ m n, f m n = g m n) : f = g :=
linear_map.ext (λ m, linear_map.ext $ λ n, H m n)

lemma congr_fun₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x y) : f x y = g x y :=
linear_map.congr_fun (linear_map.congr_fun h x) y

section

local attribute [instance] smul_comm_class.symm

/-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map from `M × N` to
`P`, change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
def flip (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P :=
mk₂'ₛₗ σ₁₂ ρ₁₂ (λ n m, f m n)
  (λ n₁ n₂ m, (f m).map_add _ _)
  (λ c n m, (f m).map_smulₛₗ _ _)
  (λ n m₁ m₂, by rw f.map_add; refl)
  (λ c n m, by rw f.map_smulₛₗ; refl)

end

@[simp] theorem flip_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) : flip f n m = f m n := rfl

@[simp] lemma flip_flip [smul_comm_class R₂ S₂ P] (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
  f.flip.flip = f := linear_map.ext₂ (λ x y, ((f.flip).flip_apply _ _).trans (f.flip_apply _ _))

open_locale big_operators

variables {R}
theorem flip_inj {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : flip f = flip g) : f = g :=
ext₂ $ λ m n, show flip f n m = flip g n m, by rw H

theorem map_zero₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y) : f 0 y = 0 :=
(flip f y).map_zero

theorem map_neg₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y) : f (-x) y = -f x y :=
(flip f y).map_neg _

theorem map_sub₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y z) : f (x - y) z = f x z - f y z :=
(flip f z).map_sub _ _

theorem map_add₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=
(flip f y).map_add _ _

theorem map_smul₂ (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R) (x y) : f (r • x) y = r • f x y :=
(flip f y).map_smul _ _

theorem map_smulₛₗ₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x y) : f (r • x) y = (ρ₁₂ r) • f x y :=
(flip f y).map_smulₛₗ _ _

theorem map_sum₂ {ι : Type*} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : finset ι) (x : ι → M) (y) :
  f (∑ i in t, x i) y = ∑ i in t, f (x i) y :=
(flip f y).map_sum

/-- Restricting a bilinear map in the second entry -/
def dom_restrict₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : submodule S N) :
  M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P :=
{ to_fun := λ m, (f m).dom_restrict q,
  map_add' := λ m₁ m₂, linear_map.ext $ λ _, by simp only [map_add, dom_restrict_apply, add_apply],
  map_smul' := λ c m, linear_map.ext $ λ _, by simp only [f.map_smulₛₗ, dom_restrict_apply,
    smul_apply]}

lemma dom_restrict₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : submodule S N) (x : M) (y : q) :
  f.dom_restrict₂ q x y = f x y := rfl

/-- Restricting a bilinear map in both components -/
def dom_restrict₁₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : submodule R M) (q : submodule S N) :
  p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P := (f.dom_restrict p).dom_restrict₂ q

lemma dom_restrict₁₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : submodule R M) (q : submodule S N)
  (x : p) (y : q) : f.dom_restrict₁₂ p q x y = f x y := rfl

end semiring

section comm_semiring

variables {R : Type*} [comm_semiring R] {R₂ : Type*} [comm_semiring R₂]
variables {R₃ : Type*} [comm_semiring R₃] {R₄ : Type*} [comm_semiring R₄]
variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
variables {Mₗ : Type*} {Nₗ : Type*} {Pₗ : Type*} {Qₗ Qₗ': Type*}

variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
variables [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ]
variables [add_comm_monoid Qₗ] [add_comm_monoid Qₗ']
variables [module R M] [module R₂ N] [module R₃ P] [module R₄ Q]
variables [module R Mₗ] [module R Nₗ] [module R Pₗ] [module R Qₗ] [module R Qₗ']
variables {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
variables {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
variables [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃]

variables (R)

/-- Create a bilinear map from a function that is linear in each component.

This is a shorthand for `mk₂'` for the common case when `R = S`. -/
def mk₂ (f : M → Nₗ → Pₗ)
  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c:R) m n, f m (c • n) = c • f m n) : M →ₗ[R] Nₗ →ₗ[R] Pₗ :=
mk₂' R R f H1 H2 H3 H4

@[simp] theorem mk₂_apply
  (f : M → Nₗ → Pₗ) {H1 H2 H3 H4} (m : M) (n : Nₗ) :
  (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] Nₗ →ₗ[R] Pₗ) m n = f m n := rfl

variables (R M N P)
/-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map `M → N → P`,
change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
def lflip : (M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →ₗ[R₃] N →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P :=
{ to_fun := flip, map_add' := λ _ _, rfl, map_smul' := λ _ _, rfl }
variables {R M N P}

variables (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)

@[simp] theorem lflip_apply (m : M) (n : N) : lflip R M N P f n m = f m n := rfl

variables (R Pₗ)
/-- Composing a linear map `M → N` and a linear map `N → P` to form a linear map `M → P`. -/
def lcomp (f : M →ₗ[R] Nₗ) : (Nₗ →ₗ[R] Pₗ) →ₗ[R] M →ₗ[R] Pₗ :=
flip $ linear_map.comp (flip id) f

variables {R Pₗ}

@[simp] theorem lcomp_apply (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) :
  lcomp R Pₗ f g x = g (f x) := rfl

theorem lcomp_apply' (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) :
  lcomp R Pₗ f g = g ∘ₗ f := rfl

variables (P σ₂₃)
/-- Composing a semilinear map `M → N` and a semilinear map `N → P` to form a semilinear map
`M → P` is itself a linear map. -/
def lcompₛₗ (f : M →ₛₗ[σ₁₂] N) : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P :=
flip $ linear_map.comp (flip id) f
variables {P σ₂₃}

include σ₁₃
@[simp] theorem lcompₛₗ_apply (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
  lcompₛₗ P σ₂₃ f g x = g (f x) := rfl
omit σ₁₃

variables (R M Nₗ Pₗ)
/-- Composing a linear map `M → N` and a linear map `N → P` to form a linear map `M → P`. -/
def llcomp : (Nₗ →ₗ[R] Pₗ) →ₗ[R] (M →ₗ[R] Nₗ) →ₗ[R] M →ₗ[R] Pₗ :=
flip { to_fun := lcomp R Pₗ,
       map_add' := λ f f', ext₂ $ λ g x, g.map_add _ _,
       map_smul' := λ (c : R) f, ext₂ $ λ g x, g.map_smul _ _ }
variables {R M Nₗ Pₗ}

section
@[simp] theorem llcomp_apply (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) (x : M) :
  llcomp R M Nₗ Pₗ f g x = f (g x) := rfl

theorem llcomp_apply' (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) :
  llcomp R M Nₗ Pₗ f g = f ∘ₗ g := rfl
end

/-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
form a bilinear map `M → Q → P`. -/
def compl₂ (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₃] Q →ₛₗ[σ₄₃] P := (lcompₛₗ _ _ g).comp f

include σ₄₃
@[simp]

@[simp] theorem compl₂_id : f.compl₂ linear_map.id = f :=
by { ext, rw [compl₂_apply, id_coe, id.def] }

/-- Composing linear maps `Q → M` and `Q' → N` with a bilinear map `M → N → P` to
form a bilinear map `Q → Q' → P`. -/
def compl₁₂ (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) :
  Qₗ →ₗ[R] Qₗ' →ₗ[R] Pₗ :=
(f.comp g).compl₂ g'

@[simp] theorem compl₁₂_apply (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ)
  (x : Qₗ) (y : Qₗ') : f.compl₁₂ g g' x y = f (g x) (g' y) := rfl

@[simp] theorem compl₁₂_id_id (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) :
  f.compl₁₂ (linear_map.id) (linear_map.id) = f :=
by { ext, simp_rw [compl₁₂_apply, id_coe, id.def] }

lemma compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ}
  (hₗ : function.surjective g) (hᵣ : function.surjective g') :
  f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂ :=
begin
  split; intros h,
  { -- B₁.comp l r = B₂.comp l r → B₁ = B₂
    ext x y,
    cases hₗ x with x' hx, subst hx,
    cases hᵣ y with y' hy, subst hy,
    convert linear_map.congr_fun₂ h x' y' },
  { -- B₁ = B₂ → B₁.comp l r = B₂.comp l r
    subst h },
end

/-- Composing a linear map `P → Q` and a bilinear map `M → N → P` to
form a bilinear map `M → N → Q`. -/
def compr₂ (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) : M →ₗ[R] Nₗ →ₗ[R] Qₗ :=
(llcomp R Nₗ Pₗ Qₗ g) ∘ₗ f

@[simp] theorem compr₂_apply (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (m : M) (n : Nₗ) :
  f.compr₂ g m n = g (f m n) := rfl

variables (R M)
/-- Scalar multiplication as a bilinear map `R → M → M`. -/
def lsmul : R →ₗ[R] M →ₗ[R] M :=
mk₂ R (•) add_smul (λ _ _ _, mul_smul _ _ _) smul_add
(λ r s m, by simp only [smul_smul, smul_eq_mul, mul_comm])
variables {R M}

@[simp] theorem lsmul_apply (r : R) (m : M) : lsmul R M r m = r • m := rfl

end comm_semiring

section comm_ring

variables {R R₂ S S₂ M N P : Type*}
variables {Mₗ Nₗ Pₗ : Type*}
variables [comm_ring R] [comm_ring S] [comm_ring R₂] [comm_ring S₂]

section add_comm_group

variables [add_comm_group M] [add_comm_group N] [add_comm_group P]
variables [module R M] [module S N] [module R₂ P] [module S₂ P]

lemma lsmul_injective [no_zero_smul_divisors R M] {x : R} (hx : x ≠ 0) :
  function.injective (lsmul R M x) :=
smul_right_injective _ hx

lemma ker_lsmul [no_zero_smul_divisors R M] {a : R} (ha : a ≠ 0) :
  (linear_map.lsmul R M a).ker = ⊥ :=
linear_map.ker_eq_bot_of_injective (linear_map.lsmul_injective ha)

end add_comm_group

end comm_ring

end linear_map


text:
/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
-/
import algebra.group_ring_action.basic
import algebra.hom.aut
import algebra.ring.equiv

/-!
# Ring automorphisms

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file defines the automorphism group structure on `ring_aut R := ring_equiv R R`.

## Implementation notes

The definition of multiplication in the automorphism group agrees with function composition,
multiplication in `equiv.perm`, and multiplication in `category_theory.End`, but not with
`category_theory.comp`.

This file is kept separate from `data/equiv/ring` so that `group_theory.perm` is free to use
equivalences (and other files that use them) before the group structure is defined.

## Tags

ring_aut
-/

/-- The group of ring automorphisms. -/
@[reducible] def ring_aut (R : Type*) [has_mul R] [has_add R] := ring_equiv R R

namespace ring_aut

section mul_add

variables (R : Type*) [has_mul R] [has_add R]

/--
The group operation on automorphisms of a ring is defined by
`λ g h, ring_equiv.trans h g`.
This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.
-/
instance : group (ring_aut R) :=
by refine_struct
{ mul := λ g h, ring_equiv.trans h g,
  one := ring_equiv.refl R,
  inv := ring_equiv.symm,
  div := _,
  npow := @npow_rec _ ⟨ring_equiv.refl R⟩ ⟨λ g h, ring_equiv.trans h g⟩,
  zpow := @zpow_rec _ ⟨ring_equiv.refl R⟩ ⟨λ g h, ring_equiv.trans h g⟩ ⟨ring_equiv.symm⟩ };
intros; ext; try { refl }; apply equiv.left_inv

instance : inhabited (ring_aut R) := ⟨1⟩

/-- Monoid homomorphism from ring automorphisms to additive automorphisms. -/
def to_add_aut : ring_aut R →* add_aut R :=
by refine_struct { to_fun := ring_equiv.to_add_equiv }; intros; refl

/-- Monoid homomorphism from ring automorphisms to multiplicative automorphisms. -/
def to_mul_aut : ring_aut R →* mul_aut R :=
by refine_struct { to_fun := ring_equiv.to_mul_equiv }; intros; refl

/-- Monoid homomorphism from ring automorphisms to permutations. -/
def to_perm : ring_aut R →* equiv.perm R :=
by refine_struct { to_fun := ring_equiv.to_equiv }; intros; refl

end mul_add

section semiring

variables {G R : Type*} [group G] [semiring R]

/-- The tautological action by the group of automorphism of a ring `R` on `R`.-/
instance apply_mul_semiring_action : mul_semiring_action (ring_aut R) R :=
{ smul := ($),
  smul_zero := ring_equiv.map_zero,
  smul_add := ring_equiv.map_add,
  smul_one := ring_equiv.map_one,
  smul_mul := ring_equiv.map_mul,
  one_smul := λ _, rfl,
  mul_smul := λ _ _ _, rfl }

@[simp]
protected lemma smul_def (f : ring_aut R) (r : R) : f • r = f r := rfl

instance apply_has_faithful_smul : has_faithful_smul (ring_aut R) R := ⟨λ _ _, ring_equiv.ext⟩

variables (G R)

/-- Each element of the group defines a ring automorphism.

This is a stronger version of `distrib_mul_action.to_add_aut` and
`mul_distrib_mul_action.to_mul_aut`. -/
@[simps] def _root_.mul_semiring_action.to_ring_aut [mul_semiring_action G R] : G →* ring_aut R :=
{ to_fun := mul_semiring_action.to_ring_equiv G R,
  map_mul' := λ g h, ring_equiv.ext $ mul_smul g h,
  map_one' := ring_equiv.ext $ one_smul _, }

end semiring

end ring_aut


text:
/-
Copyright (c) 2021 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Yury Kudryashov
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.topology.metric_space.isometry
import Mathlib.PostPort

universes u_6 u_7 u_8 l u_1 u_2 u_3 u_4 u_5

namespace Mathlib

/-!
# Linear isometries

In this file we define `linear_isometry R E F` (notation: `E →ₗᵢ[R] F`) to be a linear isometric
embedding of `E` into `F` and `linear_isometry_equiv` (notation: `E ≃ₗᵢ[R] F`) to be a linear
isometric equivalence between `E` and `F`.

We also prove some trivial lemmas and provide convenience constructors.
-/

/-- An `R`-linear isometric embedding of one normed `R`-module into another. -/
structure linear_isometry (R : Type u_6) (E : Type u_7) (F : Type u_8) [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F]
    extends linear_map R E F where
  norm_map' : ∀ (x : E), norm (coe_fn _to_linear_map x) = norm x

namespace linear_isometry

protected instance has_coe_to_fun {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F] :
    has_coe_to_fun (linear_isometry R E F) :=
  has_coe_to_fun.mk (fun (f : linear_isometry R E F) => E → F)
    fun (f : linear_isometry R E F) => linear_map.to_fun (to_linear_map f)

@[simp] theorem coe_to_linear_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : ⇑(to_linear_map f) = ⇑f :=
  rfl

theorem to_linear_map_injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F] :
    function.injective to_linear_map :=
  sorry

theorem coe_fn_injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] :
    function.injective fun (f : linear_isometry R E F) (x : E) => coe_fn f x :=
  function.injective.comp linear_map.coe_injective to_linear_map_injective

theorem ext {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] {f : linear_isometry R E F}
    {g : linear_isometry R E F} (h : ∀ (x : E), coe_fn f x = coe_fn g x) : f = g :=
  coe_fn_injective (funext h)

@[simp] theorem map_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) :
    coe_fn f 0 = 0 :=
  linear_map.map_zero (to_linear_map f)

@[simp] theorem map_add {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (x : E) (y : E) :
    coe_fn f (x + y) = coe_fn f x + coe_fn f y :=
  linear_map.map_add (to_linear_map f) x y

@[simp] theorem map_sub {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (x : E) (y : E) :
    coe_fn f (x - y) = coe_fn f x - coe_fn f y :=
  linear_map.map_sub (to_linear_map f) x y

@[simp] theorem map_smul {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (c : R) (x : E) :
    coe_fn f (c • x) = c • coe_fn f x :=
  linear_map.map_smul (to_linear_map f) c x

@[simp] theorem norm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (x : E) :
    norm (coe_fn f x) = norm x :=
  norm_map' f x

@[simp] theorem nnnorm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F)
    (x : E) : nnnorm (coe_fn f x) = nnnorm x :=
  nnreal.eq (norm_map f x)

protected theorem isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : isometry ⇑f :=
  add_monoid_hom.isometry_of_norm (linear_map.to_add_monoid_hom (to_linear_map f)) (norm_map f)

@[simp] theorem dist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (x : E) (y : E) :
    dist (coe_fn f x) (coe_fn f y) = dist x y :=
  isometry.dist_eq (linear_isometry.isometry f) x y

@[simp] theorem edist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (x : E) (y : E) :
    edist (coe_fn f x) (coe_fn f y) = edist x y :=
  isometry.edist_eq (linear_isometry.isometry f) x y

protected theorem injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : function.injective ⇑f :=
  isometry.injective (linear_isometry.isometry f)

theorem map_eq_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) {x : E} {y : E} :
    coe_fn f x = coe_fn f y ↔ x = y :=
  function.injective.eq_iff (linear_isometry.injective f)

theorem map_ne {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) {x : E} {y : E}
    (h : x ≠ y) : coe_fn f x ≠ coe_fn f y :=
  function.injective.ne (linear_isometry.injective f) h

protected theorem lipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : lipschitz_with 1 ⇑f :=
  isometry.lipschitz (linear_isometry.isometry f)

protected theorem antilipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : antilipschitz_with 1 ⇑f :=
  isometry.antilipschitz (linear_isometry.isometry f)

protected theorem continuous {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : continuous ⇑f :=
  isometry.continuous (linear_isometry.isometry f)

theorem ediam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (s : set E) :
    emetric.diam (⇑f '' s) = emetric.diam s :=
  isometry.ediam_image (linear_isometry.isometry f) s

theorem ediam_range {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) :
    emetric.diam (set.range ⇑f) = emetric.diam set.univ :=
  isometry.ediam_range (linear_isometry.isometry f)

theorem diam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) (s : set E) :
    metric.diam (⇑f '' s) = metric.diam s :=
  isometry.diam_image (linear_isometry.isometry f) s

theorem diam_range {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) :
    metric.diam (set.range ⇑f) = metric.diam set.univ :=
  isometry.diam_range (linear_isometry.isometry f)

/-- Interpret a linear isometry as a continuous linear map. -/
def to_continuous_linear_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : continuous_linear_map R E F :=
  continuous_linear_map.mk (to_linear_map f)

@[simp] theorem coe_to_continuous_linear_map {R : Type u_1} {E : Type u_2} {F : Type u_3}
    [semiring R] [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (f : linear_isometry R E F) : ⇑(to_continuous_linear_map f) = ⇑f :=
  rfl

@[simp] theorem comp_continuous_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F)
    {α : Type u_4} [topological_space α] {g : α → E} : continuous (⇑f ∘ g) ↔ continuous g :=
  sorry

/-- The identity linear isometry. -/
def id {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E] [semimodule R E] :
    linear_isometry R E E :=
  mk linear_map.id sorry

@[simp] theorem coe_id {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : ⇑id = ⇑id :=
  rfl

protected instance inhabited {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : Inhabited (linear_isometry R E E) :=
  { default := id }

/-- Composition of linear isometries. -/
def comp {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [normed_group E]
    [normed_group F] [normed_group G] [semimodule R E] [semimodule R F] [semimodule R G]
    (g : linear_isometry R F G) (f : linear_isometry R E F) : linear_isometry R E G :=
  mk (linear_map.comp (to_linear_map g) (to_linear_map f)) sorry

@[simp] theorem coe_comp {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R]
    [normed_group E] [normed_group F] [normed_group G] [semimodule R E] [semimodule R F]
    [semimodule R G] (g : linear_isometry R F G) (f : linear_isometry R E F) :
    ⇑(comp g f) = ⇑g ∘ ⇑f :=
  rfl

@[simp] theorem id_comp {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) :
    comp id f = f :=
  ext fun (x : E) => rfl

@[simp] theorem comp_id {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (f : linear_isometry R E F) :
    comp f id = f :=
  ext fun (x : E) => rfl

theorem comp_assoc {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5}
    [semiring R] [normed_group E] [normed_group F] [normed_group G] [normed_group G']
    [semimodule R E] [semimodule R F] [semimodule R G] [semimodule R G']
    (f : linear_isometry R G G') (g : linear_isometry R F G) (h : linear_isometry R E F) :
    comp (comp f g) h = comp f (comp g h) :=
  rfl

protected instance monoid {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : monoid (linear_isometry R E E) :=
  monoid.mk comp comp_assoc id id_comp comp_id

@[simp] theorem coe_one {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : ⇑1 = ⇑id :=
  rfl

@[simp] theorem coe_mul {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E] [semimodule R E]
    (f : linear_isometry R E E) (g : linear_isometry R E E) : ⇑(f * g) = ⇑f ∘ ⇑g :=
  rfl

end linear_isometry

/-- A linear isometric equivalence between two normed vector spaces. -/
structure linear_isometry_equiv (R : Type u_6) (E : Type u_7) (F : Type u_8) [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    extends linear_equiv R E F where
  norm_map' : ∀ (x : E), norm (coe_fn _to_linear_equiv x) = norm x

namespace linear_isometry_equiv

protected instance has_coe_to_fun {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F] :
    has_coe_to_fun (linear_isometry_equiv R E F) :=
  has_coe_to_fun.mk (fun (f : linear_isometry_equiv R E F) => E → F)
    fun (f : linear_isometry_equiv R E F) => linear_equiv.to_fun (to_linear_equiv f)

@[simp] theorem coe_mk {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_equiv R E F)
    (he : ∀ (x : E), norm (coe_fn e x) = norm x) : ⇑(mk e he) = ⇑e :=
  rfl

@[simp] theorem coe_to_linear_equiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : ⇑(to_linear_equiv e) = ⇑e :=
  rfl

theorem to_linear_equiv_injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F] :
    function.injective to_linear_equiv :=
  sorry

theorem ext {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] {e : linear_isometry_equiv R E F}
    {e' : linear_isometry_equiv R E F} (h : ∀ (x : E), coe_fn e x = coe_fn e' x) : e = e' :=
  to_linear_equiv_injective (linear_equiv.ext h)

/-- Construct a `linear_isometry_equiv` from a `linear_equiv` and two inequalities:
`∀ x, ∥e x∥ ≤ ∥x∥` and `∀ y, ∥e.symm y∥ ≤ ∥y∥`. -/
def of_bounds {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_equiv R E F)
    (h₁ : ∀ (x : E), norm (coe_fn e x) ≤ norm x)
    (h₂ : ∀ (y : F), norm (coe_fn (linear_equiv.symm e) y) ≤ norm y) :
    linear_isometry_equiv R E F :=
  mk e sorry

@[simp] theorem norm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) (x : E) :
    norm (coe_fn e x) = norm x :=
  norm_map' e x

/-- Reinterpret a `linear_isometry_equiv` as a `linear_isometry`. -/
def to_linear_isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) :
    linear_isometry R E F :=
  linear_isometry.mk (↑(to_linear_equiv e)) (norm_map' e)

protected theorem isometry {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : isometry ⇑e :=
  linear_isometry.isometry (to_linear_isometry e)

/-- Reinterpret a `linear_isometry_equiv` as an `isometric`. -/
def to_isometric {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) : E ≃ᵢ F :=
  isometric.mk (linear_equiv.to_equiv (to_linear_equiv e)) (linear_isometry_equiv.isometry e)

protected theorem continuous {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : continuous ⇑e :=
  isometry.continuous (linear_isometry_equiv.isometry e)

/-- Identity map as a `linear_isometry_equiv`. -/
def refl (R : Type u_1) (E : Type u_2) [semiring R] [normed_group E] [semimodule R E] :
    linear_isometry_equiv R E E :=
  mk (linear_equiv.refl R E) sorry

protected instance inhabited {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : Inhabited (linear_isometry_equiv R E E) :=
  { default := refl R E }

@[simp] theorem coe_refl {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : ⇑(refl R E) = id :=
  rfl

/-- The inverse `linear_isometry_equiv`. -/
def symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E] [normed_group F]
    [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) :
    linear_isometry_equiv R F E :=
  mk (linear_equiv.symm (to_linear_equiv e)) sorry

@[simp] theorem apply_symm_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) (x : F) : coe_fn e (coe_fn (symm e) x) = x :=
  linear_equiv.apply_symm_apply (to_linear_equiv e) x

@[simp] theorem symm_apply_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) (x : E) : coe_fn (symm e) (coe_fn e x) = x :=
  linear_equiv.symm_apply_apply (to_linear_equiv e) x

@[simp] theorem map_eq_zero_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) {x : E} : coe_fn e x = 0 ↔ x = 0 :=
  linear_equiv.map_eq_zero_iff (to_linear_equiv e)

@[simp] theorem symm_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) :
    symm (symm e) = e :=
  ext fun (x : E) => rfl

@[simp] theorem coe_symm_to_linear_equiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : ⇑(linear_equiv.symm (to_linear_equiv e)) = ⇑(symm e) :=
  rfl

/-- Composition of `linear_isometry_equiv`s as a `linear_isometry_equiv`. -/
def trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R] [normed_group E]
    [normed_group F] [normed_group G] [semimodule R E] [semimodule R F] [semimodule R G]
    (e : linear_isometry_equiv R E F) (e' : linear_isometry_equiv R F G) :
    linear_isometry_equiv R E G :=
  mk (linear_equiv.trans (to_linear_equiv e) (to_linear_equiv e')) sorry

@[simp] theorem coe_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [semiring R]
    [normed_group E] [normed_group F] [normed_group G] [semimodule R E] [semimodule R F]
    [semimodule R G] (e₁ : linear_isometry_equiv R E F) (e₂ : linear_isometry_equiv R F G) :
    ⇑(trans e₁ e₂) = ⇑e₂ ∘ ⇑e₁ :=
  rfl

@[simp] theorem trans_refl {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : trans e (refl R F) = e :=
  ext fun (x : E) => rfl

@[simp] theorem refl_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : trans (refl R E) e = e :=
  ext fun (x : E) => rfl

@[simp] theorem trans_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : trans e (symm e) = refl R E :=
  ext (symm_apply_apply e)

@[simp] theorem symm_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : trans (symm e) e = refl R F :=
  ext (apply_symm_apply e)

@[simp] theorem coe_symm_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4}
    [semiring R] [normed_group E] [normed_group F] [normed_group G] [semimodule R E]
    [semimodule R F] [semimodule R G] (e₁ : linear_isometry_equiv R E F)
    (e₂ : linear_isometry_equiv R F G) : ⇑(symm (trans e₁ e₂)) = ⇑(symm e₁) ∘ ⇑(symm e₂) :=
  rfl

theorem trans_assoc {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {G' : Type u_5}
    [semiring R] [normed_group E] [normed_group F] [normed_group G] [normed_group G']
    [semimodule R E] [semimodule R F] [semimodule R G] [semimodule R G']
    (eEF : linear_isometry_equiv R E F) (eFG : linear_isometry_equiv R F G)
    (eGG' : linear_isometry_equiv R G G') :
    trans eEF (trans eFG eGG') = trans (trans eEF eFG) eGG' :=
  rfl

protected instance group {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : group (linear_isometry_equiv R E E) :=
  group.mk (fun (e₁ e₂ : linear_isometry_equiv R E E) => trans e₂ e₁) sorry (refl R E) trans_refl
    refl_trans symm
    (div_inv_monoid.div._default (fun (e₁ e₂ : linear_isometry_equiv R E E) => trans e₂ e₁) sorry
      (refl R E) trans_refl refl_trans symm)
    trans_symm

@[simp] theorem coe_one {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E]
    [semimodule R E] : ⇑1 = id :=
  rfl

@[simp] theorem coe_mul {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E] [semimodule R E]
    (e : linear_isometry_equiv R E E) (e' : linear_isometry_equiv R E E) : ⇑(e * e') = ⇑e ∘ ⇑e' :=
  rfl

@[simp] theorem coe_inv {R : Type u_1} {E : Type u_2} [semiring R] [normed_group E] [semimodule R E]
    (e : linear_isometry_equiv R E E) : ⇑(e⁻¹) = ⇑(symm e) :=
  rfl

/-- Reinterpret a `linear_isometry_equiv` as a `continuous_linear_equiv`. -/
def to_continuous_linear_equiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : continuous_linear_equiv R E F :=
  continuous_linear_equiv.mk (to_linear_equiv e)

@[simp] theorem map_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) :
    coe_fn e 0 = 0 :=
  linear_equiv.map_zero (to_linear_equiv e)

@[simp] theorem map_add {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) (x : E)
    (y : E) : coe_fn e (x + y) = coe_fn e x + coe_fn e y :=
  linear_equiv.map_add (to_linear_equiv e) x y

@[simp] theorem map_sub {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) (x : E)
    (y : E) : coe_fn e (x - y) = coe_fn e x - coe_fn e y :=
  linear_equiv.map_sub (to_linear_equiv e) x y

@[simp] theorem map_smul {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) (c : R)
    (x : E) : coe_fn e (c • x) = c • coe_fn e x :=
  linear_equiv.map_smul (to_linear_equiv e) c x

@[simp] theorem nnnorm_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) (x : E) : nnnorm (coe_fn e x) = nnnorm x :=
  linear_isometry.nnnorm_map (to_linear_isometry e) x

@[simp] theorem dist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) (x : E)
    (y : E) : dist (coe_fn e x) (coe_fn e y) = dist x y :=
  linear_isometry.dist_map (to_linear_isometry e) x y

@[simp] theorem edist_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) (x : E)
    (y : E) : edist (coe_fn e x) (coe_fn e y) = edist x y :=
  linear_isometry.edist_map (to_linear_isometry e) x y

protected theorem bijective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : function.bijective ⇑e :=
  linear_equiv.bijective (to_linear_equiv e)

protected theorem injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : function.injective ⇑e :=
  linear_equiv.injective (to_linear_equiv e)

protected theorem surjective {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : function.surjective ⇑e :=
  linear_equiv.surjective (to_linear_equiv e)

theorem map_eq_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) {x : E}
    {y : E} : coe_fn e x = coe_fn e y ↔ x = y :=
  function.injective.eq_iff (linear_isometry_equiv.injective e)

theorem map_ne {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F) {x : E}
    {y : E} (h : x ≠ y) : coe_fn e x ≠ coe_fn e y :=
  function.injective.ne (linear_isometry_equiv.injective e) h

protected theorem lipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : lipschitz_with 1 ⇑e :=
  isometry.lipschitz (linear_isometry_equiv.isometry e)

protected theorem antilipschitz {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R]
    [normed_group E] [normed_group F] [semimodule R E] [semimodule R F]
    (e : linear_isometry_equiv R E F) : antilipschitz_with 1 ⇑e :=
  isometry.antilipschitz (linear_isometry_equiv.isometry e)

theorem ediam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F)
    (s : set E) : emetric.diam (⇑e '' s) = emetric.diam s :=
  isometry.ediam_image (linear_isometry_equiv.isometry e) s

theorem diam_image {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [normed_group E]
    [normed_group F] [semimodule R E] [semimodule R F] (e : linear_isometry_equiv R E F)
    (s : set E) : metric.diam (⇑e '' s) = metric.diam s :=
  isometry.diam_image (linear_isometry_equiv.isometry e) s

end Mathlib

author: AurelienSaue


import topology.basic
import topology.compact_open
import data.nat.prime
import data.real.basic
import data.real.irrational
import data.complex.basic
import data.fin.basic
import geometry.euclidean.basic
import analysis.inner_product_space.pi_L2
import algebra.group.defs
import algebra.field.basic
import combinatorics.configuration
import ring_theory.polynomial.basic
import group_theory.free_group
import combinatorics.simple_graph.basic
import ring_theory.integral_closure
import data.fintype.card
import category_theory.category.basic
import ring_theory.discrete_valuation_ring
import group_theory.torsion
import linear_algebra.matrix.charpoly.basic
import algebra.order.absolute_value
import analysis.convex.basic
import topology.uniform_space.uniform_convergence_topology
import topology.sequences
import analysis.normed.group.infinite_sum
import data.nat.choose.sum
import group_theory.specific_groups.cyclic
import group_theory.order_of_element
import analysis.mean_inequalities
import analysis.normed_space.banach
import topology.algebra.continuous_monoid_hom
import linear_algebra.matrix.symmetric
import analysis.inner_product_space.spectrum
import ring_theory.class_group
import ring_theory.dedekind_domain.basic
import ring_theory.principal_ideal_domain
import model_theory.satisfiability
import probability.integration
import ring_theory.simple_module
import category_theory.preadditive.schur
import representation_theory.maschke
import topology.paracompact
import combinatorics.simple_graph.coloring
--Prove that \mathbb{R}^n is paracompact in Lean mathlib

--OUTPUT 1
theorem paracompact_real_n (n : ℕ) : paracompact_space (euclidean_space n) :=
begin
  sorry

--OUTPUT 2
theorem paracompact_real_n (n : ℕ) : paracompact_space (euclidean_space n) :=
begin
  sorry

--OUTPUT 3
theorem paracompact_Rn : paracompact (euclidean_space n) :=
begin
  --Let's start by proving that \mathbb{R}^n is locally compact
  let X := euclidean_space n,
  have H_loc_comp : locally_compact_space X,
  {
    --We need to show that every point has a compact neighborhood
    intros x,
    --Let's start by proving that the ball of radius 1 around x is compact
    have H_compact : compact_space (ball x 1),
    {
      --We need to show that every open cover of the ball has a finite subcover
      intros U H_cover,
      --Let's start by showing that the ball is covered by the open balls of radius 1/2
      --centered at the points of U
      have H_cover_2 : ∀ (u : X), u ∈ U → ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2) :=
      begin
        intros u H_u,
        --Let's prove that every point in the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        intros y H_y,
        --Let's start by proving that y is covered by the open ball of radius 1/2 centered at u
        have H_y_u : y ∈ ball u (1/2),
        {
          --Let's start by proving that the distance between y and u is less than 1/2
          have H_dist : dist y u < 1/2,
          {
            --Let's start by proving that the distance between y and x is less than 1
            have H_dist_2 : dist y x < 1,
            {
              --This follows from the fact that y is in the ball of radius 1 around x
              exact H_y,
            },
            --Let's prove that the distance between x and u is less than 1/2
            have H_dist_3 : dist x u < 1/2,
            {
              --This follows from the fact that u is in the open ball of radius 1 around x
              exact H_u,
            },
            --Let's prove that the distance between y and u is less than 1/2
            have H_dist_4 : dist y u < 1/2,
            {
              --This follows from the triangle inequality
              exact dist_triangle_lt _ _ _ H_dist_2 H_dist_3,
            },
            --This is what we wanted to prove
            exact H_dist_4,
          },
          --This is what we wanted to prove
          exact ball_subset_ball_of_dist_lt _ _ H_dist,
        },
        --This is what we wanted to prove
        exact mem_bUnion H_u H_y_u,
      end,
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_3 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that every point in the ball is covered by the open balls
        --of radius 1/2 centered at the points of U
        exact ball_subset_bUnion_of_mem H_cover_2,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_4 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_3,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_5 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_4,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_6 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_5,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_7 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_6,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_8 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_7,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_9 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_8,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_10 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_9,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_11 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_10,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_12 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_11,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_13 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2
        --centered at the points of U
        exact H_cover_12,
      },
      --Let's prove that the ball is covered by the open balls of radius 1/2 centered at the
      --points of U
      have H_cover_14 : ball x 1 ⊆ ⋃ (v : X), v ∈ U ∧ ball v (1/2),
      {
        --This follows from the fact that the ball is covered by the open balls of radius 1/2


text:
/-
Copyright (c) 2017 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import .support
open tactic expr

namespace hott

private meta def open_pis : expr → tactic (expr × list expr) | e := do
e ← whnf e,
if e.is_pi then do
    x ← mk_local' e.binding_name e.binding_info e.binding_domain,
    (e, xs) ← open_pis (e.binding_body.instantiate_var x),
    return (e, x::xs)
else return (e, [])

/- For any hott-equality proven by reflexivity, we add a Prop-equality lemma equating the same, which is used for dsimp -/
private meta def copy_idp_lemma (cn : name) (prio : option ℕ) (pers : bool) : tactic unit := do
let rfl_lemma_name := cn <.> "_idp_to_rfl",
d ← get_decl cn,
(t, xs) ← open_pis d.type,
match t.get_app_fn with
| (const `hott.eq [u]) := do
    [A, lhs, rhs] ← return t.get_app_args,
    is_idp ← option.is_some <$> try_core (is_def_eq lhs rhs), when is_idp $ do
    let t' := pis xs (app_of_list (const ``eq [u.succ]) [A, lhs, rhs]),
    let v' := lambdas xs (app_of_list (const ``rfl [u.succ]) [A, lhs]),
    add_decl (mk_definition rfl_lemma_name d.univ_params t' v'),
    set_basic_attribute `_refl_lemma rfl_lemma_name tt,
    set_basic_attribute `simp rfl_lemma_name tt
| _ := skip
end

-- TODO(gabriel): propagate priority & persistence (currently crashes)

@[user_attribute]
meta def hsimp_attr : user_attribute := {
    name := `hsimp,
    descr := "HoTT simplification lemma (converts idp-lemmas to rfl-lemmas for dsimp)",
    after_set := some (λ n prio pers, do
        copy_idp_lemma n none pers,
        set_basic_attribute `simp n pers none),
}

end hott

author: gebner


text:
/-
Copyright (c) 2022 Thomas Browning. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Thomas Browning

! This file was ported from Lean 3 source module topology.algebra.continuous_monoid_hom
! leanprover-community/mathlib commit 6ca1a09bc9aa75824bf97388c9e3b441fc4ccf3f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Analysis.Complex.Circle
import Mathbin.Topology.ContinuousFunction.Algebra

/-!

# Continuous Monoid Homs

This file defines the space of continuous homomorphisms between two topological groups.

## Main definitions

* `continuous_monoid_hom A B`: The continuous homomorphisms `A →* B`.
* `continuous_add_monoid_hom A B`: The continuous additive homomorphisms `A →+ B`.
-/

open Pointwise

open Function

variable (F A B C D E : Type _) [Monoid A] [Monoid B] [Monoid C] [Monoid D] [CommGroup E]
  [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D]
  [TopologicalSpace E] [TopologicalGroup E]

/-- The type of continuous additive monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : continuous_add_monoid_hom A B)`,
you should parametrize over `(F : Type*) [continuous_add_monoid_hom_class F A B] (f : F)`.

When you extend this structure, make sure to extend `continuous_add_monoid_hom_class`. -/
structure ContinuousAddMonoidHom (A B : Type _) [AddMonoid A] [AddMonoid B] [TopologicalSpace A]
  [TopologicalSpace B] extends A →+ B where
  continuous_toFun : Continuous to_fun
#align continuous_add_monoid_hom ContinuousAddMonoidHom

/-- The type of continuous monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : continuous_monoid_hom A B)`,
you should parametrize over `(F : Type*) [continuous_monoid_hom_class F A B] (f : F)`.

When you extend this structure, make sure to extend `continuous_add_monoid_hom_class`. -/
@[to_additive]
structure ContinuousMonoidHom extends A →* B where
  continuous_toFun : Continuous to_fun
#align continuous_monoid_hom ContinuousMonoidHom
#align continuous_add_monoid_hom ContinuousAddMonoidHom

section

/-- `continuous_add_monoid_hom_class F A B` states that `F` is a type of continuous additive monoid
homomorphisms.

You should also extend this typeclass when you extend `continuous_add_monoid_hom`. -/
class ContinuousAddMonoidHomClass (A B : Type _) [AddMonoid A] [AddMonoid B] [TopologicalSpace A]
  [TopologicalSpace B] extends AddMonoidHomClass F A B where
  map_continuous (f : F) : Continuous f
#align continuous_add_monoid_hom_class ContinuousAddMonoidHomClass

/-- `continuous_monoid_hom_class F A B` states that `F` is a type of continuous additive monoid
homomorphisms.

You should also extend this typeclass when you extend `continuous_monoid_hom`. -/
@[to_additive]
class ContinuousMonoidHomClass extends MonoidHomClass F A B where
  map_continuous (f : F) : Continuous f
#align continuous_monoid_hom_class ContinuousMonoidHomClass
#align continuous_add_monoid_hom_class ContinuousAddMonoidHomClass

attribute [to_additive ContinuousAddMonoidHomClass.toAddMonoidHomClass]
  ContinuousMonoidHomClass.toMonoidHomClass

end

/-- Reinterpret a `continuous_monoid_hom` as a `monoid_hom`. -/
add_decl_doc ContinuousMonoidHom.toMonoidHom

/-- Reinterpret a `continuous_add_monoid_hom` as an `add_monoid_hom`. -/
add_decl_doc ContinuousAddMonoidHom.toAddMonoidHom

-- See note [lower instance priority]
@[to_additive]
instance (priority := 100) ContinuousMonoidHomClass.toContinuousMapClass
    [ContinuousMonoidHomClass F A B] : ContinuousMapClass F A B :=
  { ‹ContinuousMonoidHomClass F A B› with }
#align continuous_monoid_hom_class.to_continuous_map_class ContinuousMonoidHomClass.toContinuousMapClass
#align continuous_add_monoid_hom_class.to_continuous_map_class ContinuousAddMonoidHomClass.to_continuous_map_class

namespace ContinuousMonoidHom

variable {A B C D E}

@[to_additive]
instance : ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B
    where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr
  map_mul f := f.map_mul'
  map_one f := f.map_one'
  map_continuous f := f.continuous_toFun

/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
directly. -/
@[to_additive
      "Helper instance for when there's too many metavariables to apply\n`fun_like.has_coe_to_fun` directly."]
instance : CoeFun (ContinuousMonoidHom A B) fun _ => A → B :=
  FunLike.hasCoeToFun

@[to_additive, ext]
theorem ext {f g : ContinuousMonoidHom A B} (h : ∀ x, f x = g x) : f = g :=
  FunLike.ext _ _ h
#align continuous_monoid_hom.ext ContinuousMonoidHom.ext
#align continuous_add_monoid_hom.ext ContinuousAddMonoidHom.ext

/-- Reinterpret a `continuous_monoid_hom` as a `continuous_map`. -/
@[to_additive "Reinterpret a `continuous_add_monoid_hom` as a `continuous_map`."]
def toContinuousMap (f : ContinuousMonoidHom A B) : C(A, B) :=
  { f with }
#align continuous_monoid_hom.to_continuous_map ContinuousMonoidHom.toContinuousMap
#align continuous_add_monoid_hom.to_continuous_map ContinuousAddMonoidHom.toContinuousMap

@[to_additive]
theorem toContinuousMap_injective : Injective (toContinuousMap : _ → C(A, B)) := fun f g h =>
  ext <| by convert FunLike.ext_iff.1 h
#align continuous_monoid_hom.to_continuous_map_injective ContinuousMonoidHom.toContinuousMap_injective
#align continuous_add_monoid_hom.to_continuous_map_injective ContinuousAddMonoidHom.toContinuousMap_injective

/-- Construct a `continuous_monoid_hom` from a `continuous` `monoid_hom`. -/
@[to_additive "Construct a `continuous_add_monoid_hom` from a `continuous` `add_monoid_hom`.",
  simps]
def mk' (f : A →* B) (hf : Continuous f) : ContinuousMonoidHom A B :=
  { f with continuous_toFun := hf }
#align continuous_monoid_hom.mk' ContinuousMonoidHom.mk'
#align continuous_add_monoid_hom.mk' ContinuousAddMonoidHom.mk'

/-- Composition of two continuous homomorphisms. -/
@[to_additive "Composition of two continuous homomorphisms.", simps]
def comp (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : ContinuousMonoidHom A C :=
  mk' (g.toMonoidHom.comp f.toMonoidHom) (g.continuous_toFun.comp f.continuous_toFun)
#align continuous_monoid_hom.comp ContinuousMonoidHom.comp
#align continuous_add_monoid_hom.comp ContinuousAddMonoidHom.comp

/-- Product of two continuous homomorphisms on the same space. -/
@[to_additive "Product of two continuous homomorphisms on the same space.", simps]
def prod (f : ContinuousMonoidHom A B) (g : ContinuousMonoidHom A C) :
    ContinuousMonoidHom A (B × C) :=
  mk' (f.toMonoidHom.Prod g.toMonoidHom) (f.continuous_toFun.prod_mk g.continuous_toFun)
#align continuous_monoid_hom.prod ContinuousMonoidHom.prod
#align continuous_add_monoid_hom.sum ContinuousAddMonoidHom.sum

/-- Product of two continuous homomorphisms on different spaces. -/
@[to_additive "Product of two continuous homomorphisms on different spaces.", simps]
def prodMap (f : ContinuousMonoidHom A C) (g : ContinuousMonoidHom B D) :
    ContinuousMonoidHom (A × B) (C × D) :=
  mk' (f.toMonoidHom.Prod_map g.toMonoidHom) (f.continuous_toFun.Prod_map g.continuous_toFun)
#align continuous_monoid_hom.prod_map ContinuousMonoidHom.prodMap
#align continuous_add_monoid_hom.sum_map ContinuousAddMonoidHom.sumMap

variable (A B C D E)

/-- The trivial continuous homomorphism. -/
@[to_additive "The trivial continuous homomorphism.", simps]
def one : ContinuousMonoidHom A B :=
  mk' 1 continuous_const
#align continuous_monoid_hom.one ContinuousMonoidHom.one
#align continuous_add_monoid_hom.zero ContinuousAddMonoidHom.zero

@[to_additive]
instance : Inhabited (ContinuousMonoidHom A B) :=
  ⟨one A B⟩

/-- The identity continuous homomorphism. -/
@[to_additive "The identity continuous homomorphism.", simps]
def id : ContinuousMonoidHom A A :=
  mk' (MonoidHom.id A) continuous_id
#align continuous_monoid_hom.id ContinuousMonoidHom.id
#align continuous_add_monoid_hom.id ContinuousAddMonoidHom.id

/-- The continuous homomorphism given by projection onto the first factor. -/
@[to_additive "The continuous homomorphism given by projection onto the first factor.", simps]
def fst : ContinuousMonoidHom (A × B) A :=
  mk' (MonoidHom.fst A B) continuous_fst
#align continuous_monoid_hom.fst ContinuousMonoidHom.fst
#align continuous_add_monoid_hom.fst ContinuousAddMonoidHom.fst

/-- The continuous homomorphism given by projection onto the second factor. -/
@[to_additive "The continuous homomorphism given by projection onto the second factor.", simps]
def snd : ContinuousMonoidHom (A × B) B :=
  mk' (MonoidHom.snd A B) continuous_snd
#align continuous_monoid_hom.snd ContinuousMonoidHom.snd
#align continuous_add_monoid_hom.snd ContinuousAddMonoidHom.snd

/-- The continuous homomorphism given by inclusion of the first factor. -/
@[to_additive "The continuous homomorphism given by inclusion of the first factor.", simps]
def inl : ContinuousMonoidHom A (A × B) :=
  prod (id A) (one A B)
#align continuous_monoid_hom.inl ContinuousMonoidHom.inl
#align continuous_add_monoid_hom.inl ContinuousAddMonoidHom.inl

/-- The continuous homomorphism given by inclusion of the second factor. -/
@[to_additive "The continuous homomorphism given by inclusion of the second factor.", simps]
def inr : ContinuousMonoidHom B (A × B) :=
  prod (one B A) (id B)
#align continuous_monoid_hom.inr ContinuousMonoidHom.inr
#align continuous_add_monoid_hom.inr ContinuousAddMonoidHom.inr

/-- The continuous homomorphism given by the diagonal embedding. -/
@[to_additive "The continuous homomorphism given by the diagonal embedding.", simps]
def diag : ContinuousMonoidHom A (A × A) :=
  prod (id A) (id A)
#align continuous_monoid_hom.diag ContinuousMonoidHom.diag
#align continuous_add_monoid_hom.diag ContinuousAddMonoidHom.diag

/-- The continuous homomorphism given by swapping components. -/
@[to_additive "The continuous homomorphism given by swapping components.", simps]
def swap : ContinuousMonoidHom (A × B) (B × A) :=
  prod (snd A B) (fst A B)
#align continuous_monoid_hom.swap ContinuousMonoidHom.swap
#align continuous_add_monoid_hom.swap ContinuousAddMonoidHom.swap

/-- The continuous homomorphism given by multiplication. -/
@[to_additive "The continuous homomorphism given by addition.", simps]
def mul : ContinuousMonoidHom (E × E) E :=
  mk' mulMonoidHom continuous_mul
#align continuous_monoid_hom.mul ContinuousMonoidHom.mul
#align continuous_add_monoid_hom.add ContinuousAddMonoidHom.add

/-- The continuous homomorphism given by inversion. -/
@[to_additive "The continuous homomorphism given by negation.", simps]
def inv : ContinuousMonoidHom E E :=
  mk' invMonoidHom continuous_inv
#align continuous_monoid_hom.inv ContinuousMonoidHom.inv
#align continuous_add_monoid_hom.neg ContinuousAddMonoidHom.neg

variable {A B C D E}

/-- Coproduct of two continuous homomorphisms to the same space. -/
@[to_additive "Coproduct of two continuous homomorphisms to the same space.", simps]
def coprod (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) :
    ContinuousMonoidHom (A × B) E :=
  (mul E).comp (f.Prod_map g)
#align continuous_monoid_hom.coprod ContinuousMonoidHom.coprod
#align continuous_add_monoid_hom.coprod ContinuousAddMonoidHom.coprod

@[to_additive]
instance : CommGroup (ContinuousMonoidHom A E)
    where
  mul f g := (mul E).comp (f.Prod g)
  mul_comm f g := ext fun x => mul_comm (f x) (g x)
  mul_assoc f g h := ext fun x => mul_assoc (f x) (g x) (h x)
  one := one A E
  one_mul f := ext fun x => one_mul (f x)
  mul_one f := ext fun x => mul_one (f x)
  inv f := (inv E).comp f
  mul_left_inv f := ext fun x => mul_left_inv (f x)

@[to_additive]
instance : TopologicalSpace (ContinuousMonoidHom A B) :=
  TopologicalSpace.induced toContinuousMap ContinuousMap.compactOpen

variable (A B C D E)

@[to_additive]
theorem inducing_toContinuousMap : Inducing (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
  ⟨rfl⟩
#align continuous_monoid_hom.inducing_to_continuous_map ContinuousMonoidHom.inducing_toContinuousMap
#align continuous_add_monoid_hom.inducing_to_continuous_map ContinuousAddMonoidHom.inducing_toContinuousMap

@[to_additive]
theorem embedding_toContinuousMap :
    Embedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
  ⟨inducing_toContinuousMap A B, toContinuousMap_injective⟩
#align continuous_monoid_hom.embedding_to_continuous_map ContinuousMonoidHom.embedding_toContinuousMap
#align continuous_add_monoid_hom.embedding_to_continuous_map ContinuousAddMonoidHom.embedding_toContinuousMap

/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (x y) -/
/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (U V W) -/
@[to_additive]
theorem closedEmbedding_toContinuousMap [ContinuousMul B] [T2Space B] :
    ClosedEmbedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
  ⟨embedding_toContinuousMap A B,
    ⟨by
      suffices
        Set.range (to_continuous_map : ContinuousMonoidHom A B → C(A, B)) =
          ({ f | f '' {1} ⊆ {1}ᶜ } ∪
              ⋃ (x) (y) (U) (V) (W) (hU : IsOpen U) (hV : IsOpen V) (hW : IsOpen W) (h :
                Disjoint (U * V) W),
                { f | f '' {x} ⊆ U } ∩ { f | f '' {y} ⊆ V } ∩ { f | f '' {x * y} ⊆ W })ᶜ
        by
        rw [this, compl_compl]
        refine' (ContinuousMap.isOpen_gen isCompact_singleton isOpen_compl_singleton).union _
        repeat' apply isOpen_unionᵢ; intro
        repeat' apply IsOpen.inter
        all_goals apply ContinuousMap.isOpen_gen isCompact_singleton; assumption
      simp_rw [Set.compl_union, Set.compl_unionᵢ, Set.image_singleton, Set.singleton_subset_iff,
        Set.ext_iff, Set.mem_inter_iff, Set.mem_interᵢ, Set.mem_compl_iff]
      refine' fun f => ⟨_, _⟩
      · rintro ⟨f, rfl⟩
        exact
          ⟨fun h => h (map_one f), fun x y U V W hU hV hW h ⟨⟨hfU, hfV⟩, hfW⟩ =>
            h.le_bot ⟨Set.mul_mem_mul hfU hfV, (congr_arg (· ∈ W) (map_mul f x y)).mp hfW⟩⟩
      · rintro ⟨hf1, hf2⟩
        suffices ∀ x y, f (x * y) = f x * f y by
          refine'
            ⟨({ f with
                  map_one' := of_not_not hf1
                  map_mul' := this } :
                ContinuousMonoidHom A B),
              ContinuousMap.ext fun _ => rfl⟩
        intro x y
        contrapose! hf2
        obtain ⟨UV, W, hUV, hW, hfUV, hfW, h⟩ := t2_separation hf2.symm
        have hB := @continuous_mul B _ _ _
        obtain ⟨U, V, hU, hV, hfU, hfV, h'⟩ :=
          is_open_prod_iff.mp (hUV.preimage hB) (f x) (f y) hfUV
        refine' ⟨x, y, U, V, W, hU, hV, hW, h.mono_left _, ⟨hfU, hfV⟩, hfW⟩
        rintro _ ⟨x, y, hx : (x, y).1 ∈ U, hy : (x, y).2 ∈ V, rfl⟩
        exact h' ⟨hx, hy⟩⟩⟩
#align continuous_monoid_hom.closed_embedding_to_continuous_map ContinuousMonoidHom.closedEmbedding_toContinuousMap
#align continuous_add_monoid_hom.closed_embedding_to_continuous_map ContinuousAddMonoidHom.closedEmbedding_toContinuousMap

variable {A B C D E}

@[to_additive]
instance [T2Space B] : T2Space (ContinuousMonoidHom A B) :=
  (embedding_toContinuousMap A B).T2Space

@[to_additive]
instance : TopologicalGroup (ContinuousMonoidHom A E) :=
  let hi := inducing_toContinuousMap A E
  let hc := hi.Continuous
  { continuous_mul := hi.continuous_iff.mpr (continuous_mul.comp (Continuous.prod_map hc hc))
    continuous_inv := hi.continuous_iff.mpr (continuous_inv.comp hc) }

@[to_additive]
theorem continuous_of_continuous_uncurry {A : Type _} [TopologicalSpace A]
    (f : A → ContinuousMonoidHom B C) (h : Continuous (Function.uncurry fun x y => f x y)) :
    Continuous f :=
  (inducing_toContinuousMap _ _).continuous_iff.mpr
    (ContinuousMap.continuous_of_continuous_uncurry _ h)
#align continuous_monoid_hom.continuous_of_continuous_uncurry ContinuousMonoidHom.continuous_of_continuous_uncurry
#align continuous_add_monoid_hom.continuous_of_continuous_uncurry ContinuousAddMonoidHom.continuous_of_continuous_uncurry

@[to_additive]
theorem continuous_comp [LocallyCompactSpace B] :
    Continuous fun f : ContinuousMonoidHom A B × ContinuousMonoidHom B C => f.2.comp f.1 :=
  (inducing_toContinuousMap A C).continuous_iff.2 <|
    ContinuousMap.continuous_comp'.comp
      ((inducing_toContinuousMap A B).prod_mk (inducing_toContinuousMap B C)).Continuous
#align continuous_monoid_hom.continuous_comp ContinuousMonoidHom.continuous_comp
#align continuous_add_monoid_hom.continuous_comp ContinuousAddMonoidHom.continuous_comp

@[to_additive]
theorem continuous_comp_left (f : ContinuousMonoidHom A B) :
    Continuous fun g : ContinuousMonoidHom B C => g.comp f :=
  (inducing_toContinuousMap A C).continuous_iff.2 <|
    f.toContinuousMap.continuous_comp_left.comp (inducing_toContinuousMap B C).Continuous
#align continuous_monoid_hom.continuous_comp_left ContinuousMonoidHom.continuous_comp_left
#align continuous_add_monoid_hom.continuous_comp_left ContinuousAddMonoidHom.continuous_comp_left

@[to_additive]
theorem continuous_comp_right (f : ContinuousMonoidHom B C) :
    Continuous fun g : ContinuousMonoidHom A B => f.comp g :=
  (inducing_toContinuousMap A C).continuous_iff.2 <|
    f.toContinuousMap.continuous_comp.comp (inducing_toContinuousMap A B).Continuous
#align continuous_monoid_hom.continuous_comp_right ContinuousMonoidHom.continuous_comp_right
#align continuous_add_monoid_hom.continuous_comp_right ContinuousAddMonoidHom.continuous_comp_right

variable (E)

/-- `continuous_monoid_hom _ f` is a functor. -/
@[to_additive "`continuous_add_monoid_hom _ f` is a functor."]
def compLeft (f : ContinuousMonoidHom A B) :
    ContinuousMonoidHom (ContinuousMonoidHom B E) (ContinuousMonoidHom A E)
    where
  toFun g := g.comp f
  map_one' := rfl
  map_mul' g h := rfl
  continuous_toFun := f.continuous_comp_left
#align continuous_monoid_hom.comp_left ContinuousMonoidHom.compLeft
#align continuous_add_monoid_hom.comp_left ContinuousAddMonoidHom.compLeft

variable (A) {E}

/-- `continuous_monoid_hom f _` is a functor. -/
@[to_additive "`continuous_add_monoid_hom f _` is a functor."]
def compRight {B : Type _} [CommGroup B] [TopologicalSpace B] [TopologicalGroup B]
    (f : ContinuousMonoidHom B E) :
    ContinuousMonoidHom (ContinuousMonoidHom A B) (ContinuousMonoidHom A E)
    where
  toFun g := f.comp g
  map_one' := ext fun a => map_one f
  map_mul' g h := ext fun a => map_mul f (g a) (h a)
  continuous_toFun := f.continuous_comp_right
#align continuous_monoid_hom.comp_right ContinuousMonoidHom.compRight
#align continuous_add_monoid_hom.comp_right ContinuousAddMonoidHom.compRight

end ContinuousMonoidHom

/-- The Pontryagin dual of `A` is the group of continuous homomorphism `A → circle`. -/
def PontryaginDual :=
  ContinuousMonoidHom A circle deriving TopologicalSpace, T2Space, CommGroup, TopologicalGroup,
  Inhabited
#align pontryagin_dual PontryaginDual

variable {A B C D E}

namespace PontryaginDual

open ContinuousMonoidHom

noncomputable instance : ContinuousMonoidHomClass (PontryaginDual A) A circle :=
  ContinuousMonoidHom.continuousMonoidHomClass

/-- `pontryagin_dual` is a functor. -/
noncomputable def map (f : ContinuousMonoidHom A B) :
    ContinuousMonoidHom (PontryaginDual B) (PontryaginDual A) :=
  f.compLeft circle
#align pontryagin_dual.map PontryaginDual.map

@[simp]
theorem map_apply (f : ContinuousMonoidHom A B) (x : PontryaginDual B) (y : A) :
    map f x y = x (f y) :=
  rfl
#align pontryagin_dual.map_apply PontryaginDual.map_apply

@[simp]
theorem map_one : map (one A B) = one (PontryaginDual B) (PontryaginDual A) :=
  ext fun x => ext fun y => map_one x
#align pontryagin_dual.map_one PontryaginDual.map_one

@[simp]
theorem map_comp (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) :
    map (comp g f) = comp (map f) (map g) :=
  ext fun x => ext fun y => rfl
#align pontryagin_dual.map_comp PontryaginDual.map_comp

@[simp]
theorem map_mul (f g : ContinuousMonoidHom A E) : map (f * g) = map f * map g :=
  ext fun x => ext fun y => map_mul x (f y) (g y)
#align pontryagin_dual.map_mul PontryaginDual.map_mul

variable (A B C D E)

/-- `continuous_monoid_hom.dual` as a `continuous_monoid_hom`. -/
noncomputable def mapHom [LocallyCompactSpace E] :
    ContinuousMonoidHom (ContinuousMonoidHom A E)
      (ContinuousMonoidHom (PontryaginDual E) (PontryaginDual A))
    where
  toFun := map
  map_one' := map_one
  map_mul' := map_mul
  continuous_toFun := continuous_of_continuous_uncurry _ continuous_comp
#align pontryagin_dual.map_hom PontryaginDual.mapHom

end PontryaginDual