Mathlib.Algebra.Algebra.Subalgebra.Operations

AlgHom.ker_rangeRestrict theorem

(f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f

Full source

theorem ker_rangeRestrict (f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f :=
  Ideal.ext fun _ ↦ Subtype.ext_iff

Kernel Equality for Range-Restricted Algebra Homomorphism

Informal description

For any $R$-algebra homomorphism $f \colon A \to B$, the kernel of the range-restricted homomorphism $f_{\text{rangeRestrict}} \colon A \to \text{range}(f)$ is equal to the kernel of $f$.

Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem theorem

 {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S) (e : ∑ i ∈ ι', l i * s i = 1) (hs : ∀ i, s i ∈ S')
  (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S'

Full source

/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` ∈ `S`, and `S'` a subalgebra of `S` that contains
`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
    {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S)
    (e : ∑ i ∈ ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
    (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
  suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range by
    obtain ⟨x, rfl⟩ := this
    exact x.2
  choose n hn using H
  let s' : ι → S' := fun x => ⟨s x, hs x⟩
  let l' : ι → S' := fun x => ⟨l x, hl x⟩
  have e' : ∑ i ∈ ι', l' i * s' i = 1 := by
    ext
    show S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
    simpa only [map_sum, map_mul] using e
  have : Ideal.span (s' '' ι') = ⊤ := by
    rw [Ideal.eq_top_iff_one, ← e']
    apply sum_mem
    intros i hi
    exact Ideal.mul_mem_left _ _ <| Ideal.subset_span <| Set.mem_image_of_mem s' hi
  let N := ι'.sup n
  have hN := Ideal.span_pow_eq_top _ this N
  apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hN
  rintro ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩
  change s' i ^ N • x ∈ _
  rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]
  refine Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_
  exact ⟨⟨_, hn i⟩, rfl⟩

Membership Criterion via Power-Scalar Condition in Subalgebras

Informal description

Let $S$ be an $R$-algebra and $S'$ a subalgebra of $S$. Suppose there exists a finite set $\iota'$ and elements $s_i, l_i \in S$ for each $i \in \iota'$ such that: 1. $\sum_{i \in \iota'} l_i s_i = 1$, 2. $s_i \in S'$ and $l_i \in S'$ for all $i \in \iota'$. Then for any $x \in S$, if for each $i \in \iota'$ there exists a natural number $n$ such that $s_i^n \cdot x \in S'$, it follows that $x \in S'$.

Subalgebra.mem_of_span_eq_top_of_smul_pow_mem theorem

 (s : Set S) (l : s →₀ S) (hs : Finsupp.linearCombination S ((↑) : s → S) l = 1) (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S')
  (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') : x ∈ S'

Full source

theorem mem_of_span_eq_top_of_smul_pow_mem
    (s : Set S) (l : s →₀ S) (hs : Finsupp.linearCombination S ((↑) : s → S) l = 1)
    (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
    x ∈ S' :=
  mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H

Subalgebra Membership Criterion via Span and Power-Scalar Condition

Informal description

Let $S$ be an $R$-algebra and $S'$ a subalgebra of $S$. Given a subset $s \subseteq S$ such that: 1. There exists a finitely supported function $l \colon s \to S$ with $\sum_{r \in s} l(r) \cdot r = 1$, 2. $s \subseteq S'$ and $l(r) \in S'$ for all $r \in s$, then for any $x \in S$, if for each $r \in s$ there exists a natural number $n$ such that $r^n \cdot x \in S'$, it follows that $x \in S'$.