text:
import tactic
import data.real.basic
import data.set
import data.set.lattice
import logics
import definitions

set_option trace.simplify.rewrite true
-- set_option pp.all true

variables {X : Type} {Y : Type}
-- mem_compl_iff
--lemma complement {A : set X} {x : X} : x ∈ - A ↔ ¬ x ∈ A :=
--iff.rfl

----------------------------------------------
namespace set_theory
----------------------------------------------

lemma definition.inclusion (A B : set X) : A ⊆ B ↔ ∀ {{x:X}}, x ∈ A → x ∈ B :=
iff.rfl

lemma definition.egalite_ensembles {A A' : set X} : (A = A') ↔ ( ∀ x, x ∈ A ↔ x ∈ A' ) :=
/- dEAduction
PrettyName
    Egalité d'ensembles
-/
by exact set.ext_iff

lemma theorem.double_inclusion {A A' : set X} : (A = A') ↔ (A ⊆ A' ∧ A' ⊆ A) :=
begin
    exact le_antisymm_iff
end

----------------------------------------------
namespace unions_and_intersections -- section 1
----------------------------------------------

lemma definition.intersection_deux  (A B : set X) (x : X) :  x ∈ A ∩ B ↔ ( x ∈ A ∧ x ∈ B) :=
iff.rfl
/- dEAduction
PrettyName
    Intersection de deux ensembles
-/

lemma theorem.intersection_ensemble  (A B C : set X) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B :=
begin
    exact ball_and_distrib
end

lemma definition.intersection_quelconque (I : Type) (O : I → set X)  (x : X) : (x ∈ set.Inter O) ↔ (∀ i:I, x ∈ O i) :=
set.mem_Inter
/- dEAduction
PrettyName
    Intersection quelconque
-/

-- Les deux lemmes suivants seront à regroupé au sein d'une même tactique : essayer le premier,
-- en cas d'échec essayer le second. Un seul bouton dans l'interface graphique
lemma definition.union  (A : set X) (B : set X) (x : X) :  x ∈ A ∪ B ↔ ( x ∈ A ∨ x ∈ B) :=
iff.rfl
/- dEAduction
PrettyName
    Union de deux ensembles
-/

lemma definition.union_quelconque (I : Type) (O : I → set X)  (x : X) : (x ∈ set.Union O) ↔ (∃ i:I, x ∈ O i) :=
set.mem_Union
/- dEAduction
PrettyName
    Union quelconque
-/

end unions_and_intersections

-----------------------------------------
namespace complements -- section 2
----------------------------------------------

lemma definition.complement {A : set X} {x : X} : x ∈ set.univ \ A ↔ x ∉ A :=
by finish

lemma definition.complement_1 {A : set X} {x : X} : x ∈ set.compl A ↔ x ∉ A :=
by finish

lemma definition.complement_2 {A B : set X} {x : X} : x ∈ B \ A ↔ (x ∈ B ∧ x ∉ A) :=
iff.rfl

end complements

end set_theory

author: dEAduction

repo: dEAduction-lean


text:
/-
Copyright (c) 2022 Chris Birkbeck. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Birkbeck
-/
import number_theory.modular_forms.slash_actions

/-!
# Slash invariant forms

This file defines functions that are invariant under a `slash_action` which forms the basis for
defining `modular_form` and `cusp_form`. We prove several instances for such spaces, in particular
that they form a module.
-/

open complex upper_half_plane

open_locale upper_half_plane

noncomputable theory

local prefix `↑ₘ`:1024 := @coe _ (matrix (fin 2) (fin 2) _) _

-- like `↑ₘ`, but allows the user to specify the ring `R`. Useful to help Lean elaborate.
local notation `↑ₘ[` R `]` := @coe _ (matrix (fin 2) (fin 2) R) _

local notation `GL(` n `, ` R `)`⁺ := matrix.GL_pos (fin n) R

local notation `SL(` n `, ` R `)` := matrix.special_linear_group (fin n) R

section slash_invariant_forms

set_option old_structure_cmd true

open modular_form

variables (F : Type*) (Γ : out_param $ subgroup SL(2, ℤ)) (k : out_param ℤ)

localized "notation f `∣[`:73 k:0, A `]` :72 := slash_action.map ℂ k A f" in slash_invariant_forms

/--Functions `ℍ → ℂ` that are invariant under the `slash_action`. -/
structure slash_invariant_form :=
(to_fun : ℍ → ℂ)
(slash_action_eq' : ∀ γ : Γ, to_fun ∣[k, γ] = to_fun)

/--`slash_invariant_form_class F Γ k` asserts `F` is a type of bundled functions that are invariant
under the `slash_action`. -/
class slash_invariant_form_class extends fun_like F ℍ (λ _, ℂ) :=
(slash_action_eq : ∀ (f : F) (γ : Γ), (f : ℍ → ℂ) ∣[k, γ] = f)

attribute [nolint dangerous_instance] slash_invariant_form_class.to_fun_like

@[priority 100]
instance slash_invariant_form_class.slash_invariant_form :
   slash_invariant_form_class (slash_invariant_form Γ k) Γ k :=
{ coe := slash_invariant_form.to_fun,
  coe_injective' := λ f g h, by cases f; cases g; congr',
  slash_action_eq := slash_invariant_form.slash_action_eq' }

variables {F Γ k}

instance : has_coe_to_fun (slash_invariant_form Γ k) (λ _, ℍ → ℂ) := fun_like.has_coe_to_fun

@[simp] lemma slash_invariant_form_to_fun_eq_coe {f : slash_invariant_form Γ k} :
  f.to_fun = (f : ℍ → ℂ) := rfl

@[ext] theorem slash_invariant_form_ext {f g : slash_invariant_form Γ k} (h : ∀ x, f x = g x) :
  f = g := fun_like.ext f g h

/-- Copy of a `slash_invariant_form` with a new `to_fun` equal to the old one.
Useful to fix definitional equalities. -/
protected def slash_invariant_form.copy (f : slash_invariant_form Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) :
  slash_invariant_form Γ k :=
{ to_fun := f',
  slash_action_eq' := h.symm ▸ f.slash_action_eq',}

end slash_invariant_forms

namespace slash_invariant_form

open slash_invariant_form

variables {F : Type*} {Γ : out_param $ subgroup SL(2, ℤ)} {k : out_param ℤ}

@[priority 100, nolint dangerous_instance]
instance slash_invariant_form_class.coe_to_fun [slash_invariant_form_class F Γ k] :
  has_coe_to_fun F (λ _, ℍ → ℂ) := fun_like.has_coe_to_fun

@[simp] lemma slash_action_eqn [slash_invariant_form_class F Γ k] (f : F) (γ : Γ) :
   slash_action.map ℂ k γ ⇑f = ⇑f := slash_invariant_form_class.slash_action_eq f γ

lemma slash_action_eqn' (k : ℤ) (Γ : subgroup SL(2, ℤ)) [slash_invariant_form_class F Γ k] (f : F)
  (γ : Γ) (z : ℍ) : f (γ • z) = ((↑ₘ[ℤ]γ 1 0 : ℂ) * z +(↑ₘ[ℤ]γ 1 1 : ℂ))^k * f z :=
begin
  rw ←modular_form.slash_action_eq'_iff,
  simp,
end

instance [slash_invariant_form_class F Γ k] : has_coe_t F (slash_invariant_form Γ k) :=
⟨λ f, { to_fun := f, slash_action_eq' := slash_action_eqn f }⟩

@[simp] lemma slash_invariant_form_class.coe_coe [slash_invariant_form_class F Γ k] (f : F) :
  ((f : slash_invariant_form Γ k) : ℍ → ℂ) = f := rfl

instance has_add : has_add (slash_invariant_form Γ k) :=
⟨ λ f g,
  { to_fun := f + g,
    slash_action_eq' := λ γ, by convert slash_action.add_action k γ (f : ℍ → ℂ) g; simp } ⟩

@[simp] lemma coe_add (f g : slash_invariant_form Γ k) : ⇑(f + g) = f + g := rfl
@[simp] lemma add_apply (f g : slash_invariant_form Γ k) (z : ℍ) : (f + g) z = f z + g z := rfl

instance has_zero : has_zero (slash_invariant_form Γ k) :=
⟨ { to_fun := 0,
    slash_action_eq' := slash_action.zero_slash _} ⟩

@[simp] lemma coe_zero : ⇑(0 : slash_invariant_form Γ k) = (0 : ℍ → ℂ) := rfl

section
variables {α : Type*} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ]

instance has_smul : has_smul α (slash_invariant_form Γ k) :=
⟨ λ c f,
  { to_fun := c • f,
    slash_action_eq' := λ γ, by rw [←smul_one_smul ℂ c ⇑f, slash_action.smul_action k γ ⇑f,
                                    slash_action_eqn] }⟩

@[simp] lemma coe_smul (f : slash_invariant_form Γ k) (n : α) : ⇑(n • f) = n • f := rfl
@[simp] lemma smul_apply (f : slash_invariant_form Γ k) (n : α) (z : ℍ) :
  (n • f) z = n • (f z) := rfl

end

instance has_neg : has_neg (slash_invariant_form Γ k) :=
⟨ λ f,
  { to_fun := -f,
    slash_action_eq' := λ γ, by simpa [modular_form.subgroup_slash,
      modular_form.neg_slash] using f.slash_action_eq' γ } ⟩

@[simp] lemma coe_neg (f : slash_invariant_form Γ k) : ⇑(-f) = -f := rfl
@[simp] lemma neg_apply (f : slash_invariant_form Γ k) (z : ℍ) : (-f) z = - (f z) := rfl

instance has_sub : has_sub (slash_invariant_form Γ k) := ⟨ λ f g, f + -g ⟩

@[simp] lemma coe_sub (f g : slash_invariant_form Γ k) : ⇑(f - g) = f - g := rfl
@[simp] lemma sub_apply (f g : slash_invariant_form Γ k) (z : ℍ) : (f - g) z = f z - g z := rfl

instance : add_comm_group (slash_invariant_form Γ k) :=
fun_like.coe_injective.add_comm_group _ rfl coe_add coe_neg coe_sub coe_smul coe_smul

/--Additive coercion from `slash_invariant_form` to `ℍ → ℂ`.-/
def coe_hom : slash_invariant_form Γ k →+ (ℍ → ℂ) :=
{ to_fun := λ f, f,
  map_zero' := rfl,
  map_add' := λ _ _, rfl }

lemma coe_hom_injective : function.injective (@coe_hom Γ k) :=
fun_like.coe_injective

instance : module ℂ (slash_invariant_form Γ k) :=
coe_hom_injective.module ℂ coe_hom (λ _ _, rfl)

instance : has_one (slash_invariant_form Γ 0) :=
⟨ { to_fun := 1,
    slash_action_eq' := λ A, modular_form.is_invariant_one A } ⟩

@[simp] lemma one_coe_eq_one : ((1 : slash_invariant_form Γ 0) : ℍ → ℂ) = 1 := rfl

instance : inhabited (slash_invariant_form Γ k) := ⟨0⟩

end slash_invariant_form

author: leanprover-community

repo: mathlib


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

! This file was ported from Lean 3 source module number_theory.ADE_inequality
! leanprover-community/mathlib commit 0a0ec35061ed9960bf0e7ffb0335f44447b58977
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Multiset.Sort
import Mathlib.Data.PNat.Interval
import Mathlib.Data.Rat.Order
import Mathlib.Data.PNat.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.IntervalCases

/-!
# The inequality `p⁻¹ + q⁻¹ + r⁻¹ > 1`

In this file we classify solutions to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`, for positive natural numbers `p`, `q`, and `r`.

The solutions are exactly of the form.
* `A' q r := {1,q,r}`
* `D' r := {2,2,r}`
* `E6 := {2,3,3}`, or `E7 := {2,3,4}`, or `E8 := {2,3,5}`

This inequality shows up in Lie theory,
in the classification of Dynkin diagrams, root systems, and semisimple Lie algebras.

## Main declarations

* `pqr.A' q r`, the multiset `{1,q,r}`
* `pqr.D' r`, the multiset `{2,2,r}`
* `pqr.E6`, the multiset `{2,3,3}`
* `pqr.E7`, the multiset `{2,3,4}`
* `pqr.E8`, the multiset `{2,3,5}`
* `pqr.classification`, the classification of solutions to `p⁻¹ + q⁻¹ + r⁻¹ > 1`

-/

namespace ADEInequality

open Multiset
-- porting note: ADE is a special name, exceptionally in upper case in Lean3
set_option linter.uppercaseLean3 false

/-- `A' q r := {1,q,r}` is a `multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`. -/
def A' (q r : ℕ+) : Multiset ℕ+ :=
  {1, q, r}
#align ADE_inequality.A' ADEInequality.A'

/-- `A r := {1,1,r}` is a `multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

These solutions are related to the Dynkin diagrams $A_r$. -/
def A (r : ℕ+) : Multiset ℕ+ :=
  A' 1 r
#align ADE_inequality.A ADEInequality.A

/-- `D' r := {2,2,r}` is a `multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

These solutions are related to the Dynkin diagrams $D_{r+2}$. -/
def D' (r : ℕ+) : Multiset ℕ+ :=
  {2, 2, r}
#align ADE_inequality.D' ADEInequality.D'

/-- `E' r := {2,3,r}` is a `multiset ℕ+`.
For `r ∈ {3,4,5}` is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

These solutions are related to the Dynkin diagrams $E_{r+3}$. -/
def E' (r : ℕ+) : Multiset ℕ+ :=
  {2, 3, r}
#align ADE_inequality.E' ADEInequality.E'

/-- `E6 := {2,3,3}` is a `multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

This solution is related to the Dynkin diagrams $E_6$. -/
def E6 : Multiset ℕ+ :=
  E' 3
#align ADE_inequality.E6 ADEInequality.E6

/-- `E7 := {2,3,4}` is a `multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

This solution is related to the Dynkin diagrams $E_7$. -/
def E7 : Multiset ℕ+ :=
  E' 4
#align ADE_inequality.E7 ADEInequality.E7

/-- `E8 := {2,3,5}` is a `multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

This solution is related to the Dynkin diagrams $E_8$. -/
def E8 : Multiset ℕ+ :=
  E' 5
#align ADE_inequality.E8 ADEInequality.E8

/-- `sum_inv pqr` for a `pqr : multiset ℕ+` is the sum of the inverses
of the elements of `pqr`, as rational number.

The intended argument is a multiset `{p,q,r}` of cardinality `3`. -/
def sumInv (pqr : Multiset ℕ+) : ℚ :=
  Multiset.sum (pqr.map fun (x : ℕ+) => x⁻¹)
#align ADE_inequality.sum_inv ADEInequality.sumInv

theorem sumInv_pqr (p q r : ℕ+) : sumInv {p, q, r} = (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ := by
  simp only [sumInv, add_zero, insert_eq_cons, add_assoc, map_cons, sum_cons,
    map_singleton, sum_singleton]
#align ADE_inequality.sum_inv_pqr ADEInequality.sumInv_pqr

/-- A multiset `pqr` of positive natural numbers is `admissible`
if it is equal to `A' q r`, or `D' r`, or one of `E6`, `E7`, or `E8`. -/
def Admissible (pqr : Multiset ℕ+) : Prop :=
  (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr
#align ADE_inequality.admissible ADEInequality.Admissible

theorem admissible_A' (q r : ℕ+) : Admissible (A' q r) :=
  Or.inl ⟨q, r, rfl⟩
#align ADE_inequality.admissible_A' ADEInequality.admissible_A'

theorem admissible_D' (n : ℕ+) : Admissible (D' n) :=
  Or.inr <| Or.inl ⟨n, rfl⟩
#align ADE_inequality.admissible_D' ADEInequality.admissible_D'

theorem admissible_E'3 : Admissible (E' 3) :=
  Or.inr <| Or.inr <| Or.inl rfl
#align ADE_inequality.admissible_E'3 ADEInequality.admissible_E'3

theorem admissible_E'4 : Admissible (E' 4) :=
  Or.inr <| Or.inr <| Or.inr <| Or.inl rfl
#align ADE_inequality.admissible_E'4 ADEInequality.admissible_E'4

theorem admissible_E'5 : Admissible (E' 5) :=
  Or.inr <| Or.inr <| Or.inr <| Or.inr rfl
#align ADE_inequality.admissible_E'5 ADEInequality.admissible_E'5

theorem admissible_E6 : Admissible E6 :=
  admissible_E'3
#align ADE_inequality.admissible_E6 ADEInequality.admissible_E6

theorem admissible_E7 : Admissible E7 :=
  admissible_E'4
#align ADE_inequality.admissible_E7 ADEInequality.admissible_E7

theorem admissible_E8 : Admissible E8 :=
  admissible_E'5
#align ADE_inequality.admissible_E8 ADEInequality.admissible_E8

theorem Admissible.one_lt_sumInv {pqr : Multiset ℕ+} : Admissible pqr → 1 < sumInv pqr := by
  rw [Admissible]
  rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)
  · rw [← H, A', sumInv_pqr, add_assoc]
    simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
    apply add_pos <;> simp only [PNat.pos, Nat.cast_pos, inv_pos]
  · rw [← H, D', sumInv_pqr]
    conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]
    norm_num
  all_goals
    rw [← H, E', sumInv_pqr]
    conv_rhs => simp only [OfNat.ofNat, PNat.mk_coe]

#align ADE_inequality.admissible.one_lt_sum_inv ADEInequality.Admissible.one_lt_sumInv

theorem lt_three {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r) (H : 1 < sumInv {p, q, r}) : p < 3 := by
  have h3 : (0 : ℚ) < 3 := by norm_num
  contrapose! H
  rw [sumInv_pqr]
  have h3q := (not_lt.mp H).trans hpq
  have h3r := h3q.trans hqr
  simp at H
  have hp: (p : ℚ)⁻¹ ≤ 3⁻¹ := by
    rw [inv_le_inv _ h3]
    assumption_mod_cast
    norm_num
  have hq: (q : ℚ)⁻¹ ≤ 3⁻¹ := by
    rw [inv_le_inv _ h3]
    assumption_mod_cast
    norm_num
  have hr: (r : ℚ)⁻¹ ≤ 3⁻¹ := by
    rw [inv_le_inv _ h3]
    assumption_mod_cast
    norm_num
  calc
    (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
    _ = 1 := by norm_num
#align ADE_inequality.lt_three ADEInequality.lt_three

theorem lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < sumInv {2, q, r}) : q < 4 := by
  have h4 : (0 : ℚ) < 4 := by norm_num
  contrapose! H
  rw [sumInv_pqr]
  have h4r := (not_lt.mp H).trans hqr
  simp at H
  have hq: (q : ℚ)⁻¹ ≤ 4⁻¹ := by
    rw [inv_le_inv _ h4]
    assumption_mod_cast
    norm_num
  have hr: (r : ℚ)⁻¹ ≤ 4⁻¹ := by
    rw [inv_le_inv _ h4]
    assumption_mod_cast
    norm_num
  calc
    (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
    _ = 1 := by norm_num
#align ADE_inequality.lt_four ADEInequality.lt_four

theorem lt_six {r : ℕ+} (H : 1 < sumInv {2, 3, r}) : r < 6 := by
  have h6 : (0 : ℚ) < 6 := by norm_num
  contrapose! H
  rw [sumInv_pqr]
  simp at H
  have hr: (r : ℚ)⁻¹ ≤ 6⁻¹ := by
    rw [inv_le_inv _ h6]
    assumption_mod_cast
    norm_num
  calc
    (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
    _ = 1 := by norm_num
#align ADE_inequality.lt_six ADEInequality.lt_six

theorem admissible_of_one_lt_sumInv_aux' {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r)
    (H : 1 < sumInv {p, q, r}) : Admissible {p, q, r} := by
  have hp3 : p < 3 := lt_three hpq hqr H
  -- Porting note: `interval_cases` doesn't support `ℕ+` yet.
  replace hp3 := Finset.mem_Iio.mpr hp3
  conv at hp3 => change p ∈ ({1, 2} : Multiset ℕ+)
  fin_cases hp3
  · exact admissible_A' q r
  have hq4 : q < 4 := lt_four hqr H
  replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩; clear hpq
  conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)
  fin_cases hq4
  · exact admissible_D' r
  have hr6 : r < 6 := lt_six H
  replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩; clear hqr
  conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)
  fin_cases hr6
  · exact admissible_E6
  · exact admissible_E7
  · exact admissible_E8
#align ADE_inequality.admissible_of_one_lt_sum_inv_aux' ADEInequality.admissible_of_one_lt_sumInv_aux'

theorem admissible_of_one_lt_sumInv_aux :
    ∀ {pqr : List ℕ+} (_ : pqr.Sorted (· ≤ ·)) (_ : pqr.length = 3) (_ : 1 < sumInv pqr),
      Admissible pqr
  | [p, q, r], hs, _, H =>
    by
    obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r
    simpa using hs
    exact admissible_of_one_lt_sumInv_aux' hpq hqr H
#align ADE_inequality.admissible_of_one_lt_sum_inv_aux ADEInequality.admissible_of_one_lt_sumInv_aux

theorem admissible_of_one_lt_sumInv {p q r : ℕ+} (H : 1 < sumInv {p, q, r}) :
    Admissible {p, q, r} := by
  simp only [Admissible]
  let S := sort ((· ≤ ·) : ℕ+ → ℕ+ → Prop) {p, q, r}
  have hS : S.Sorted (· ≤ ·) := sort_sorted _ _
  have hpqr : ({p, q, r} : Multiset ℕ+) = S := (sort_eq LE.le {p, q, r}).symm
  rw [hpqr]
  rw [hpqr] at H
  apply admissible_of_one_lt_sumInv_aux hS _ H
  simp only [ge_iff_le, insert_eq_cons, length_sort, card_cons, card_singleton]
#align ADE_inequality.admissible_of_one_lt_sum_inv ADEInequality.admissible_of_one_lt_sumInv

/-- A multiset `{p,q,r}` of positive natural numbers
is a solution to `(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1` if and only if
it is `admissible` which means it is one of:

* `A' q r := {1,q,r}`
* `D' r := {2,2,r}`
* `E6 := {2,3,3}`, or `E7 := {2,3,4}`, or `E8 := {2,3,5}`
-/
theorem classification (p q r : ℕ+) : 1 < sumInv {p, q, r} ↔ Admissible {p, q, r} :=
  ⟨admissible_of_one_lt_sumInv, Admissible.one_lt_sumInv⟩
#align ADE_inequality.classification ADEInequality.classification

end ADEInequality


text:
/-
Copyright (c) 2021 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
-/
import linear_algebra.basic
import linear_algebra.prod
import linear_algebra.pi
import data.set_like.fintype
import linear_algebra.linear_independent
import tactic.linarith
import algebra.algebra.basic
import ring_theory.noetherian
import ring_theory.jacobson_ideal
import ring_theory.nilpotent
import ring_theory.nakayama

/-!
# Artinian rings and modules

A module satisfying these equivalent conditions is said to be an *Artinian* R-module
if every decreasing chain of submodules is eventually constant, or equivalently,
if the relation `<` on submodules is well founded.

A ring is said to be left (or right) Artinian if it is Artinian as a left (or right) module over
itself, or simply Artinian if it is both left and right Artinian.

## Main definitions

Let `R` be a ring and let `M` and `P` be `R`-modules. Let `N` be an `R`-submodule of `M`.

* `is_artinian R M` is the proposition that `M` is a Artinian `R`-module. It is a class,
  implemented as the predicate that the `<` relation on submodules is well founded.
* `is_artinian_ring R` is the proposition that `R` is a left Artinian ring.

## References

* [M. F. Atiyah and I. G. Macdonald, *Introduction to commutative algebra*][atiyah-macdonald]
* [samuel]

## Tags

Artinian, artinian, Artinian ring, Artinian module, artinian ring, artinian module

-/
open set
open_locale big_operators pointwise

/--
`is_artinian R M` is the proposition that `M` is an Artinian `R`-module,
implemented as the well-foundedness of submodule inclusion.
-/
class is_artinian (R M) [semiring R] [add_comm_monoid M] [module R M] : Prop :=
(well_founded_submodule_lt [] : well_founded ((<) : submodule R M → submodule R M → Prop))

section
variables {R : Type*} {M : Type*} {P : Type*} {N : Type*}
variables [ring R] [add_comm_group M] [add_comm_group P] [add_comm_group N]
variables [module R M] [module R P] [module R N]
open is_artinian
include R

theorem is_artinian_of_injective (f : M →ₗ[R] P) (h : function.injective f)
  [is_artinian R P] : is_artinian R M :=
⟨subrelation.wf
  (λ A B hAB, show A.map f < B.map f,
    from submodule.map_strict_mono_of_injective h hAB)
  (inv_image.wf (submodule.map f) (is_artinian.well_founded_submodule_lt R P))⟩

instance is_artinian_submodule' [is_artinian R M] (N : submodule R M) : is_artinian R N :=
is_artinian_of_injective N.subtype subtype.val_injective

lemma is_artinian_of_le {s t : submodule R M} [ht : is_artinian R t]
   (h : s ≤ t) : is_artinian R s :=
is_artinian_of_injective (submodule.of_le h) (submodule.of_le_injective h)

variable (M)
theorem is_artinian_of_surjective (f : M →ₗ[R] P) (hf : function.surjective f)
  [is_artinian R M] : is_artinian R P :=
⟨subrelation.wf
  (λ A B hAB, show A.comap f < B.comap f,
    from submodule.comap_strict_mono_of_surjective hf hAB)
  (inv_image.wf (submodule.comap f) (is_artinian.well_founded_submodule_lt _ _))⟩
variable {M}

theorem is_artinian_of_linear_equiv (f : M ≃ₗ[R] P)
  [is_artinian R M] : is_artinian R P :=
is_artinian_of_surjective _ f.to_linear_map f.to_equiv.surjective

theorem is_artinian_of_range_eq_ker
  [is_artinian R M] [is_artinian R P]
  (f : M →ₗ[R] N) (g : N →ₗ[R] P)
  (hf : function.injective f)
  (hg : function.surjective g)
  (h : f.range = g.ker) :
  is_artinian R N :=
⟨well_founded_lt_exact_sequence
  (is_artinian.well_founded_submodule_lt _ _)
  (is_artinian.well_founded_submodule_lt _ _)
  f.range
  (submodule.map f)
  (submodule.comap f)
  (submodule.comap g)
  (submodule.map g)
  (submodule.gci_map_comap hf)
  (submodule.gi_map_comap hg)
  (by simp [submodule.map_comap_eq, inf_comm])
  (by simp [submodule.comap_map_eq, h])⟩

instance is_artinian_prod [is_artinian R M]
  [is_artinian R P] : is_artinian R (M × P) :=
is_artinian_of_range_eq_ker
  (linear_map.inl R M P)
  (linear_map.snd R M P)
  linear_map.inl_injective
  linear_map.snd_surjective
  (linear_map.range_inl R M P)

@[instance, priority 100]
lemma is_artinian_of_fintype [fintype M] : is_artinian R M :=
⟨fintype.well_founded_of_trans_of_irrefl _⟩

local attribute [elab_as_eliminator] fintype.induction_empty_option

instance is_artinian_pi {R ι : Type*} [fintype ι] : Π {M : ι → Type*} [ring R]
  [Π i, add_comm_group (M i)], by exactI Π [Π i, module R (M i)],
  by exactI Π [∀ i, is_artinian R (M i)], is_artinian R (Π i, M i) :=
fintype.induction_empty_option
  (begin
    introsI α β e hα M _ _ _ _,
    exact is_artinian_of_linear_equiv
      (linear_equiv.Pi_congr_left R M e)
  end)
  (by { introsI M _ _ _ _, apply_instance })
  (begin
     introsI α _ ih M _ _ _ _,
     exact is_artinian_of_linear_equiv
        (linear_equiv.pi_option_equiv_prod R).symm,
  end)
  ι

/-- A version of `is_artinian_pi` for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that `ι → ℝ` is finite dimensional over `ℝ`). -/
instance is_artinian_pi' {R ι M : Type*} [ring R] [add_comm_group M] [module R M] [fintype ι]
  [is_artinian R M] : is_artinian R (ι → M) :=
is_artinian_pi

end

open is_artinian submodule function

section
variables {R M : Type*} [ring R] [add_comm_group M] [module R M]

theorem is_artinian_iff_well_founded :
  is_artinian R M ↔ well_founded ((<) : submodule R M → submodule R M → Prop) :=
⟨λ h, h.1, is_artinian.mk⟩

variables {R M}

lemma is_artinian.finite_of_linear_independent [nontrivial R] [is_artinian R M]
  {s : set M} (hs : linear_independent R (coe : s → M)) : s.finite :=
begin
  refine classical.by_contradiction (λ hf, (rel_embedding.well_founded_iff_no_descending_seq.1
    (well_founded_submodule_lt R M)).elim' _),
  have f : ℕ ↪ s, from set.infinite.nat_embedding s hf,
  have : ∀ n, (coe ∘ f) '' {m | n ≤ m} ⊆ s,
  { rintros n x ⟨y, hy₁, rfl⟩, exact (f y).2 },
  have : ∀ a b : ℕ, a ≤ b ↔
    span R ((coe ∘ f) '' {m | b ≤ m}) ≤ span R ((coe ∘ f) '' {m | a ≤ m}),
  { assume a b,
    rw [span_le_span_iff hs (this b) (this a),
      set.image_subset_image_iff (subtype.coe_injective.comp f.injective),
      set.subset_def],
    simp only [set.mem_set_of_eq],
    exact ⟨λ hab x, le_trans hab, λ h, (h _ le_rfl)⟩ },
  exact ⟨⟨λ n, span R ((coe ∘ f) '' {m | n ≤ m}),
      λ x y, by simp [le_antisymm_iff, (this _ _).symm] {contextual := tt}⟩,
    begin
      intros a b,
      conv_rhs { rw [gt, lt_iff_le_not_le, this, this, ← lt_iff_le_not_le] },
      simp
    end⟩
end

/-- A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.
-/
theorem set_has_minimal_iff_artinian :
  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M') ↔
  is_artinian R M :=
by rw [is_artinian_iff_well_founded, well_founded.well_founded_iff_has_min']

theorem is_artinian.set_has_minimal [is_artinian R M] (a : set $ submodule R M) (ha : a.nonempty) :
  ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M' :=
set_has_minimal_iff_artinian.mpr ‹_› a ha

/-- A module is Artinian iff every decreasing chain of submodules stabilizes. -/
theorem monotone_stabilizes_iff_artinian :
  (∀ (f : ℕ →o (submodule R M)ᵒᵈ), ∃ n, ∀ m, n ≤ m → f n = f m)
    ↔ is_artinian R M :=
by rw [is_artinian_iff_well_founded];
  exact (well_founded.monotone_chain_condition (submodule R M)ᵒᵈ).symm

theorem is_artinian.monotone_stabilizes [is_artinian R M] (f : ℕ →o (submodule R M)ᵒᵈ) :
  ∃ n, ∀ m, n ≤ m → f n = f m :=
monotone_stabilizes_iff_artinian.mpr ‹_› f

/-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
lemma is_artinian.induction [is_artinian R M] {P : submodule R M → Prop}
  (hgt : ∀ I, (∀ J < I, P J) → P I) (I : submodule R M) : P I :=
well_founded.recursion (well_founded_submodule_lt R M) I hgt

/--
For any endomorphism of a Artinian module, there is some nontrivial iterate
with disjoint kernel and range.
-/
theorem is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top
  [I : is_artinian R M] (f : M →ₗ[R] M) : ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊔ (f ^ n).range = ⊤ :=
begin
  obtain ⟨n, w⟩ := monotone_stabilizes_iff_artinian.mpr I
    (f.iterate_range.comp ⟨λ n, n+1, λ n m w, by linarith⟩),
  specialize w ((n + 1) + n) (by linarith),
  dsimp at w,
  refine ⟨n + 1, nat.succ_ne_zero _, _⟩,
  simp_rw [eq_top_iff', mem_sup],
  intro x,
  have : (f^(n + 1)) x ∈ (f ^ ((n + 1) + n + 1)).range,
  { rw ← w, exact mem_range_self _ },
  rcases this with ⟨y, hy⟩,
  use x - (f ^ (n+1)) y,
  split,
  { rw [linear_map.mem_ker, linear_map.map_sub, ← hy, sub_eq_zero, pow_add],
    simp [iterate_add_apply], },
  { use (f^ (n+1)) y,
    simp }
end

/-- Any injective endomorphism of an Artinian module is surjective. -/
theorem is_artinian.surjective_of_injective_endomorphism [is_artinian R M]
  (f : M →ₗ[R] M) (s : injective f) : surjective f :=
begin
  obtain ⟨n, ne, w⟩ := is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top f,
  rw [linear_map.ker_eq_bot.mpr (linear_map.iterate_injective s n), bot_sup_eq,
    linear_map.range_eq_top] at w,
  exact linear_map.surjective_of_iterate_surjective ne w,
end

/-- Any injective endomorphism of an Artinian module is bijective. -/
theorem is_artinian.bijective_of_injective_endomorphism [is_artinian R M]
  (f : M →ₗ[R] M) (s : injective f) : bijective f :=
⟨s, is_artinian.surjective_of_injective_endomorphism f s⟩

/--
A sequence `f` of submodules of a artinian module,
with the supremum `f (n+1)` and the infinum of `f 0`, ..., `f n` being ⊤,
is eventually ⊤.
-/
lemma is_artinian.disjoint_partial_infs_eventually_top [I : is_artinian R M]
  (f : ℕ → submodule R M) (h : ∀ n, disjoint
    (partial_sups (order_dual.to_dual ∘ f) n) (order_dual.to_dual (f (n+1)))) :
  ∃ n : ℕ, ∀ m, n ≤ m → f m = ⊤  :=
begin
  -- A little off-by-one cleanup first:
  suffices t : ∃ n : ℕ, ∀ m, n ≤ m → order_dual.to_dual f (m+1) = ⊤,
  { obtain ⟨n, w⟩ := t,
    use n+1,
    rintros (_|m) p,
    { cases p, },
    { apply w,
      exact nat.succ_le_succ_iff.mp p }, },

  obtain ⟨n, w⟩ := monotone_stabilizes_iff_artinian.mpr I (partial_sups (order_dual.to_dual ∘ f)),
  exact ⟨n, λ m p, (h m).eq_bot_of_ge $ sup_eq_left.1 $ (w (m + 1) $ le_add_right p).symm.trans $
    w m p⟩
end

universe w
variables {N : Type w} [add_comm_group N] [module R N]

-- TODO: Prove this for artinian modules
-- /--
-- If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial.
-- -/
-- noncomputable def is_noetherian.equiv_punit_of_prod_injective [is_noetherian R M]
--   (f : M × N →ₗ[R] M) (i : injective f) : N ≃ₗ[R] punit.{w+1} :=
-- begin
--   apply nonempty.some,
--   obtain ⟨n, w⟩ := is_noetherian.disjoint_partial_sups_eventually_bot (f.tailing i)
--     (f.tailings_disjoint_tailing i),
--   specialize w n (le_refl n),
--   apply nonempty.intro,
--   refine (f.tailing_linear_equiv i n).symm.trans _,
--   rw w,
--   exact submodule.bot_equiv_punit,
-- end

end

/-- A ring is Artinian if it is Artinian as a module over itself.

Strictly speaking, this should be called `is_left_artinian_ring` but we omit the `left_` for
convenience in the commutative case. For a right Artinian ring, use `is_artinian Rᵐᵒᵖ R`. -/
class is_artinian_ring (R) [ring R] extends is_artinian R R : Prop

theorem is_artinian_ring_iff {R} [ring R] : is_artinian_ring R ↔ is_artinian R R :=
⟨λ h, h.1, @is_artinian_ring.mk _ _⟩

theorem ring.is_artinian_of_zero_eq_one {R} [ring R] (h01 : (0 : R) = 1) : is_artinian_ring R :=
by haveI := subsingleton_of_zero_eq_one h01;
   haveI := fintype.of_subsingleton (0:R); split;
  apply_instance

theorem is_artinian_of_submodule_of_artinian (R M) [ring R] [add_comm_group M] [module R M]
  (N : submodule R M) (h : is_artinian R M) : is_artinian R N :=
by apply_instance

theorem is_artinian_of_quotient_of_artinian (R) [ring R] (M) [add_comm_group M] [module R M]
  (N : submodule R M) (h : is_artinian R M) : is_artinian R (M ⧸ N) :=
is_artinian_of_surjective M (submodule.mkq N) (submodule.quotient.mk_surjective N)

/-- If `M / S / R` is a scalar tower, and `M / R` is Artinian, then `M / S` is
also Artinian. -/
theorem is_artinian_of_tower (R) {S M} [comm_ring R] [ring S]
  [add_comm_group M] [algebra R S] [module S M] [module R M] [is_scalar_tower R S M]
  (h : is_artinian R M) : is_artinian S M :=
begin
  rw is_artinian_iff_well_founded at h ⊢,
  refine (submodule.restrict_scalars_embedding R S M).well_founded h
end

theorem is_artinian_of_fg_of_artinian {R M} [ring R] [add_comm_group M] [module R M]
  (N : submodule R M) [is_artinian_ring R] (hN : N.fg) : is_artinian R N :=
let ⟨s, hs⟩ := hN in
begin
  haveI := classical.dec_eq M,
  haveI := classical.dec_eq R,
  letI : is_artinian R R := by apply_instance,
  have : ∀ x ∈ s, x ∈ N, from λ x hx, hs ▸ submodule.subset_span hx,
  refine @@is_artinian_of_surjective ((↑s : set M) → R) _ _ _ (pi.module _ _ _)
    _ _ _ is_artinian_pi,
  { fapply linear_map.mk,
    { exact λ f, ⟨∑ i in s.attach, f i • i.1, N.sum_mem (λ c _, N.smul_mem _ $ this _ c.2)⟩ },
    { intros f g, apply subtype.eq,
      change ∑ i in s.attach, (f i + g i) • _ = _,
      simp only [add_smul, finset.sum_add_distrib], refl },
    { intros c f, apply subtype.eq,
      change ∑ i in s.attach, (c • f i) • _ = _,
      simp only [smul_eq_mul, mul_smul],
      exact finset.smul_sum.symm } },
  rintro ⟨n, hn⟩, change n ∈ N at hn,
  rw [← hs, ← set.image_id ↑s, finsupp.mem_span_image_iff_total] at hn,
  rcases hn with ⟨l, hl1, hl2⟩,
  refine ⟨λ x, l x, subtype.ext _⟩,
  change ∑ i in s.attach, l i • (i : M) = n,
  rw [@finset.sum_attach M M s _ (λ i, l i • i), ← hl2,
      finsupp.total_apply, finsupp.sum, eq_comm],
  refine finset.sum_subset hl1 (λ x _ hx, _),
  rw [finsupp.not_mem_support_iff.1 hx, zero_smul]
end

lemma is_artinian_of_fg_of_artinian' {R M} [ring R] [add_comm_group M] [module R M]
  [is_artinian_ring R] (h : (⊤ : submodule R M).fg) : is_artinian R M :=
have is_artinian R (⊤ : submodule R M), from is_artinian_of_fg_of_artinian _ h,
by exactI is_artinian_of_linear_equiv (linear_equiv.of_top (⊤ : submodule R M) rfl)

/-- In a module over a artinian ring, the submodule generated by finitely many vectors is
artinian. -/
theorem is_artinian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R M]
  [is_artinian_ring R] {A : set M} (hA : A.finite) : is_artinian R (submodule.span R A) :=
is_artinian_of_fg_of_artinian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)

theorem is_artinian_ring_of_surjective (R) [ring R] (S) [ring S]
  (f : R →+* S) (hf : function.surjective f)
  [H : is_artinian_ring R] : is_artinian_ring S :=
begin
  rw [is_artinian_ring_iff, is_artinian_iff_well_founded] at H ⊢,
  exact order_embedding.well_founded (ideal.order_embedding_of_surjective f hf) H,
end

instance is_artinian_ring_range {R} [ring R] {S} [ring S] (f : R →+* S)
  [is_artinian_ring R] : is_artinian_ring f.range :=
is_artinian_ring_of_surjective R f.range f.range_restrict
  f.range_restrict_surjective

theorem is_artinian_ring_of_ring_equiv (R) [ring R] {S} [ring S]
  (f : R ≃+* S) [is_artinian_ring R] : is_artinian_ring S :=
is_artinian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective

namespace is_artinian_ring

open is_artinian

variables {R : Type*} [comm_ring R] [is_artinian_ring R]

lemma is_nilpotent_jacobson_bot : is_nilpotent (ideal.jacobson (⊥ : ideal R)) :=
begin
  let Jac := ideal.jacobson (⊥ : ideal R),
  let f : ℕ →o (ideal R)ᵒᵈ := ⟨λ n, Jac ^ n, λ _ _ h, ideal.pow_le_pow h⟩,
  obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → Jac ^ n = Jac ^ m := is_artinian.monotone_stabilizes f,
  refine ⟨n, _⟩,
  let J : ideal R := annihilator (Jac ^ n),
  suffices : J = ⊤,
  { have hJ : J • Jac ^ n = ⊥ := annihilator_smul (Jac ^ n),
    simpa only [this, top_smul, ideal.zero_eq_bot] using hJ },
  by_contradiction hJ, change J ≠ ⊤ at hJ,
  rcases is_artinian.set_has_minimal {J' : ideal R | J < J'} ⟨⊤, hJ.lt_top⟩
    with ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → I ≤ J' → I = J'⟩,
  rcases set_like.exists_of_lt hJJ' with ⟨x, hxJ', hxJ⟩,
  obtain rfl : J ⊔ ideal.span {x} = J',
  { refine hJ' (J ⊔ ideal.span {x}) _ _,
    { rw set_like.lt_iff_le_and_exists,
      exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩ },
    { exact (sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))) } },
  have : J ⊔ Jac • ideal.span {x} ≤ J ⊔ ideal.span {x},
    from sup_le_sup_left (smul_le.2 (λ _ _ _, submodule.smul_mem _ _)) _,
  have : Jac * ideal.span {x} ≤ J, --Need version 4 of Nakayamas lemma on Stacks
  { classical, by_contradiction H,
    refine H (smul_sup_le_of_le_smul_of_le_jacobson_bot
      (fg_span_singleton _) le_rfl (hJ' _ _ this).ge),
    exact lt_of_le_of_ne le_sup_left (λ h, H $ h.symm ▸ le_sup_right) },
  have : ideal.span {x} * Jac ^ (n + 1) ≤ ⊥,
    calc ideal.span {x} * Jac ^ (n + 1) = ideal.span {x} * Jac * Jac ^ n :
      by rw [pow_succ, ← mul_assoc]
    ... ≤ J * Jac ^ n : mul_le_mul (by rwa mul_comm) le_rfl
    ... = ⊥ : by simp [J],
  refine hxJ (mem_annihilator.2 (λ y hy, (mem_bot R).1 _)),
  refine this (mul_mem_mul (mem_span_singleton_self x) _),
  rwa [← hn (n + 1) (nat.le_succ _)]
end

end is_artinian_ring

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools


text:
-- Pruebas de la relación entre longitud y conc
-- ============================================

import tactic
open list

variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)

-- ----------------------------------------------------
-- Nota. Se usarán las definiciones y propiedades de
-- las funciones longitud y conc estudiadas
-- anteriormente.
-- ----------------------------------------------------

def longitud : list α → nat
| []        := 0
| (x :: xs) := longitud xs + 1

@[simp]
lemma longitud_nil :
  longitud ([] : list α) = 0 :=
rfl

@[simp]
lemma longitud_cons :
  longitud (x :: xs) = longitud xs + 1 :=
rfl

def conc : list α → list α → list α
| []        ys := ys
| (x :: xs) ys := x :: (conc xs ys)

@[simp]
lemma conc_nil :
  conc ([] : list α) ys = ys :=
rfl

@[simp]
lemma conc_cons :
  conc (x :: xs) ys = x :: (conc xs ys) :=
rfl

-- ----------------------------------------------------
-- Ejercicio 1. (p. 30) Demostrar que
--    longitud (conc xs ys) = longitud xs + longitud ys
-- ----------------------------------------------------

-- 1ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
begin
  induction xs with a as HI,
  { rw conc_nil,
    rw longitud_nil,
    rw zero_add, },
  { rw conc_cons,
    rw longitud_cons,
    rw HI,
    rw longitud_cons,
    rw add_assoc,
    rw add_comm (longitud ys),
    rw add_assoc, },
end

-- 2ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
begin
  induction xs with a as HI,
  { rw conc_nil,
    rw longitud_nil,
    rw zero_add, },
  { rw conc_cons,
    rw longitud_cons,
    rw HI,
    rw longitud_cons,
    -- library_search,
    exact add_right_comm (longitud as) (longitud ys) 1 },
end

-- 3ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
begin
  induction xs with a as HI,
  { rw conc_nil,
    rw longitud_nil,
    rw zero_add, },
  { rw conc_cons,
    rw longitud_cons,
    rw HI,
    rw longitud_cons,
    -- by hint,
    linarith, },
end

-- 4ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
begin
  induction xs with a as HI,
  { simp, },
  { simp [HI],
    linarith, },
end

-- 5ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
begin
  induction xs with a as HI,
  { simp, },
  { finish [HI],},
end

-- 6ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
by induction xs ; finish [*]

-- 7ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
begin
  induction xs with a as HI,
  { calc longitud (conc [] ys)
         = longitud ys                      : by rw conc_nil
     ... = 0 + longitud ys                  : by exact (zero_add (longitud ys)).symm
     ... = longitud [] + longitud ys        : by rw longitud_nil },
  { calc longitud (conc (a :: as) ys)
         = longitud (a :: conc as ys)       : by rw conc_cons
     ... = longitud (conc as ys) + 1        : by rw longitud_cons
     ... = (longitud as + longitud ys) + 1  : by rw HI
     ... = (longitud as + 1) + longitud ys  : by exact add_right_comm (longitud as) (longitud ys) 1
     ... = longitud (a :: as) + longitud ys : by rw longitud_cons, },
end

-- 8ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
list.rec_on xs
  ( show longitud (conc [] ys) = longitud [] + longitud ys, from
      calc longitud (conc [] ys)
           = longitud ys                      : by rw conc_nil
       ... = 0 + longitud ys                  : by exact (zero_add (longitud ys)).symm
       ... = longitud [] + longitud ys        : by rw longitud_nil )
  ( assume a as,
    assume HI : longitud (conc as ys) = longitud as + longitud ys,
    show longitud (conc (a :: as) ys) = longitud (a :: as) + longitud ys, from
      calc longitud (conc (a :: as) ys)
           = longitud (a :: conc as ys)       : by rw conc_cons
       ... = longitud (conc as ys) + 1        : by rw longitud_cons
       ... = (longitud as + longitud ys) + 1  : by rw HI
       ... = (longitud as + 1) + longitud ys  : by exact add_right_comm (longitud as) (longitud ys) 1
       ... = longitud (a :: as) + longitud ys : by rw longitud_cons)

-- 9ª demostración
example :
  longitud (conc xs ys) = longitud xs + longitud ys :=
list.rec_on xs
  ( by simp)
  ( λ a as HI, by simp [HI, add_right_comm])

-- 10ª demostración
lemma longitud_conc_1 :
  ∀ xs, longitud (conc xs ys) = longitud xs + longitud ys
| [] := by calc
    longitud (conc [] ys)
        = longitud ys                      : by rw conc_nil
    ... = 0 + longitud ys                  : by rw zero_add
    ... = longitud [] + longitud ys        : by rw longitud_nil
| (a :: as) := by calc
    longitud (conc (a :: as) ys)
        = longitud (a :: conc as ys)       : by rw conc_cons
    ... = longitud (conc as ys) + 1        : by rw longitud_cons
    ... = (longitud as + longitud ys) + 1  : by rw longitud_conc_1
    ... = (longitud as + 1) + longitud ys  : by exact add_right_comm (longitud as) (longitud ys) 1
    ... = longitud (a :: as) + longitud ys : by rw longitud_cons

-- 11ª demostración
lemma longitud_conc_2 :
  ∀ xs, longitud (conc xs ys) = longitud xs + longitud ys
| []        := by simp
| (a :: as) := by simp [longitud_conc_2 as, add_right_comm]

-- Comentarios sobre las funciones length y (++)
-- + Para usarlas hay que abrir el espacio de nombre
--   list escribiendo al principio del fichero
--      open list
-- + Se puede demostrar. Por ejemplo,
example :
  length (xs ++ ys) = length xs + length ys :=
by induction xs ; finish [*]

example :
  length (xs ++ ys) = length xs + length ys :=
-- by library_search
length_append xs ys

example :
  length (xs ++ ys) = length xs + length ys :=
by simp

author: jaalonso


text:
/-
Copyright (c) 2021 Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Heather Macbeth
-/
import analysis.normed_space.linear_isometry
import analysis.normed.group.add_torsor
import analysis.normed_space.basic
import linear_algebra.affine_space.restrict
import linear_algebra.affine_space.midpoint_zero

/-!
# Affine isometries

In this file we define `affine_isometry 𝕜 P P₂` to be an affine isometric embedding of normed
add-torsors `P` into `P₂` over normed `𝕜`-spaces and `affine_isometry_equiv` to be an affine
isometric equivalence between `P` and `P₂`.

We also prove basic lemmas and provide convenience constructors.  The choice of these lemmas and
constructors is closely modelled on those for the `linear_isometry` and `affine_map` theories.

Since many elementary properties don't require `‖x‖ = 0 → x = 0` we initially set up the theory for
`seminormed_add_comm_group` and specialize to `normed_add_comm_group` only when needed.

## Notation

We introduce the notation `P →ᵃⁱ[𝕜] P₂` for `affine_isometry 𝕜 P P₂`, and `P ≃ᵃⁱ[𝕜] P₂` for
`affine_isometry_equiv 𝕜 P P₂`.  In contrast with the notation `→ₗᵢ` for linear isometries, `≃ᵢ`
for isometric equivalences, etc., the "i" here is a superscript.  This is for aesthetic reasons to
match the superscript "a" (note that in mathlib `→ᵃ` is an affine map, since `→ₐ` has been taken by
algebra-homomorphisms.)

-/
open function set

variables (𝕜 : Type*) {V V₁ V₂ V₃ V₄ : Type*} {P₁ : Type*} (P P₂ : Type*) {P₃ P₄ : Type*}
  [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₁]
  [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃]
    [seminormed_add_comm_group V₄]
  [normed_space 𝕜 V] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃]
    [normed_space 𝕜 V₄]
  [pseudo_metric_space P] [metric_space P₁] [pseudo_metric_space P₂] [pseudo_metric_space P₃]
    [pseudo_metric_space P₄]
  [normed_add_torsor V P] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂]
    [normed_add_torsor V₃ P₃] [normed_add_torsor V₄ P₄]

include V V₂

/-- An `𝕜`-affine isometric embedding of one normed add-torsor over a normed `𝕜`-space into
another. -/
structure affine_isometry extends P →ᵃ[𝕜] P₂ :=
(norm_map : ∀ x : V, ‖linear x‖ = ‖x‖)

omit V V₂
variables {𝕜 P P₂}

-- `→ᵃᵢ` would be more consistent with the linear isometry notation, but it is uglier
notation P ` →ᵃⁱ[`:25 𝕜:25 `] `:0 P₂:0 := affine_isometry 𝕜 P P₂

namespace affine_isometry
variables (f : P →ᵃⁱ[𝕜] P₂)

/-- The underlying linear map of an affine isometry is in fact a linear isometry. -/
protected def linear_isometry : V →ₗᵢ[𝕜] V₂ :=
{ norm_map' := f.norm_map,
  .. f.linear }

@[simp] lemma linear_eq_linear_isometry : f.linear = f.linear_isometry.to_linear_map :=
by { ext, refl }

include V V₂
instance : has_coe_to_fun (P →ᵃⁱ[𝕜] P₂) (λ _, P → P₂) := ⟨λ f, f.to_fun⟩
omit V V₂

@[simp] lemma coe_to_affine_map : ⇑f.to_affine_map = f := rfl

include V V₂
lemma to_affine_map_injective : injective (to_affine_map : (P →ᵃⁱ[𝕜] P₂) → (P →ᵃ[𝕜] P₂))
| ⟨f, _⟩ ⟨g, _⟩ rfl := rfl

lemma coe_fn_injective : @injective (P →ᵃⁱ[𝕜] P₂) (P → P₂) coe_fn :=
affine_map.coe_fn_injective.comp to_affine_map_injective

@[ext] lemma ext {f g : P →ᵃⁱ[𝕜] P₂} (h : ∀ x, f x = g x) : f = g :=
coe_fn_injective $ funext h
omit V V₂

end affine_isometry

namespace linear_isometry
variables (f : V →ₗᵢ[𝕜] V₂)

/-- Reinterpret a linear isometry as an affine isometry. -/
def to_affine_isometry : V →ᵃⁱ[𝕜] V₂ :=
{ norm_map := f.norm_map,
  .. f.to_linear_map.to_affine_map }

@[simp] lemma coe_to_affine_isometry : ⇑(f.to_affine_isometry : V →ᵃⁱ[𝕜] V₂) = f := rfl

@[simp] lemma to_affine_isometry_linear_isometry : f.to_affine_isometry.linear_isometry = f :=
by { ext, refl }

-- somewhat arbitrary choice of simp direction
@[simp] lemma to_affine_isometry_to_affine_map :
  f.to_affine_isometry.to_affine_map = f.to_linear_map.to_affine_map :=
rfl

end linear_isometry

namespace affine_isometry

/-- We use `f₁` when we need the domain to be a `normed_space`. -/
variables (f : P →ᵃⁱ[𝕜] P₂) (f₁ : P₁ →ᵃⁱ[𝕜] P₂)

@[simp] lemma map_vadd (p : P) (v : V) : f (v +ᵥ p) = f.linear_isometry v +ᵥ f p :=
f.to_affine_map.map_vadd p v

@[simp] lemma map_vsub (p1 p2 : P) : f.linear_isometry (p1 -ᵥ p2) = f p1 -ᵥ f p2 :=
f.to_affine_map.linear_map_vsub p1 p2

@[simp] lemma dist_map (x y : P) : dist (f x) (f y) = dist x y :=
by rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linear_isometry.norm_map]

@[simp] lemma nndist_map (x y : P) : nndist (f x) (f y) = nndist x y := by simp [nndist_dist]

@[simp] lemma edist_map (x y : P) : edist (f x) (f y) = edist x y := by simp [edist_dist]

protected lemma isometry : isometry f := f.edist_map

protected lemma injective : injective f₁ := f₁.isometry.injective

@[simp] lemma map_eq_iff {x y : P₁} : f₁ x = f₁ y ↔ x = y := f₁.injective.eq_iff

lemma map_ne {x y : P₁} (h : x ≠ y) : f₁ x ≠ f₁ y := f₁.injective.ne h

protected lemma lipschitz : lipschitz_with 1 f := f.isometry.lipschitz

protected lemma antilipschitz : antilipschitz_with 1 f := f.isometry.antilipschitz

@[continuity] protected lemma continuous : continuous f := f.isometry.continuous

lemma ediam_image (s : set P) : emetric.diam (f '' s) = emetric.diam s :=
f.isometry.ediam_image s

lemma ediam_range : emetric.diam (range f) = emetric.diam (univ : set P) :=
f.isometry.ediam_range

lemma diam_image (s : set P) : metric.diam (f '' s) = metric.diam s :=
f.isometry.diam_image s

lemma diam_range : metric.diam (range f) = metric.diam (univ : set P) :=
f.isometry.diam_range

@[simp] lemma comp_continuous_iff {α : Type*} [topological_space α] {g : α → P} :
  continuous (f ∘ g) ↔ continuous g :=
f.isometry.comp_continuous_iff

include V
/-- The identity affine isometry. -/
def id : P →ᵃⁱ[𝕜] P := ⟨affine_map.id 𝕜 P, λ x, rfl⟩

@[simp] lemma coe_id : ⇑(id : P →ᵃⁱ[𝕜] P) = _root_.id := rfl

@[simp] lemma id_apply (x : P) : (affine_isometry.id : P →ᵃⁱ[𝕜] P) x = x := rfl

@[simp] lemma id_to_affine_map : (id.to_affine_map : P →ᵃ[𝕜] P) = affine_map.id 𝕜 P := rfl

instance : inhabited (P →ᵃⁱ[𝕜] P) := ⟨id⟩

include V₂ V₃
/-- Composition of affine isometries. -/
def comp (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) : P →ᵃⁱ[𝕜] P₃ :=
⟨g.to_affine_map.comp f.to_affine_map, λ x, (g.norm_map _).trans (f.norm_map _)⟩

@[simp] lemma coe_comp (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) :
  ⇑(g.comp f) = g ∘ f :=
rfl

omit V V₂ V₃

@[simp] lemma id_comp : (id : P₂ →ᵃⁱ[𝕜] P₂).comp f = f := ext $ λ x, rfl

@[simp] lemma comp_id : f.comp id = f := ext $ λ x, rfl

include V V₂ V₃ V₄
lemma comp_assoc (f : P₃ →ᵃⁱ[𝕜] P₄) (g : P₂ →ᵃⁱ[𝕜] P₃) (h : P →ᵃⁱ[𝕜] P₂) :
  (f.comp g).comp h = f.comp (g.comp h) :=
rfl
omit V₂ V₃ V₄

instance : monoid (P →ᵃⁱ[𝕜] P) :=
{ one := id,
  mul := comp,
  mul_assoc := comp_assoc,
  one_mul := id_comp,
  mul_one := comp_id }

@[simp] lemma coe_one : ⇑(1 : P →ᵃⁱ[𝕜] P) = _root_.id := rfl
@[simp] lemma coe_mul (f g : P →ᵃⁱ[𝕜] P) : ⇑(f * g) = f ∘ g := rfl

end affine_isometry

namespace affine_subspace

include V

/-- `affine_subspace.subtype` as an `affine_isometry`. -/
def subtypeₐᵢ (s : affine_subspace 𝕜 P) [nonempty s] : s →ᵃⁱ[𝕜] P :=
{ norm_map := s.direction.subtypeₗᵢ.norm_map,
  .. s.subtype }

lemma subtypeₐᵢ_linear (s : affine_subspace 𝕜 P) [nonempty s] :
  s.subtypeₐᵢ.linear = s.direction.subtype :=
rfl

@[simp] lemma subtypeₐᵢ_linear_isometry (s : affine_subspace 𝕜 P) [nonempty s] :
  s.subtypeₐᵢ.linear_isometry = s.direction.subtypeₗᵢ :=
rfl

@[simp] lemma coe_subtypeₐᵢ (s : affine_subspace 𝕜 P) [nonempty s] : ⇑s.subtypeₐᵢ = s.subtype :=
rfl

@[simp] lemma subtypeₐᵢ_to_affine_map (s : affine_subspace 𝕜 P) [nonempty s] :
  s.subtypeₐᵢ.to_affine_map = s.subtype :=
rfl

end affine_subspace

variables (𝕜 P P₂)
include V V₂

/-- A affine isometric equivalence between two normed vector spaces. -/
structure affine_isometry_equiv extends P ≃ᵃ[𝕜] P₂ :=
(norm_map : ∀ x, ‖linear x‖ = ‖x‖)

variables {𝕜 P P₂}
omit V V₂

-- `≃ᵃᵢ` would be more consistent with the linear isometry equiv notation, but it is uglier
notation P ` ≃ᵃⁱ[`:25 𝕜:25 `] `:0 P₂:0 := affine_isometry_equiv 𝕜 P P₂

namespace affine_isometry_equiv

variables (e : P ≃ᵃⁱ[𝕜] P₂)

/-- The underlying linear equiv of an affine isometry equiv is in fact a linear isometry equiv. -/
protected def linear_isometry_equiv : V ≃ₗᵢ[𝕜] V₂ :=
{ norm_map' := e.norm_map,
  .. e.linear }

@[simp] lemma linear_eq_linear_isometry : e.linear = e.linear_isometry_equiv.to_linear_equiv :=
by { ext, refl }

include V V₂
instance : has_coe_to_fun (P ≃ᵃⁱ[𝕜] P₂) (λ _, P → P₂) := ⟨λ f, f.to_fun⟩

@[simp] lemma coe_mk (e : P ≃ᵃ[𝕜] P₂) (he : ∀ x, ‖e.linear x‖ = ‖x‖) :
  ⇑(mk e he) = e :=
rfl

@[simp] lemma coe_to_affine_equiv (e : P ≃ᵃⁱ[𝕜] P₂) : ⇑e.to_affine_equiv = e := rfl

lemma to_affine_equiv_injective : injective (to_affine_equiv : (P ≃ᵃⁱ[𝕜] P₂) → (P ≃ᵃ[𝕜] P₂))
| ⟨e, _⟩ ⟨_, _⟩ rfl := rfl

@[ext] lemma ext {e e' : P ≃ᵃⁱ[𝕜] P₂} (h : ∀ x, e x = e' x) : e = e' :=
to_affine_equiv_injective $ affine_equiv.ext h
omit V V₂

/-- Reinterpret a `affine_isometry_equiv` as a `affine_isometry`. -/
def to_affine_isometry : P →ᵃⁱ[𝕜] P₂ := ⟨e.1.to_affine_map, e.2⟩

@[simp] lemma coe_to_affine_isometry : ⇑e.to_affine_isometry = e := rfl

/-- Construct an affine isometry equivalence by verifying the relation between the map and its
linear part at one base point. Namely, this function takes a map `e : P₁ → P₂`, a linear isometry
equivalence `e' : V₁ ≃ᵢₗ[k] V₂`, and a point `p` such that for any other point `p'` we have
`e p' = e' (p' -ᵥ p) +ᵥ e p`. -/
def mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁) (h : ∀ p' : P₁, e p' = e' (p' -ᵥ p) +ᵥ e p) :
  P₁ ≃ᵃⁱ[𝕜] P₂ :=
{ norm_map := e'.norm_map,
  .. affine_equiv.mk' e e'.to_linear_equiv p h }

@[simp] lemma coe_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) : ⇑(mk' e e' p h) = e := rfl
@[simp] lemma linear_isometry_equiv_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) :
  (mk' e e' p h).linear_isometry_equiv = e' := by { ext, refl }

end affine_isometry_equiv

namespace linear_isometry_equiv
variables (e : V ≃ₗᵢ[𝕜] V₂)

/-- Reinterpret a linear isometry equiv as an affine isometry equiv. -/
def to_affine_isometry_equiv  : V ≃ᵃⁱ[𝕜] V₂ :=
{ norm_map := e.norm_map,
  .. e.to_linear_equiv.to_affine_equiv }

@[simp] lemma coe_to_affine_isometry_equiv : ⇑(e.to_affine_isometry_equiv : V ≃ᵃⁱ[𝕜] V₂) = e := rfl

@[simp] lemma to_affine_isometry_equiv_linear_isometry_equiv :
  e.to_affine_isometry_equiv.linear_isometry_equiv = e :=
by { ext, refl }

-- somewhat arbitrary choice of simp direction
@[simp] lemma to_affine_isometry_equiv_to_affine_equiv :
  e.to_affine_isometry_equiv.to_affine_equiv = e.to_linear_equiv.to_affine_equiv :=
rfl

-- somewhat arbitrary choice of simp direction
@[simp] lemma to_affine_isometry_equiv_to_affine_isometry :
  e.to_affine_isometry_equiv.to_affine_isometry = e.to_linear_isometry.to_affine_isometry :=
rfl

end linear_isometry_equiv

namespace affine_isometry_equiv
variables (e : P ≃ᵃⁱ[𝕜] P₂)

protected lemma isometry : isometry e := e.to_affine_isometry.isometry

/-- Reinterpret a `affine_isometry_equiv` as an `isometry_equiv`. -/
def to_isometry_equiv : P ≃ᵢ P₂ := ⟨e.to_affine_equiv.to_equiv, e.isometry⟩

@[simp] lemma coe_to_isometry_equiv : ⇑e.to_isometry_equiv = e := rfl

include V V₂
lemma range_eq_univ (e : P ≃ᵃⁱ[𝕜] P₂) : set.range e = set.univ :=
by { rw ← coe_to_isometry_equiv, exact isometry_equiv.range_eq_univ _, }
omit V V₂

/-- Reinterpret a `affine_isometry_equiv` as an `homeomorph`. -/
def to_homeomorph : P ≃ₜ P₂ := e.to_isometry_equiv.to_homeomorph

@[simp] lemma coe_to_homeomorph : ⇑e.to_homeomorph = e := rfl

protected lemma continuous : continuous e := e.isometry.continuous
protected lemma continuous_at {x} : continuous_at e x := e.continuous.continuous_at
protected lemma continuous_on {s} : continuous_on e s := e.continuous.continuous_on

protected lemma continuous_within_at {s x} : continuous_within_at e s x :=
e.continuous.continuous_within_at

variables (𝕜 P)
include V

/-- Identity map as a `affine_isometry_equiv`. -/
def refl : P ≃ᵃⁱ[𝕜] P := ⟨affine_equiv.refl 𝕜 P, λ x, rfl⟩

variables {𝕜 P}

instance : inhabited (P ≃ᵃⁱ[𝕜] P) := ⟨refl 𝕜 P⟩

@[simp] lemma coe_refl : ⇑(refl 𝕜 P) = id := rfl
@[simp] lemma to_affine_equiv_refl : (refl 𝕜 P).to_affine_equiv = affine_equiv.refl 𝕜 P := rfl
@[simp] lemma to_isometry_equiv_refl : (refl 𝕜 P).to_isometry_equiv = isometry_equiv.refl P := rfl
@[simp] lemma to_homeomorph_refl : (refl 𝕜 P).to_homeomorph = homeomorph.refl P := rfl
omit V

/-- The inverse `affine_isometry_equiv`. -/
def symm : P₂ ≃ᵃⁱ[𝕜] P :=
{ norm_map := e.linear_isometry_equiv.symm.norm_map,
  .. e.to_affine_equiv.symm }

@[simp] lemma apply_symm_apply (x : P₂) : e (e.symm x) = x := e.to_affine_equiv.apply_symm_apply x
@[simp] lemma symm_apply_apply (x : P) : e.symm (e x) = x := e.to_affine_equiv.symm_apply_apply x
@[simp] lemma symm_symm : e.symm.symm = e := ext $ λ x, rfl

@[simp] lemma to_affine_equiv_symm : e.to_affine_equiv.symm = e.symm.to_affine_equiv := rfl
@[simp] lemma to_isometry_equiv_symm : e.to_isometry_equiv.symm = e.symm.to_isometry_equiv := rfl
@[simp] lemma to_homeomorph_symm : e.to_homeomorph.symm = e.symm.to_homeomorph := rfl

include V₃
/-- Composition of `affine_isometry_equiv`s as a `affine_isometry_equiv`. -/
def trans (e' : P₂ ≃ᵃⁱ[𝕜] P₃) : P ≃ᵃⁱ[𝕜] P₃ :=
⟨e.to_affine_equiv.trans e'.to_affine_equiv, λ x, (e'.norm_map _).trans (e.norm_map _)⟩

include V V₂
@[simp] lemma coe_trans (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ := rfl
omit V V₂ V₃

@[simp] lemma trans_refl : e.trans (refl 𝕜 P₂) = e := ext $ λ x, rfl
@[simp] lemma refl_trans : (refl 𝕜 P).trans e = e := ext $ λ x, rfl
@[simp] lemma self_trans_symm : e.trans e.symm = refl 𝕜 P := ext e.symm_apply_apply
@[simp] lemma symm_trans_self : e.symm.trans e = refl 𝕜 P₂ := ext e.apply_symm_apply

include V V₂ V₃
@[simp] lemma coe_symm_trans (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) :
  ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm :=
rfl

include V₄
lemma trans_assoc (ePP₂ : P ≃ᵃⁱ[𝕜] P₂) (eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃) (eGG' : P₃ ≃ᵃⁱ[𝕜] P₄) :
  ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG' :=
rfl
omit V₂ V₃ V₄

/-- The group of affine isometries of a `normed_add_torsor`, `P`. -/
instance : group (P ≃ᵃⁱ[𝕜] P) :=
{ mul := λ e₁ e₂, e₂.trans e₁,
  one := refl _ _,
  inv := symm,
  one_mul := trans_refl,
  mul_one := refl_trans,
  mul_assoc := λ _ _ _, trans_assoc _ _ _,
  mul_left_inv := self_trans_symm }

@[simp] lemma coe_one : ⇑(1 : P ≃ᵃⁱ[𝕜] P) = id := rfl
@[simp] lemma coe_mul (e e' : P ≃ᵃⁱ[𝕜] P) : ⇑(e * e') = e ∘ e' := rfl
@[simp] lemma coe_inv (e : P ≃ᵃⁱ[𝕜] P) : ⇑(e⁻¹) = e.symm := rfl

omit V

@[simp] lemma map_vadd (p : P) (v : V) : e (v +ᵥ p) = e.linear_isometry_equiv v +ᵥ e p :=
e.to_affine_isometry.map_vadd p v

@[simp] lemma map_vsub (p1 p2 : P) : e.linear_isometry_equiv (p1 -ᵥ p2) = e p1 -ᵥ e p2 :=
e.to_affine_isometry.map_vsub p1 p2

@[simp] lemma dist_map (x y : P) : dist (e x) (e y) = dist x y :=
e.to_affine_isometry.dist_map x y

@[simp] lemma edist_map (x y : P) : edist (e x) (e y) = edist x y :=
e.to_affine_isometry.edist_map x y

protected lemma bijective : bijective e := e.1.bijective
protected lemma injective : injective e := e.1.injective
protected lemma surjective : surjective e := e.1.surjective

@[simp] lemma map_eq_iff {x y : P} : e x = e y ↔ x = y := e.injective.eq_iff

lemma map_ne {x y : P} (h : x ≠ y) : e x ≠ e y := e.injective.ne h

protected lemma lipschitz : lipschitz_with 1 e := e.isometry.lipschitz

protected lemma antilipschitz : antilipschitz_with 1 e := e.isometry.antilipschitz

@[simp] lemma ediam_image (s : set P) : emetric.diam (e '' s) = emetric.diam s :=
e.isometry.ediam_image s

@[simp] lemma diam_image (s : set P) : metric.diam (e '' s) = metric.diam s :=
e.isometry.diam_image s

variables {α : Type*} [topological_space α]

@[simp] lemma comp_continuous_on_iff {f : α → P} {s : set α} :
  continuous_on (e ∘ f) s ↔ continuous_on f s :=
e.isometry.comp_continuous_on_iff

@[simp] lemma comp_continuous_iff {f : α → P} :
  continuous (e ∘ f) ↔ continuous f :=
e.isometry.comp_continuous_iff

section constructions

variables (𝕜)
/-- The map `v ↦ v +ᵥ p` as an affine isometric equivalence between `V` and `P`. -/
def vadd_const (p : P) : V ≃ᵃⁱ[𝕜] P :=
{ norm_map := λ x, rfl,
  .. affine_equiv.vadd_const 𝕜 p }
variables {𝕜}

include V
@[simp] lemma coe_vadd_const (p : P) : ⇑(vadd_const 𝕜 p) = λ v, v +ᵥ p := rfl

@[simp] lemma coe_vadd_const_symm (p : P) : ⇑(vadd_const 𝕜 p).symm = λ p', p' -ᵥ p :=
rfl

@[simp] lemma vadd_const_to_affine_equiv (p : P) :
  (vadd_const 𝕜 p).to_affine_equiv = affine_equiv.vadd_const 𝕜 p :=
rfl
omit V

variables (𝕜)
/-- `p' ↦ p -ᵥ p'` as an affine isometric equivalence. -/
def const_vsub (p : P) : P ≃ᵃⁱ[𝕜] V :=
{ norm_map := norm_neg,
  .. affine_equiv.const_vsub 𝕜 p }
variables {𝕜}

include V
@[simp] lemma coe_const_vsub (p : P) : ⇑(const_vsub 𝕜 p) = (-ᵥ) p := rfl

@[simp] lemma symm_const_vsub (p : P) :
  (const_vsub 𝕜 p).symm
  = (linear_isometry_equiv.neg 𝕜).to_affine_isometry_equiv.trans (vadd_const 𝕜 p) :=
by { ext, refl }
omit V

variables (𝕜 P)
/-- Translation by `v` (that is, the map `p ↦ v +ᵥ p`) as an affine isometric automorphism of `P`.
-/
def const_vadd (v : V) : P ≃ᵃⁱ[𝕜] P :=
{ norm_map := λ x, rfl,
  .. affine_equiv.const_vadd 𝕜 P v }
variables {𝕜 P}

@[simp] lemma coe_const_vadd (v : V) : ⇑(const_vadd 𝕜 P v : P ≃ᵃⁱ[𝕜] P) = (+ᵥ) v := rfl

@[simp] lemma const_vadd_zero : const_vadd 𝕜 P (0:V) = refl 𝕜 P := ext $ zero_vadd V

include 𝕜 V
/-- The map `g` from `V` to `V₂` corresponding to a map `f` from `P` to `P₂`, at a base point `p`,
is an isometry if `f` is one. -/
lemma vadd_vsub {f : P → P₂} (hf : isometry f) {p : P} {g : V → V₂}
  (hg : ∀ v, g v = f (v +ᵥ p) -ᵥ f p) : isometry g :=
begin
  convert (vadd_const 𝕜 (f p)).symm.isometry.comp (hf.comp (vadd_const 𝕜 p).isometry),
  exact funext hg
end
omit 𝕜

variables (𝕜)
/-- Point reflection in `x` as an affine isometric automorphism. -/
def point_reflection (x : P) : P ≃ᵃⁱ[𝕜] P := (const_vsub 𝕜 x).trans (vadd_const 𝕜 x)
variables {𝕜}

lemma point_reflection_apply (x y : P) : (point_reflection 𝕜 x) y = x -ᵥ y +ᵥ x := rfl

@[simp] lemma point_reflection_to_affine_equiv (x : P) :
  (point_reflection 𝕜 x).to_affine_equiv = affine_equiv.point_reflection 𝕜 x := rfl

@[simp] lemma point_reflection_self (x : P) : point_reflection 𝕜 x x = x :=
affine_equiv.point_reflection_self 𝕜 x

lemma point_reflection_involutive (x : P) : function.involutive (point_reflection 𝕜 x) :=
equiv.point_reflection_involutive x

@[simp] lemma point_reflection_symm (x : P) : (point_reflection 𝕜 x).symm = point_reflection 𝕜 x :=
to_affine_equiv_injective $ affine_equiv.point_reflection_symm 𝕜 x

@[simp] lemma dist_point_reflection_fixed (x y : P) :
  dist (point_reflection 𝕜 x y) x = dist y x :=
by rw [← (point_reflection 𝕜 x).dist_map y x, point_reflection_self]

lemma dist_point_reflection_self' (x y : P) :
  dist (point_reflection 𝕜 x y) y = ‖bit0 (x -ᵥ y)‖ :=
by rw [point_reflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, bit0]

lemma dist_point_reflection_self (x y : P) :
  dist (point_reflection 𝕜 x y) y = ‖(2:𝕜)‖ * dist x y :=
by rw [dist_point_reflection_self', ← two_smul' 𝕜 (x -ᵥ y), norm_smul, ← dist_eq_norm_vsub V]

lemma point_reflection_fixed_iff [invertible (2:𝕜)] {x y : P} :
  point_reflection 𝕜 x y = y ↔ y = x :=
affine_equiv.point_reflection_fixed_iff_of_module 𝕜

variables [normed_space ℝ V]

lemma dist_point_reflection_self_real (x y : P) :
  dist (point_reflection ℝ x y) y = 2 * dist x y :=
by { rw [dist_point_reflection_self, real.norm_two] }

@[simp] lemma point_reflection_midpoint_left (x y : P) :
  point_reflection ℝ (midpoint ℝ x y) x = y :=
affine_equiv.point_reflection_midpoint_left x y

@[simp] lemma point_reflection_midpoint_right (x y : P) :
  point_reflection ℝ (midpoint ℝ x y) y = x :=
affine_equiv.point_reflection_midpoint_right x y

end constructions

end affine_isometry_equiv

include V V₂

/-- If `f` is an affine map, then its linear part is continuous iff `f` is continuous. -/
lemma affine_map.continuous_linear_iff {f : P →ᵃ[𝕜] P₂} :
  continuous f.linear ↔ continuous f :=
begin
  inhabit P,
  have : (f.linear : V → V₂) =
    (affine_isometry_equiv.vadd_const 𝕜 $ f default).to_homeomorph.symm ∘ f ∘
      (affine_isometry_equiv.vadd_const 𝕜 default).to_homeomorph,
  { ext v, simp },
  rw this,
  simp only [homeomorph.comp_continuous_iff, homeomorph.comp_continuous_iff'],
end

/-- If `f` is an affine map, then its linear part is an open map iff `f` is an open map. -/
lemma affine_map.is_open_map_linear_iff {f : P →ᵃ[𝕜] P₂} :
  is_open_map f.linear ↔ is_open_map f :=
begin
  inhabit P,
  have : (f.linear : V → V₂) =
    (affine_isometry_equiv.vadd_const 𝕜 $ f default).to_homeomorph.symm ∘ f ∘
      (affine_isometry_equiv.vadd_const 𝕜 default).to_homeomorph,
  { ext v, simp },
  rw this,
  simp only [homeomorph.comp_is_open_map_iff, homeomorph.comp_is_open_map_iff'],
end

local attribute [instance, nolint fails_quickly] affine_subspace.nonempty_map

include V₁
omit V

namespace affine_subspace

/--
An affine subspace is isomorphic to its image under an injective affine map.
This is the affine version of `submodule.equiv_map_of_injective`.
-/
@[simps]
noncomputable def equiv_map_of_injective (E: affine_subspace 𝕜 P₁) [nonempty E]
  (φ : P₁ →ᵃ[𝕜] P₂) (hφ : function.injective φ) : E ≃ᵃ[𝕜] E.map φ :=
{ linear :=
    (E.direction.equiv_map_of_injective φ.linear (φ.linear_injective_iff.mpr hφ)).trans
      (linear_equiv.of_eq _ _ (affine_subspace.map_direction _ _).symm),
  map_vadd' := λ p v, subtype.ext $ φ.map_vadd p v,
  .. equiv.set.image _ (E : set P₁) hφ }

/--
Restricts an affine isometry to an affine isometry equivalence between a nonempty affine
subspace `E` and its image.

This is an isometry version of `affine_subspace.equiv_map`, having a stronger premise and a stronger
conclusion.
-/
noncomputable def isometry_equiv_map
  (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] : E ≃ᵃⁱ[𝕜] E.map φ.to_affine_map :=
⟨E.equiv_map_of_injective φ.to_affine_map φ.injective, (λ _, φ.norm_map _)⟩

@[simp]
lemma isometry_equiv_map.apply_symm_apply
  {E : affine_subspace 𝕜 P₁} [nonempty E]
  {φ : P₁ →ᵃⁱ[𝕜] P₂} (x : E.map φ.to_affine_map) :
  φ ((E.isometry_equiv_map φ).symm x) = x :=
congr_arg coe $ (E.isometry_equiv_map φ).apply_symm_apply _

@[simp]
lemma isometry_equiv_map.coe_apply
  (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] (g: E) :
  ↑(E.isometry_equiv_map φ g) = φ g := rfl

@[simp]
lemma isometry_equiv_map.to_affine_map_eq
  (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] :
  (E.isometry_equiv_map φ).to_affine_map = E.equiv_map_of_injective φ.to_affine_map φ.injective :=
rfl

end affine_subspace