<commit_before>/-
Copyright (c) 2021 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import analysis.complex.circle
import linear_algebra.determinant
import linear_algebra.general_linear_group

/-!
# Isometries of the Complex Plane

The lemma `linear_isometry_complex` states the classification of isometries in the complex plane.
Specifically, isometries with rotations but without translation.
The proof involves:
1. creating a linear isometry `g` with two fixed points, `g(0) = 0`, `g(1) = 1`
2. applying `linear_isometry_complex_aux` to `g`
The proof of `linear_isometry_complex_aux` is separated in the following parts:
1. show that the real parts match up: `linear_isometry.re_apply_eq_re`
2. show that I maps to either I or -I
3. every z is a linear combination of a + b * I

## References

* [Isometries of the Complex Plane](http://helmut.knaust.info/mediawiki/images/b/b5/Iso.pdf)
-/
noncomputable theory

open complex
open_locale complex_conjugate

local notation `|` x `|` := complex.abs x

/-- An element of the unit circle defines a `linear_isometry_equiv` from `ℂ` to itself, by
rotation. -/
def rotation : circle →* (ℂ ≃ₗᵢ[ℝ] ℂ) :=
{ to_fun := λ a,
  { norm_map' := λ x, show |a * x| = |x|, by rw [complex.abs_mul, abs_coe_circle, one_mul],
    ..distrib_mul_action.to_linear_equiv ℝ ℂ a },
  map_one' := linear_isometry_equiv.ext $ one_smul _,
  map_mul' := λ _ _, linear_isometry_equiv.ext $ mul_smul _ _ }

@[simp] lemma rotation_apply (a : circle) (z : ℂ) : rotation a z = a * z := rfl

lemma rotation_ne_conj_lie (a : circle) : rotation a ≠ conj_lie :=
begin
  intro h,
  have h1 : rotation a 1 = conj 1 := linear_isometry_equiv.congr_fun h 1,<commit_msg>feat(analysis/complex/isometry): `rotation_symm` (#11891)<commit_after>/-
Copyright (c) 2021 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import analysis.complex.circle
import linear_algebra.determinant
import linear_algebra.general_linear_group

/-!
# Isometries of the Complex Plane

The lemma `linear_isometry_complex` states the classification of isometries in the complex plane.
Specifically, isometries with rotations but without translation.
The proof involves:
1. creating a linear isometry `g` with two fixed points, `g(0) = 0`, `g(1) = 1`
2. applying `linear_isometry_complex_aux` to `g`
The proof of `linear_isometry_complex_aux` is separated in the following parts:
1. show that the real parts match up: `linear_isometry.re_apply_eq_re`
2. show that I maps to either I or -I
3. every z is a linear combination of a + b * I

## References

* [Isometries of the Complex Plane](http://helmut.knaust.info/mediawiki/images/b/b5/Iso.pdf)
-/
noncomputable theory

open complex
open_locale complex_conjugate

local notation `|` x `|` := complex.abs x

/-- An element of the unit circle defines a `linear_isometry_equiv` from `ℂ` to itself, by
rotation. -/
def rotation : circle →* (ℂ ≃ₗᵢ[ℝ] ℂ) :=
{ to_fun := λ a,
  { norm_map' := λ x, show |a * x| = |x|, by rw [complex.abs_mul, abs_coe_circle, one_mul],
    ..distrib_mul_action.to_linear_equiv ℝ ℂ a },
  map_one' := linear_isometry_equiv.ext $ one_smul _,
  map_mul' := λ _ _, linear_isometry_equiv.ext $ mul_smul _ _ }

@[simp] lemma rotation_apply (a : circle) (z : ℂ) : rotation a z = a * z := rfl

@[simp] lemma rotation_symm (a : circle) : (rotation a).symm = rotation a⁻¹ :=
linear_isometry_equiv.ext $ λ x, rfl

lemma rotation_ne_conj_lie (a : circle) : rotation a ≠ conj_lie :=
begin
  intro h,
  have h1 : rotation a 1 = conj 1 := linear_isometry_equiv.congr_fun h 1,
{'fraction_non_alphanumeric': 0.1077007399287476, 'fraction_numerical': 0.012332145793368046, 'mean_word_length': 4.33625730994152, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3204119', 'n_tokens_mistral': 1358, 'n_tokens_neox': 1277, 'n_words': 438}