text:
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon

The writer monad transformer for passing immutable state.
-/
import algebra.group.defs
import logic.equiv.basic

universes u v w u₀ u₁ v₀ v₁

structure writer_t (ω : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
(run : m (α × ω))

@[reducible] def writer (ω : Type u) := writer_t ω id

attribute [pp_using_anonymous_constructor] writer_t

namespace writer_t
section
  variable  {ω : Type u}
  variable  {m : Type u → Type v}
  variable  [monad m]
  variables {α β : Type u}
  open function

  @[ext]
  protected

  @[inline] protected def tell (w : ω) : writer_t ω m punit :=
  ⟨pure (punit.star, w)⟩

  @[inline] protected def listen : writer_t ω m α → writer_t ω m (α × ω)
  | ⟨ cmd ⟩ := ⟨ (λ x : α × ω, ((x.1,x.2),x.2)) <$> cmd ⟩

  @[inline] protected def pass : writer_t ω m (α × (ω → ω)) → writer_t ω m α
  | ⟨ cmd ⟩ := ⟨ uncurry (uncurry $ λ x (f : ω → ω) w, (x,f w)) <$> cmd ⟩

  @[inline] protected def pure [has_one ω] (a : α) : writer_t ω m α :=
  ⟨ pure (a,1) ⟩

  @[inline] protected def bind [has_mul ω] (x : writer_t ω m α) (f : α → writer_t ω m β) :
    writer_t ω m β :=
  ⟨ do x  ← x.run,
       x' ← (f x.1).run,
       pure (x'.1,x.2 * x'.2) ⟩

  instance [has_one ω] [has_mul ω] : monad (writer_t ω m) :=
  { pure := λ α, writer_t.pure, bind := λ α β, writer_t.bind }

  instance [monoid ω] [is_lawful_monad m] : is_lawful_monad (writer_t ω m) :=
  { id_map := by { intros, cases x, simp [(<$>),writer_t.bind,writer_t.pure] },
    pure_bind := by { intros, simp [has_pure.pure,writer_t.pure,(>>=),writer_t.bind], ext; refl },
    bind_assoc := by { intros, simp [(>>=),writer_t.bind,mul_assoc] with functor_norm } }

  @[inline] protected def lift [has_one ω] (a : m α) : writer_t ω m α :=
  ⟨ flip prod.mk 1 <$> a ⟩

  instance (m) [monad m] [has_one ω] : has_monad_lift m (writer_t ω m) :=
  ⟨ λ α, writer_t.lift  ⟩

  @[inline] protected def monad_map {m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) :
    writer_t ω m α → writer_t ω m' α :=
  λ x, ⟨ f x.run ⟩

  instance (m m') [monad m] [monad m'] : monad_functor m m' (writer_t ω m) (writer_t ω m') :=
  ⟨@writer_t.monad_map ω m m' _ _⟩

  @[inline] protected def adapt {ω' : Type u} {α : Type u} (f : ω → ω') :
    writer_t ω m α → writer_t ω' m α :=
  λ x, ⟨prod.map id f <$> x.run⟩

  instance (ε) [has_one ω] [monad m] [monad_except ε m] : monad_except ε (writer_t ω m) :=
  { throw := λ α, writer_t.lift ∘ throw,
    catch := λ α x c, ⟨catch x.run (λ e, (c e).run)⟩ }
end
end writer_t

/--
An implementation of [MonadReader](
https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader).
It does not contain `local` because this function cannot be lifted using `monad_lift`.
Instead, the `monad_reader_adapter` class provides the more general `adapt_reader` function.

Note: This class can be seen as a simplification of the more "principled" definition
```
class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) :=
(lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
```
-/
class monad_writer (ω : out_param (Type u)) (m : Type u → Type v) :=
(tell (w : ω) : m punit)
(listen {α} : m α → m (α × ω))
(pass {α : Type u} : m (α × (ω → ω)) → m α)

export monad_writer

instance {ω : Type u} {m : Type u → Type v} [monad m] : monad_writer ω (writer_t ω m) :=
{ tell := writer_t.tell,
  listen := λ α, writer_t.listen,
  pass := λ α, writer_t.pass }

instance {ω ρ : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
  monad_writer ω (reader_t ρ m) :=
{ tell := λ x, monad_lift (tell x : m punit),
  listen := λ α ⟨ cmd ⟩, ⟨ λ r, listen (cmd r) ⟩,
  pass := λ α ⟨ cmd ⟩, ⟨ λ r, pass (cmd r) ⟩ }

def swap_right {α β γ} : (α × β) × γ → (α × γ) × β
| ⟨⟨x,y⟩,z⟩ := ((x,z),y)

instance {ω σ : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
  monad_writer ω (state_t σ m) :=
{ tell := λ x, monad_lift (tell x : m punit),
  listen := λ α ⟨ cmd ⟩, ⟨ λ r, swap_right <$> listen (cmd r) ⟩,
  pass := λ α ⟨ cmd ⟩, ⟨ λ r, pass (swap_right <$> cmd r) ⟩ }
open function

def except_t.pass_aux {ε α ω} : except ε (α × (ω → ω)) → except ε α × (ω → ω)
| (except.error a) := (except.error a,id)
| (except.ok (x,y)) := (except.ok x,y)

instance {ω ε : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
  monad_writer ω (except_t ε m) :=
{ tell := λ x, monad_lift (tell x : m punit),
  listen := λ α ⟨ cmd ⟩, ⟨ uncurry (λ x y, flip prod.mk y <$> x) <$> listen cmd ⟩,
  pass := λ α ⟨ cmd ⟩, ⟨ pass (except_t.pass_aux <$> cmd) ⟩ }

def option_t.pass_aux {α ω} : option (α × (ω → ω)) → option α × (ω → ω)
| none := (none ,id)
| (some (x,y)) := (some x,y)

instance {ω : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
  monad_writer ω (option_t m) :=
{ tell := λ x, monad_lift (tell x : m punit),
  listen := λ α ⟨ cmd ⟩, ⟨ uncurry (λ x y, flip prod.mk y <$> x) <$> listen cmd ⟩,
  pass := λ α ⟨ cmd ⟩, ⟨ pass (option_t.pass_aux <$> cmd) ⟩ }

/-- Adapt a monad stack, changing the type of its top-most environment.

This class is comparable to
[Control.Lens.Magnify](https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Magnify),
but does not use lenses (why would it), and is derived automatically for any transformer
implementing `monad_functor`.

Note: This class can be seen as a simplification of the more "principled" definition
```
class monad_reader_functor (ρ ρ' : out_param (Type u)) (n n' : Type u → Type u) :=
(map {α : Type u} :
  (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
```
-/
class monad_writer_adapter (ω ω' : out_param (Type u)) (m m' : Type u → Type v) :=
(adapt_writer {α : Type u} : (ω → ω') → m α → m' α)
export monad_writer_adapter (adapt_writer)

section
variables {ω ω' : Type u} {m m' : Type u → Type v}

/-- Transitivity.

This instance generates the type-class problem with a metavariable argument (which is why this
is marked as `[nolint dangerous_instance]`).
Currently that is not a problem, as there are almost no instances of `monad_functor` or
`monad_writer_adapter`.

see Note [lower instance priority] -/
@[nolint dangerous_instance, priority 100]
instance monad_writer_adapter_trans {n n' : Type u → Type v} [monad_writer_adapter ω ω' m m']
  [monad_functor m m' n n'] : monad_writer_adapter ω ω' n n' :=
⟨λ α f, monad_map (λ α, (adapt_writer f : m α → m' α))⟩

instance [monad m] : monad_writer_adapter ω ω' (writer_t ω m) (writer_t ω' m) :=
⟨λ α, writer_t.adapt⟩
end

instance (ω : Type u) (m out) [monad_run out m] : monad_run (λ α, out (α × ω)) (writer_t ω m) :=
⟨λ α x, run $ x.run ⟩

/-- reduce the equivalence between two writer monads to the equivalence between
their underlying monad -/
def writer_t.equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁}
  {α₁ ω₁ : Type u₀} {α₂ ω₂ : Type u₁} (F : (m₁ (α₁ × ω₁)) ≃ (m₂ (α₂ × ω₂))) :
  writer_t ω₁ m₁ α₁ ≃ writer_t ω₂ m₂ α₂ :=
{ to_fun := λ ⟨f⟩, ⟨F f⟩,
  inv_fun := λ ⟨f⟩, ⟨F.symm f⟩,
  left_inv := λ ⟨f⟩, congr_arg writer_t.mk $ F.left_inv _,
  right_inv := λ ⟨f⟩, congr_arg writer_t.mk $ F.right_inv _ }

author: saisurbehera

repo: mathProof


text:
/-
Copyright (c) 2023 Kevin Buzzard. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author : Kevin Buzzard
-/

import tactic

/-

# Prove that for every positive integer n the number 3(1^5 +2^5 +...+n^5)
# is divisible by 1^3+2^3+...+n^3

This is question 9 in Sierpinski's book

-/

open_locale big_operators

open finset

-- I knew this one
lemma sum_cubes (n : ℕ) : ∑ i in range n, (i : ℚ)^3 = (n*(n-1)/2)^2 :=
begin
  induction n with d hd,
  { simp, },
  { rw [finset.sum_range_succ, hd],
    simp,
    ring }
end

-- I looked this one up on Wikipedia
lemma sum_fifths (n : ℕ) : ∑ i in range n, (i : ℚ)^5 = (4 * (n * (n-1)/2)^3-(n*(n-1)/2)^2)/3 :=
begin
  induction n with d hd,
  { simp, },
  { rw [finset.sum_range_succ, hd],
    simp,
    ring }
end

example (n : ℕ) : (∑ i in range n, i^3) ∣ (3 * ∑ i in range n, i^5) :=
begin
  rw ← int.coe_nat_dvd,
  use 2 * n * (n-1) - 1, -- I used a computer algebra package to work out the ratio
  rw ← @int.cast_inj ℚ _ _ _ _,
  push_cast,
  rw sum_cubes,
  rw sum_fifths,
  ring,
end

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Yury Kudryashov
-/
import algebra.group.type_tags
import algebra.hom.group
import algebra.opposites
import logic.embedding

/-!
# Definitions of group actions

This file defines a hierarchy of group action type-classes on top of the previously defined
notation classes `has_scalar` and its additive version `has_vadd`:

* `mul_action M α` and its additive version `add_action G P` are typeclasses used for
  actions of multiplicative and additive monoids and groups; they extend notation classes
  `has_scalar` and `has_vadd` that are defined in `algebra.group.defs`;
* `distrib_mul_action M A` is a typeclass for an action of a multiplicative monoid on
  an additive monoid such that `a • (b + c) = a • b + a • c` and `a • 0 = 0`.

The hierarchy is extended further by `module`, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the
interaction of different group actions,

* `smul_comm_class M N α` and its additive version `vadd_comm_class M N α`;
* `is_scalar_tower M N α` (no additive version).
* `is_central_scalar M α` (no additive version).

## Notation

- `a • b` is used as notation for `has_scalar.smul a b`.
- `a +ᵥ b` is used as notation for `has_vadd.vadd a b`.

## Implementation details

This file should avoid depending on other parts of `group_theory`, to avoid import cycles.
More sophisticated lemmas belong in `group_theory.group_action`.

## Tags

group action
-/

variables {M N G A B α β γ δ : Type*}

open function (injective surjective)

/-!
### Faithful actions
-/

/-- Typeclass for faithful actions. -/
class has_faithful_vadd (G : Type*) (P : Type*) [has_vadd G P] : Prop :=
(eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ p : P, g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂)

/-- Typeclass for faithful actions. -/
@[to_additive]
class has_faithful_smul (M : Type*) (α : Type*) [has_scalar M α] : Prop :=
(eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ a : α, m₁ • a = m₂ • a) → m₁ = m₂)

export has_faithful_smul (eq_of_smul_eq_smul) has_faithful_vadd (eq_of_vadd_eq_vadd)

@[to_additive]
lemma smul_left_injective' [has_scalar M α] [has_faithful_smul M α] :
  function.injective ((•) : M → α → α) :=
λ m₁ m₂ h, has_faithful_smul.eq_of_smul_eq_smul (congr_fun h)

/-- See also `monoid.to_mul_action` and `mul_zero_class.to_smul_with_zero`. -/
@[priority 910, to_additive] -- see Note [lower instance priority]
instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := ⟨(*)⟩

@[simp, to_additive] lemma smul_eq_mul (α : Type*) [has_mul α] {a a' : α} : a • a' = a * a' := rfl

/-- Type class for additive monoid actions. -/
@[ext, protect_proj] class add_action (G : Type*) (P : Type*) [add_monoid G] extends has_vadd G P :=
(zero_vadd : ∀ p : P, (0 : G) +ᵥ p = p)
(add_vadd : ∀ (g₁ g₂ : G) (p : P), (g₁ + g₂) +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p))

/-- Typeclass for multiplicative actions by monoids. This generalizes group actions. -/
@[ext, protect_proj, to_additive]
class mul_action (α : Type*) (β : Type*) [monoid α] extends has_scalar α β :=
(one_smul : ∀ b : β, (1 : α) • b = b)
(mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)

instance additive.add_action [monoid α] [mul_action α β] : add_action (additive α) β :=
{ vadd := (•) ∘ additive.to_mul,
  zero_vadd := mul_action.one_smul,
  add_vadd := mul_action.mul_smul }

@[simp] lemma additive.of_mul_vadd [monoid α] [mul_action α β] (a : α) (b : β) :
  additive.of_mul a +ᵥ b = a • b :=
rfl

instance multiplicative.mul_action [add_monoid α] [add_action α β] :
  mul_action (multiplicative α) β :=
{ smul := (+ᵥ) ∘ multiplicative.to_add,
  one_smul := add_action.zero_vadd,
  mul_smul := add_action.add_vadd }

@[simp] lemma multiplicative.of_add_smul [add_monoid α] [add_action α β] (a : α) (b : β) :
  multiplicative.of_add a • b = a +ᵥ b :=
rfl

/-!
### (Pre)transitive action

`M` acts pretransitively on `α` if for any `x y` there is `g` such that `g • x = y` (or `g +ᵥ x = y`
for an additive action). A transitive action should furthermore have `α` nonempty.

In this section we define typeclasses `mul_action.is_pretransitive` and
`add_action.is_pretransitive` and provide `mul_action.exists_smul_eq`/`add_action.exists_vadd_eq`,
`mul_action.surjective_smul`/`add_action.surjective_vadd` as public interface to access this
property. We do not provide typeclasses `*_action.is_transitive`; users should assume
`[mul_action.is_pretransitive M α] [nonempty α]` instead. -/

/-- `M` acts pretransitively on `α` if for any `x y` there is `g` such that `g +ᵥ x = y`.
  A transitive action should furthermore have `α` nonempty. -/
class add_action.is_pretransitive (M α : Type*) [has_vadd M α] : Prop :=
(exists_vadd_eq : ∀ x y : α, ∃ g : M, g +ᵥ x = y)

/-- `M` acts pretransitively on `α` if for any `x y` there is `g` such that `g • x = y`.
  A transitive action should furthermore have `α` nonempty. -/
@[to_additive] class mul_action.is_pretransitive (M α : Type*) [has_scalar M α] : Prop :=
(exists_smul_eq : ∀ x y : α, ∃ g : M, g • x = y)

namespace mul_action

variables (M) {α} [has_scalar M α] [is_pretransitive M α]

@[to_additive] lemma exists_smul_eq (x y : α) : ∃ m : M, m • x = y :=
is_pretransitive.exists_smul_eq x y

@[to_additive] lemma surjective_smul (x : α) : surjective (λ c : M, c • x) := exists_smul_eq M x

/-- The regular action of a group on itself is transitive. -/
@[to_additive] instance regular.is_pretransitive [group G] : is_pretransitive G G :=
⟨λ x y, ⟨y * x⁻¹, inv_mul_cancel_right _ _⟩⟩

end mul_action

/-!
### Scalar tower and commuting actions
-/

/-- A typeclass mixin saying that two additive actions on the same space commute. -/
class vadd_comm_class (M N α : Type*) [has_vadd M α] [has_vadd N α] : Prop :=
(vadd_comm : ∀ (m : M) (n : N) (a : α), m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a))

/-- A typeclass mixin saying that two multiplicative actions on the same space commute. -/
@[to_additive] class smul_comm_class (M N α : Type*) [has_scalar M α] [has_scalar N α] : Prop :=
(smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a)

export mul_action (mul_smul) add_action (add_vadd) smul_comm_class (smul_comm)
  vadd_comm_class (vadd_comm)

/--
Frequently, we find ourselves wanting to express a bilinear map `M →ₗ[R] N →ₗ[R] P` or an
equivalence between maps `(M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N')` where the maps have an associated ring
`R`. Unfortunately, using definitions like these requires that `R` satisfy `comm_semiring R`, and
not just `semiring R`. Using `M →ₗ[R] N →+ P` and `(M →ₗ[R] N) ≃+ (M' →ₗ[R] N')` avoids this
problem, but throws away structure that is useful for when we _do_ have a commutative (semi)ring.

To avoid making this compromise, we instead state these definitions as `M →ₗ[R] N →ₗ[S] P` or
`(M →ₗ[R] N) ≃ₗ[S] (M' →ₗ[R] N')` and require `smul_comm_class S R` on the appropriate modules. When
the caller has `comm_semiring R`, they can set `S = R` and `smul_comm_class_self` will populate the
instance. If the caller only has `semiring R` they can still set either `R = ℕ` or `S = ℕ`, and
`add_comm_monoid.nat_smul_comm_class` or `add_comm_monoid.nat_smul_comm_class'` will populate
the typeclass, which is still sufficient to recover a `≃+` or `→+` structure.

An example of where this is used is `linear_map.prod_equiv`.
-/
library_note "bundled maps over different rings"

/-- Commutativity of actions is a symmetric relation. This lemma can't be an instance because this
would cause a loop in the instance search graph. -/
@[to_additive] lemma smul_comm_class.symm (M N α : Type*) [has_scalar M α] [has_scalar N α]
  [smul_comm_class M N α] : smul_comm_class N M α :=
⟨λ a' a b, (smul_comm a a' b).symm⟩

/-- Commutativity of additive actions is a symmetric relation. This lemma can't be an instance
because this would cause a loop in the instance search graph. -/
add_decl_doc vadd_comm_class.symm

@[to_additive] instance smul_comm_class_self (M α : Type*) [comm_monoid M] [mul_action M α] :
  smul_comm_class M M α :=
⟨λ a a' b, by rw [← mul_smul, mul_comm, mul_smul]⟩

/-- An instance of `is_scalar_tower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`. -/
class is_scalar_tower (M N α : Type*) [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop :=
(smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • (y • z))

@[simp] lemma smul_assoc {M N} [has_scalar M N] [has_scalar N α] [has_scalar M α]
  [is_scalar_tower M N α] (x : M) (y : N) (z : α) :
  (x • y) • z = x • y • z :=
is_scalar_tower.smul_assoc x y z

instance semigroup.is_scalar_tower [semigroup α] : is_scalar_tower α α α := ⟨mul_assoc⟩

/-- A typeclass indicating that the right (aka `mul_opposite`) and left actions by `M` on `α` are
equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
for `•`. -/
class is_central_scalar (M α : Type*) [has_scalar M α] [has_scalar Mᵐᵒᵖ α] : Prop :=
(op_smul_eq_smul : ∀ (m : M) (a : α), mul_opposite.op m • a = m • a)

lemma is_central_scalar.unop_smul_eq_smul {M α : Type*} [has_scalar M α] [has_scalar Mᵐᵒᵖ α]
  [is_central_scalar M α] (m : Mᵐᵒᵖ) (a : α) : (mul_opposite.unop m) • a = m • a :=
mul_opposite.rec (by exact λ m, (is_central_scalar.op_smul_eq_smul _ _).symm) m

export is_central_scalar (op_smul_eq_smul unop_smul_eq_smul)

-- these instances are very low priority, as there is usually a faster way to find these instances

@[priority 50]
instance smul_comm_class.op_left [has_scalar M α] [has_scalar Mᵐᵒᵖ α]
  [is_central_scalar M α] [has_scalar N α] [smul_comm_class M N α] : smul_comm_class Mᵐᵒᵖ N α :=
⟨λ m n a, by rw [←unop_smul_eq_smul m (n • a), ←unop_smul_eq_smul m a, smul_comm]⟩

@[priority 50]
instance smul_comm_class.op_right [has_scalar M α] [has_scalar N α] [has_scalar Nᵐᵒᵖ α]
  [is_central_scalar N α] [smul_comm_class M N α] : smul_comm_class M Nᵐᵒᵖ α :=
⟨λ m n a, by rw [←unop_smul_eq_smul n (m • a), ←unop_smul_eq_smul n a, smul_comm]⟩

@[priority 50]
instance is_scalar_tower.op_left
  [has_scalar M α] [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α]
  [has_scalar M N] [has_scalar Mᵐᵒᵖ N] [is_central_scalar M N]
  [has_scalar N α] [is_scalar_tower M N α] : is_scalar_tower Mᵐᵒᵖ N α :=
⟨λ m n a, by rw [←unop_smul_eq_smul m (n • a), ←unop_smul_eq_smul m n, smul_assoc]⟩

@[priority 50]
instance is_scalar_tower.op_right [has_scalar M α] [has_scalar M N]
  [has_scalar N α] [has_scalar Nᵐᵒᵖ α] [is_central_scalar N α]
  [is_scalar_tower M N α] : is_scalar_tower M Nᵐᵒᵖ α :=
⟨λ m n a, by rw [←unop_smul_eq_smul n a, ←unop_smul_eq_smul (m • n) a, mul_opposite.unop_smul,
                 smul_assoc]⟩

namespace has_scalar
variables [has_scalar M α]

/-- Auxiliary definition for `has_scalar.comp`, `mul_action.comp_hom`,
`distrib_mul_action.comp_hom`, `module.comp_hom`, etc. -/
@[simp, to_additive  /-" Auxiliary definition for `has_vadd.comp`, `add_action.comp_hom`, etc. "-/]
def comp.smul (g : N → M) (n : N) (a : α) : α :=
g n • a

variables (α)

/-- An action of `M` on `α` and a function `N → M` induces an action of `N` on `α`.

See note [reducible non-instances]. Since this is reducible, we make sure to go via
`has_scalar.comp.smul` to prevent typeclass inference unfolding too far. -/
@[reducible, to_additive /-" An additive action of `M` on `α` and a function `N → M` induces
  an additive action of `N` on `α` "-/]
def comp (g : N → M) : has_scalar N α :=
{ smul := has_scalar.comp.smul g }

variables {α}

/-- Given a tower of scalar actions `M → α → β`, if we use `has_scalar.comp`
to pull back both of `M`'s actions by a map `g : N → M`, then we obtain a new
tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `has_scalar` arguments
are still metavariables.
-/
@[priority 100]
lemma comp.is_scalar_tower [has_scalar M β] [has_scalar α β] [is_scalar_tower M α β]
  (g : N → M) :
  (by haveI := comp α g; haveI := comp β g; exact is_scalar_tower N α β) :=
by exact {smul_assoc := λ n, @smul_assoc _ _ _ _ _ _ _ (g n) }

/--
This cannot be an instance because it can cause infinite loops whenever the `has_scalar` arguments
are still metavariables.
-/
@[priority 100]
lemma comp.smul_comm_class [has_scalar β α] [smul_comm_class M β α] (g : N → M) :
  (by haveI := comp α g; exact smul_comm_class N β α) :=
by exact {smul_comm := λ n, @smul_comm _ _ _ _ _ _ (g n) }

/--
This cannot be an instance because it can cause infinite loops whenever the `has_scalar` arguments
are still metavariables.
-/
@[priority 100]
lemma comp.smul_comm_class' [has_scalar β α] [smul_comm_class β M α] (g : N → M) :
  (by haveI := comp α g; exact smul_comm_class β N α) :=
by exact {smul_comm := λ _ n, @smul_comm _ _ _ _ _ _ _ (g n) }

end has_scalar

section

/-- Note that the `smul_comm_class α β β` typeclass argument is usually satisfied by `algebra α β`.
-/
@[to_additive]
lemma mul_smul_comm [has_mul β] [has_scalar α β] [smul_comm_class α β β] (s : α) (x y : β) :
  x * (s • y) = s • (x * y) :=
(smul_comm s x y).symm

/-- Note that the `is_scalar_tower α β β` typeclass argument is usually satisfied by `algebra α β`.
-/
lemma smul_mul_assoc [has_mul β] [has_scalar α β] [is_scalar_tower α β β] (r : α) (x y : β)  :
  (r • x) * y = r • (x * y) :=
smul_assoc r x y

lemma smul_smul_smul_comm [has_scalar α β] [has_scalar α γ] [has_scalar β δ] [has_scalar α δ]
  [has_scalar γ δ] [is_scalar_tower α β δ] [is_scalar_tower α γ δ] [smul_comm_class β γ δ]
  (a : α) (b : β) (c : γ) (d : δ) : (a • b) • (c • d) = (a • c) • b • d :=
by { rw [smul_assoc, smul_assoc, smul_comm b], apply_instance }

variables [has_scalar M α]

lemma commute.smul_right [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
  {a b : α} (h : commute a b) (r : M) :
  commute a (r • b) :=
(mul_smul_comm _ _ _).trans ((congr_arg _ h).trans $ (smul_mul_assoc _ _ _).symm)

lemma commute.smul_left [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
  {a b : α} (h : commute a b) (r : M) :
  commute (r • a) b :=
(h.symm.smul_right r).symm

end

section ite
variables [has_scalar M α] (p : Prop) [decidable p]

@[to_additive] lemma ite_smul (a₁ a₂ : M) (b : α) : (ite p a₁ a₂) • b = ite p (a₁ • b) (a₂ • b) :=
by split_ifs; refl

@[to_additive] lemma smul_ite (a : M) (b₁ b₂ : α) : a • (ite p b₁ b₂) = ite p (a • b₁) (a • b₂) :=
by split_ifs; refl

end ite

section
variables [monoid M] [mul_action M α]

@[to_additive] lemma smul_smul (a₁ a₂ : M) (b : α) : a₁ • a₂ • b = (a₁ * a₂) • b :=
(mul_smul _ _ _).symm

variable (M)
@[simp, to_additive] theorem one_smul (b : α) : (1 : M) • b = b := mul_action.one_smul _

/-- `has_scalar` version of `one_mul_eq_id` -/
@[to_additive]
lemma one_smul_eq_id : ((•) (1 : M) : α → α) = id := funext $ one_smul _

/-- `has_scalar` version of `comp_mul_left` -/
@[to_additive]
lemma comp_smul_left (a₁ a₂ : M) : (•) a₁ ∘ (•) a₂ = ((•) (a₁ * a₂) : α → α) :=
funext $ λ _, (mul_smul _ _ _).symm

variables {M}

/-- Pullback a multiplicative action along an injective map respecting `•`.
See note [reducible non-instances]. -/
@[reducible, to_additive "Pullback an additive action along an injective map respecting `+ᵥ`."]
protected def function.injective.mul_action [has_scalar M β] (f : β → α)
  (hf : injective f) (smul : ∀ (c : M) x, f (c • x) = c • f x) :
  mul_action M β :=
{ smul := (•),
  one_smul := λ x, hf $ (smul _ _).trans $ one_smul _ (f x),
  mul_smul := λ c₁ c₂ x, hf $ by simp only [smul, mul_smul] }

/-- Pushforward a multiplicative action along a surjective map respecting `•`.
See note [reducible non-instances]. -/
@[reducible, to_additive "Pushforward an additive action along a surjective map respecting `+ᵥ`."]
protected def function.surjective.mul_action [has_scalar M β] (f : α → β) (hf : surjective f)
  (smul : ∀ (c : M) x, f (c • x) = c • f x) :
  mul_action M β :=
{ smul := (•),
  one_smul := λ y, by { rcases hf y with ⟨x, rfl⟩, rw [← smul, one_smul] },
  mul_smul := λ c₁ c₂ y, by { rcases hf y with ⟨x, rfl⟩, simp only [← smul, mul_smul] } }

/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.

See also `function.surjective.distrib_mul_action_left` and `function.surjective.module_left`.
-/
@[reducible, to_additive "Push forward the action of `R` on `M` along a compatible
surjective map `f : R →+ S`."]
def function.surjective.mul_action_left {R S M : Type*} [monoid R] [mul_action R M]
  [monoid S] [has_scalar S M]
  (f : R →* S) (hf : function.surjective f) (hsmul : ∀ c (x : M), f c • x = c • x) :
  mul_action S M :=
{ smul := (•),
  one_smul := λ b, by rw [← f.map_one, hsmul, one_smul],
  mul_smul := hf.forall₂.mpr $ λ a b x, by simp only [← f.map_mul, hsmul, mul_smul] }

section

variables (M)

/-- The regular action of a monoid on itself by left multiplication.

This is promoted to a module by `semiring.to_module`. -/
@[priority 910, to_additive] -- see Note [lower instance priority]
instance monoid.to_mul_action : mul_action M M :=
{ smul := (*),
  one_smul := one_mul,
  mul_smul := mul_assoc }

/-- The regular action of a monoid on itself by left addition.

This is promoted to an `add_torsor` by `add_group_is_add_torsor`. -/
add_decl_doc add_monoid.to_add_action

instance is_scalar_tower.left : is_scalar_tower M M α :=
⟨λ x y z, mul_smul x y z⟩

variables {M}

/-- Note that the `is_scalar_tower M α α` and `smul_comm_class M α α` typeclass arguments are
usually satisfied by `algebra M α`. -/
lemma smul_mul_smul [has_mul α] (r s : M) (x y : α)
  [is_scalar_tower M α α] [smul_comm_class M α α] :
  (r • x) * (s • y) = (r * s) • (x * y) :=
by rw [smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]

end

namespace mul_action

variables (M α)

/-- Embedding of `α` into functions `M → α` induced by a multiplicative action of `M` on `α`. -/
@[to_additive] def to_fun : α ↪ (M → α) :=
⟨λ y x, x • y, λ y₁ y₂ H, one_smul M y₁ ▸ one_smul M y₂ ▸ by convert congr_fun H 1⟩

/-- Embedding of `α` into functions `M → α` induced by an additive action of `M` on `α`. -/
add_decl_doc add_action.to_fun

variables {M α}

@[simp, to_additive] lemma to_fun_apply (x : M) (y : α) : mul_action.to_fun M α y x = x • y :=
rfl

variable (α)

/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
a multiplicative action of `N` on `α`.

See note [reducible non-instances]. -/
@[reducible, to_additive] def comp_hom [monoid N] (g : N →* M) :
  mul_action N α :=
{ smul := has_scalar.comp.smul g,
  one_smul := by simp [g.map_one, mul_action.one_smul],
  mul_smul := by simp [g.map_mul, mul_action.mul_smul] }

/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
an additive action of `N` on `α`.

See note [reducible non-instances]. -/
add_decl_doc add_action.comp_hom

end mul_action

end

section compatible_scalar

@[simp] lemma smul_one_smul {M} (N) [monoid N] [has_scalar M N] [mul_action N α] [has_scalar M α]
  [is_scalar_tower M N α] (x : M) (y : α) :
  (x • (1 : N)) • y = x • y :=
by rw [smul_assoc, one_smul]

@[simp] lemma smul_one_mul {M N} [monoid N] [has_scalar M N] [is_scalar_tower M N N] (x : M)
  (y : N) : (x • 1) * y = x • y :=
smul_one_smul N x y

@[simp, to_additive] lemma mul_smul_one
  {M N} [mul_one_class N] [has_scalar M N] [smul_comm_class M N N] (x : M) (y : N) :
  y * (x • 1) = x • y :=
by rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]

lemma is_scalar_tower.of_smul_one_mul {M N} [monoid N] [has_scalar M N]
  (h : ∀ (x : M) (y : N), (x • (1 : N)) * y = x • y) :
  is_scalar_tower M N N :=
⟨λ x y z, by rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]⟩

@[to_additive] lemma smul_comm_class.of_mul_smul_one {M N} [monoid N] [has_scalar M N]
  (H : ∀ (x : M) (y : N), y * (x • (1 : N)) = x • y) : smul_comm_class M N N :=
⟨λ x y z, by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩

end compatible_scalar

/-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
@[ext] class distrib_mul_action (M : Type*) (A : Type*) [monoid M] [add_monoid A]
  extends mul_action M A :=
(smul_add : ∀(r : M) (x y : A), r • (x + y) = r • x + r • y)
(smul_zero : ∀(r : M), r • (0 : A) = 0)

section
variables [monoid M] [add_monoid A] [distrib_mul_action M A]

theorem smul_add (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
distrib_mul_action.smul_add _ _ _

@[simp] theorem smul_zero (a : M) : a • (0 : A) = 0 :=
distrib_mul_action.smul_zero _

/-- Pullback a distributive multiplicative action along an injective additive monoid
homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def function.injective.distrib_mul_action [add_monoid B] [has_scalar M B] (f : B →+ A)
  (hf : injective f) (smul : ∀ (c : M) x, f (c • x) = c • f x) :
  distrib_mul_action M B :=
{ smul := (•),
  smul_add := λ c x y, hf $ by simp only [smul, f.map_add, smul_add],
  smul_zero := λ c, hf $ by simp only [smul, f.map_zero, smul_zero],
  .. hf.mul_action f smul }

/-- Pushforward a distributive multiplicative action along a surjective additive monoid
homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def function.surjective.distrib_mul_action [add_monoid B] [has_scalar M B] (f : A →+ B)
  (hf : surjective f) (smul : ∀ (c : M) x, f (c • x) = c • f x) :
  distrib_mul_action M B :=
{ smul := (•),
  smul_add := λ c x y, by { rcases hf x with ⟨x, rfl⟩, rcases hf y with ⟨y, rfl⟩,
    simp only [smul_add, ← smul, ← f.map_add] },
  smul_zero := λ c, by simp only [← f.map_zero, ← smul, smul_zero],
  .. hf.mul_action f smul }

/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.

See also `function.surjective.mul_action_left` and `function.surjective.module_left`.
-/
@[reducible]
def function.surjective.distrib_mul_action_left {R S M : Type*} [monoid R] [add_monoid M]
  [distrib_mul_action R M] [monoid S] [has_scalar S M]
  (f : R →* S) (hf : function.surjective f) (hsmul : ∀ c (x : M), f c • x = c • x) :
  distrib_mul_action S M :=
{ smul := (•),
  smul_zero := hf.forall.mpr $ λ c, by rw [hsmul, smul_zero],
  smul_add := hf.forall.mpr $ λ c x y, by simp only [hsmul, smul_add],
  .. hf.mul_action_left f hsmul }

variable (A)

/-- Compose a `distrib_mul_action` with a `monoid_hom`, with action `f r' • m`.
See note [reducible non-instances]. -/
@[reducible] def distrib_mul_action.comp_hom [monoid N] (f : N →* M) :
  distrib_mul_action N A :=
{ smul := has_scalar.comp.smul f,
  smul_zero := λ x, smul_zero (f x),
  smul_add := λ x, smul_add (f x),
  .. mul_action.comp_hom A f }

/-- Each element of the monoid defines a additive monoid homomorphism. -/
@[simps]
def distrib_mul_action.to_add_monoid_hom (x : M) : A →+ A :=
{ to_fun := (•) x,
  map_zero' := smul_zero x,
  map_add' := smul_add x }

variables (M)

/-- Each element of the monoid defines an additive monoid homomorphism. -/
@[simps]
def distrib_mul_action.to_add_monoid_End : M →* add_monoid.End A :=
{ to_fun := distrib_mul_action.to_add_monoid_hom A,
  map_one' := add_monoid_hom.ext $ one_smul M,
  map_mul' := λ x y, add_monoid_hom.ext $ mul_smul x y }

instance add_monoid.nat_smul_comm_class : smul_comm_class ℕ M A :=
{ smul_comm := λ n x y, ((distrib_mul_action.to_add_monoid_hom A x).map_nsmul y n).symm }

-- `smul_comm_class.symm` is not registered as an instance, as it would cause a loop
instance add_monoid.nat_smul_comm_class' : smul_comm_class M ℕ A :=
smul_comm_class.symm _ _ _

end

section
variables [monoid M] [add_group A] [distrib_mul_action M A]

instance add_group.int_smul_comm_class : smul_comm_class ℤ M A :=
{ smul_comm := λ n x y, ((distrib_mul_action.to_add_monoid_hom A x).map_zsmul y n).symm }

-- `smul_comm_class.symm` is not registered as an instance, as it would cause a loop
instance add_group.int_smul_comm_class' : smul_comm_class M ℤ A :=
smul_comm_class.symm _ _ _

@[simp] theorem smul_neg (r : M) (x : A) : r • (-x) = -(r • x) :=
eq_neg_of_add_eq_zero_left $ by rw [← smul_add, neg_add_self, smul_zero]

theorem smul_sub (r : M) (x y : A) : r • (x - y) = r • x - r • y :=
by rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]

end

/-- Typeclass for multiplicative actions on multiplicative structures. This generalizes
conjugation actions. -/
@[ext] class mul_distrib_mul_action (M : Type*) (A : Type*) [monoid M] [monoid A]
  extends mul_action M A :=
(smul_mul : ∀ (r : M) (x y : A), r • (x * y) = (r • x) * (r • y))
(smul_one : ∀ (r : M), r • (1 : A) = 1)

export mul_distrib_mul_action (smul_one)

section
variables [monoid M] [monoid A] [mul_distrib_mul_action M A]

theorem smul_mul' (a : M) (b₁ b₂ : A) : a • (b₁ * b₂) = (a • b₁) * (a • b₂) :=
mul_distrib_mul_action.smul_mul _ _ _

/-- Pullback a multiplicative distributive multiplicative action along an injective monoid
homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def function.injective.mul_distrib_mul_action [monoid B] [has_scalar M B] (f : B →* A)
  (hf : injective f) (smul : ∀ (c : M) x, f (c • x) = c • f x) :
  mul_distrib_mul_action M B :=
{ smul := (•),
  smul_mul := λ c x y, hf $ by simp only [smul, f.map_mul, smul_mul'],
  smul_one := λ c, hf $ by simp only [smul, f.map_one, smul_one],
  .. hf.mul_action f smul }

/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def function.surjective.mul_distrib_mul_action [monoid B] [has_scalar M B] (f : A →* B)
  (hf : surjective f) (smul : ∀ (c : M) x, f (c • x) = c • f x) :
  mul_distrib_mul_action M B :=
{ smul := (•),
  smul_mul := λ c x y, by { rcases hf x with ⟨x, rfl⟩, rcases hf y with ⟨y, rfl⟩,
    simp only [smul_mul', ← smul, ← f.map_mul] },
  smul_one := λ c, by simp only [← f.map_one, ← smul, smul_one],
  .. hf.mul_action f smul }

variable (A)

/-- Compose a `mul_distrib_mul_action` with a `monoid_hom`, with action `f r' • m`.
See note [reducible non-instances]. -/
@[reducible] def mul_distrib_mul_action.comp_hom [monoid N] (f : N →* M) :
  mul_distrib_mul_action N A :=
{ smul := has_scalar.comp.smul f,
  smul_one := λ x, smul_one (f x),
  smul_mul := λ x, smul_mul' (f x),
  .. mul_action.comp_hom A f }

/-- Scalar multiplication by `r` as a `monoid_hom`. -/
def mul_distrib_mul_action.to_monoid_hom (r : M) : A →* A :=
{ to_fun := (•) r,
  map_one' := smul_one r,
  map_mul' := smul_mul' r }

variable {A}

@[simp] lemma mul_distrib_mul_action.to_monoid_hom_apply (r : M) (x : A) :
  mul_distrib_mul_action.to_monoid_hom A r x = r • x := rfl

variables (M A)

/-- Each element of the monoid defines a monoid homomorphism. -/
@[simps]
def mul_distrib_mul_action.to_monoid_End : M →* monoid.End A :=
{ to_fun := mul_distrib_mul_action.to_monoid_hom A,
  map_one' := monoid_hom.ext $ one_smul M,
  map_mul' := λ x y, monoid_hom.ext $ mul_smul x y }

end

section
variables [monoid M] [group A] [mul_distrib_mul_action M A]

@[simp] theorem smul_inv' (r : M) (x : A) : r • (x⁻¹) = (r • x)⁻¹ :=
(mul_distrib_mul_action.to_monoid_hom A r).map_inv x

theorem smul_div' (r : M) (x y : A) : r • (x / y) = (r • x) / (r • y) :=
(mul_distrib_mul_action.to_monoid_hom A r).map_div x y

end

variable (α)

/-- The monoid of endomorphisms.

Note that this is generalized by `category_theory.End` to categories other than `Type u`. -/
protected def function.End := α → α

instance : monoid (function.End α) :=
{ one := id,
  mul := (∘),
  mul_assoc := λ f g h, rfl,
  mul_one := λ f, rfl,
  one_mul := λ f, rfl, }

instance : inhabited (function.End α) := ⟨1⟩

variable {α}

/-- The tautological action by `function.End α` on `α`.

This is generalized to bundled endomorphisms by:
* `equiv.perm.apply_mul_action`
* `add_monoid.End.apply_distrib_mul_action`
* `add_aut.apply_distrib_mul_action`
* `mul_aut.apply_mul_distrib_mul_action`
* `ring_hom.apply_distrib_mul_action`
* `linear_equiv.apply_distrib_mul_action`
* `linear_map.apply_module`
* `ring_hom.apply_mul_semiring_action`
* `alg_equiv.apply_mul_semiring_action`
-/
instance function.End.apply_mul_action : mul_action (function.End α) α :=
{ smul := ($),
  one_smul := λ _, rfl,
  mul_smul := λ _ _ _, rfl }

@[simp] lemma function.End.smul_def (f : function.End α) (a : α) : f • a = f a := rfl

/-- `function.End.apply_mul_action` is faithful. -/
instance function.End.apply_has_faithful_smul : has_faithful_smul (function.End α) α :=
⟨λ x y, funext⟩

/-- The tautological action by `add_monoid.End α` on `α`.

This generalizes `function.End.apply_mul_action`. -/
instance add_monoid.End.apply_distrib_mul_action [add_monoid α] :
  distrib_mul_action (add_monoid.End α) α :=
{ smul := ($),
  smul_zero := add_monoid_hom.map_zero,
  smul_add := add_monoid_hom.map_add,
  one_smul := λ _, rfl,
  mul_smul := λ _ _ _, rfl }

@[simp] lemma add_monoid.End.smul_def [add_monoid α] (f : add_monoid.End α) (a : α) :
  f • a = f a := rfl

/-- `add_monoid.End.apply_distrib_mul_action` is faithful. -/
instance add_monoid.End.apply_has_faithful_smul [add_monoid α] :
  has_faithful_smul (add_monoid.End α) α :=
⟨add_monoid_hom.ext⟩

/-- The monoid hom representing a monoid action.

When `M` is a group, see `mul_action.to_perm_hom`. -/
def mul_action.to_End_hom [monoid M] [mul_action M α] : M →* function.End α :=
{ to_fun := (•),
  map_one' := funext (one_smul M),
  map_mul' := λ x y, funext (mul_smul x y) }

/-- The monoid action induced by a monoid hom to `function.End α`

See note [reducible non-instances]. -/
@[reducible]
def mul_action.of_End_hom [monoid M] (f : M →* function.End α) : mul_action M α :=
mul_action.comp_hom α f

/-- The tautological additive action by `additive (function.End α)` on `α`. -/
instance add_action.function_End : add_action (additive (function.End α)) α :=
{ vadd := ($),
  zero_vadd := λ _, rfl,
  add_vadd := λ _ _ _, rfl }

/-- The additive monoid hom representing an additive monoid action.

When `M` is a group, see `add_action.to_perm_hom`. -/
def add_action.to_End_hom [add_monoid M] [add_action M α] : M →+ additive (function.End α) :=
{ to_fun := (+ᵥ),
  map_zero' := funext (zero_vadd M),
  map_add' := λ x y, funext (add_vadd x y) }

/-- The additive action induced by a hom to `additive (function.End α)`

See note [reducible non-instances]. -/
@[reducible]
def add_action.of_End_hom [add_monoid M] (f : M →+ additive (function.End α)) : add_action M α :=
add_action.comp_hom α f

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools


/-
There are two key things we do with proofs.

(1) We build them
(2) We use them

In logic, the basic rules for building,
or constructing, proofs go by the name
of introduction rules. The basic rules
for using proofs are called elimination
rules.

Each *form* of proposition has its own
introduction and elimination rules. For
example, to build a proof of P ∧ Q, one
must use the introduction rule for and,
while using a proof of P ∧ Q relies on
the two elimination rules, which serve
to extract from a proof of P ∧ Q a proof
of P or a proof of Q.

In this class, we assume (P Q : Prop),
(T : Type), (x y : T) then summarize,
review,  and practice using the rules
to build and use proofs of these forms:

- ∀ (p : P), Q [Q usually a predicate] -- intro rule for all - for all; Q - what form of prop and continue

- x = y -- intro rule : eq.refl
- P → Q
- P ∧ Q -- and.intro
- ∃ (x : P), Q  [Q usually a predicate]

A key to understanding how to build
proofs is that it's a top-down and
recursive process. For example, to
build a proof of ∀ (p : P), Q, we
use the introduction rule for ∀. It
tells us to assume that p is some
arbitrary but specific value of type
P, and then to prove Q for that p.
To do this, we recursively apply
our approach to building proofs to
build a proof of Q, but now within
a context in which we can use the
assumption that p is some specific
value of type P. We now repeat the
same process: (1) ask what form is
Q; (2) choose an introduction rule
for that form of proposition. Often
we need smaller proofs to apply the
introduction rules, and for this, we
use proofs we have already built or
assumed, using elimination rules as
necessary.
-/

/-
FORALL INTRODUCTION

Assume that you have an arbitrary but specified valu of the quantiied type, ( p: P), then prove Q.

#0: Formalize Proposition
∀ (b:Ball), Green b

#1: We start by assuming that b0 is an arbitrary but specific ball, and now all that remains to be proved is Green b (that this b in particular) is Green.

Formally: Green b. Remaining goal.

∀ (n:nat), n=n

Example: prove ∀ (n:nat), n=n.

#0 Assume that you have an arbitrary but specified valu of the quantiied type, (n:nat), then prove n=n.
#1 Use the introduction rule for equality
#2: Need a proof of n

Proof: We begin by supposing that n0 is an arbitrary but specific natural number.  What remains to be proved in the context is that n0 = n0. [∀ intro]. To prove that n0 =n0 is trivial by the axiom that tells us that the equality relation id reflexive. Thus we have proved the propostion. [By reflexive property of equality.]
-/

theorem foo : ∀ (n:nat), n=n :=
_

theorem all_n_eq_n : ∀ (n:nat), n=n :=
    λ (n0 : nat), eq.refl n0
example : nat := 5

example : ∀ (n: nat) , nat.pred(nat.succ n) = n :=
λ (n0:nat),
    eq.refl (nat.pred(nat.succ n0))

/-
FORALL ELIMINATION

-/

/-
Example:

Prove that is every ball is green, then a specific ball, b0, is green.

(∀ (b:Ball, Green b)) → ((b0: Ball) → (Green b0))

See below. Elim rule for fall is based that we can apply a proof of a forall to a specific value to build
-/

/-
IMPLICATIONS
INTRO FOR →
Asume that we have a proof of the premise.

Example : Prove
(∀ (b:Ball, Green b)) → ((b0: Ball) → (Green b0))

Introduction rule: assume the preduction is true

Begin by assuming every ball is green, Must see nowwhether or not b0 is ball and is b0 is green.

To prove this, we assume b0 is specific and inthis context all that remains to be proved is: b0 is green. this is proved by use of forall elimination. We apply our assumed* proof of (∀ (b:Ball, Green b)) → ((b0: Ball) → (Green b0)) to b) to obtain that b0 is green

-/
axioms (Ball: Type) (Green : Ball → Prop)

example : (∀ (b:Ball), Green b) →  ∀ (b0: Ball), Green  b0 :=
λ h,
    λ a,
        (h a)

/-
Assume that we have a proof, h, that every ball is green. In this context what remains to be proved is that any particular ball is green.

So now we assume that b0 is some arbitrary but specific ball, and inthis extend context of assumptions all that remains to be proved is that b0 is green.

But we already have a proof that every bal is green so all we need to is apply it to b0 and that gives a proof that b0 is green.

-/

/-

Build a syntax and evaluator for a language

Translate between props logic, predicate logic proofs etc. (Nobody likes anybody etc. )

Understand intro and elim rules for above props.
-/


text:
import category_theory.limits.shapes.finite_limits
import category_theory.closed.cartesian
import category_theory.closed.types
import category_theory.limits.shapes.functor_category
import category_theory.limits.functor_category
import category_theory.limits.types
import category_theory.functor
import category_theory.sites.sieves

import topos
import subobject_classifier
import pullbacks

open category_theory category_theory.category category_theory.limits classifier functor

universes v u

noncomputable theory

variables {C : Type u} [category.{u} C] [small_category C]

local notation `°`:std.prec.max_plus C := Cᵒᵖ ⥤ Type u
local notation `₸` := ⊤_ (°C)

namespace presheaf

/- We show that any presheaf over a small category has a suboject classifier
   This is done elementarily, wihtout any appeal to Yoneda, and we work with sieves

  Ω in a presheaf topos is defined to be Ω_c = all the sieves on c -/

-- First are some results about limits in °C

-- Some basics types in Type u to work with --
def uUnit : Type u := ulift unit
def uStar : uUnit := ulift.up unit.star

def uBool : Type u := ulift bool
def fuBool (x y : ⊤_ (Type u)) (b : uBool) : ⊤_ (Type u) :=
match b.down with
| tt := x
| ff := y
end

namespace terminal
/- Let us prove that the terminimport tactic.simp_rwal object in Type u is iso the one element type -/

lemma type_subsingleton (b a : ⊤_ (Type u)) : a = b :=
begin
  have h : (fuBool a b : uBool ⟶ ⊤_ (Type u)) = (fuBool b a : uBool ⟶ ⊤_ (Type u)) := by
    rw [←is_terminal.hom_ext terminal_is_terminal (terminal.from uBool) (fuBool b a),
        ←is_terminal.hom_ext terminal_is_terminal (terminal.from uBool) (fuBool a b)],
  exact congr_fun h (ulift.up tt),
end

instance type_unique : unique (⊤_ (Type u)) :=
{ default := (terminal.from uUnit : uUnit → (⊤_ (Type u))) uStar,
  uniq := type_subsingleton _ }

/- Explicit construction of a terminal presheaf, named T -/
def T : °C := (category_theory.functor.const (Cᵒᵖ)).obj (⊤_ (Type u))

lemma T_proj (c : Cᵒᵖ) : T.obj c = ⊤_ (Type u) := by refl
instance T_unique (c : Cᵒᵖ) : unique (T.obj c) := by rw T_proj; apply_instance

def T_from (X : °C) : X ⟶ T := { app := λ _ _, default }

instance T_hom_unique (X : °C) : unique (X ⟶ T) :=
{ default := T_from X,
  uniq :=
  begin
    intro, apply nat_trans.ext,
    funext, simp
  end }

lemma T_is_terminal : is_terminal (@T C _ _) := is_terminal.of_unique _
lemma T_iso : T ≅ ₸ := is_terminal.unique_up_to_iso T_is_terminal terminal_is_terminal

/- A (maybe) useful lemma, telling that we can transfer unicity along iso -/
lemma unique_iso {X Y : °C} (f : X ≅ Y) (c : Cᵒᵖ) : unique (X.obj c) → unique (Y.obj c) :=
begin
  intro h, resetI,
  refine { default := (iso.app f c).hom default, uniq := _},
  intro a,
  apply ((is_iso_iff_bijective (iso.app f c).inv).elim_left _).left,
  { simp },
  { resetI, apply_instance }
end

/- Now, we show that the terminal presheaf has object the one element type -/
instance unique_obj (c : Cᵒᵖ) : unique (₸.obj c) := unique_iso T_iso c (terminal.T_unique c)

-- weirdly, this is needed, because we cannot write directly (terminal.from X).app, I don't know why
abbreviation tfrom (X : °C) : X ⟶ ⊤_ °C:= terminal.from X

@[simp] lemma terminal_app (X : °C) (c : Cᵒᵖ) (x : X.obj c) : ((tfrom X).app c) x = default := by dec_trivial

-- Pick the object
def tto_app (X : °C) (c : Cᵒᵖ) (x : X.obj c) : ₸.obj c ⟶ X.obj c := λ _, x

-- def tto (X : °C) (α : Π c : Cᵒᵖ, X.obj c) : ₸ ⟶ X :=
-- { app := λ c, tto_app X c (α c),
--   naturality' := begin
--   intros c d f, ext x, unfold tto_app, simp,
--   end }
end terminal

namespace initial
-- We show that the initial presheaf is the empty type at each level
lemma pempty_obj_iso (c : Cᵒᵖ) : (⊥_ °C).obj c ≅ pempty :=
begin
  apply iso.trans _ (limits.types.initial_iso),
  have to_init := initial.to ((category_theory.functor.const Cᵒᵖ).obj (⊥_ Type u)),
  have h := strict_initial initial_is_initial (to_init.app c),
  resetI,
  apply as_iso (to_init.app c),
end

end initial
namespace pullback
/-
  Here we show that pullbacks are computed pointwise in °C, so we have
  a cartesian square of natural transformation iff for each c : Cᵒᵖ the
  "applied" square is a pullback.
  As a consequence a natural transormation is mono iff each component are mono

  Notation :
           Y
           |
           t
           |
  X --s--> Z
  We show that we have an isomorphism of pullback cones, between the applied pullback cone in c
  and the canonical pullback cone from s_c and t_c.

  We constuct an explicit cone isomorphim between the pullback cone of s_c and t_c
  and the (pullback cone of s and t)_c
-/

variables {X Y Z : °C} (s : X ⟶ Z) (t : Y ⟶ Z) (c : Cᵒᵖ)

lemma app_cone_of_cone_comm {s : X ⟶ Z} {t : Y ⟶ Z} (w : pullback_cone s t) (c : Cᵒᵖ) :
  w.fst.app c ≫ s.app c = w.snd.app c ≫ t.app c :=
begin
  rw [←nat_trans.vcomp_app, ←nat_trans.vcomp_app, nat_trans.vcomp_eq_comp,
      pullback_cone.condition w],
  refl
end

def app_cone_of_cone {s : X ⟶ Z} {t : Y ⟶ Z} (w : pullback_cone s t) (c : Cᵒᵖ) :=
  pullback_cone.mk (w.fst.app c) (w.snd.app c) (app_cone_of_cone_comm w c)

abbreviation pullback_fst_app : (pullback s t).obj c ⟶ X.obj c :=
(pullback.fst : pullback s t ⟶ X).app c
abbreviation pullback_snd_app : (pullback s t).obj c ⟶ Y.obj c :=
(pullback.snd : pullback s t ⟶ Y).app c

def app_cone : pullback_cone (s.app c) (t.app c) :=
app_cone_of_cone (pullback_cone.mk pullback.fst pullback.snd pullback.condition) c
  -- pullback_cone.mk (pullback_fst_app s t c) (pullback_snd_app s t c) (app_comm s t c)

@[simp] lemma eval_obj_eq_simp (x : walking_cospan) :
  (cospan (s.app c) (t.app c)).obj x = (cospan s t ⋙ (evaluation Cᵒᵖ (Type u)).obj c).obj x :=
begin
  cases x; simp, cases x; simp,
end

@[simp] lemma eval_obj_eq_simp' (x : walking_cospan) :
  (cospan (s.app c) (t.app c)).obj x = ((cospan s t).obj x).obj c := by simp

@[simp] lemma eval_map_eq_simp (x y : walking_cospan) (f : x ⟶ y) :
  (cospan (s.app c) (t.app c)).map f =
  (eq_to_hom (eval_obj_eq_simp' _ _ _ x)) ≫ ((cospan s t).map f).app c ≫
    (eq_to_hom (eval_obj_eq_simp' _ _ _ y).symm) :=
begin
  cases f, cases x, refl, cases x; refl,
  cases f_1; refl,
end

@[simp] lemma cospan_evaluation :
  cospan s t ⋙ (evaluation Cᵒᵖ (Type u)).obj c = cospan (s.app c) (t.app c) :=
begin
  symmetry,
  apply category_theory.functor.ext,
  swap,
  { simp, },
  { intros x y f, rw eval_map_eq_simp, refl }
end

lemma coerce_pullback_limit_evaluation :
  limit (cospan s t ⋙ (evaluation Cᵒᵖ (Type u)).obj c) = pullback (s.app c) (t.app c) :=
by simp only [cospan_evaluation]

-- The cone isomorphism we use to show pullback are computed pointwise
def iso_app_cone_X := (limit_obj_iso_limit_comp_evaluation (cospan s t) c) ≪≫
                eq_to_iso (coerce_pullback_limit_evaluation s t c)

lemma iso_fst_comm : pullback_fst_app s t c =
  (iso_app_cone_X s t c).hom ≫ (pullback.fst : pullback (s.app c) (t.app c) ⟶ X.obj c) :=
begin
  unfold iso_app_cone_X, simp,
  dunfold pullback_fst_app, symmetry,
  convert limit_obj_iso_limit_comp_evaluation_hom_π (cospan s t) walking_cospan.left c,
  dunfold pullback.fst,
  rw ←id_comp (limit.π (cospan s t ⋙ (evaluation Cᵒᵖ (Type u)).obj c) walking_cospan.left),
  rw ←eq_to_hom_refl,
  congr; simp, refl
end

lemma iso_snd_comm : pullback_snd_app s t c =
  (iso_app_cone_X s t c).hom ≫ (pullback.snd : pullback (s.app c) (t.app c) ⟶ Y.obj c) :=
begin
  unfold iso_app_cone_X, simp,
  dunfold pullback_snd_app, symmetry,
  convert limit_obj_iso_limit_comp_evaluation_hom_π (cospan s t) walking_cospan.right c,
  dunfold pullback.snd,
  rw ←id_comp (limit.π (cospan s t ⋙ (evaluation Cᵒᵖ (Type u)).obj c) walking_cospan.right),
  rw ←eq_to_hom_refl,
  congr; simp, refl
end

@[simp] lemma app_cone_X : (app_cone s t c).X = (limit (cospan s t)).obj c  := by refl
@[simp] lemma pulback_cone_X :
  (limit.cone (cospan (s.app c) (t.app c))).X = pullback (s.app c) (t.app c) := by refl

def iso_app_cone_X' : (app_cone s t c).X ≅ (limit.cone (cospan (s.app c) (t.app c))).X :=
begin
simp, exact iso_app_cone_X s t c
end

-- This is the isomorphism
def iso_app_cone : app_cone s t c ≅ limit.cone (cospan (s.app c) (t.app c)) :=
begin
  unfold app_cone,
  apply pullback_cone.ext (iso_app_cone_X' s t c) (iso_fst_comm s t c) (iso_snd_comm s t c),
end

lemma app_cone_is_limit : is_limit (app_cone s t c) :=
is_limit.of_iso_limit (limit_cone.is_limit _) (iso_app_cone s t c).symm

variables {s t}
-- More generally, we can get an iso of cone from a any limit cone
lemma iso_app_cone_of_is_limit (wc : pullback_cone (s.app c) (t.app c)) (hwc : is_limit wc) :
  app_cone s t c ≅ wc :=
begin
exact is_limit.unique_up_to_iso (app_cone_is_limit s t c) hwc
end

@[simp] lemma app_cone_cano :
  app_cone_of_cone (pullback_cone.mk pullback.fst pullback.snd pullback.condition) c = app_cone s t c := by refl

def app_cone_iso_of_iso_cone_X (w w' : pullback_cone s t) (c : Cᵒᵖ) (i : w ≅ w') :
  (app_cone_of_cone w c).X ≅ (app_cone_of_cone w' c).X :=
{ hom := i.hom.hom.app c,
  inv := i.inv.hom.app c,
  hom_inv_id' :=
  begin
   rw ←nat_trans.vcomp_app, rw nat_trans.vcomp_eq_comp,
   change i.hom.hom ≫ i.inv.hom with (i.hom ≫ i.inv).hom,
   simp, refl,
  end,
  inv_hom_id' :=
  begin
   rw ←nat_trans.vcomp_app, rw nat_trans.vcomp_eq_comp,
   change i.inv.hom ≫ i.hom.hom with (i.inv ≫ i.hom).hom,
   simp, refl,
  end }

lemma app_cone_fst (w : pullback_cone s t) (c : Cᵒᵖ) :
  (w.π.app walking_cospan.left).app c = (app_cone_of_cone w c).fst := by refl

lemma app_cone_snd (w : pullback_cone s t) (c : Cᵒᵖ) :
  (w.π.app walking_cospan.right).app c = (app_cone_of_cone w c).snd := by refl

lemma app_cone_iso_of_iso_cone_fst_comm (w w' : pullback_cone s t) (c : Cᵒᵖ) (i : w ≅ w') :
  (app_cone_of_cone w c).fst =
  (app_cone_iso_of_iso_cone_X w w' c i).hom ≫ (app_cone_of_cone w' c).fst :=
begin
  change (app_cone_iso_of_iso_cone_X w w' c i).hom with i.hom.hom.app c,
  rw [←app_cone_fst w, ←app_cone_fst w', ←nat_trans.vcomp_app,
      nat_trans.vcomp_eq_comp, i.hom.w' walking_cospan.left]
end

lemma app_cone_iso_of_iso_cone_snd_comm (w w' : pullback_cone s t) (c : Cᵒᵖ) (i : w ≅ w') :
  (app_cone_of_cone w c).snd =
  (app_cone_iso_of_iso_cone_X w w' c i).hom ≫ (app_cone_of_cone w' c).snd :=
begin
  change (app_cone_iso_of_iso_cone_X w w' c i).hom with i.hom.hom.app c,
  rw [←app_cone_snd w, ←app_cone_snd w', ←nat_trans.vcomp_app,
      nat_trans.vcomp_eq_comp, i.hom.w' walking_cospan.right]
end

lemma app_cone_iso_of_iso_cone (w w' : pullback_cone s t) (c : Cᵒᵖ) (i : w ≅ w') :
  (app_cone_of_cone w c) ≅ (app_cone_of_cone w' c) :=
pullback_cone.ext (app_cone_iso_of_iso_cone_X w w' c i)
                  (app_cone_iso_of_iso_cone_fst_comm w w' c i)
                  (app_cone_iso_of_iso_cone_snd_comm w w' c i)

-- Useful result : if a cone is limit in the presheaves world, then every applied cone is limit
theorem is_limit_app_cone_of_cone (w : pullback_cone s t) (hw : is_limit w) (c : Cᵒᵖ) :
  is_limit (app_cone_of_cone w c) :=
begin
  have g := app_cone_iso_of_iso_cone _ w c (is_limit.unique_up_to_iso (pullback_is_pullback s t) hw),
  simp at g,
  apply is_limit.of_iso_limit (app_cone_is_limit s t c) g,
end

end pullback

-- Some problems see:
-- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Category.20Type
-- local attribute [-instance]
--   limits.has_kernel_pair_of_mono
--   limits.has_pullback_of_left_factors_mono
--   limits.has_pullback_of_right_factors_mono
--   limits.has_pullback_of_comp_mono

instance mono_app_of_mono {S X : °C} (m : S ⟶ X) [mono m] (c : Cᵒᵖ) : mono (m.app c) :=
begin
  apply pullback_cone.mono_of_is_limit_mk_id_id,
  exact pullback.is_limit_app_cone_of_cone _ (pullback_cone.is_limit_mk_id_id m) c,
end

def sieve_map (c d : C) (f : c ⟶ d) : sieve d ⟶ sieve c := sieve.pullback f

abbreviation Ω_obj (c : Cᵒᵖ) := (sieve c.unop)
abbreviation Ω_map (c d : Cᵒᵖ) (f : c ⟶ d) : (Ω_obj c ⟶ Ω_obj d ):= sieve_map _ _ f.unop

def Ω : °C := {
  obj := Ω_obj,
  map := Ω_map,
  map_id' :=
  begin
    intro, dunfold Ω_map sieve_map,
    funext, simp
  end,
  map_comp' :=
  begin
    intros X Y Z f g, dunfold Ω_map sieve_map,
    funext, simp [sieve.pullback_comp]
  end,
}

@[simp] lemma obj' (c : Cᵒᵖ) : (Ω.obj c) = (Ω_obj c) := by refl
@[simp] lemma map' {c d : Cᵒᵖ} (f : c ⟶ d) : (Ω.map f) = (Ω_map c d f) := by refl

instance (c : Cᵒᵖ) : complete_lattice (Ω.obj c) := by simp; apply_instance

def truth : ₸ ⟶ Ω := { app := λ c x, ⊤ }

@[simp] lemma truth_app (c : Cᵒᵖ) (x : ₸.obj c) : truth.app c x = ⊤ := by refl

namespace classifier
variables {S X : °C} (m : S ⟶ X) [mono m]

/- The classifiyng arrow of m : S ⟶ X is the sieve
  χ_c(x) = {g : d ⟶ c | ∃ y : S(d), m_d(y) = X(g)(x) }
-/
def χ_app (c : Cᵒᵖ) (x : X.obj c) : sieve c.unop :=
{ arrows := λ d f, ∃ (y : S.obj (opposite.op d)), m.app (opposite.op d) y = X.map f.op x,
  downward_closed' :=
  begin
  intros d e f h g,
  cases h with w hw,
  use S.map (g.op) w,
  rw [op_comp, functor_to_types.naturality, hw, functor.map_comp'], refl
  end
}

def χ : X ⟶ Ω :=
{ app := χ_app m,
  naturality' :=
  begin
    intros c d f,
    funext, dsimp,
    ext1, fsplit;
    { intro a, cases a, fsplit, exact a_w, rw [op_comp, functor.map_comp'] at *, assumption },
  end }

-- We work at the level of type, and we will gather everything into a natural transformation
namespace app
variable (c : Cᵒᵖ)

lemma subtype_iff (y : X.obj c) : (∃ x : S.obj c, m.app c x = y) ↔ (χ m).app c y = ⊤ :=
begin
  split,
  { intro h, cases h with w h,
    ext d, simp,
    use S.map (f.op) w, rw ←h,
    rw [functor_to_types.naturality], refl },
  { intro h, rw sieve.ext_iff  at h, simp at h,
    specialize h (𝟙 c.unop), cases h with w h,
    change c with opposite.op (opposite.unop c),
    use w, rw h, simp,
    conv_rhs { rw ←id.def y},
    rw [←types_id, ←functor.map_id'] }
end

-- The pullback object of χ_m and true is (at c) the following:
abbreviation pb_object := { y : X.obj c // ∃ x : S.obj c, m.app c x = y }
abbreviation pb_object' := { p : (X.obj c) × (₸.obj c) // (χ m).app c p.1 = truth.app c p.2 }

-- There is often two version of the maps we develop, the one with '
-- is the one in in the hom set of Types as a category
-- Sometimes Lean doesn't want to directly type it correctly

def map_hom : pb_object m c → pb_object' m c :=
λ w, ⟨ (w.val, default), by { simp [←subtype_iff], exact w.prop }⟩

def map_hom' : pb_object m c ⟶ pb_object' m c := map_hom m c

def map_inv : pb_object' m c → pb_object m c :=
λ w, ⟨w.val.1, by { rw subtype_iff, exact w.prop }⟩

def map_inv' : pb_object' m c ⟶ pb_object m c := map_inv m c

def iso_pb_objects : iso (pb_object m c) (pb_object' m c) :=
{ hom := map_hom' m c,
  inv := map_inv' m c,
  hom_inv_id' := by { ext, rw [types_id, types_comp_apply], refl },
  inv_hom_id' := by ext; simp [types_id, types_comp_apply]; refl }

lemma pullback_condition_to_prop (u : pullback_cone (χ m) truth) (c : Cᵒᵖ) :
  ∀ x : u.X.obj c, (u.fst.app c ≫ (χ m).app c) x = ⊤ :=
by simp [←nat_trans.comp_app, u.condition]

def lift_to_pb_object (u : pullback_cone (χ m) truth) (c : Cᵒᵖ) :
  u.X.obj c → pb_object m c :=
λ x : u.X.obj c, ⟨ u.fst.app c x, by rw [subtype_iff, ←types_comp_apply _ ((χ m).app c),
                                         pullback_condition_to_prop]⟩

def lift_to_pb_object' (u : pullback_cone (χ m) truth) (c : Cᵒᵖ) :
  u.X.obj c ⟶ pb_object m c := lift_to_pb_object m u c

-- Can we do differently?
noncomputable def pb_object_to_subtype_obj (x : pb_object m c) :=
  (classical.indefinite_description _ x.prop)

noncomputable def pb_object_to_obj : pb_object m c → S.obj c :=
  λ x, (pb_object_to_subtype_obj m c x).val

noncomputable def pb_object_to_obj' : pb_object m c ⟶ S.obj c := pb_object_to_obj m c

def pb_lift (u : pullback_cone (χ m) truth) (c : Cᵒᵖ) : u.X.obj c ⟶ S.obj c :=
  lift_to_pb_object' m u c ≫ pb_object_to_obj' m c

def pb_lift_fst_comm (u : pullback_cone (χ m) truth) (c : Cᵒᵖ) :
  pb_lift m u c ≫ m.app c = u.fst.app c :=
begin
  ext, simp,
  exact (pb_object_to_subtype_obj m c ⟨u.fst.app c x, _⟩).prop,
end

-- This is quite easy as we have a mono and the commutation above
def pb_lift_naturality (u : pullback_cone (χ m) truth) (c d : Cᵒᵖ) (f : c ⟶ d) :
  u.X.map f ≫ app.pb_lift m u d = app.pb_lift m u c ≫ S.map f :=
begin
  symmetry,
  rw [←cancel_mono (m.app d), assoc, nat_trans.naturality, ←assoc,  pb_lift_fst_comm,
      ←nat_trans.naturality, ←pb_lift_fst_comm, assoc],
end

-- For the converse, to pick an object from S, we use the pullback condition
-- on the terminal object
lemma subtype_iff_pb (σ : X ⟶ Ω) (classifies : classifying_pullback truth m σ) (y : X.obj c) :
  (∃ x : S.obj c, m.app c x = y) ↔ σ.app c y = ⊤ :=
begin
    split,
  { intro h, cases h with w h,
    rw [←h, ←types_comp_apply (m.app c) (σ.app c), ←nat_trans.comp_app, classifies.comm],
    refl },
  { intro h, rw sieve.ext_iff at h,
    have comm : terminal.tto_app X c y ≫ σ.app c = (𝟙 _) ≫ truth.app c := by { ext, exact h f },
    let l := pullback_cone.is_limit.lift'
             (pullback.is_limit_app_cone_of_cone (pullback_cone.mk _ _ classifies.comm)
             classifies.is_pb c) _ _ comm,
    use (l.val default),
    exact congr_fun l.prop.left default }
end

instance has_coe_fun_Ω : has_coe_to_fun (Ω.obj c) (λ _, presieve (c.unop)) :=
  by { rw obj' c, apply_instance }

-- see :
-- https://math.stackexchange.com/questions/4304431/
-- characteristic-function-for-subobject-classifier-in-the-topos-of-presheaves

variable {c}

lemma in_sieve_iff_id {d : C} (σ : X ⟶ Ω) (f : d ⟶ c.unop) (y : X.obj c) :
  (σ.app c y) f ↔ (σ.app (opposite.op d) (X.map f.op y)) (𝟙 d) :=
begin
  rw [←types_comp_apply _ (σ.app (opposite.op d)), nat_trans.naturality],
  dsimp, rw map', dunfold Ω_map sieve_map,
  rw [sieve.pullback_eq_top_iff_mem, ←sieve.id_mem_iff_eq_top],
  refl
end

lemma in_sieve_iff_top {d : C} (σ : X ⟶ Ω) (f : d ⟶ c.unop) (y : X.obj c) :
  (σ.app c y) f ↔ (σ.app (opposite.op d) (X.map f.op y)) = ⊤ :=
begin
  rw [←sieve.id_mem_iff_eq_top, in_sieve_iff_id], refl
end

lemma in_sieve_iff_exists {d : C} (σ : X ⟶ Ω ) (classifies : classifying_pullback truth m σ)
  (y : X.obj c) (f : d ⟶ c.unop) :
  (σ.app c y) f ↔ ∃ x : S.obj (opposite.op d), m.app (opposite.op d) x = X.map f.op y :=
by rwa [in_sieve_iff_top, subtype_iff_pb]

variable (c)

def uniquely (σ : X ⟶ Ω ) (h : classifying truth m σ) (y : X.obj c) : σ.app c y = (χ m).app c y :=
begin
  apply sieve.ext,
  intros d f,
  rw [in_sieve_iff_exists m σ h y, subtype_iff, ←in_sieve_iff_top],
end

end app

lemma pullback_condition : m ≫ χ m = terminal.from S ≫ truth :=
begin
  ext1, funext c x, simp, apply sieve.ext,
  intros d f, simp,
  use S.map f.op x,
  rw functor_to_types.naturality, dsimp, refl
end

def pb_cone : pullback_cone (χ m) truth := pullback_cone.mk m (terminal.from S) (pullback_condition m)

def pb_lift (u : pullback_cone (χ m) truth) : u.X ⟶ S :=
{ app := app.pb_lift m u,
  naturality' := app.pb_lift_naturality m u
  }

def pb_lift_fst_comm (u : pullback_cone (χ m) truth) : pb_lift m u ≫ m = u.fst :=
begin
  ext, rw [nat_trans.comp_app, ←app.pb_lift_fst_comm], refl
end

lemma is_limit_pb_cone : is_limit (pb_cone m) :=
begin
apply pullback_cone.is_limit.mk (pullback_condition m) (pb_lift m),
{ intro s, exact pb_lift_fst_comm _ _ },
{ intro s, rw terminal.comp_from _, simp },
{ intros s v h _, rwa [←pb_lift_fst_comm, cancel_mono] at h, }
end

def χ_classifying : classifying truth m (χ m) :=
{ comm := pullback_condition m,
  is_pb := is_limit_pb_cone m }

def uniquely (σ : X ⟶ Ω ) (h : classifying truth m σ) : χ m = σ :=
begin
  ext : 3, symmetry, apply app.uniquely, assumption
end

def χ_is_subobject_classifier : is_subobject_classifier (@truth C _ _) :=
{ classifier_of := @χ C _ _,
  classifies' := @χ_classifying C _ _,
  uniquely' := @uniquely C _ _ }

end classifier

instance has_subobject_classifier_presheaves_C: has_subobject_classifier °C :=
{ Ω := Ω,
  truth := truth,
  is_subobj_classifier := classifier.χ_is_subobject_classifier }

end presheaf

instance topos_presheaves_C : topos °C := topos.mk

author: cchanavat

repo: lean-topos

save_path: github-repos/lean/cchanavat-lean-topos


text:
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
-/
import ring_theory.ideal.local_ring
import ring_theory.localization.ideal

/-!
# Localizations of commutative rings at the complement of a prime ideal

## Main definitions

 * `is_localization.at_prime (I : ideal R) [is_prime I] (S : Type*)` expresses that `S` is a
   localization at (the complement of) a prime ideal `I`, as an abbreviation of
   `is_localization I.prime_compl S`

## Main results

 * `is_localization.at_prime.local_ring`: a theorem (not an instance) stating a localization at the
   complement of a prime ideal is a local ring

## Implementation notes

See `src/ring_theory/localization/basic.lean` for a design overview.

## Tags
localization, ring localization, commutative ring localization, characteristic predicate,
commutative ring, field of fractions
-/
variables {R : Type*} [comm_semiring R] (M : submonoid R) (S : Type*) [comm_semiring S]
variables [algebra R S] {P : Type*} [comm_semiring P]

section at_prime

variables (I : ideal R) [hp : I.is_prime]
include hp
namespace ideal

/-- The complement of a prime ideal `I ⊆ R` is a submonoid of `R`. -/
def prime_compl :
  submonoid R :=
{ carrier := (Iᶜ : set R),
  one_mem' := by convert I.ne_top_iff_one.1 hp.1; refl,
  mul_mem' := λ x y hnx hny hxy, or.cases_on (hp.mem_or_mem hxy) hnx hny }

end ideal

variables (S)

/-- Given a prime ideal `P`, the typeclass `is_localization.at_prime S P` states that `S` is
isomorphic to the localization of `R` at the complement of `P`. -/
protected abbreviation is_localization.at_prime := is_localization I.prime_compl S

/-- Given a prime ideal `P`, `localization.at_prime S P` is a localization of
`R` at the complement of `P`, as a quotient type. -/
protected abbreviation localization.at_prime := localization I.prime_compl

namespace is_localization

lemma at_prime.nontrivial [is_localization.at_prime S I] : nontrivial S :=
nontrivial_of_ne (0 : S) 1 $ λ hze,
begin
  rw [←(algebra_map R S).map_one, ←(algebra_map R S).map_zero] at hze,
  obtain ⟨t, ht⟩ := (eq_iff_exists I.prime_compl S).1 hze,
  have htz : (t : R) = 0, by simpa using ht.symm,
  exact t.2 (htz.symm ▸ I.zero_mem : ↑t ∈ I)
end

local attribute [instance] at_prime.nontrivial

theorem at_prime.local_ring [is_localization.at_prime S I] : local_ring S :=
local_ring.of_nonunits_add
begin
  intros x y hx hy hu,
  cases is_unit_iff_exists_inv.1 hu with z hxyz,
  have : ∀ {r : R} {s : I.prime_compl}, mk' S r s ∈ nonunits S → r ∈ I, from
    λ (r : R) (s : I.prime_compl), not_imp_comm.1
      (λ nr, is_unit_iff_exists_inv.2 ⟨mk' S ↑s (⟨r, nr⟩ : I.prime_compl),
        mk'_mul_mk'_eq_one' _ _ nr⟩),
  rcases mk'_surjective I.prime_compl x with ⟨rx, sx, hrx⟩,
  rcases mk'_surjective I.prime_compl y with ⟨ry, sy, hry⟩,
  rcases mk'_surjective I.prime_compl z with ⟨rz, sz, hrz⟩,
  rw [←hrx, ←hry, ←hrz, ←mk'_add, ←mk'_mul,
      ←mk'_self S I.prime_compl.one_mem] at hxyz,
  rw ←hrx at hx, rw ←hry at hy,
  obtain ⟨t, ht⟩ := is_localization.eq.1 hxyz,
  simp only [mul_one, one_mul, submonoid.coe_mul, subtype.coe_mk] at ht,
  suffices : ↑sx * ↑sy * ↑sz * ↑t ∈ I, from
    not_or (mt hp.mem_or_mem $ not_or sx.2 sy.2) sz.2
      (hp.mem_or_mem $ (hp.mem_or_mem this).resolve_right t.2),
  rw [←ht, mul_assoc],
  exact I.mul_mem_right _ (I.add_mem (I.mul_mem_right _ $ this hx)
                                     (I.mul_mem_right _ $ this hy))
end

end is_localization

namespace localization

/-- The localization of `R` at the complement of a prime ideal is a local ring. -/
instance at_prime.local_ring : local_ring (localization I.prime_compl) :=
is_localization.at_prime.local_ring (localization I.prime_compl) I

end localization

end at_prime

namespace is_localization

variables {A : Type*} [comm_ring A] [is_domain A]

/--
The localization of an integral domain at the complement of a prime ideal is an integral domain.
-/
instance is_domain_of_local_at_prime {P : ideal A} (hp : P.is_prime) :
  is_domain (localization.at_prime P) :=
is_domain_localization (le_non_zero_divisors_of_no_zero_divisors
  (not_not_intro P.zero_mem))

namespace at_prime

variables (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I]
include hI

lemma is_unit_to_map_iff (x : R) :
  is_unit ((algebra_map R S) x) ↔ x ∈ I.prime_compl :=
⟨λ h hx, (is_prime_of_is_prime_disjoint I.prime_compl S I hI disjoint_compl_left).ne_top $
  (ideal.map (algebra_map R S) I).eq_top_of_is_unit_mem (ideal.mem_map_of_mem _ hx) h,
λ h, map_units S ⟨x, h⟩⟩

-- Can't use typeclasses to infer the `local_ring` instance, so use an `opt_param` instead
-- (since `local_ring` is a `Prop`, there should be no unification issues.)
lemma to_map_mem_maximal_iff (x : R) (h : _root_.local_ring S := local_ring S I) :
  algebra_map R S x ∈ local_ring.maximal_ideal S ↔ x ∈ I :=
not_iff_not.mp $ by
simpa only [local_ring.mem_maximal_ideal, mem_nonunits_iff, not_not]
  using is_unit_to_map_iff S I x

lemma is_unit_mk'_iff (x : R) (y : I.prime_compl) :
  is_unit (mk' S x y) ↔ x ∈ I.prime_compl :=
⟨λ h hx, mk'_mem_iff.mpr ((to_map_mem_maximal_iff S I x).mpr hx) h,
λ h, is_unit_iff_exists_inv.mpr ⟨mk' S ↑y ⟨x, h⟩, mk'_mul_mk'_eq_one ⟨x, h⟩ y⟩⟩

lemma mk'_mem_maximal_iff (x : R) (y : I.prime_compl) (h : _root_.local_ring S := local_ring S I) :
  mk' S x y ∈ local_ring.maximal_ideal S ↔ x ∈ I :=
not_iff_not.mp $ by
simpa only [local_ring.mem_maximal_ideal, mem_nonunits_iff, not_not]
  using is_unit_mk'_iff S I x y

end at_prime

end is_localization

namespace localization

open is_localization

local attribute [instance] classical.prop_decidable

variables (I : ideal R) [hI : I.is_prime]
include hI

variables {I}
/-- The unique maximal ideal of the localization at `I.prime_compl` lies over the ideal `I`. -/
lemma at_prime.comap_maximal_ideal :
  ideal.comap (algebra_map R (localization.at_prime I))
    (local_ring.maximal_ideal (localization I.prime_compl)) = I :=
ideal.ext $ λ x, by
simpa only [ideal.mem_comap] using at_prime.to_map_mem_maximal_iff _ I x

/-- The image of `I` in the localization at `I.prime_compl` is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure `at_prime.local_ring` -/
lemma at_prime.map_eq_maximal_ideal :
  ideal.map (algebra_map R (localization.at_prime I)) I =
    (local_ring.maximal_ideal (localization I.prime_compl)) :=
begin
  convert congr_arg (ideal.map _) at_prime.comap_maximal_ideal.symm,
  rw map_comap I.prime_compl
end

lemma le_comap_prime_compl_iff {J : ideal P} [hJ : J.is_prime] {f : R →+* P} :
  I.prime_compl ≤ J.prime_compl.comap f ↔ J.comap f ≤ I :=
⟨λ h x hx, by { contrapose! hx, exact h hx },
 λ h x hx hfxJ, hx (h hfxJ)⟩

variables (I)

/--
For a ring hom `f : R →+* S` and a prime ideal `J` in `S`, the induced ring hom from the
localization of `R` at `J.comap f` to the localization of `S` at `J`.

To make this definition more flexible, we allow any ideal `I` of `R` as input, together with a proof
that `I = J.comap f`. This can be useful when `I` is not definitionally equal to `J.comap f`.
 -/
noncomputable def local_ring_hom (J : ideal P) [hJ : J.is_prime] (f : R →+* P)
  (hIJ : I = J.comap f) :
  localization.at_prime I →+* localization.at_prime J :=
is_localization.map (localization.at_prime J) f (le_comap_prime_compl_iff.mpr (ge_of_eq hIJ))

lemma local_ring_hom_to_map (J : ideal P) [hJ : J.is_prime] (f : R →+* P)
  (hIJ : I = J.comap f) (x : R) :
  local_ring_hom I J f hIJ (algebra_map _ _ x) = algebra_map _ _ (f x) :=
map_eq _ _

lemma local_ring_hom_mk' (J : ideal P) [hJ : J.is_prime] (f : R →+* P)
  (hIJ : I = J.comap f) (x : R) (y : I.prime_compl) :
  local_ring_hom I J f hIJ (is_localization.mk' _ x y) =
    is_localization.mk' (localization.at_prime J) (f x)
      (⟨f y, le_comap_prime_compl_iff.mpr (ge_of_eq hIJ) y.2⟩ : J.prime_compl) :=
map_mk' _ _ _

instance is_local_ring_hom_local_ring_hom (J : ideal P) [hJ : J.is_prime] (f : R →+* P)
  (hIJ : I = J.comap f) :
  is_local_ring_hom (local_ring_hom I J f hIJ) :=
is_local_ring_hom.mk $ λ x hx,
begin
  rcases is_localization.mk'_surjective I.prime_compl x with ⟨r, s, rfl⟩,
  rw local_ring_hom_mk' at hx,
  rw at_prime.is_unit_mk'_iff at hx ⊢,
  exact λ hr, hx ((set_like.ext_iff.mp hIJ r).mp hr),
end

lemma local_ring_hom_unique (J : ideal P) [hJ : J.is_prime] (f : R →+* P)
  (hIJ : I = J.comap f) {j : localization.at_prime I →+* localization.at_prime J}
  (hj : ∀ x : R, j (algebra_map _ _ x) = algebra_map _ _ (f x)) :
  local_ring_hom I J f hIJ = j :=
map_unique _ _ hj

@[simp] lemma local_ring_hom_id :
  local_ring_hom I I (ring_hom.id R) (ideal.comap_id I).symm = ring_hom.id _ :=
local_ring_hom_unique _ _ _ _ (λ x, rfl)

@[simp] lemma local_ring_hom_comp {S : Type*} [comm_semiring S]
  (J : ideal S) [hJ : J.is_prime] (K : ideal P) [hK : K.is_prime]
  (f : R →+* S) (hIJ : I = J.comap f) (g : S →+* P) (hJK : J = K.comap g) :
  local_ring_hom I K (g.comp f) (by rw [hIJ, hJK, ideal.comap_comap f g]) =
  (local_ring_hom J K g hJK).comp (local_ring_hom I J f hIJ) :=
local_ring_hom_unique _ _ _ _
  (λ r, by simp only [function.comp_app, ring_hom.coe_comp, local_ring_hom_to_map])

end localization


text:
/-
Copyright (c) 2022 Riccardo Brasca. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Riccardo Brasca, Eric Rodriguez
-/

import number_theory.number_field.basic
import ring_theory.norm

/-!
# Norm in number fields
Given a finite extension of number fields, we define the norm morphism as a function between the
rings of integers.

## Main definitions
* `ring_of_integers.norm K` : `algebra.norm` as a morphism `(𝓞 L) →* (𝓞 K)`.
## Main results
* `algebra.dvd_norm` : if `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)`
  we have that `x ∣ algebra_map (𝓞 K) (𝓞 L) (norm K x)`.

-/

open_locale number_field big_operators

open finset number_field algebra

namespace ring_of_integers

variables {L : Type*} (K : Type*) [field K] [field L] [algebra K L] [finite_dimensional K L]

/-- `algebra.norm` as a morphism betwen the rings of integers. -/
@[simps] noncomputable def norm [is_separable K L] : (𝓞 L) →* (𝓞 K) :=
((algebra.norm K).restrict (𝓞 L)).cod_restrict (𝓞 K) (λ x, is_integral_norm K x.2)

local attribute [instance] number_field.ring_of_integers_algebra

lemma coe_algebra_map_norm [is_separable K L] (x : 𝓞 L) :
  (algebra_map (𝓞 K) (𝓞 L) (norm K x) : L) = algebra_map K L (algebra.norm K (x : L)) := rfl

/-- If `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)` we have that
`x ∣ algebra_map (𝓞 K) (𝓞 L) (norm K x)`. -/
lemma dvd_norm [is_galois K L] (x : 𝓞 L) : x ∣ algebra_map (𝓞 K) (𝓞 L) (norm K x) :=
begin
  classical,
  have hint : (∏ (σ : L ≃ₐ[K] L) in univ.erase alg_equiv.refl, σ x) ∈ 𝓞 L :=
    subalgebra.prod_mem _ (λ σ hσ, (mem_ring_of_integers _ _).2
    (map_is_integral σ (ring_of_integers.is_integral_coe x))),
  refine ⟨⟨_, hint⟩, subtype.ext _⟩,
  rw [coe_algebra_map_norm K x, norm_eq_prod_automorphisms],
  simp [← finset.mul_prod_erase _ _ (mem_univ alg_equiv.refl)]
end

end ring_of_integers

author: leanprover-community

repo: mathlib


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
-/
import data.polynomial.derivative
import tactic.linear_combination
import tactic.ring_exp

/-!
# Theory of univariate polynomials

The main def is `binom_expansion`.
-/

noncomputable theory

namespace polynomial
open_locale polynomial
universes u v w x y z
variables {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A : Type z}
  {a b : R} {m n : ℕ}

section identities

/- @TODO: pow_add_expansion and pow_sub_pow_factor are not specific to polynomials.
  These belong somewhere else. But not in group_power because they depend on tactic.ring_exp

Maybe use data.nat.choose to prove it.
 -/
/--
`(x + y)^n` can be expressed as `x^n + n*x^(n-1)*y + k * y^2` for some `k` in the ring.
-/
def pow_add_expansion {R : Type*} [comm_semiring R] (x y : R) : ∀ (n : ℕ),
  {k // (x + y)^n = x^n + n*x^(n-1)*y + k * y^2}
| 0 := ⟨0, by simp⟩
| 1 := ⟨0, by simp⟩
| (n+2) :=
  begin
    cases pow_add_expansion (n+1) with z hz,
    existsi x*z + (n+1)*x^n+z*y,
    calc (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) : by ring_exp
    ... = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) : by rw hz
    ... = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x*z + (n+1)*x^n+z*y) * y ^ 2 :
      by { push_cast, ring_exp! }
  end

variables [comm_ring R]

private def poly_binom_aux1 (x y : R) (e : ℕ) (a : R) :
  {k : R // a * (x + y)^e = a * (x^e + e*x^(e-1)*y + k*y^2)} :=
begin
  existsi (pow_add_expansion x y e).val,
  congr,
  apply (pow_add_expansion _ _ _).property
end

private lemma poly_binom_aux2 (f : R[X]) (x y : R) :
  f.eval (x + y) = f.sum (λ e a, a * (x^e + e*x^(e-1)*y + (poly_binom_aux1 x y e a).val*y^2)) :=
begin
  unfold eval eval₂, congr' with n z,
  apply (poly_binom_aux1 x y _ _).property
end

private lemma poly_binom_aux3 (f : R[X]) (x y : R) : f.eval (x + y) =
  f.sum (λ e a, a * x^e) +
  f.sum (λ e a, (a * e * x^(e-1)) * y) +
  f.sum (λ e a, (a *(poly_binom_aux1 x y e a).val)*y^2) :=
by { rw poly_binom_aux2, simp [left_distrib, sum_add, mul_assoc] }

/--
A polynomial `f` evaluated at `x + y` can be expressed as
the evaluation of `f` at `x`, plus `y` times the (polynomial) derivative of `f` at `x`,
plus some element `k : R` times `y^2`.
-/
def binom_expansion (f : R[X]) (x y : R) :
  {k : R // f.eval (x + y) = f.eval x + (f.derivative.eval x) * y + k * y^2} :=
begin
  existsi f.sum (λ e a, a *((poly_binom_aux1 x y e a).val)),
  rw poly_binom_aux3,
  congr,
  { rw [←eval_eq_sum], },
  { rw derivative_eval, exact finset.sum_mul.symm },
  { exact finset.sum_mul.symm }
end

/--
`x^n - y^n` can be expressed as `z * (x - y)` for some `z` in the ring.
-/
def pow_sub_pow_factor (x y : R) : Π (i : ℕ), {z : R // x^i - y^i = z * (x - y)}
| 0 := ⟨0, by simp⟩
| 1 := ⟨1, by simp⟩
| (k+2) :=
  begin
    cases @pow_sub_pow_factor (k+1) with z hz,
    existsi z*x + y^(k+1),
    linear_combination (hz, x) { normalization_tactic := `[ring_exp] }
  end

/--
For any polynomial `f`, `f.eval x - f.eval y` can be expressed as `z * (x - y)`
for some `z` in the ring.
-/
def eval_sub_factor (f : R[X]) (x y : R) :
  {z : R // f.eval x - f.eval y = z * (x - y)} :=
begin
  refine ⟨f.sum (λ i r, r * (pow_sub_pow_factor x y i).val), _⟩,
  delta eval eval₂,
  simp only [sum, ← finset.sum_sub_distrib, finset.sum_mul],
  dsimp,
  congr' with i r,
  rw [mul_assoc, ←(pow_sub_pow_factor x y _).prop, mul_sub],
end

end identities

end polynomial