text:
/-
Copyright (c) 2022 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz, Junyan Xu
-/
import ring_theory.localization.localization_localization

/-!

# Localizations of domains as subalgebras of the fraction field.

Given a domain `A` with fraction field `K`, and a submonoid `S` of `A` which
does not contain zero, this file constructs the localization of `A` at `S`
as a subalgebra of the field `K` over `A`.

-/

namespace localization
open_locale non_zero_divisors
variables {A : Type*} (K : Type*) [comm_ring A] (S : submonoid A) (hS : S ≤ A⁰)

section comm_ring
variables [comm_ring K] [algebra A K] [is_fraction_ring A K]

lemma map_is_unit_of_le (hS : S ≤ A⁰) (s : S) : is_unit (algebra_map A K s) :=
by apply is_localization.map_units K (⟨s.1, hS s.2⟩ : A⁰)

/-- The canonical map from a localization of `A` at `S` to the fraction ring
  of `A`, given that `S ≤ A⁰`. -/
noncomputable
def map_to_fraction_ring (B : Type*) [comm_ring B] [algebra A B]
  [is_localization S B] (hS : S ≤ A⁰) :
  B →ₐ[A] K :=
{ commutes' := λ a, by simp,
  ..is_localization.lift (map_is_unit_of_le K S hS) }

@[simp]
lemma map_to_fraction_ring_apply {B : Type*} [comm_ring B] [algebra A B]
  [is_localization S B] (hS : S ≤ A⁰) (b : B) :
  map_to_fraction_ring K S B hS b = is_localization.lift (map_is_unit_of_le K S hS) b := rfl

lemma mem_range_map_to_fraction_ring_iff (B : Type*) [comm_ring B] [algebra A B]
  [is_localization S B] (hS : S ≤ A⁰) (x : K) :
  x ∈ (map_to_fraction_ring K S B hS).range ↔
  ∃ (a s : A) (hs : s ∈ S), x = is_localization.mk' K a ⟨s, hS hs⟩ :=
⟨ by { rintro ⟨x,rfl⟩, obtain ⟨a,s,rfl⟩ := is_localization.mk'_surjective S x,
    use [a, s, s.2], apply is_localization.lift_mk' },
  by { rintro ⟨a,s,hs,rfl⟩, use is_localization.mk' _ a ⟨s,hs⟩,
    apply is_localization.lift_mk' } ⟩

instance is_localization_range_map_to_fraction_ring (B : Type*) [comm_ring B] [algebra A B]
  [is_localization S B] (hS : S ≤ A⁰) :
  is_localization S (map_to_fraction_ring K S B hS).range :=
is_localization.is_localization_of_alg_equiv S $ show B ≃ₐ[A] _, from alg_equiv.of_bijective
(map_to_fraction_ring K S B hS).range_restrict
begin
  refine ⟨λ a b h, _, set.surjective_onto_range⟩,
  refine (is_localization.lift_injective_iff _).2 (λ a b, _) (subtype.ext_iff.1 h),
  exact ⟨λ h, congr_arg _ (is_localization.injective _ hS h),
         λ h, congr_arg _ (is_fraction_ring.injective A K h)⟩,
end

instance is_fraction_ring_range_map_to_fraction_ring
  (B : Type*) [comm_ring B] [algebra A B]
  [is_localization S B] (hS : S ≤ A⁰) :
  is_fraction_ring (map_to_fraction_ring K S B hS).range K :=
is_fraction_ring.is_fraction_ring_of_is_localization S _ _ hS

/--
Given a commutative ring `A` with fraction ring `K`, and a submonoid `S` of `A` which
contains no zero divisor, this is the localization of `A` at `S`, considered as
a subalgebra of `K` over `A`.

The carrier of this subalgebra is defined as the set of all `x : K` of the form
`is_localization.mk' K a ⟨s, _⟩`, where `s ∈ S`.
-/
noncomputable
def subalgebra (hS : S ≤ A⁰) : subalgebra A K :=
(map_to_fraction_ring K S (localization S) hS).range.copy
{ x | ∃ (a s : A) (hs : s ∈ S), x = is_localization.mk' K a ⟨s, hS hs⟩ } $
by { ext, symmetry, apply mem_range_map_to_fraction_ring_iff }

namespace subalgebra

instance is_localization_subalgebra :
  is_localization S (subalgebra K S hS) :=
by { dunfold localization.subalgebra, rw subalgebra.copy_eq, apply_instance }

instance is_fraction_ring : is_fraction_ring (subalgebra K S hS) K :=
is_fraction_ring.is_fraction_ring_of_is_localization S _ _ hS

end subalgebra
end comm_ring

section field
variables [field K] [algebra A K] [is_fraction_ring A K]
namespace subalgebra

lemma mem_range_map_to_fraction_ring_iff_of_field
  (B : Type*) [comm_ring B] [algebra A B] [is_localization S B] (x : K) :
  x ∈ (map_to_fraction_ring K S B hS).range ↔
  ∃ (a s : A) (hs : s ∈ S), x = algebra_map A K a * (algebra_map A K s)⁻¹ :=
begin
  rw mem_range_map_to_fraction_ring_iff,
  iterate 3 { congr' with }, convert iff.rfl, rw units.coe_inv, refl,
end

/--
Given a domain `A` with fraction field `K`, and a submonoid `S` of `A` which
contains no zero divisor, this is the localization of `A` at `S`, considered as
a subalgebra of `K` over `A`.

The carrier of this subalgebra is defined as the set of all `x : K` of the form
`algebra_map A K a * (algebra_map A K s)⁻¹` where `a s : A` and `s ∈ S`.
-/
noncomputable
def of_field : _root_.subalgebra A K :=
(map_to_fraction_ring K S (localization S) hS).range.copy
{ x | ∃ (a s : A) (hs : s ∈ S), x = algebra_map A K a * (algebra_map A K s)⁻¹ } $
by { ext, symmetry, apply mem_range_map_to_fraction_ring_iff_of_field }

instance is_localization_of_field :
  is_localization S (subalgebra.of_field K S hS) :=
by { dunfold localization.subalgebra.of_field, rw subalgebra.copy_eq, apply_instance }

instance is_fraction_ring_of_field : is_fraction_ring (subalgebra.of_field K S hS) K :=
is_fraction_ring.is_fraction_ring_of_is_localization S _ _ hS

end subalgebra
end field

end localization

subset_name: curated


TITLE: Factorial Divisors
QUESTION [4 upvotes]: Q. For what maximum value of $n$ will the expression $\frac{10200!}{504^n}$ be an integer? I have the solution to this question and I would like you to please go through the solution below. My doubt follows the solution :)
The solution can be found by writing $504 = 2^3 \cdot 3^2 \cdot 7$ and then finding the number of $2^3$s, $3^2$s and $7$s in the numerator, which can be obtained by
Number of $2$s = $\left\lfloor\frac{10200}{2}\right\rfloor + \left\lfloor\frac{10200}{2^2}\right\rfloor + \left\lfloor\frac{10200}{2^3}\right\rfloor + \dots + \left\lfloor\frac{10200}{2^{13}}\right\rfloor= 10192$
where $\left\lfloor\dots\right\rfloor$ is the floor function.
Therefore, the number of $2^3\textrm{s} = \left\lfloor\frac{10192}{3}\right\rfloor = 3397$
$\begin{align}\textrm{Similarly, the number of }3^2\textrm{s} &= 2457\\
      \textrm{and the number of }7\textrm{s}  & = 1698\end{align}$
The number of factors of $2^3 \cdot 3^2 \cdot 7$ is clearly constrained by the number of $7$s, therefore $n = 1698$.
My question is, whether there is any way I can simply look at the prime factors of the divisor and know which prime factor is going to be the constraining factor? (as $7$ was, in this particular example)

REPLY [5 votes]: In this answer, it is shown that the number of factors of $p$ in $n!$ is
$$
\frac{n-\sigma_p(n)}{p-1}\tag{1}
$$
where $\sigma_p(n)$ is the sum of the base-$p$ digits of $n$.
Factor
$$
504=2^3\cdot3^2\cdot7\tag{2}
$$
Write $10200$ in base-$2$, base-$3$, and base-$7$:
$$
\begin{array}{}10011111011000_2&111222210_3&41511_7\end{array}\tag{3}
$$
The number of factors of $2$ in $10200!$ is $\frac{10200-8}{2-1}=10192$.
The number of factors of $3$ in $10200!$ is $\frac{10200-12}{3-1}=5094$.
The number of factors of $7$ in $10200!$ is $\frac{10200-12}{7-1}=1698$.
Since $\left\lfloor\frac{10192}{3}\right\rfloor=3397$, $\left\lfloor\frac{5094}{2}\right\rfloor=2547$, and $\left\lfloor\frac{1698}{1}\right\rfloor=1698$, the maximum value of $n$ so that $\frac{10200!}{504^n}$ is an integer is $n=1698$.
To answer the question asked:
For large $n$, the sum of the digits of $n$ is small compared to $n$, so suppose
$$
d=p_1^{e_1}p_2^{e_2}\dots p_m^{e_m}\tag{4}
$$
Following the computations above, the greatest power of $d$ that divides $n!$ is
$$
\min_k \left\lfloor\frac{n-\sigma_{p_k}(n)}{e_k(p_k-1)}\right\rfloor\tag{5}
$$
Ignoring $\sigma_{p_k}(n)$ as negligible, the greatest of $e_k(p_k-1)$ is a strong indicator of which $p_k$ is the constraining factor.
In the current case, the greatest of $3(2-1)=3$,  $2(3-1)=4$, and $1(7-1)=6$ hints strongly that $7$ is the constraining factor.


TITLE: How would I find the solutions for $AX = 0?$
QUESTION [0 upvotes]: \begin{pmatrix}4&-6&2&-6\\ \:-2&3&-1&3\end{pmatrix}
Am I supposed to move the $0 $ to the other side of the equation and find the inverse of the matrix above or is there another way?

REPLY [0 votes]: You have 4 variables and 2 equations. This implies that you have infinitly many solutions.


TITLE: Showing $A=F(K)$ where $F(K)$ denotes the set of complex-valued functions on $K$?
QUESTION [2 upvotes]: If $K$ is a finite set and $\mathcal{A}$ is a set of functions that is a self-adjoint algebra, separates points, and vanishes nowhere. Show that $\mathcal{A}$ has to contain every complex function on $K$.
a Self-Adjoint Algebra means that for $f,g\in \mathcal{A}$, $c\in \mathbb{C}$ it follows that $f+g\in \mathcal{A}$, $f\cdot g\in \mathcal{A}$, $cf\in \mathcal{A}$ and $\bar{f}\in \mathcal{A}$.
Separates Points means $\forall x,y\in K$ with $x\neq y$. $\exists f\in \mathcal{A}$ so that $f(x)\neq f(y)$.
Vanishes Nowhere means $\forall x\in K, \exists f\in \mathcal{A}$ so that $f(x)\neq 0$.

REPLY [0 votes]: Note that the cases where $|K| \leq 1$ are easy, so suppose $|K| \geq 2$. It suffices to show that for every distinct pair of points $p, q \in K$ that there is a function $f_{p, q} \in \mathcal{A}$ such that $f_{p, q}(p) \neq 0$ and $f_{p, q}(q) = 0$, since then the indicator function $\delta_p$ may be written as a re-normalisation of the function
$ D_p := \prod_{q \neq p} f_{p, q}$.
Given a pair of distinct points $p, q \in K$, such a function $f_{p, q} \in \mathcal{A}$ does always exist. By the assumption that $\mathcal{A}$ separates points, there exists a $g \in \mathcal{A}$ such that $g(p) \neq g(q)$. We then have two cases:

If $g(p) \neq 0$, then set $f_{p, q} = g^2 - g(q)g$.
If $g(p) = 0$ (and so $g(q) \neq 0$), then set $f_{p, q} = h - \frac{h(q)}{g(q)}g$, where $h \in \mathcal{A}$ is a function with $h(p) \neq 0$ (which exists by the nowhere-vanishing assumption).


TITLE: 1-model complete
QUESTION [1 upvotes]: For $L$ structures $A$ and $B$ we write $A\preceq_{1}B$ if $A\subseteq{B}$ and $A\models{\varphi(a)}$ iff $B\models{\varphi(a)}$ for any finite tuple (of the correct length) $a$ from $A$ and for any universal formula $\varphi(x)$.
An $L$ theory $T$ is 1-model complete if whenever $A\preceq_{1}B$ with $A,B\models{T}$, we have $A\preceq{B}$.
There are several equivalent statements for a theory being model complete (see here: http://modeltheory.wikia.com/wiki/Model_completeness for a list of equivalent statments). Are there such equivalence statements in the above case. And if so what would be a good reference for them?

REPLY [1 votes]: You might find what you're looking for in this paper.