NormQuotient.lean

def localNormSubgroup (K L : Type u) [Field K] [Field L] [Algebra K L] : Subgroup Kˣ

def NormQuotient (K L : Type u) [Field K] [Field L] [Algebra K L] : Type u

instance normQuotientCommGroup (K L : Type u) [Field K] [Field L] [Algebra K L] :
    CommGroup (NormQuotient K L)

def normQuotientConcreteEquiv
    (K L : Type u) [Field K] [Field L] [Algebra K L] :
    NormQuotient K L ≃* Kˣ ⧸ localNormSubgroup K L

def normClass (K L : Type u) [Field K] [Field L] [Algebra K L] :
    Kˣ →* NormQuotient K L

theorem normQuotientConcreteEquiv_normClass
    (K L : Type u) [Field K] [Field L] [Algebra K L] (x : Kˣ) :
    normQuotientConcreteEquiv K L (normClass K L x) =
      QuotientGroup.mk x

def normQuotientLift {K L : Type u} {M : Type v} [Field K] [Field L] [Algebra K L]
    [Group M] (f : Kˣ →* M) (h : localNormSubgroup K L ≤ f.ker) :
    NormQuotient K L →* M

theorem normQuotientLift_normClass {K L : Type u} {M : Type v} [Field K] [Field L]
    [Algebra K L] [Group M] (f : Kˣ →* M)
    (h : localNormSubgroup K L ≤ f.ker) (x : Kˣ) :
    normQuotientLift f h (normClass K L x) = f x

theorem normQuotientLift_surjective {K L : Type u} {M : Type v} [Field K] [Field L]
    [Algebra K L] [Group M] (f : Kˣ →* M)
    (h : localNormSubgroup K L ≤ f.ker) (hf : Function.Surjective f) :
    Function.Surjective (normQuotientLift f h)

def normQuotientEquivOfSubgroupEq
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (N : Subgroup Kˣ) (h : localNormSubgroup K L = N) :
    NormQuotient K L ≃* Kˣ ⧸ N

theorem normQuotientEquivOfSubgroupEq_normClass
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (N : Subgroup Kˣ) (h : localNormSubgroup K L = N) (x : Kˣ) :
    normQuotientEquivOfSubgroupEq K L N h (normClass K L x) =
      QuotientGroup.mk x

def normQuotientEquivOfNormSubgroupEq
    (K L M : Type u) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (h : localNormSubgroup K L = localNormSubgroup K M) :
    NormQuotient K L ≃* NormQuotient K M

theorem normQuotientEquivOfNormSubgroupEq_normClass
    (K L M : Type u) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (h : localNormSubgroup K L = localNormSubgroup K M) (x : Kˣ) :
    normQuotientEquivOfNormSubgroupEq K L M h (normClass K L x) =
      normClass K M x

def normQuotientEquivOfSurjective
    {K L : Type u} {M : Type v} [Field K] [Field L] [Algebra K L]
    [Group M] (f : Kˣ →* M) (hf : Function.Surjective f)
    (hker : f.ker = localNormSubgroup K L) : NormQuotient K L ≃* M

theorem normQuotientEquivOfSurjective_normClass
    {K L : Type u} {M : Type v} [Field K] [Field L] [Algebra K L]
    [Group M] (f : Kˣ →* M) (hf : Function.Surjective f)
    (hker : f.ker = localNormSubgroup K L) (x : Kˣ) :
    normQuotientEquivOfSurjective f hf hker (normClass K L x) = f x

theorem NormQuotient.inductionOn {K L : Type u} [Field K] [Field L]
    [Algebra K L] {motive : NormQuotient K L → Prop}
    (q : NormQuotient K L)
    (h : ∀ x : Kˣ, motive (normClass K L x)) : motive q

theorem mk_normUnits_eq_one (K L : Type u) [Field K] [Field L] [Algebra K L] (x : Lˣ) :
    normClass K L (normUnits K L x) = 1

theorem normClass_eq_one_iff (K L : Type u) [Field K] [Field L]
    [Algebra K L] (x : Kˣ) :
    normClass K L x = 1 ↔ ∃ y : Lˣ, normUnits K L y = x

theorem normClass_eq_iff_div_mem (K L : Type u) [Field K] [Field L]
    [Algebra K L] (x y : Kˣ) :
    normClass K L x = normClass K L y ↔
      x / y ∈ localNormSubgroup K L

theorem normClass_ker (K L : Type u) [Field K] [Field L] [Algebra K L] :
    MonoidHom.ker (normClass K L) = localNormSubgroup K L

theorem normClass_mem_ker_iff (K L : Type u) [Field K] [Field L]
    [Algebra K L] (x : Kˣ) :
    x ∈ MonoidHom.ker (normClass K L) ↔ x ∈ localNormSubgroup K L

theorem normClass_eq_one_iff_mem (K L : Type u) [Field K] [Field L]
    [Algebra K L] (x : Kˣ) :
    normClass K L x = 1 ↔ x ∈ localNormSubgroup K L

def normQuotientMapOfLE
    (K L M : Type u) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (h : localNormSubgroup K L ≤ localNormSubgroup K M) :
    NormQuotient K L →* NormQuotient K M

theorem normQuotientMapOfLE_normClass
    (K L M : Type u) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (h : localNormSubgroup K L ≤ localNormSubgroup K M) (x : Kˣ) :
    normQuotientMapOfLE K L M h (normClass K L x) = normClass K M x

theorem normUnits_self_apply (K : Type u) [Field K] (x : Kˣ) :
    normUnits K K x = x

theorem localNormSubgroup_self (K : Type u) [Field K] :
    localNormSubgroup K K = ⊤

theorem normQuotient_self_eq_one (K : Type u) [Field K] (x : NormQuotient K K) :
    x = 1

instance normQuotient_self_subsingleton (K : Type u) [Field K] :
    Subsingleton (NormQuotient K K) where
  allEq x y := by
    rw [normQuotient_self_eq_one K x, normQuotient_self_eq_one K y]

theorem normClass_eq_one_of_mem (K L : Type u) [Field K] [Field L]
    [Algebra K L] {x : Kˣ} (hx : x ∈ localNormSubgroup K L) :
    normClass K L x = 1

theorem normClass_normUnits_zpow_eq_one
    (K L : Type u) [Field K] [Field L] [Algebra K L] (x : Lˣ) (n : Int) :
    normClass K L ((normUnits K L x) ^ n) = 1

theorem normClass_eq_iff_exists_norm_div (K L : Type u)
    [Field K] [Field L] [Algebra K L] (x y : Kˣ) :
    normClass K L x = normClass K L y ↔
      ∃ z : Lˣ, x / y = normUnits K L z

theorem normClass_normUnits_mul (K L : Type u)
    [Field K] [Field L] [Algebra K L] (z : Lˣ) (x : Kˣ) :
    normClass K L (normUnits K L z * x) = normClass K L x

theorem normClass_mul_normUnits (K L : Type u)
    [Field K] [Field L] [Algebra K L] (x : Kˣ) (z : Lˣ) :
    normClass K L (x * normUnits K L z) = normClass K L x

theorem normClass_normUnits_zpow_mul (K L : Type u)
    [Field K] [Field L] [Algebra K L] (z : Lˣ) (n : Int) (x : Kˣ) :
    normClass K L ((normUnits K L z) ^ n * x) =
      normClass K L x

theorem normClass_mul_normUnits_zpow (K L : Type u)
    [Field K] [Field L] [Algebra K L] (x : Kˣ) (z : Lˣ) (n : Int) :
    normClass K L (x * (normUnits K L z) ^ n) =
      normClass K L x

theorem normClass_eq_of_eq_normUnits_mul (K L : Type u)
    [Field K] [Field L] [Algebra K L] {x y : Kˣ} (z : Lˣ)
    (h : x = normUnits K L z * y) :
    normClass K L x = normClass K L y

theorem normClass_eq_iff_mul_inv_mem (K L : Type u)
    [Field K] [Field L] [Algebra K L] (x y : Kˣ) :
    normClass K L x = normClass K L y ↔
      x * y⁻¹ ∈ localNormSubgroup K L

theorem normClass_eq_iff_exists_norm_mul_left (K L : Type u)
    [Field K] [Field L] [Algebra K L] (x y : Kˣ) :
    normClass K L x = normClass K L y ↔
      ∃ z : Lˣ, x = normUnits K L z * y

theorem normClass_eq_iff_exists_norm_mul_right (K L : Type u)
    [Field K] [Field L] [Algebra K L] (x y : Kˣ) :
    normClass K L x = normClass K L y ↔
      ∃ z : Lˣ, x = y * normUnits K L z

theorem normClass_eq_all_of_normUnits_surjective (K L : Type u)
    [Field K] [Field L] [Algebra K L]
    (h : Function.Surjective (normUnits K L)) (x y : Kˣ) :
    normClass K L x = normClass K L y

theorem normClass_eq_of_localNormSubgroup_eq_top (K L : Type u)
    [Field K] [Field L] [Algebra K L] (h : localNormSubgroup K L = ⊤) (x y : Kˣ) :
    normClass K L x = normClass K L y