TITLE: Group Action determined by equations
QUESTION [1 upvotes]: Let $G$ a group, $X$ a set. An action of $G$ on $X$ is given by a mapping $(g,x) \to g \cdot x$, which satisfies $g \cdot (h \cdot x) = (gh) \cdot x$ and $e_G \cdot x = x$.
In other words, to determine an action one must know how every element of the group acts on every element of the set.

Can an action be determined by means other then giving explicitly the
  action of every element of $G$ on every element of $X$?

What if I have several equations (depending on elements of X and G, and the action of G) that give some information of the action - when are the equations strong enough so they induce an action on the entire set? Furthermore, are there cases where I can fully recover the action?
For example, suppose that $X$ is a (given) set of elements of a field extension $K/k$, and $G \subseteq Gal(K / k)$. We would like to extend that action of $G$ to $K(X)$, such that the extended action satisfies several equations.
Is there any theory in mathematics that asks and answers this sort of questions?

REPLY [1 votes]: Let $F_n$ denote the free group of rank $n$. You can characterise the action of $\operatorname{Aut}(F_2)$ on $F_2$ by an equation as follows:

Theorem (Theorem 3.9, Magnus, Karrass and Solitar, Combinatorial group theory, 1975 (2nd Ed.))
A map $f: a\mapsto x$, $b\mapsto y$, where $x, y\in F_2$, is an automorphism of $F_2$ if and only if there exists an element $z\in F_2$ such that $$z^{-1}[x, y]z=[a, b]~\text{or}~z^{-1}[x, y]z=[a, b]^{-1}.$$

Hence, automorphisms somehow correspond to solutions to the equations $z^{-1}[x, y]z=[a, b]^{\pm1}$. On the other hand, automorphisms of $F_n$ for $n>2$ cannot be described in this way. In fact, I understand that they cannot be characterised precisely using first-order sentences (although I cannot find a reference for this).


text:
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Chris Hughes, Mario Carneiro
-/
import algebra.associated
import linear_algebra.basic
import order.zorn
import order.atoms
import order.compactly_generated
import tactic.abel
import data.nat.choose.sum
import linear_algebra.finsupp
/-!

# Ideals over a ring

This file defines `ideal R`, the type of (left) ideals over a ring `R`.
Note that over commutative rings, left ideals and two-sided ideals are equivalent.

## Implementation notes

`ideal R` is implemented using `submodule R R`, where `•` is interpreted as `*`.

## TODO

Support right ideals, and two-sided ideals over non-commutative rings.
-/

universes u v w
variables {α : Type u} {β : Type v}
open set function

open_locale classical big_operators pointwise

/-- A (left) ideal in a semiring `R` is an additive submonoid `s` such that
`a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup.  -/
@[reducible] def ideal (R : Type u) [semiring R] := submodule R R

section semiring

namespace ideal
variables [semiring α] (I : ideal α) {a b : α}

protected lemma zero_mem : (0 : α) ∈ I := I.zero_mem

protected lemma add_mem : a ∈ I → b ∈ I → a + b ∈ I := I.add_mem

variables (a)
lemma mul_mem_left : b ∈ I → a * b ∈ I := I.smul_mem a
variables {a}

@[ext] lemma ext {I J : ideal α} (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J :=
submodule.ext h

lemma sum_mem (I : ideal α) {ι : Type*} {t : finset ι} {f : ι → α} :
  (∀c∈t, f c ∈ I) → (∑ i in t, f i) ∈ I := submodule.sum_mem I

theorem eq_top_of_unit_mem
  (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤ :=
eq_top_iff.2 $ λ z _, calc
    z = z * (y * x) : by simp [h]
  ... = (z * y) * x : eq.symm $ mul_assoc z y x
  ... ∈ I : I.mul_mem_left _ hx

theorem eq_top_of_is_unit_mem {x} (hx : x ∈ I) (h : is_unit x) : I = ⊤ :=
let ⟨y, hy⟩ := h.exists_left_inv in eq_top_of_unit_mem I x y hx hy

theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I :=
⟨by rintro rfl; trivial,
 λ h, eq_top_of_unit_mem _ _ 1 h (by simp)⟩

theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I :=
not_congr I.eq_top_iff_one

@[simp]
theorem unit_mul_mem_iff_mem {x y : α} (hy : is_unit y) : y * x ∈ I ↔ x ∈ I :=
begin
  refine ⟨λ h, _, λ h, I.mul_mem_left y h⟩,
  obtain ⟨y', hy'⟩ := hy.exists_left_inv,
  have := I.mul_mem_left y' h,
  rwa [← mul_assoc, hy', one_mul] at this,
end

/-- The ideal generated by a subset of a ring -/
def span (s : set α) : ideal α := submodule.span α s

@[simp] lemma submodule_span_eq {s : set α} :
  submodule.span α s = ideal.span s :=
rfl

@[simp] lemma span_empty : span (∅ : set α) = ⊥ := submodule.span_empty

@[simp] lemma span_univ : span (set.univ : set α) = ⊤ := submodule.span_univ

lemma span_union (s t : set α) : span (s ∪ t) = span s ⊔ span t :=
submodule.span_union _ _

lemma span_Union {ι} (s : ι → set α) : span (⋃ i, s i) = ⨆ i, span (s i) :=
submodule.span_Union _

lemma mem_span {s : set α} (x) : x ∈ span s ↔ ∀ p : ideal α, s ⊆ p → x ∈ p :=
mem_Inter₂

lemma subset_span {s : set α} : s ⊆ span s := submodule.subset_span

lemma span_le {s : set α} {I} : span s ≤ I ↔ s ⊆ I := submodule.span_le

lemma span_mono {s t : set α} : s ⊆ t → span s ≤ span t := submodule.span_mono

@[simp] lemma span_eq : span (I : set α) = I := submodule.span_eq _

@[simp] lemma span_singleton_one : span ({1} : set α) = ⊤ :=
(eq_top_iff_one _).2 $ subset_span $ mem_singleton _

lemma mem_span_insert {s : set α} {x y} :
  x ∈ span (insert y s) ↔ ∃ a (z ∈ span s), x = a * y + z := submodule.mem_span_insert

lemma mem_span_singleton' {x y : α} :
  x ∈ span ({y} : set α) ↔ ∃ a, a * y = x := submodule.mem_span_singleton

lemma span_insert (x) (s : set α) : span (insert x s) = span ({x} : set α) ⊔ span s :=
submodule.span_insert x s

lemma span_eq_bot {s : set α} : span s = ⊥ ↔ ∀ x ∈ s, (x:α) = 0 := submodule.span_eq_bot

@[simp] lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 :=
submodule.span_singleton_eq_bot

@[simp] lemma span_zero : span (0 : set α) = ⊥ := by rw [←set.singleton_zero, span_singleton_eq_bot]

@[simp] lemma span_one : span (1 : set α) = ⊤ := by rw [←set.singleton_one, span_singleton_one]

lemma span_eq_top_iff_finite (s : set α) :
  span s = ⊤ ↔ ∃ s' : finset α, ↑s' ⊆ s ∧ span (s' : set α) = ⊤ :=
begin
  simp_rw eq_top_iff_one,
  exact ⟨submodule.mem_span_finite_of_mem_span, λ ⟨s', h₁, h₂⟩, span_mono h₁ h₂⟩
end

/--
The ideal generated by an arbitrary binary relation.
-/
def of_rel (r : α → α → Prop) : ideal α :=
submodule.span α { x | ∃ (a b) (h : r a b), x + b = a }

/-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/
class is_prime (I : ideal α) : Prop :=
(ne_top' : I ≠ ⊤)
(mem_or_mem' : ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I)

theorem is_prime_iff {I : ideal α} :
  is_prime I ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I :=
⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩

theorem is_prime.ne_top {I : ideal α} (hI : I.is_prime) : I ≠ ⊤ := hI.1

theorem is_prime.mem_or_mem {I : ideal α} (hI : I.is_prime) :
  ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I := hI.2

theorem is_prime.mem_or_mem_of_mul_eq_zero {I : ideal α} (hI : I.is_prime)
  {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I :=
hI.mem_or_mem (h.symm ▸ I.zero_mem)

theorem is_prime.mem_of_pow_mem {I : ideal α} (hI : I.is_prime)
  {r : α} (n : ℕ) (H : r^n ∈ I) : r ∈ I :=
begin
  induction n with n ih,
  { rw pow_zero at H, exact (mt (eq_top_iff_one _).2 hI.1).elim H },
  { rw pow_succ at H, exact or.cases_on (hI.mem_or_mem H) id ih }
end

lemma not_is_prime_iff {I : ideal α} : ¬ I.is_prime ↔ I = ⊤ ∨ ∃ (x ∉ I) (y ∉ I), x * y ∈ I :=
begin
  simp_rw [ideal.is_prime_iff, not_and_distrib, ne.def, not_not, not_forall, not_or_distrib],
  exact or_congr iff.rfl
    ⟨λ ⟨x, y, hxy, hx, hy⟩, ⟨x, hx, y, hy, hxy⟩, λ ⟨x, hx, y, hy, hxy⟩, ⟨x, y, hxy, hx, hy⟩⟩
end

theorem zero_ne_one_of_proper {I : ideal α} (h : I ≠ ⊤) : (0:α) ≠ 1 :=
λ hz, I.ne_top_iff_one.1 h $ hz ▸ I.zero_mem

lemma bot_prime {R : Type*} [ring R] [is_domain R] : (⊥ : ideal R).is_prime :=
⟨λ h, one_ne_zero (by rwa [ideal.eq_top_iff_one, submodule.mem_bot] at h),
 λ x y h, mul_eq_zero.mp (by simpa only [submodule.mem_bot] using h)⟩

/-- An ideal is maximal if it is maximal in the collection of proper ideals. -/
class is_maximal (I : ideal α) : Prop := (out : is_coatom I)

theorem is_maximal_def {I : ideal α} : I.is_maximal ↔ is_coatom I := ⟨λ h, h.1, λ h, ⟨h⟩⟩

theorem is_maximal.ne_top {I : ideal α} (h : I.is_maximal) : I ≠ ⊤ := (is_maximal_def.1 h).1

theorem is_maximal_iff {I : ideal α} : I.is_maximal ↔
  (1:α) ∉ I ∧ ∀ (J : ideal α) x, I ≤ J → x ∉ I → x ∈ J → (1:α) ∈ J :=
is_maximal_def.trans $ and_congr I.ne_top_iff_one $ forall_congr $ λ J,
by rw [lt_iff_le_not_le]; exact
 ⟨λ H x h hx₁ hx₂, J.eq_top_iff_one.1 $
    H ⟨h, not_subset.2 ⟨_, hx₂, hx₁⟩⟩,
  λ H ⟨h₁, h₂⟩, let ⟨x, xJ, xI⟩ := not_subset.1 h₂ in
   J.eq_top_iff_one.2 $ H x h₁ xI xJ⟩

theorem is_maximal.eq_of_le {I J : ideal α}
  (hI : I.is_maximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J :=
eq_iff_le_not_lt.2 ⟨IJ, λ h, hJ (hI.1.2 _ h)⟩

instance : is_coatomic (ideal α) :=
begin
  apply complete_lattice.coatomic_of_top_compact,
  rw ←span_singleton_one,
  exact submodule.singleton_span_is_compact_element 1,
end

/-- **Krull's theorem**: if `I` is an ideal that is not the whole ring, then it is included in some
    maximal ideal. -/
theorem exists_le_maximal (I : ideal α) (hI : I ≠ ⊤) :
  ∃ M : ideal α, M.is_maximal ∧ I ≤ M :=
let ⟨m, hm⟩ := (eq_top_or_exists_le_coatom I).resolve_left hI in ⟨m, ⟨⟨hm.1⟩, hm.2⟩⟩

variables (α)

/-- Krull's theorem: a nontrivial ring has a maximal ideal. -/
theorem exists_maximal [nontrivial α] : ∃ M : ideal α, M.is_maximal :=
let ⟨I, ⟨hI, _⟩⟩ := exists_le_maximal (⊥ : ideal α) bot_ne_top in ⟨I, hI⟩

variables {α}

instance [nontrivial α] : nontrivial (ideal α) :=
begin
  rcases @exists_maximal α _ _ with ⟨M, hM, _⟩,
  exact nontrivial_of_ne M ⊤ hM
end

/-- If P is not properly contained in any maximal ideal then it is not properly contained
  in any proper ideal -/
lemma maximal_of_no_maximal {R : Type u} [semiring R] {P : ideal R}
(hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ :=
begin
  by_contradiction hnonmax,
  rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩,
  exact hmax M (lt_of_lt_of_le hPJ hM2) hM1,
end

theorem mem_span_pair {x y z : α} :
  z ∈ span ({x, y} : set α) ↔ ∃ a b, a * x + b * y = z :=
by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z]

theorem is_maximal.exists_inv {I : ideal α}
  (hI : I.is_maximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1 :=
begin
  cases is_maximal_iff.1 hI with H₁ H₂,
  rcases mem_span_insert.1 (H₂ (span (insert x I)) x
    (set.subset.trans (subset_insert _ _) subset_span)
    hx (subset_span (mem_insert _ _))) with ⟨y, z, hz, hy⟩,
  refine ⟨y, z, _, hy.symm⟩,
  rwa ← span_eq I,
end

section lattice
variables {R : Type u} [semiring R]

lemma mem_sup_left {S T : ideal R} : ∀ {x : R}, x ∈ S → x ∈ S ⊔ T :=
show S ≤ S ⊔ T, from le_sup_left

lemma mem_sup_right {S T : ideal R} : ∀ {x : R}, x ∈ T → x ∈ S ⊔ T :=
show T ≤ S ⊔ T, from le_sup_right

lemma mem_supr_of_mem {ι : Sort*} {S : ι → ideal R} (i : ι) :
  ∀ {x : R}, x ∈ S i → x ∈ supr S :=
show S i ≤ supr S, from le_supr _ _

lemma mem_Sup_of_mem {S : set (ideal R)} {s : ideal R}
  (hs : s ∈ S) : ∀ {x : R}, x ∈ s → x ∈ Sup S :=
show s ≤ Sup S, from le_Sup hs

theorem mem_Inf {s : set (ideal R)} {x : R} :
  x ∈ Inf s ↔ ∀ ⦃I⦄, I ∈ s → x ∈ I :=
⟨λ hx I his, hx I ⟨I, infi_pos his⟩, λ H I ⟨J, hij⟩, hij ▸ λ S ⟨hj, hS⟩, hS ▸ H hj⟩

@[simp] lemma mem_inf {I J : ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J := iff.rfl

@[simp] lemma mem_infi {ι : Sort*} {I : ι → ideal R} {x : R} : x ∈ infi I ↔ ∀ i, x ∈ I i :=
submodule.mem_infi _

@[simp] lemma mem_bot {x : R} : x ∈ (⊥ : ideal R) ↔ x = 0 :=
submodule.mem_bot _

end lattice

section pi
variables (ι : Type v)

/-- `I^n` as an ideal of `R^n`. -/
def pi : ideal (ι → α) :=
{ carrier := { x | ∀ i, x i ∈ I },
  zero_mem' := λ i, I.zero_mem,
  add_mem' := λ a b ha hb i, I.add_mem (ha i) (hb i),
  smul_mem' := λ a b hb i, I.mul_mem_left (a i) (hb i) }

lemma mem_pi (x : ι → α) : x ∈ I.pi ι ↔ ∀ i, x i ∈ I := iff.rfl

end pi

end ideal

end semiring

section comm_semiring

variables {a b : α}

-- A separate namespace definition is needed because the variables were historically in a different
-- order.
namespace ideal
variables [comm_semiring α] (I : ideal α)

@[simp]
theorem mul_unit_mem_iff_mem {x y : α} (hy : is_unit y) : x * y ∈ I ↔ x ∈ I :=
mul_comm y x ▸ unit_mul_mem_iff_mem I hy

lemma mem_span_singleton {x y : α} :
  x ∈ span ({y} : set α) ↔ y ∣ x :=
mem_span_singleton'.trans $ exists_congr $ λ _, by rw [eq_comm, mul_comm]

lemma span_singleton_le_span_singleton {x y : α} :
  span ({x} : set α) ≤ span ({y} : set α) ↔ y ∣ x :=
span_le.trans $ singleton_subset_iff.trans mem_span_singleton

lemma span_singleton_eq_span_singleton {α : Type u} [comm_ring α] [is_domain α] {x y : α} :
  span ({x} : set α) = span ({y} : set α) ↔ associated x y :=
begin
  rw [←dvd_dvd_iff_associated, le_antisymm_iff, and_comm],
  apply and_congr;
  rw span_singleton_le_span_singleton,
end

lemma span_singleton_mul_right_unit {a : α} (h2 : is_unit a) (x : α) :
  span ({x * a} : set α) = span {x} :=
begin
  apply le_antisymm,
  { rw span_singleton_le_span_singleton, use a},
  { rw span_singleton_le_span_singleton, rw is_unit.mul_right_dvd h2}
end

lemma span_singleton_mul_left_unit {a : α} (h2 : is_unit a) (x : α) :
  span ({a * x} : set α) = span {x} := by rw [mul_comm, span_singleton_mul_right_unit h2]

lemma span_singleton_eq_top {x} : span ({x} : set α) = ⊤ ↔ is_unit x :=
by rw [is_unit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one,
  eq_top_iff]

theorem span_singleton_prime {p : α} (hp : p ≠ 0) :
  is_prime (span ({p} : set α)) ↔ prime p :=
by simp [is_prime_iff, prime, span_singleton_eq_top, hp, mem_span_singleton]

theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime :=
⟨H.1.1, λ x y hxy, or_iff_not_imp_left.2 $ λ hx, begin
  let J : ideal α := submodule.span α (insert x ↑I),
  have IJ : I ≤ J  := (set.subset.trans (subset_insert _ _) subset_span),
  have xJ : x ∈ J := ideal.subset_span (set.mem_insert x I),
  cases is_maximal_iff.1 H with _ oJ,
  specialize oJ J x IJ hx xJ,
  rcases submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩,
  obtain (F : y * 1 = y * (a • x + b)) := congr_arg (λ g : α, y * g) oe,
  rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc],
  refine submodule.add_mem I (I.mul_mem_left a hxy) (submodule.smul_mem I y _),
  rwa submodule.span_eq at h,
end⟩

@[priority 100] -- see Note [lower instance priority]
instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prime :=
is_maximal.is_prime

lemma span_singleton_lt_span_singleton [comm_ring β] [is_domain β] {x y : β} :
  span ({x} : set β) < span ({y} : set β) ↔ dvd_not_unit y x :=
by rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
  dvd_and_not_dvd_iff]

lemma factors_decreasing [comm_ring β] [is_domain β]
  (b₁ b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬ is_unit b₂) :
  span ({b₁ * b₂} : set β) < span {b₁} :=
lt_of_le_not_le (ideal.span_le.2 $ singleton_subset_iff.2 $
  ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) $ λ h,
h₂ $ is_unit_of_dvd_one _ $ (mul_dvd_mul_iff_left h₁).1 $
by rwa [mul_one, ← ideal.span_singleton_le_span_singleton]

variables (b)
lemma mul_mem_right (h : a ∈ I) : a * b ∈ I := mul_comm b a ▸ I.mul_mem_left b h
variables {b}

lemma pow_mem_of_mem (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I :=
nat.cases_on n (not.elim dec_trivial) (λ m hm, (pow_succ a m).symm ▸ I.mul_mem_right (a^m) ha) hn

theorem is_prime.mul_mem_iff_mem_or_mem {I : ideal α} (hI : I.is_prime) :
  ∀ {x y : α}, x * y ∈ I ↔ x ∈ I ∨ y ∈ I :=
λ x y, ⟨hI.mem_or_mem, by { rintro (h | h), exacts [I.mul_mem_right y h, I.mul_mem_left x h] }⟩

theorem is_prime.pow_mem_iff_mem {I : ideal α} (hI : I.is_prime)
  {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I :=
⟨hI.mem_of_pow_mem n, (λ hr, I.pow_mem_of_mem hr n hn)⟩

theorem pow_multiset_sum_mem_span_pow (s : multiset α) (n : ℕ) :
  s.sum ^ (s.card * n + 1) ∈ span ((s.map (λ x, x ^ (n + 1))).to_finset : set α) :=
begin
  induction s using multiset.induction_on with a s hs,
  { simp },
  simp only [finset.coe_insert, multiset.map_cons, multiset.to_finset_cons, multiset.sum_cons,
    multiset.card_cons, add_pow],
  refine submodule.sum_mem _ _,
  intros c hc,
  rw mem_span_insert,
  by_cases h : n+1 ≤ c,
  { refine ⟨a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) *
      (((s.card + 1) * n + 1).choose c), 0, submodule.zero_mem _, _⟩,
    rw mul_comm _ (a ^ (n + 1)),
    simp_rw ← mul_assoc,
    rw [← pow_add, add_zero, add_tsub_cancel_of_le h], },
  { use 0,
    simp_rw [zero_mul, zero_add],
    refine ⟨_,_,rfl⟩,
    replace h : c ≤ n := nat.lt_succ_iff.mp (not_le.mp h),
    have : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c),
    { rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h] },
    rw [this, pow_add],
    simp_rw [mul_assoc, mul_comm (s.sum ^ (s.card * n + 1)), ← mul_assoc],
    exact mul_mem_left _ _ hs }
end

theorem sum_pow_mem_span_pow {ι} (s : finset ι) (f : ι → α) (n : ℕ) :
  (∑ i in s, f i) ^ (s.card * n + 1) ∈ span ((λ i, f i ^ (n + 1)) '' s) :=
begin
  convert pow_multiset_sum_mem_span_pow (s.1.map f) n,
  { rw multiset.card_map, refl },
  rw [multiset.map_map, multiset.to_finset_map, finset.val_to_finset, finset.coe_image]
end

theorem span_pow_eq_top (s : set α)
  (hs : span s = ⊤) (n : ℕ) : span ((λ x, x ^ n) '' s) = ⊤ :=
begin
  rw eq_top_iff_one,
  cases n,
  { obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s,
    { rw [set.image_empty, hs],
      trivial },
    { exact subset_span ⟨_, hx, pow_zero _⟩ } },
  rw [eq_top_iff_one, span, finsupp.mem_span_iff_total] at hs,
  rcases hs with ⟨f, hf⟩,
  change f.support.sum (λ a, f a * a) = 1 at hf,
  have := sum_pow_mem_span_pow f.support (λ a, f a * a) n,
  rw [hf, one_pow] at this,
  refine (span_le).mpr _ this,
  rintros _ hx,
  simp_rw [finset.mem_coe, set.mem_image] at hx,
  rcases hx with ⟨x, hx, rfl⟩,
  have : span ({x ^ (n + 1)} : set α) ≤ span ((λ (x : α), x ^ (n + 1)) '' s),
  { rw [span_le, set.singleton_subset_iff],
    exact subset_span ⟨x, x.prop, rfl⟩ },
  refine this _,
  rw [mul_pow, mem_span_singleton],
  exact ⟨f x ^ (n + 1), mul_comm _ _⟩
end

end ideal

end comm_semiring

section ring

namespace ideal

variables [ring α] (I : ideal α) {a b : α}

protected lemma neg_mem_iff : -a ∈ I ↔ a ∈ I := neg_mem_iff
protected lemma add_mem_iff_left : b ∈ I → (a + b ∈ I ↔ a ∈ I) := I.add_mem_iff_left
protected lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff_right
protected lemma sub_mem : a ∈ I → b ∈ I → a - b ∈ I := sub_mem

lemma mem_span_insert' {s : set α} {x y} :
  x ∈ span (insert y s) ↔ ∃a, x + a * y ∈ span s := submodule.mem_span_insert'

end ideal

end ring

section division_ring
variables {K : Type u} [division_ring K] (I : ideal K)

namespace ideal

/-- All ideals in a division ring are trivial. -/
lemma eq_bot_or_top : I = ⊥ ∨ I = ⊤ :=
begin
  rw or_iff_not_imp_right,
  change _ ≠ _ → _,
  rw ideal.ne_top_iff_one,
  intro h1,
  rw eq_bot_iff,
  intros r hr,
  by_cases H : r = 0, {simpa},
  simpa [H, h1] using I.mul_mem_left r⁻¹ hr,
end

lemma eq_bot_of_prime [h : I.is_prime] : I = ⊥ :=
or_iff_not_imp_right.mp I.eq_bot_or_top h.1

lemma bot_is_maximal : is_maximal (⊥ : ideal K) :=
⟨⟨λ h, absurd ((eq_top_iff_one (⊤ : ideal K)).mp rfl) (by rw ← h; simp),
λ I hI, or_iff_not_imp_left.mp (eq_bot_or_top I) (ne_of_gt hI)⟩⟩

end ideal

end division_ring

section comm_ring

namespace ideal

theorem mul_sub_mul_mem {R : Type*} [comm_ring R] (I : ideal R) {a b c d : R}
  (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I :=
begin
  rw (show a * c - b * d = (a - b) * c + b * (c - d), by {rw [sub_mul, mul_sub], abel}),
  exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2),
end

end ideal

end comm_ring

namespace ring

variables {R : Type*} [comm_ring R]

lemma not_is_field_of_subsingleton {R : Type*} [ring R] [subsingleton R] : ¬ is_field R :=
λ ⟨⟨x, y, hxy⟩, _, _⟩, hxy (subsingleton.elim x y)

lemma exists_not_is_unit_of_not_is_field [nontrivial R] (hf : ¬ is_field R) :
  ∃ x ≠ (0 : R), ¬ is_unit x :=
begin
  have : ¬ _ := λ h, hf ⟨exists_pair_ne R, mul_comm, h⟩,
  simp_rw is_unit_iff_exists_inv,
  push_neg at ⊢ this,
  obtain ⟨x, hx, not_unit⟩ := this,
  exact ⟨x, hx, not_unit⟩
end

lemma not_is_field_iff_exists_ideal_bot_lt_and_lt_top [nontrivial R] :
  ¬ is_field R ↔ ∃ I : ideal R, ⊥ < I ∧ I < ⊤ :=
begin
  split,
  { intro h,
    obtain ⟨x, nz, nu⟩ := exists_not_is_unit_of_not_is_field h,
    use ideal.span {x},
    rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top],
    exact ⟨mt ideal.span_singleton_eq_bot.mp nz, mt ideal.span_singleton_eq_top.mp nu⟩ },
  { rintros ⟨I, bot_lt, lt_top⟩ hf,
    obtain ⟨x, mem, ne_zero⟩ := set_like.exists_of_lt bot_lt,
    rw submodule.mem_bot at ne_zero,
    obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero,
    rw [lt_top_iff_ne_top, ne.def, ideal.eq_top_iff_one, ← hy] at lt_top,
    exact lt_top (I.mul_mem_right _ mem), }
end

lemma not_is_field_iff_exists_prime [nontrivial R] :
  ¬ is_field R ↔ ∃ p : ideal R, p ≠ ⊥ ∧ p.is_prime :=
not_is_field_iff_exists_ideal_bot_lt_and_lt_top.trans
  ⟨λ ⟨I, bot_lt, lt_top⟩, let ⟨p, hp, le_p⟩ := I.exists_le_maximal (lt_top_iff_ne_top.mp lt_top) in
    ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.is_prime⟩,
   λ ⟨p, ne_bot, prime⟩, ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr prime.1⟩⟩

/-- When a ring is not a field, the maximal ideals are nontrivial. -/
lemma ne_bot_of_is_maximal_of_not_is_field [nontrivial R] {M : ideal R} (max : M.is_maximal)
  (not_field : ¬ is_field R) : M ≠ ⊥ :=
begin
  rintros h,
  rw h at max,
  rcases max with ⟨⟨h1, h2⟩⟩,
  obtain ⟨I, hIbot, hItop⟩ := not_is_field_iff_exists_ideal_bot_lt_and_lt_top.mp not_field,
  exact ne_of_lt hItop (h2 I hIbot),
end

end ring

namespace ideal

/-- Maximal ideals in a non-field are nontrivial. -/
variables {R : Type u} [comm_ring R] [nontrivial R]
lemma bot_lt_of_maximal (M : ideal R) [hm : M.is_maximal] (non_field : ¬ is_field R) : ⊥ < M :=
begin
  rcases (ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top.1 non_field)
    with ⟨I, Ibot, Itop⟩,
  split, { simp },
  intro mle,
  apply @irrefl _ (<) _ (⊤ : ideal R),
  have : M = ⊥ := eq_bot_iff.mpr mle,
  rw this at *,
  rwa hm.1.2 I Ibot at Itop,
end

end ideal

variables {a b : α}

/-- The set of non-invertible elements of a monoid. -/
def nonunits (α : Type u) [monoid α] : set α := { a | ¬is_unit a }

@[simp] theorem mem_nonunits_iff [monoid α] : a ∈ nonunits α ↔ ¬ is_unit a := iff.rfl

theorem mul_mem_nonunits_right [comm_monoid α] :
  b ∈ nonunits α → a * b ∈ nonunits α :=
mt is_unit_of_mul_is_unit_right

theorem mul_mem_nonunits_left [comm_monoid α] :
  a ∈ nonunits α → a * b ∈ nonunits α :=
mt is_unit_of_mul_is_unit_left

theorem zero_mem_nonunits [semiring α] : 0 ∈ nonunits α ↔ (0:α) ≠ 1 :=
not_congr is_unit_zero_iff

@[simp] theorem one_not_mem_nonunits [monoid α] : (1:α) ∉ nonunits α :=
not_not_intro is_unit_one

theorem coe_subset_nonunits [semiring α] {I : ideal α} (h : I ≠ ⊤) :
  (I : set α) ⊆ nonunits α :=
λ x hx hu, h $ I.eq_top_of_is_unit_mem hx hu

lemma exists_max_ideal_of_mem_nonunits [comm_semiring α] (h : a ∈ nonunits α) :
  ∃ I : ideal α, I.is_maximal ∧ a ∈ I :=
begin
  have : ideal.span ({a} : set α) ≠ ⊤,
  { intro H, rw ideal.span_singleton_eq_top at H, contradiction },
  rcases ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩,
  use [I, Imax], apply H, apply ideal.subset_span, exact set.mem_singleton a
end

subset_name: curated


TITLE: Prove continuity from preservation of sequential limits but do not use $f(\bar{A}) \subseteq \overline{f(A)}$
QUESTION [1 upvotes]: Munkres Topology:

Theorem 21.3. Let $f : X \rightarrow Y$. If the function $f$ is continuous, then for every convergent sequence $x_n \rightarrow x$ in $X$, the sequence $f(x_n)$ converges to $f(x)$. The converse holds if $X$ is metrizable.

I understand the first statement. My question is about the converse assuming that $X$ is metrizable. Munkres does this by proving the equivalent formulation of continuity $f(\bar{A}) \subseteq \overline{f(A)}, A \subseteq X$. How do I prove that $f$ directly satisfies the original definition of continuity?

Definition of continuity: For each open subset V of Y, the set $f^{-1}(V)$ is an open subset of X.

I can type up my proof later (I have to organize my messy notes), but for now: I was able to show that $f^{-1}(V)$ is a subset of $f^{-1}(V)'$, which I discovered to be something called dense-in-itself which means no isolated points.
I think I can show $f^{-1}(V)$ is open by showing that $f^{-1}(V)' \cap f^{-1}(V^c)'$ is empty because

$f^{-1}(V^c) = f^{-1}(V)^c$,
$U$ is open if and only if $Bd(U)=\overline{U} \setminus U$
showing that $f^{-1}(V)' \cap f^{-1}(V^c)'$ is empty would imply $Bd(U)=\overline{U} \setminus U$ for $U=f^{-1}(V)$ because $f^{-1}(V) \subseteq f^{-1}(V)'$

What is the contradiction if we say that $f^{-1}(V)' \cap f^{-1}(V^c)'$ is not empty? I'm very confused as to what we get from assuming there is some $z \in f^{-1}(V)'$ and $z \in f^{-1}(V^c)'$.
From $z \in f^{-1}(V)'$, I think I was able to show that $(f^{-1}(V)')'=f^{-1}(V)'$, which means that $f^{-1}(V^c)'$ is something I discovered to be called a perfect set, which means closed and dense-in-itself. According to proofwiki.org, the Union of Set of Dense-in-itself Sets is Dense-in-itself. This means $f^{-1}(V) \cup f^{-1}(V)'$ is dense-in-itself, but $f^{-1}(V) \cup f^{-1}(V)' = \overline{f^{-1}(V)}$, the closure of $f^{-1}(V)$ which is closed. Therefore, $\overline{f^{-1}(V)}$ is perfect.

Is this related? Does continuity of $f$ imply $f^{-1}(\bar A)\subset\overline{f^{-1}(A)}$?

I do not know how to proceed from $z \in f^{-1}(V^c)'$. I think this somehow contradicts with $\overline{f^{-1}(V)}$ being perfect.
Also, I showed $f^{-1}(V)$ is infinite if we let $x \in f^{-1}(V)'$ because the sequence lemma gives us a sequence $x_n \to x$ where $x_n \in f^{-1}(V)$ . Also, $f(x_n) \in V$ and $f \in \overline{V}$.
However, $f^{-1}(V)$ is infinite, $\overline{f^{-1}(V)}$ is dense-in-itself and $(f^{-1}(V)')' \subseteq f^{-1}(V)'$ can be shown from $T_1$ axiom because according to proofwiki.org again, Dense-in-itself Subset of T1 Space is Infinite, Closure of Dense-in-itself is Dense-in-itself in T1 Space and Derivative of Derivative is Subset of Derivative in T1 Space. Thus, I think there's something else I'm not using. (Of course, I'm not using $f(\bar{A}) \subseteq \overline{f(A)}$ because that's what this question is about.)

REPLY [0 votes]: Use the sequence lemma (as Munkres formulates it):

If $A \subseteq X$ and $x_n$ is a sequence from $A$ with $x_n \to x$, then $x \in \overline{A}$ and the reverse holds in metrisable spaces.

Then suppose $f: X \to Y$ is sequentially continuous and $X$ is metrisable then $f$ is continuous. We can also show continuity by showing $f^{-1}[C]$ to be closed for $C \subseteq Y$ closed. So let $C$ be closed and let $x \in \overline{f^{-1}[C]}$. By the sequence lemma (reverse) there is a sequence $x_n$ from $f^{-1}[C]$ that converges to $x$.
So $f(x_n) \to f(x)$ by sequential continuity. Also, all $f(x_n) \in C$. As $C$ is closed by the sequence lemma again $f(x) \in \overline{C}=C$, so $x \in f^{-1}[C]$. As $x \in \overline{f^{-1}[C]}$ was arbitrary, $f^{-1}[C]$ is closed. Hence $f$ is continuous.


TITLE: Show: $\|u_n\|_X \leq \gamma^{n-1} \|u_0\|_X \quad \forall n \geq 1$
QUESTION [2 upvotes]: Let $H$ be a Hilbert space with norm $\|\cdot\|_X$ and scalar product $(\cdot,\cdot)_X$ , which is the direct sum of the subspaces $V$ and $W$. Regarding $V$ and $W$ it holds the intensified Cauchy Schwarz Inequality.

What do I mean with intensified Cauchy Schwarz Inequality? : There is a $\gamma$ with $0 \leq \gamma < 1$ and $|(v,w)|_X \leq \gamma \|v\|_X \|w\|_X \quad \forall v \in V, w \in W$

$P_V$ and $P_W$ are the orthogonal projections on $V$ and $W$. For a $u_0 \in X$ we compute $u_{2k-1} = P_V u_{2k-2}$ and $u_{2k} = P_W u_{2k-1}$.
Show: $\|u_n\|_X \leq \gamma^{n-1} \|u_0\|_X \quad \forall n \geq 1$
My thoughts: It is clear that we have use the Cauchy Schwarz inequality. I mean there is our $\gamma$. It seems that we have use the inequality multiple times to get $\gamma^{n-1}$.We also have to use the successive computation somehow. Maybe my idea is too simple but can induction help us?

REPLY [1 votes]: Hint: We have $\lVert P_Wv\rVert^2=(v,P_Wv)_X$ and $\lVert P_Vw\rVert^2=(P_Vw,w)_X$.


TITLE: Norm of $(1+\sqrt{2})^n$?
QUESTION [0 upvotes]: How do we find the norm of $(1+\sqrt{2})^n$ $ \forall n\geq1$?
The norm of $a+b\sqrt{D}$ is defined as $a^2-b^2D$ where $a,b\in\mathbb{Z}$ and $D$ is a square free integer.
P.S- This question comes from Ring theory when we try to find the units of the ring $\mathbb{Z}[\sqrt{2}]$
Any hint is welcome

REPLY [5 votes]: HINT: Norm is multiplicative
Prove that, then it's easy

REPLY [2 votes]: Note that the norm is multiplicative. I.e. $N(x)N(y)=N(xy)$.
Thus as an easy consequence, we can see that $N(x^n)=N(x)^n$
So we just need to find the norm of $1+\sqrt{2}$, which by definition is $1-2\cdot 1^2=-1$


TITLE: $Q$ factor of parallel RLC circuit in series with a capacitor and resistor
QUESTION [8 upvotes]: I know that for parallel RLC circuits, the $Q$ factor is given by:
$$ Q = R \sqrt {\frac{C}{L}} $$
But now suppose it is connected in series to a resistor $R_2$ and capacitor $C_2$. Would the $Q$ factor be changed?

REPLY [5 votes]: There's a really awesome trick for problems like this.
This is going to be a long post but the method presented makes problems like this really easy.
The idea is to turn the series branch $C_2$, $R_2$ into an effective parallel $R$ and $C$.
See the diagram.
The effective parallel values are denoted $C_{2,p}$ and $R_{2,p}$.
Parallel capacitances just add, so the total capacitance is now $C+C_{2,p}$.
Parallel resistances add in parallel so the total resistance is now $R||R_{2,p} = \left( 1/R + 1/R_{2,p} \right)^{-1}$.
Since we now have a purely parallel circuit, you can stick these values into your formula for $Q$ (which was wrong in the OP, by the way, but I edited it).
Of course, to actually do any of this we have to understand how to solve for $R_{2,p}$ and $C_{2,p}$.
Before we do that I want to simplify some notation.
It is extremely useful to define $Z_{LC} = \sqrt{L/C}$.
This is the "characteristic impedance" of a resonant mode, and it will show up all over the place.
With this definition, the equation for the $Q$ of a parallel $RLC$ resonator is
$$Q = R/Z_{LC}$$
which is really easy to remember:
if $R\rightarrow \infty$ then no current flows through the resistor so there's no energy loss, and as we can see $Q\rightarrow \infty$.

Series/parallel equivalence
Suppose we have a series resistance $R_s$ and reactance $X_s$.
The total series impedance is
$$Z_s = R_s + i X_s .$$
We want to find the equivalent parallel circuit.
The impedance of a parallel resistance $R_p$ and reactance $X_p$ is
$$Z_p = \frac{iR_pX_p}{R_p + iX_p} = \frac{R_pX_p^2 + iR_p^2X_p}{R_p^2 + X_p^2}$$
Now define a new symbol $Q_p \equiv R_p/X_p$.
Using this we can rewrite $Z_p$ as
$$Z_p = \frac{R_p}{1+Q_p^2} + iX_p \frac{Q_p^2}{1+Q_p^2}.$$
Since this is now just a sum of a real number and an imaginary number, it's obvious what the equivalent series values are:
$$R_s = R_p \frac{1}{1+Q_p^2} \qquad X_s = X_p\frac{Q_p^2}{1+Q_p^2} . \qquad (*)$$
Unfortunately we have solved the problem in the wrong direction: we found series values in terms of parallel ones instead of the other way around.
To solve this problem, define $Q_s \equiv X_s/R_s$, and divide the two equations in $(*)$ by one another to find
$$Q_s = Q_p .$$
Now we can easily invert $(*)$ to find
$$R_p = R_s(1 + Q^2) \qquad X_p = \frac{1 + Q^2}{Q^2} X_s$$
where we now write $Q$ instead of $Q_s$ or $Q_p$ because we just showed that they are equal.
We now have the parallel values in terms of the series values.
The best part is that almost always when you have a circuit like the one in the original post, you have $Q \gg 1$, which simplifies the transformation equations considerably to
$$R_p \approx R_s Q^2 \qquad X_p \approx X_s . $$
The take-home message is that the equivalent parallel resistance is transformed to a much larger value, and the equivalent reactance is basically the same as the series value.
Solve the original problem
In the original problem we have
$$
\begin{align}
R_s &= R_2 \\
X_s &= \frac{1}{\omega C_2} \\
Q_e &= \frac{X_s}{R_s} = \frac{1}{\omega C_2 R_2}.
\end{align}
$$
where I've written $Q_e$ to indicate that this is the $Q$ of the "external" circuit.
The equivalent parallel values are
$$
\begin{align}
R_{2,p} &\approx R_2 Q_e^2 \\
X_p &\approx X_s \rightarrow C_{2,p} \approx C_2
\end{align}
$$
We now have a new fully parallel circuit with
$$
\begin{align}
\text{resistance} &= R||R_{2,p} \\
\text{capacitance} &= C + C_{2,p} \approx C \qquad \text{assuming }C \gg C_2 \\
\text{inductance} &= L
\end{align}
$$
The $Q$ of the circuit is
$$
\begin{align}
Q &= \text{resistance} / Z_{LC} \\
&= \left(\frac{1}{R} + \frac{1}{R_2 Q_e^2} \right) ^{-1} / Z_{LC} \\
\frac{1}{Q} &= \frac{Z_{LC}}{R} + \frac{Z_{LC}}{Q_e^2 R_2} \\
&= \frac{1}{Q_i} + \frac{1}{Q_c}
\end{align}$$
where we've defined $Q_i \equiv R / Z_{LC}$ which is the internal $Q$ of the circuit without the external series branch, and $Q_c \equiv Q_e^2 R_2 / Z_{LC}$ is the extra $Q$ induced by the coupling.
In other words, when you add the series branch, the total $Q$ of the resonance winds up being a parallel combination of two components:

$Q_i$: The $Q$ you would have without the coupling to the series branch.
$Q_c$: The $Q$ you would have if $R$ were absent. This part comes from the coupling to the series branch.

This is, of course, just a result of the fact that $R$ and the effective parallel resistance of the series branch $R_{2,p}$ add in parallel.
We now write down a useful expression for $Q_c$.
First write
$$ Q_e = X_s / R_s = \frac{1}{\omega R_2 C_2} .$$
Since we're talking about properties near resonance, we take $\omega \approx 1/\sqrt{LC}$ giving
$$Q_e = \frac{\sqrt{LC}}{R_2 C_2}.$$
Then for $Q_c$ we get
$$
\begin{align}
Q_c &= \frac{Q_e^2 R_2}{Z_{LC}} \\
&=  \frac{R_2 L C \sqrt{C}}{R_2^2 C_2^2 \sqrt{L}} \\
&= \frac{Z_{LC}}{R_2}\left( \frac{C}{C_2} \right)^2 .
\end{align}
$$
The constitutes a full solution to the problem.
Summary
$$\frac{1}{Q} = \frac{1}{Q_i} + \frac{1}{Q_c}$$
where
$$Q_i = \frac{R}{Z_{LC}}$$
and
$$Q_c = \frac{Z_{LC}}{R_2}\left( \frac{C}{C_2}\right)^2.$$
The approximations made here are that $C_2 \ll C$ and $Q_s \gg 1$.
The approximation $Q_s \gg 1$ is pretty good for $Q_s>3$.


TITLE: An uncountable family of measurable sets with positive measure
QUESTION [13 upvotes]: Is there a family of measurable sets $\{E_\alpha\}_{\alpha \in A}$ , disjoint, uncountable and each one with positive measure?

REPLY [24 votes]: It depends on your measure space.  For instance, if you take as your measure space $\mathbb{R}$ with counting measure, then the family of singletons works.
However, for a $\sigma$-finite measure space (in particular, for Lebesgue measure), the answer is no.  Suppose your measure space is $(X,\mu)$ and you can write $X = \bigcup_{n = 1}^\infty X_n$ where $\mu(X_n) < \infty$.  Let $\mathcal{E}$ be any family of pairwise disjoint sets, all of which have positive measure.  Let
$$\mathcal{E}_{n,k} = \{ E \in \mathcal{E} : \mu(E \cap X_n) \ge 1/k\}.$$
Then every $E \in \mathcal{E}$ is in at least one $\mathcal{E}_{n,k}$, so $\bigcup_{n,k=1}^\infty \mathcal{E}_{n,k} = \mathcal{E}$.  Now suppose $E_1, \dots, E_m$ are distinct sets from $\mathcal{E}_{n,k}$.  Since these sets are disjoint, we have
$$\frac{m}{k} \le \sum_{i=1}^m \mu(E_i \cap X_n) \le \mu(X_n)$$
so $m \le k \mu(X_n)$.  Thus the cardinality of $\mathcal{E}_{n,k}$ is at most $k \mu(X_n)$; in particular it is finite.  So we have shown that $\mathcal{E}$ is a countable union of finite sets, hence countable.


TITLE: Predicting the oblique collision of two disks
QUESTION [1 upvotes]: Given two disks D1 and D2. Their radii, positions, and velocities are known. How can I predict whether they will collide or not? For a head-on collision, the angles that the directions of motion make with the x-axis add up to 180 degrees. But I don't know what is the condition for an oblique collision. Any help would be appreciated.

REPLY [2 votes]: Given the velocities and positions, first consider the two bodies to be point objects and find the distance of closest approach between the two points (centers). If this distance ($d_c$) is zero, then they collide head-on, if $d_c <r_1+r_2$, then they will collide, or else they won't collide.


TITLE: Puzzle in a Calculation
QUESTION [0 upvotes]: I want to calcalate $a$ from
$$\frac{d a}{d u} = \frac{\sqrt{2}}{4\pi} \oint_\alpha \frac{dx}{\sqrt{(x-1)(x+1)(x-u)}}$$
where $\alpha$ is the contour only around cut between -1 and 1. First I want to integrate $u$ and I find some trouble.
Directly integrating $u$ gives
$$ a= \frac{-2\sqrt{2}}{4\pi} \oint_\alpha \frac{dx \sqrt{(x-u)}}{\sqrt{(x-1)(x+1)}}$$
If we first change the sign of $u$
$$ \frac{d a}{d u} = \frac{\sqrt{2}}{4\pi} \oint_\alpha \frac{dx}{\sqrt{(x-1)(x+1)(x-u)}}
\\ =\frac{\sqrt{2}}{4\pi} \oint_\alpha \frac{dx}{\sqrt{(-x+1)(x+1)(-x+u)}}$$
 and then integrating $u$ gives
$$ a= \frac{2\sqrt{2}}{4\pi} \oint_\alpha \frac{dx \sqrt{(-x+u)}}{\sqrt{(-x+1)(x+1)}}$$
The answers seem different.
What is wrong with the above calculation?
Thanks in advance.

REPLY [1 votes]: EDIT: "Fuller" answer at asker's request
Well, let's look at an example $1 = \sqrt{1\cdot 1}=\sqrt{-1\cdot -1} = \sqrt{-1} \cdot \sqrt{-1} = i^2 = -1$, which is ridiculous. Where in this calculation did I go wrong? What have you implicitly assumed in your calculations? We have a branch point of $f(z) = z^{1/2}$ at $z=0$ perhaps?
The fact that $\sqrt{ab} = \sqrt{a}\cdot \sqrt{b}$ is only an identity on $\mathbb{R}^+$; it does not hold when you extend your number system to the complex plane. See the following for more details:
Why $\sqrt {-1}\cdot \sqrt{-1}=-1$ rather than $\sqrt {-1}\cdot \sqrt{-1}=1$. Pre-definition reason!