import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Ideal.Maps
import Mathlib.RingTheory.Ideal.Quotient.Operations
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.ZMod.QuotientRing
import Mathlib.RingTheory.ZMod
import Mathlib.Tactic

-- ============================================================================
-- Ideals and Quotient Rings
-- ============================================================================
--
-- Ideals are to rings what normal subgroups are to groups:
--   - Normal subgroup N ◁ G ⟹ quotient group G/N
--   - Ideal           I ◁ R ⟹ quotient ring  R/I
--
-- The idea: take the ring R and declare that everything in I is now considered
-- to be zero. Once we declare I = 0, two elements a, b ∈ R become "the same"
-- whenever their difference lies in I:
--   a ≃ b ⟺ a − b ∈ I
--
-- For example: in ℤ/5ℤ, also written as ℤ/(5), every multiple of 5 is zero,
-- so 3 and 8 represent the same element.
example : (3 : ZMod 5) = (8 : ZMod 5) := by decide
example : (3 : ZMod 5) - (8 : ZMod 5) = (0 : ZMod 5) := by decide

-- ============================================================================
-- Section 1: What is an ideal?
-- ============================================================================
--
-- An ideal I ⊆ R is a subset that is:
--   1. An additive subgroup:
--      0 ∈ I,  a, b ∈ I ⟹ a - b ∈ I
--   2. Closed under multiplication BY ANYTHING in R (the absorbing property):
--      a ∈ I, r ∈ R  ⟹  r * a ∈ I
--
-- The absorbing property is the key one — it's what distinguishes an ideal
-- from a subring.

-- The set of multiples of 3 in ℤ, written (3) or 3ℤ:
example : Ideal ℤ := Ideal.span {3}

-- 6 ∈ (3), -9 ∈ (3), 7 ∉ (3)
example : (6 : ℤ) ∈ Ideal.span ({3} : Set ℤ) := by
  rw [Ideal.mem_span_singleton]; exact ⟨2, by ring⟩

example : (-9 : ℤ) ∈ Ideal.span ({3} : Set ℤ) := by
  rw [Ideal.mem_span_singleton]; exact ⟨-3, by ring⟩

example : (7 : ℤ) ∉ Ideal.span ({3} : Set ℤ) := by
  rw [Ideal.mem_span_singleton]; decide

-- ============================================================================
-- Section 2: The inclusion order — "bigger" means "denser"
-- ============================================================================
--
-- Ideals are ordered by ⊆. In ℤ every ideal is countably infinite, so
-- "bigger" can't mean "more elements." The right intuition is DENSITY:
--
--   ℤ = (1):    ●●●●●●●●●●●●●●●●●●●●●●●●●●●  (every integer)
--   (2):        ●·●·●·●·●·●·●·●·●·●·●·●·●·●  (every 2nd)
--   (3):        ●··●··●··●··●··●··●··●··●··  (every 3rd)
--   (6):        ●·····●·····●·····●·····●··  (every 6th)
--   (12):       ●···········●···········●··  (every 12th)
--
-- Asymptotic density of (n) is 1/n. Side effect: BIGGER generator
-- → SMALLER ideal. Every multiple of 6 is a multiple of 3, so (6) ⊆ (3).

example : Ideal.span ({6} : Set ℤ) ≤ Ideal.span ({3} : Set ℤ) := by
  rw [Ideal.span_singleton_le_span_singleton]
  exact ⟨2, by ring⟩

-- The two extremes:
example : Ideal ℤ := ⊥ -- {0}, sparsest
example : Ideal ℤ := ⊤ -- ℤ, densest
example : (0 : ℤ) ∈ (⊥ : Ideal ℤ) := Ideal.zero_mem _
example : (42 : ℤ) ∈ (⊤ : Ideal ℤ) := trivial

-- An ideal contains 1 iff it's the whole ring (since r = r·1 ∈ I forces
-- everything in). We'll generalize this in §4: any UNIT in I forces I = R.
example (I : Ideal ℤ) (h : (1 : ℤ) ∈ I) : I = ⊤ :=
  (Ideal.eq_top_iff_one I).mpr h

-- Algebraic mirror of density: quotient size |ℤ/(n)| = n.
-- Sparser ideal → bigger quotient (more cosets). The construction is in §6.
example : Fintype.card (ZMod 6) = 6 := by decide
example : Fintype.card (ZMod 2) = 2 := by decide

-- ============================================================================
-- Section 3: Principal ideals — generated by one element
-- ============================================================================
--
-- The ideal "generated by a" is the smallest (sparsest) ideal containing a.
-- It equals { r * a | r ∈ R }, written (a) or Ideal.span {a}.
--
-- An ideal generated by one element is PRINCIPAL. A ring where every ideal
-- is principal is a principal ideal domain (PID). ℤ and k[X] are PIDs; most
-- rings aren't (e.g. in k[X, Y] the ideal (X, Y) needs two generators).

-- The principal ideal (6) = {..., -12, -6, 0, 6, 12, 18, ...}.
example : Ideal ℤ := Ideal.span {6}

-- Members are of the form r·6 for some r ∈ ℤ.
example : (12 : ℤ) ∈ Ideal.span ({6} : Set ℤ) := by  -- 12 = 2·6
  rw [Ideal.mem_span_singleton]; exact ⟨2, by ring⟩

example : (-18 : ℤ) ∈ Ideal.span ({6} : Set ℤ) := by -- -18 = (-3)·6
  rw [Ideal.mem_span_singleton]; exact ⟨-3, by ring⟩

-- And (6) really is the SMALLEST ideal containing 6:
-- any ideal I with 6 ∈ I must contain every multiple of 6, hence all of (6).
example (I : Ideal ℤ) (h : (6 : ℤ) ∈ I) : Ideal.span ({6} : Set ℤ) ≤ I :=
  Ideal.span_le.mpr (Set.singleton_subset_iff.mpr h)

-- Edge cases:
example : Ideal.span ({0} : Set ℤ) = ⊥ := by simp
example : Ideal.span ({1} : Set ℤ) = ⊤ := by simp

-- ============================================================================
-- Section 4: Units
-- ============================================================================
--
-- An element u ∈ R is a UNIT if it has a multiplicative inverse u⁻¹ ∈ R.
--
-- Units detect when a principal ideal is the whole ring:
--   u is a unit ⟺ (u) = R ⟺ 1 ∈ (u)
--
-- More generally, an ideal I contains a unit ⟺ I = R. This is why
-- ideals "see" non-units: they can be proper precisely because they
-- avoid the units. (Recall §2: 1 ∈ I ⟹ I = R; units are how 1 sneaks in.)
--
-- The units of R form a group Rˣ under multiplication.

example : IsUnit (1 : ℤ)   := isUnit_one
example : ¬ IsUnit (2 : ℤ) := by rw [Int.isUnit_iff]; decide

-- ℤ has only two units: 1 and -1. Despite ℤ being infinite, ℤˣ ≅ ℤ/2ℤ.
example : Fintype.card ℤˣ = 2 := by decide

-- (ℤ/Nℤ)ˣ consists of residues coprime to N, so |(ℤ/Nℤ)ˣ| = φ(N),
-- Euler's totient function.
example : Fintype.card (ZMod 6)ˣ = 2 := by decide -- φ(6) = 2 units: {1, 5}
example : Fintype.card (ZMod 9)ˣ = 6 := by decide -- φ(9) = 6 units: {1,2,4,5,7,8}

-- ============================================================================
-- Section 5: Kernels
-- ============================================================================
--
-- For a ring hom φ : R → S, the KERNEL is { r ∈ R | φ(r) = 0 }.
--
-- Theorem: ker φ is always an ideal. Conversely, every ideal is the kernel
-- of some hom (the projection R → R/I from §6). So ideals = kernels.
--
-- Classic example: reduction mod n. φ : ℤ → ℤ/nℤ, ker φ = nℤ.

example : ℤ →+* ZMod 5 := Int.castRingHom (ZMod 5)
example : (Int.castRingHom (ZMod 5)) 5  = 0 := by decide
example : (Int.castRingHom (ZMod 5)) 10 = 0 := by decide
example : (Int.castRingHom (ZMod 5)) 7  = 2 := by decide   -- not in kernel
example : Ideal ℤ := RingHom.ker (Int.castRingHom (ZMod 5))

-- ============================================================================
-- Section 6: Quotient rings — the construction
-- ============================================================================
--
-- Given an ideal I ⊆ R, form R/I by declaring a ≃ b ⟺ a - b ∈ I.
--
-- ----------------------------------------------------------------------------
-- Aside: equivalence classes
-- ----------------------------------------------------------------------------
--
-- An equivalence relation ~ groups elements into EQUIVALENCE CLASSES:
--   [a] := { x ∈ R | x ~ a }   "everything equivalent to a"
--
-- Two key facts:
--   1. Classes PARTITION R: every element lives in exactly one class.
--   2. Many names, one class: [a] = [b] ⟺ a ~ b.
--      So [3], [8], [13], [-2] are four names for the same class in ℤ/(5).
--
-- Examples in ℤ with a ~ b ⟺ 5 ∣ (a - b):
--   [0] = {..., -10, -5, 0, 5, 10, ...} (multiples of 5 — this IS the ideal (5))
--   [1] = {..., -9, -4, 1, 6, 11, ...}
--   [2] = {..., -8, -3, 2, 7, 12, ...}
--   [3] = {..., -7, -2, 3, 8, 13, ...}
--   [4] = {..., -6, -1, 4, 9, 14, ...}
--
-- The quotient set R/~ is the set of these classes. Set-theoretically each
-- [a] is a subset of R, but in R/~ we treat it as a SINGLE ELEMENT — a point
-- in a new space. (So ℤ/(5) has exactly 5 elements: [0], [1], [2], [3], [4].)
--
-- ----------------------------------------------------------------------------
--
-- For an ideal I, the relation a ~ b ⟺ a - b ∈ I is automatically an
-- equivalence relation (0 ∈ I, I closed under negation, I closed under +).
-- The classes take the concrete form [a] = a + I = { a + i : i ∈ I },
-- called COSETS. They form a new ring, and I literally becomes the new
-- zero: [a] = 0 ⟺ a ∈ I. (In particular, [0] is the class equal to I itself.)
--
-- Mathlib's API:
--   R ⧸ I                the quotient ring
--   Ideal.Quotient.mk I  projection R → R ⧸ I,  a ↦ [a]
--   Ideal.Quotient.eq    [a] = [b] ⟺ a - b ∈ I

private abbrev I5 : Ideal ℤ := Ideal.span {(5 : ℤ)}
private abbrev π5 : ℤ →+* (ℤ ⧸ I5) := Ideal.Quotient.mk _

example : Type := ℤ ⧸ I5
example (a b : ℤ) : Ideal.Quotient.mk (I5) a = Ideal.Quotient.mk (I5) b ↔ a - b ∈ I5 :=
  Ideal.Quotient.eq

-- ============================================================================
-- Section 7: ℤ/(5) — modular arithmetic in Lean
-- ============================================================================
--
-- ℤ/(5) has 5 cosets {[0], [1], [2], [3], [4]}. (We'll see in §9 that (5) is
-- maximal, which is why ℤ/(5) ends up being a field.)

-- Reduction: integers wrap mod 5
example : π5 7 = π5 2 := by
  rw [Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨1, by ring⟩

example : π5 12 = π5 2 := by
  rw [Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨2, by ring⟩

example : π5 (-3) = π5 2 := by
  rw [Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨-1, by ring⟩

-- Arithmetic: + and · respect the projection
example : π5 2 + π5 3 = π5 0 := by
  rw [← map_add, Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨1, by ring⟩

example : π5 2 * π5 3 = π5 1 := by
  rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨1, by ring⟩

example : π5 4 * π5 4 = π5 1 := by
  rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨3, by ring⟩

-- Inverses (read off the multiplications above):
--   [1]⁻¹ = [1],  [2]⁻¹ = [3],  [3]⁻¹ = [2],  [4]⁻¹ = [4]

-- Mathlib's `ZMod 5` is the same field, built differently:
example : (ℤ ⧸ I5) ≃+* ZMod 5 := Int.quotientSpanNatEquivZMod 5

-- ============================================================================
-- Section 8: When the quotient ISN'T a field — ℤ/(6)
-- ============================================================================
--
-- (6) ⊆ ℤ is not maximal (§9) — and not even prime as an ideal: 2 · 3 = 6 ∈ (6)
-- but neither 2 nor 3 is. So ℤ/(6) is just a ring, with zero divisors:

private abbrev I6 : Ideal ℤ := Ideal.span {(6 : ℤ)}
private abbrev π6 : ℤ →+* (ℤ ⧸ I6) := Ideal.Quotient.mk _

-- [2] · [3] = [6] = [0] yet [2] and [3] are nonzero
example : π6 2 * π6 3 = π6 0 := by
  rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton]
  exact ⟨1, by ring⟩

example : π6 2 ≠ π6 0 := by
  rw [Ne, Ideal.Quotient.eq, Ideal.mem_span_singleton]
  decide

example : π6 3 ≠ π6 0 := by
  rw [Ne, Ideal.Quotient.eq, Ideal.mem_span_singleton]
  decide

-- ℤ/(5) prime → maximal → field (no zero divisors)
-- ℤ/(6) composite → just a ring (zero divisors, no cancellation)
--
-- Polynomial analog: ℝ[X]/(X² - 1) has [X-1] · [X+1] = [0] via the
-- factorization X² - 1 = (X-1)(X+1). Same moral. This concrete failure
-- is exactly what "prime ideal" is defined to prevent (§9).

-- ============================================================================
-- Section 9: Maximal and prime ideals
-- ============================================================================
--
-- §8 showed a quotient with zero divisors. Two properties of the ideal rule
-- those out (and more):
--
--   M is MAXIMAL if M ≠ R and no ideal squeezes strictly between M and R.
--     Theorem: R/M is a field ⟺ M is maximal.
--
--   P is PRIME if P ≠ R and a·b ∈ P ⟹ a ∈ P or b ∈ P.
--     Theorem: R/P is an integral domain ⟺ P is prime.
--
-- ----------------------------------------------------------------------------
-- The inclusion lattice in ℤ
-- ----------------------------------------------------------------------------
--
-- Recall from §2: bigger generator → sparser ideal. So the lattice grows
-- denser going UP, and maximal ideals sit JUST BELOW ℤ:
--
--   ℤ = (1)
--        │
--       (2)    (3)    (5)    (7)    ...
--        │      │
--       (4)    (9)
--        │      │
--       (8)    (27)
--        ⋮     ⋮
--
-- In ℤ: (n) is maximal ⟺ n is prime.
--
-- So ℤ has INFINITELY MANY maximal ideals — one for every prime — and each
-- gives a different field quotient:
--   ℤ/(2) = 𝔽₂, ℤ/(3) = 𝔽₃, ℤ/(5) = 𝔽₅, ℤ/(7) = 𝔽₇, ...
--
-- (Rings with exactly one maximal ideal are called LOCAL rings; ℤ isn't one.)
--
-- BY CONTRAST: a FIELD has only TWO ideals — {0} and itself — because every
-- nonzero element is a unit, and units force I = R (§4). Trivial lattice.
-- That's why ring theory cares about non-fields like ℤ and k[X]: they have
-- the RICH ideal structure to quotient by, and those quotients are often
-- where new fields come from (𝔽ₚ, GF(9), ℂ).

example : (Ideal.span ({5} : Set ℤ)).IsMaximal :=
  PrincipalIdealRing.isMaximal_of_irreducible <|
    (Int.prime_iff_natAbs_prime.mpr (by decide)).irreducible

example : (Ideal.span ({7} : Set ℤ)).IsMaximal :=
  PrincipalIdealRing.isMaximal_of_irreducible <|
    (Int.prime_iff_natAbs_prime.mpr (by decide)).irreducible

-- And so ℤ/(5) is a field (Mathlib derives the Field instance automatically):
noncomputable example : Field (ℤ ⧸ Ideal.span ({5} : Set ℤ)) :=
  haveI : (Ideal.span ({5} : Set ℤ)).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible <|
      (Int.prime_iff_natAbs_prime.mpr (by decide)).irreducible
  Ideal.Quotient.field _

-- Why "maximal ⟹ field": take nonzero [a] ∈ R/M, so a ∉ M. Then M + (a)
-- strictly contains M, so by maximality M + (a) = R. Hence 1 = m + r·a, and
-- mod M this gives [r][a] = 1. So [a] is invertible (Bézout in disguise.)
--
-- Every maximal ideal is prime, but not vice versa. Classic: in ℤ[X], (X)
-- is prime (quotient ≅ ℤ, a domain) but not maximal. (X, 5) is maximal,
-- with quotient ≅ 𝔽₅.
--
-- The hierarchy:
--
--   maximal ideal  ⟹  prime ideal  ⟹  proper ideal
--      │                  │                │
--      ▼                  ▼                ▼
--      field          integral domain     ring
--      (R/M)             (R/P)            (R/I)

-- TODO: Expand this
-- ============================================================================
-- Section 10: The First Isomorphism Theorem
-- ============================================================================
--
-- The bridge between ideals-as-kernels (§5) and quotients (§6):
--
--   For any ring hom φ : R → S,  R / ker(φ) ≅ image(φ).
--
-- Mathlib: `RingHom.quotientKerEquivOfSurjective` / `quotientKerEquivRange`.

-- Applied to the cast ℤ → ZMod 5 (surjective, with kernel (5)):
noncomputable example :
    (ℤ ⧸ RingHom.ker (Int.castRingHom (ZMod 5))) ≃+* ZMod 5 :=
  RingHom.quotientKerEquivOfSurjective ZMod.intCast_surjective

-- Same recipe builds ℝ[X]/(X²+1) ≅ ℂ, 𝔽₃[X]/(X²+1) ≅ GF(9), etc.
-- (See Polynomials.lean.)

-- TODO: Expand this
-- ============================================================================
-- Section 11: The universal property of the quotient
-- ============================================================================
--
-- §6 sends elements INTO the quotient. The universal property maps OUT:
--
--   For any ring hom φ : R → S with I ⊆ ker(φ),
--   there is a UNIQUE φ̄ : R ⧸ I → S with φ = φ̄ ∘ π.
--
--     R ──φ──→ S
--      \     ↗
--       π   ∃! φ̄
--        ↘ /
--        R⧸I
--
-- Mathlib: `Ideal.Quotient.lift`.

example : (ℤ ⧸ I5) →+* ZMod 5 :=
  Ideal.Quotient.lift I5 (Int.castRingHom (ZMod 5)) (fun _ ha => by
    rw [← RingHom.mem_ker, ZMod.ker_intCastRingHom]; exact ha)